Posterior Mixture Kernel Realization

Abstract

A Bayes-plausible finite posterior mixture is realized by its canonical signal kernel.

Theorem 1.1 (Bayes-plausible posterior mixtures are realizable).

$$\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),muPost\in Signal\to \mathrm{PMF}\left(World\right),lambda\in \mathrm{PMF}\left(Signal\right),\left(\forall omega\in World,0<\mathrm{toReal}\left(mu\left(omega\right)\right)\right)\Rightarrow \left(\left(\forall omega\in World,\sum _{s\in Signal}\mathrm{toReal}\left(lambda\left(s\right)\right)\cdot \mathrm{toReal}\left(muPost\left(s,omega\right)\right)=\mathrm{toReal}\left(mu\left(omega\right)\right)\right)\Rightarrow \mathrm{let}kappa:World\to \left(Signal\to \mathbb{R}\right):=(omega,s)\mapsto \frac{\mathrm{toReal}\left(lambda\left(s\right)\right)\cdot \mathrm{toReal}\left(muPost\left(s,omega\right)\right)}{\mathrm{toReal}\left(mu\left(omega\right)\right)};\mathrm{let}jointLaw:Signal\times World\to \mathbb{R}:=(s,omega)\mapsto \mathrm{toReal}\left(mu\left(omega\right)\right)\cdot kappa\left(omega,s\right);\left(\forall omega\in World,s\in Signal,0\le kappa\left(omega,s\right)\right)\wedge \left(\left(\forall omega\in World,\sum _{s\in Signal}kappa\left(omega,s\right)=1\right)\wedge \left(\mathrm{marginal}\left(jointLaw\right)=(s\mapsto \mathrm{toReal}\left(lambda\left(s\right)\right))\wedge \left(\forall s\in Signal,0<\mathrm{toReal}\left(lambda\left(s\right)\right)\Rightarrow \mathrm{conditional}\left(jointLaw,s\right)=(omega\mapsto \mathrm{toReal}\left(muPost\left(s,omega\right)\right))\right)\right)\right)\right)\right)$$

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

Source. Repository-derived.

Commentary.

The prior, every prescribed posterior, and the signal weights are finite PMFs. Thus the nonnegativity and unit-mass requirements on the posterior family and weights are part of their public carriers.

The theorem exposes the canonical signal kernel as the prescribed signal weight times posterior mass, divided by the positive prior mass. The accompanying joint law is induced from that kernel and prior.

The posterior-mixture equation normalizes the kernel at every world. Posterior normalization gives the prescribed signal marginal, and division by a positive signal weight recovers its posterior.

The imported forward plausibility theorem uses the same canonical marginal and conditional operations. Repository search found no prior reverse realization theorem containing all displayed clauses.

References

• Truth anchor: D5/S3/ConceptDynamics/ObservationOrder/PosteriorMixtureKernelRealization.posterior_mixture_kernel_realization
• Dependency: D5/S3/ConceptDynamics/ObservationOrder/BayesPlausibility