Bayesian Observation Models and Posterior Update

The ergonomic ℝ-typed interface for finite Bayesian inference with explicit experiment indexing. Provides the same algorithm as mathlib's canonical PMF.posterior (Core/Probability/Posterior.lean): P(w|o,e) = prior(w) · P(o|w,e) / Σ_w' prior(w') · P(o|w',e).

Relationship to PMF.posterior

PMF.posterior is the canonical mathlib probability-theoretic primitive (κ : α → PMF β, μ : PMF α, observation b, returns PMF α). This module's posterior is mathematically the same Bayes' rule formula but with three ergonomic differences:

1. ℝ instead of ℝ≥0∞ — keeps arithmetic in the reals so consumers can use signed value functions ((W → ℝ) → ℝ for utility / entropy theorems) without ENNReal coercions.
2. Experiment indexing E — ObservationModel W E O carries an explicit experiment-index parameter that PMF kernels lack. For each fixed e : E, an ObservationModel IS a kernel W → PMF O (see ObservationModel.toPMFKernel).
3. Permissive prior — accepts any prior : W → ℝ rather than requiring a PMF W (the formula gives 0 when the marginal is 0).

Use PMF.posterior for general probability work; use this module for finite Bayesian inference where experiment indexing or (W → ℝ)-typed value functions are needed (e.g., ExperimentDesign.eig).

Key Results

• posterior_nonneg: posteriors inherit non-negativity from priors
• posterior_sum_one: posteriors sum to 1 (when marginal is nonzero)
• posterior_marginalizes_to_prior: the law of total probability — marginalized posteriors reconstruct the prior: ∑ o, P(o|e) · P(w|o,e) = prior(w)
• ObservationModel.toPMFKernel: PMF-typed view of the likelihood at fixed experiment, enabling interop with PMF.posterior.

Usage

This module is imported by ExperimentDesign.lean (for EIG computation) and can be imported independently wherever Bayesian updating is needed.

structure Core.ObservationModel (W : Type u_1) (E : Type u_2) (O : Type u_3) [Fintype O] : Type (max (max u_1 u_2) u_3)

An observation model: how experiments generate observations in different worlds. P(o|w,e) — the probability of observing o when the true world is w and experiment e is conducted.

• likelihood : W → E → O → ℝ

  Likelihood: P(o|w,e)

• likelihood_nonneg (w : W) (e : E) (o : O) : 0 ≤ self.likelihood w e o

  Likelihood is non-negative

• likelihood_sum (w : W) (e : E) : ∑ o : O, self.likelihood w e o = 1

  Likelihood sums to 1 for each (w,e)

noncomputable def Core.marginalObs {W : Type u_1} {E : Type u_2} {O : Type u_3} [Fintype W] [Fintype O] (om : ObservationModel W E O) (prior : W → ℝ) (e : E) (o : O) : ℝ

Marginal probability of observation o under experiment e: P(o|e) = Σ_w prior(w) · P(o|w,e)

Equations

• Core.marginalObs om prior e o = ∑ w : W, prior w * om.likelihood w e o

noncomputable def Core.posterior {W : Type u_1} {E : Type u_2} {O : Type u_3} [Fintype W] [Fintype O] (om : ObservationModel W E O) (prior : W → ℝ) (e : E) (o : O) : W → ℝ

Bayesian posterior after observing o under experiment e: P(w|o,e) = prior(w) · P(o|w,e) / P(o|e)

Equations

• Core.posterior om prior e o w = if Core.marginalObs om prior e o = 0 then 0 else prior w * om.likelihood w e o / Core.marginalObs om prior e o

theorem Core.marginalObs_nonneg {W : Type u_1} {E : Type u_2} {O : Type u_3} [Fintype W] [Fintype O] (om : ObservationModel W E O) (prior : W → ℝ) (hprior : ∀ (w : W), 0 ≤ prior w) (e : E) (o : O) : 0 ≤ marginalObs om prior e o

Marginal observation probability is non-negative when prior is.

theorem Core.posterior_nonneg {W : Type u_1} {E : Type u_2} {O : Type u_3} [Fintype W] [Fintype O] (om : ObservationModel W E O) (prior : W → ℝ) (hprior : ∀ (w : W), 0 ≤ prior w) (e : E) (o : O) (w : W) : 0 ≤ posterior om prior e o w

Posterior is non-negative when prior is.

theorem Core.posterior_sum_one {W : Type u_1} {E : Type u_2} {O : Type u_3} [Fintype W] [Fintype O] (om : ObservationModel W E O) (prior : W → ℝ) (_hprior : ∀ (w : W), 0 ≤ prior w) (e : E) (o : O) (hm : marginalObs om prior e o ≠ 0) : ∑ w : W, posterior om prior e o w = 1

Posterior sums to 1 when marginal is nonzero and prior is non-negative.

theorem Core.posterior_marginalizes_to_prior {W : Type u_1} {E : Type u_2} {O : Type u_3} [Fintype W] [Fintype O] (om : ObservationModel W E O) (prior : W → ℝ) (hprior : ∀ (w : W), 0 ≤ prior w) (e : E) (w : W) : ∑ o : O, marginalObs om prior e o * posterior om prior e o w = prior w

The law of total probability for posteriors: marginalized posteriors reconstruct the prior.

Σ_o P(o|e) · P(w|o,e) = prior(w)

This is the key identity underlying EIG non-negativity.

def Core.deterministicObs {W : Type u_1} {O : Type u_3} [Fintype O] [DecidableEq O] (classify : W → O) : ObservationModel W Unit O

A deterministic observation model from a classifier: each world produces exactly the observation corresponding to its classification.

This is the partition-cell case: classify assigns each world to a cell, and the observation reveals which cell the world belongs to.

Equations

• Core.deterministicObs classify = { likelihood := fun (w : W) (x : Unit) (o : O) => if classify w = o then 1 else 0, likelihood_nonneg := ⋯, likelihood_sum := ⋯ }

PMF interop

Convert an ObservationModel at a fixed experiment to a mathlib PMF-typed kernel W → PMF O. Bridges to PMF.posterior for any downstream use that requires the canonical mathlib type.

noncomputable def Core.ObservationModel.toPMFKernel {W : Type u_1} {E : Type u_2} {O : Type u_3} [Fintype O] (om : ObservationModel W E O) (e : E) : W → PMF O

The PMF view of an ObservationModel at a fixed experiment e. For each world w, returns the PMF O whose mass at o is om.likelihood w e o. Bridges this module's ℝ-typed Bayesian machinery to mathlib's canonical PMF.posterior.

Equations

• om.toPMFKernel e w = PMF.ofFintype (fun (o : O) => ENNReal.ofReal (om.likelihood w e o)) ⋯