Bayes Plausibility

Abstract

Finite posterior mixtures reconstruct their prior distribution.

Theorem 1.1 (The posterior mixture is the prior).

$$\begin{gathered} \forall World\in Type,Signal\in Type,\left(\mathrm{Fintype}\left(World\right)\wedge \mathrm{Fintype}\left(Signal\right)\right)\Rightarrow \left(\forall mu\in \mathrm{PMF}\left(World\right),K\in World\to \mathrm{PMF}\left(Signal\right),\mathrm{let}jointLaw:Signal\times World\to \mathbb{R}:=(s,omega)\mapsto \mathrm{toReal}\left(mu\left(omega\right)\right)\cdot \mathrm{toReal}\left(K\left(omega\right)\left(s\right)\right); \\ \mathrm{let}lambda:Signal\to \mathbb{R}:=s\mapsto \mathrm{marginal}\left(jointLaw,s\right); \\ \mathrm{let}posterior:Signal\to \left(World\to \mathbb{R}\right):=(s,omega)\mapsto \mathrm{conditional}\left(jointLaw,s,omega\right); \\ (omega\mapsto \sum _{s\in Signal}lambda\left(s\right)\cdot posterior\left(s,omega\right))=(omega\mapsto \mathrm{toReal}\left(mu\left(omega\right)\right))\wedge \left(\forall omega\in World,\sum _{s\in Signal}lambda\left(s\right)\cdot posterior\left(s,omega\right)=\mathrm{toReal}\left(mu\left(omega\right)\right)\right)\right) \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/ObservationOrder/BayesPlausibility.bayes_plausibility (✓ std3). ∎

Source. Repository-derived.

Commentary.

A finite world PMF and a PMF-valued finite signal kernel construct the displayed real joint law. Its canonical first marginal is the signal weight, and its canonical conditional is the posterior.

On a positive-weight signal fiber, multiplying the conditional by its marginal recovers the joint mass. On a zero-weight fiber, nonnegativity forces every joint mass in that fiber to vanish.

Summing the recovered joint masses over signals leaves the prior mass times the normalized signal-kernel mass. This proves both the function equality and its public pointwise form.

Repository and pinned-library searches found no exact theorem on this finite PMF/kernel carrier. The proof imports the existing marginal and conditional primitives and applies Mathlib’s PMF normalization.

References

• Truth anchor: D5/S3/ConceptDynamics/ObservationOrder/BayesPlausibility.bayes_plausibility
• Dependency: D5/S3/Divergence/ChainRule