Exact Bayes for the posterior kernel at atoms

Mathlib characterizes the posterior kernel κ†μ almost everywhere. On discrete spaces an ae-fact holds at every atom of positive mass (MeasureTheory.ae_of_singleton_ne_zero), which gives Bayes' rule pointwise at any positive-mass observation — no Radon–Nikodym derivative — and reduces comparisons of posterior masses over finite events, and over the marginals of a product parameter space, to comparisons of prior-weighted likelihood sums.

Main results

• ProbabilityTheory.posterior_apply_singleton — (κ†μ) x {ω} = μ {ω} * κ ω {x} / (κ ∘ₘ μ) {x}.
• ProbabilityTheory.posterior_deterministic_eq_cond — a deterministic observation's posterior is the prior conditioned on the observation's fibre.
• ProbabilityTheory.posterior_real_finset_lt_iff — event comparison of the posterior.
• ProbabilityTheory.sum_real_mul_le_sum_posterior_real_mul — conditioning on an observation raises the expectation of a statistic that monovaries with the observation's likelihood.
• ProbabilityTheory.posterior_fst_real_lt_iff, posterior_snd_real_lt_iff — marginal comparison over a product parameter space.

theorem MeasureTheory.ae_of_singleton_ne_zero {α : Type u_1} [MeasurableSpace α] {ν : Measure α} {P : α → Prop} (h : ∀ᵐ (x : α) ∂ν, P x) {x : α} (hx : ν {x} ≠ 0) : P x

An almost-everywhere property holds at any atom of positive mass.

theorem ProbabilityTheory.posterior_apply_singleton {Ω : Type u_1} {𝓧 : Type u_2} [MeasurableSpace Ω] [MeasurableSpace 𝓧] [MeasurableSingletonClass Ω] [MeasurableSingletonClass 𝓧] [StandardBorelSpace Ω] [Nonempty Ω] (κ : Kernel Ω 𝓧) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] [IsFiniteKernel κ] {x : 𝓧} (hx : (μ.bind ⇑κ) {x} ≠ 0) (ω : Ω) : ((posterior κ μ) x) {ω} = μ {ω} * (κ ω) {x} / (μ.bind ⇑κ) {x}

Exact Bayes for the posterior kernel at a positive-mass observation: evaluate the defining compProd identity on a singleton rectangle.

theorem ProbabilityTheory.posterior_apply_singleton_ne_zero_iff {Ω : Type u_1} {𝓧 : Type u_2} [MeasurableSpace Ω] [MeasurableSpace 𝓧] [MeasurableSingletonClass Ω] [MeasurableSingletonClass 𝓧] [StandardBorelSpace Ω] [Nonempty Ω] (κ : Kernel Ω 𝓧) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] [IsFiniteKernel κ] {x : 𝓧} (hx : (μ.bind ⇑κ) {x} ≠ 0) (ω : Ω) : ((posterior κ μ) x) {ω} ≠ 0 ↔ μ {ω} ≠ 0 ∧ (κ ω) {x} ≠ 0

The posterior is positive at a state exactly when the prior and the likelihood are.

theorem ProbabilityTheory.posterior_apply_singleton_congr {Ω : Type u_1} {𝓧 : Type u_2} [MeasurableSpace Ω] [MeasurableSpace 𝓧] [MeasurableSingletonClass Ω] [MeasurableSingletonClass 𝓧] [StandardBorelSpace Ω] [Nonempty Ω] (κ : Kernel Ω 𝓧) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] [IsFiniteKernel κ] {x : 𝓧} (hx : (μ.bind ⇑κ) {x} ≠ 0) {ω₁ ω₂ : Ω} (hrow : (κ ω₁) {x} = (κ ω₂) {x}) (hμ : μ {ω₁} = μ {ω₂}) : ((posterior κ μ) x) {ω₁} = ((posterior κ μ) x) {ω₂}

Two states with the same likelihood of the observation and the same prior mass have the same posterior mass.

theorem ProbabilityTheory.posterior_real_finset_lt_iff {Ω : Type u_1} {𝓧 : Type u_2} [MeasurableSpace Ω] [MeasurableSpace 𝓧] [MeasurableSingletonClass Ω] [MeasurableSingletonClass 𝓧] [StandardBorelSpace Ω] [Nonempty Ω] (κ : Kernel Ω 𝓧) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] [IsFiniteKernel κ] {x : 𝓧} (hx : (μ.bind ⇑κ) {x} ≠ 0) (E₁ E₂ : Finset Ω) : ((posterior κ μ) x).real ↑E₁ < ((posterior κ μ) x).real ↑E₂ ↔ ∑ ω ∈ E₁, μ.real {ω} * (κ ω).real {x} < ∑ ω ∈ E₂, μ.real {ω} * (κ ω).real {x}

Comparing posterior masses of finite events reduces to comparing prior-weighted likelihood sums; the observation marginal cancels.

theorem ProbabilityTheory.posterior_apply_finset {Ω : Type u_1} {𝓧 : Type u_2} [MeasurableSpace Ω] [MeasurableSpace 𝓧] [MeasurableSingletonClass Ω] [MeasurableSingletonClass 𝓧] [StandardBorelSpace Ω] [Nonempty Ω] (κ : Kernel Ω 𝓧) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] [IsFiniteKernel κ] {x : 𝓧} (hx : (μ.bind ⇑κ) {x} ≠ 0) (E : Finset Ω) : ((posterior κ μ) x) ↑E = (∑ ω ∈ E, μ {ω} * (κ ω) {x}) / (μ.bind ⇑κ) {x}

The posterior mass of a finite event: prior-weighted likelihoods over the event, normalized by the observation marginal.

theorem ProbabilityTheory.posterior_deterministic_eq_cond {Ω : Type u_1} {𝓧 : Type u_2} [MeasurableSpace Ω] [MeasurableSpace 𝓧] [MeasurableSingletonClass Ω] [MeasurableSingletonClass 𝓧] [StandardBorelSpace Ω] [Nonempty Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] [Countable Ω] {f : Ω → 𝓧} (hf : Measurable f) {x : 𝓧} (hx : μ (f ⁻¹' {x}) ≠ 0) : (posterior (Kernel.deterministic f hf) μ) x = μ[|f ⁻¹' {x}]

A deterministic observation's posterior is the prior conditioned on the observation's fibre.

theorem MeasureTheory.Measure.comp_apply_singleton {Ω : Type u_1} {𝓧 : Type u_2} [MeasurableSpace Ω] [MeasurableSpace 𝓧] [MeasurableSingletonClass Ω] [MeasurableSingletonClass 𝓧] (κ : ProbabilityTheory.Kernel Ω 𝓧) (μ : Measure Ω) [Fintype Ω] (x : 𝓧) : (μ.bind ⇑κ) {x} = ∑ ω : Ω, μ {ω} * (κ ω) {x}

The observation marginal at an atom: prior mass times emission mass, summed over states.

theorem MeasureTheory.Measure.comp_real_singleton {Ω : Type u_1} {𝓧 : Type u_2} [MeasurableSpace Ω] [MeasurableSpace 𝓧] [MeasurableSingletonClass Ω] [MeasurableSingletonClass 𝓧] (κ : ProbabilityTheory.Kernel Ω 𝓧) (μ : Measure Ω) [IsFiniteMeasure μ] [ProbabilityTheory.IsFiniteKernel κ] [Fintype Ω] (x : 𝓧) : (μ.bind ⇑κ).real {x} = ∑ ω : Ω, μ.real {ω} * (κ ω).real {x}

theorem ProbabilityTheory.posterior_real_singleton {Ω : Type u_1} {𝓧 : Type u_2} [MeasurableSpace Ω] [MeasurableSpace 𝓧] [MeasurableSingletonClass Ω] [MeasurableSingletonClass 𝓧] [StandardBorelSpace Ω] [Nonempty Ω] (κ : Kernel Ω 𝓧) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] [IsFiniteKernel κ] {x : 𝓧} (hx : (μ.bind ⇑κ) {x} ≠ 0) (ω : Ω) : ((posterior κ μ) x).real {ω} = μ.real {ω} * (κ ω).real {x} / (μ.bind ⇑κ).real {x}

Exact Bayes on reals at a positive-mass observation.

theorem ProbabilityTheory.real_lt_posterior_real_singleton_iff {Ω : Type u_1} {𝓧 : Type u_2} [MeasurableSpace Ω] [MeasurableSpace 𝓧] [MeasurableSingletonClass Ω] [MeasurableSingletonClass 𝓧] [StandardBorelSpace Ω] [Nonempty Ω] (κ : Kernel Ω 𝓧) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] [IsFiniteKernel κ] {x : 𝓧} (hx : (μ.bind ⇑κ) {x} ≠ 0) {ω : Ω} (hω : μ {ω} ≠ 0) : μ.real {ω} < ((posterior κ μ) x).real {ω} ↔ (μ.bind ⇑κ).real {x} < (κ ω).real {x}

The posterior exceeds the prior at a state exactly when the state's likelihood of the observation exceeds the observation's marginal.

theorem ProbabilityTheory.posterior_real_singleton_lt_iff {Ω : Type u_1} {𝓧 : Type u_2} [MeasurableSpace Ω] [MeasurableSpace 𝓧] [MeasurableSingletonClass Ω] [MeasurableSingletonClass 𝓧] [StandardBorelSpace Ω] [Nonempty Ω] (κ : Kernel Ω 𝓧) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] [IsFiniteKernel κ] {x : 𝓧} (hx : (μ.bind ⇑κ) {x} ≠ 0) {ω : Ω} (hω : μ {ω} ≠ 0) : ((posterior κ μ) x).real {ω} < μ.real {ω} ↔ (κ ω).real {x} < (μ.bind ⇑κ).real {x}

The posterior falls below the prior at a state exactly when the state's likelihood of the observation falls below the observation's marginal.

Expectations under the posterior

Bayes' rule reweights the prior by the likelihood, so the posterior expectation of a statistic compares with its prior expectation as the statistic's covariance with the likelihood: the weighted Chebyshev sum inequality.

theorem ProbabilityTheory.sum_real_mul_le_sum_posterior_real_mul {Ω : Type u_1} {𝓧 : Type u_2} [MeasurableSpace Ω] [MeasurableSpace 𝓧] [MeasurableSingletonClass Ω] [MeasurableSingletonClass 𝓧] [StandardBorelSpace Ω] [Nonempty Ω] (κ : Kernel Ω 𝓧) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] [IsFiniteKernel κ] [Fintype Ω] [MeasureTheory.IsProbabilityMeasure μ] {x : 𝓧} (hx : (μ.bind ⇑κ) {x} ≠ 0) {f : Ω → ℝ} (hf : Monovary f fun (ω : Ω) => (κ ω).real {x}) : ∑ ω : Ω, μ.real {ω} * f ω ≤ ∑ ω : Ω, ((posterior κ μ) x).real {ω} * f ω

Conditioning on an observation raises the expectation of a statistic that monovaries with the observation's likelihood.

theorem ProbabilityTheory.sum_posterior_real_mul_le_sum_real_mul {Ω : Type u_1} {𝓧 : Type u_2} [MeasurableSpace Ω] [MeasurableSpace 𝓧] [MeasurableSingletonClass Ω] [MeasurableSingletonClass 𝓧] [StandardBorelSpace Ω] [Nonempty Ω] (κ : Kernel Ω 𝓧) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] [IsFiniteKernel κ] [Fintype Ω] [MeasureTheory.IsProbabilityMeasure μ] {x : 𝓧} (hx : (μ.bind ⇑κ) {x} ≠ 0) {f : Ω → ℝ} (hf : Antivary f fun (ω : Ω) => (κ ω).real {x}) : ∑ ω : Ω, ((posterior κ μ) x).real {ω} * f ω ≤ ∑ ω : Ω, μ.real {ω} * f ω

Conditioning on an observation lowers the expectation of a statistic that antivaries with the observation's likelihood.

Priors carried by two atoms

The _of_pair lemmas assume the prior's support lies in a pair {ω, ω'}, so that the observation's marginal has two terms and the comparison of the posterior with the prior at one atom is the comparison of the two likelihoods.

theorem MeasureTheory.Measure.comp_real_singleton_of_pair {Ω : Type u_1} {𝓧 : Type u_2} [MeasurableSpace Ω] [MeasurableSpace 𝓧] [MeasurableSingletonClass Ω] [MeasurableSingletonClass 𝓧] (κ : ProbabilityTheory.Kernel Ω 𝓧) (μ : Measure Ω) [IsFiniteMeasure μ] [ProbabilityTheory.IsFiniteKernel κ] [Fintype Ω] {ω ω' : Ω} (hne : ω ≠ ω') (hsupp : ∀ (ω'' : Ω), μ {ω''} ≠ 0 → ω'' = ω ∨ ω'' = ω') (x : 𝓧) : (μ.bind ⇑κ).real {x} = μ.real {ω} * (κ ω).real {x} + μ.real {ω'} * (κ ω').real {x}

Under a prior carried by two atoms, the observation's marginal is the prior-weighted sum of the two likelihoods.

theorem MeasureTheory.measureReal_singleton_add_singleton_of_pair {Ω : Type u_1} [MeasurableSpace Ω] [MeasurableSingletonClass Ω] (μ : Measure Ω) [IsFiniteMeasure μ] [Fintype Ω] {ω ω' : Ω} (hne : ω ≠ ω') (hsupp : ∀ (ω'' : Ω), μ {ω''} ≠ 0 → ω'' = ω ∨ ω'' = ω') [IsProbabilityMeasure μ] : μ.real {ω} + μ.real {ω'} = 1

A probability measure carried by two atoms puts mass one on them together.

theorem ProbabilityTheory.real_lt_posterior_real_singleton_iff_of_pair {Ω : Type u_1} {𝓧 : Type u_2} [MeasurableSpace Ω] [MeasurableSpace 𝓧] [MeasurableSingletonClass Ω] [MeasurableSingletonClass 𝓧] [StandardBorelSpace Ω] [Nonempty Ω] (κ : Kernel Ω 𝓧) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] [IsFiniteKernel κ] [Fintype Ω] {ω ω' : Ω} (hne : ω ≠ ω') (hsupp : ∀ (ω'' : Ω), μ {ω''} ≠ 0 → ω'' = ω ∨ ω'' = ω') [MeasureTheory.IsProbabilityMeasure μ] {x : 𝓧} (hx : (μ.bind ⇑κ) {x} ≠ 0) (hω : μ {ω} ≠ 0) (hω' : μ {ω'} ≠ 0) : μ.real {ω} < ((posterior κ μ) x).real {ω} ↔ (κ ω').real {x} < (κ ω).real {x}

Under a prior carried by two atoms, the posterior exceeds the prior at one of them exactly when its likelihood of the observation exceeds the other's.

theorem ProbabilityTheory.posterior_real_singleton_lt_iff_of_pair {Ω : Type u_1} {𝓧 : Type u_2} [MeasurableSpace Ω] [MeasurableSpace 𝓧] [MeasurableSingletonClass Ω] [MeasurableSingletonClass 𝓧] [StandardBorelSpace Ω] [Nonempty Ω] (κ : Kernel Ω 𝓧) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] [IsFiniteKernel κ] [Fintype Ω] {ω ω' : Ω} (hne : ω ≠ ω') (hsupp : ∀ (ω'' : Ω), μ {ω''} ≠ 0 → ω'' = ω ∨ ω'' = ω') [MeasureTheory.IsProbabilityMeasure μ] {x : 𝓧} (hx : (μ.bind ⇑κ) {x} ≠ 0) (hω : μ {ω} ≠ 0) (hω' : μ {ω'} ≠ 0) : ((posterior κ μ) x).real {ω} < μ.real {ω} ↔ (κ ω).real {x} < (κ ω').real {x}

Under a prior carried by two atoms, the posterior falls below the prior at one of them exactly when its likelihood of the observation falls below the other's.

theorem ProbabilityTheory.comp_apply_singleton_ne_zero {Ω' : Type u_3} {𝓧' : Type u_4} [MeasurableSpace Ω'] [MeasurableSpace 𝓧'] [MeasurableSingletonClass 𝓧'] (κ : Kernel Ω' 𝓧') (μ : MeasureTheory.Measure Ω') {w : Ω'} {x : 𝓧'} (hμ : μ {w} ≠ 0) (hκ : (κ w) {x} ≠ 0) : (μ.bind ⇑κ) {x} ≠ 0

A single state of positive prior mass and positive emission witnesses a positive observation marginal.

theorem MeasureTheory.Measure.compProd_apply_singleton {Ω : Type u_1} {Θ : Type u_2} [MeasurableSpace Ω] [MeasurableSpace Θ] [MeasurableSingletonClass Ω] [MeasurableSingletonClass Θ] (μ : Measure Ω) [SFinite μ] (κ : ProbabilityTheory.Kernel Ω Θ) [ProbabilityTheory.IsSFiniteKernel κ] (ω : Ω) (θ : Θ) : (μ.compProd κ) {(ω, θ)} = μ {ω} * (κ ω) {θ}

A prior-times-kernel joint at an atom is the prior mass times the kernel's mass.

theorem ProbabilityTheory.posterior_fst_real_singleton {𝓧 : Type u_1} [MeasurableSpace 𝓧] [MeasurableSingletonClass 𝓧] {A : Type u_2} {B : Type u_3} [MeasurableSpace A] [MeasurableSpace B] [MeasurableSingletonClass A] [MeasurableSingletonClass B] [StandardBorelSpace A] [Nonempty A] [StandardBorelSpace B] [Nonempty B] (κ : Kernel (A × B) 𝓧) (μ : MeasureTheory.Measure (A × B)) [MeasureTheory.IsFiniteMeasure μ] [IsFiniteKernel κ] {x : 𝓧} (hx : (μ.bind ⇑κ) {x} ≠ 0) [Fintype B] (a : A) : ((posterior κ μ) x).fst.real {a} = (∑ b : B, μ.real {(a, b)} * (κ (a, b)).real {x}) / (μ.bind ⇑κ).real {x}

The state marginal of the posterior over a product parameter space, on reals: prior-weighted likelihoods pooled over the latent, normalized by the observation marginal.

theorem ProbabilityTheory.posterior_snd_real_singleton {𝓧 : Type u_1} [MeasurableSpace 𝓧] [MeasurableSingletonClass 𝓧] {A : Type u_2} {B : Type u_3} [MeasurableSpace A] [MeasurableSpace B] [MeasurableSingletonClass A] [MeasurableSingletonClass B] [StandardBorelSpace A] [Nonempty A] [StandardBorelSpace B] [Nonempty B] (κ : Kernel (A × B) 𝓧) (μ : MeasureTheory.Measure (A × B)) [MeasureTheory.IsFiniteMeasure μ] [IsFiniteKernel κ] {x : 𝓧} (hx : (μ.bind ⇑κ) {x} ≠ 0) [Fintype A] (b : B) : ((posterior κ μ) x).snd.real {b} = (∑ a : A, μ.real {(a, b)} * (κ (a, b)).real {x}) / (μ.bind ⇑κ).real {x}

The latent marginal of the posterior over a product parameter space, on reals: prior-weighted likelihoods pooled over the states, normalized by the observation marginal.

theorem ProbabilityTheory.posterior_fst_real_lt_iff {𝓧 : Type u_1} [MeasurableSpace 𝓧] [MeasurableSingletonClass 𝓧] {A : Type u_2} {B : Type u_3} [MeasurableSpace A] [MeasurableSpace B] [MeasurableSingletonClass A] [MeasurableSingletonClass B] [StandardBorelSpace A] [Nonempty A] [StandardBorelSpace B] [Nonempty B] (κ : Kernel (A × B) 𝓧) (μ : MeasureTheory.Measure (A × B)) [MeasureTheory.IsFiniteMeasure μ] [IsFiniteKernel κ] {x : 𝓧} (hx : (μ.bind ⇑κ) {x} ≠ 0) [Fintype B] (a₁ a₂ : A) : ((posterior κ μ) x).fst.real {a₁} < ((posterior κ μ) x).fst.real {a₂} ↔ ∑ b : B, μ.real {(a₁, b)} * (κ (a₁, b)).real {x} < ∑ b : B, μ.real {(a₂, b)} * (κ (a₂, b)).real {x}

Marginal listener preference over a product parameter space, on reals: for latent-in-the-state models, the observation's marginal cancels and the latent pools.

theorem ProbabilityTheory.posterior_snd_real_lt_iff {𝓧 : Type u_1} [MeasurableSpace 𝓧] [MeasurableSingletonClass 𝓧] {A : Type u_2} {B : Type u_3} [MeasurableSpace A] [MeasurableSpace B] [MeasurableSingletonClass A] [MeasurableSingletonClass B] [StandardBorelSpace A] [Nonempty A] [StandardBorelSpace B] [Nonempty B] (κ : Kernel (A × B) 𝓧) (μ : MeasureTheory.Measure (A × B)) [MeasureTheory.IsFiniteMeasure μ] [IsFiniteKernel κ] {x : 𝓧} (hx : (μ.bind ⇑κ) {x} ≠ 0) [Fintype A] (b₁ b₂ : B) : ((posterior κ μ) x).snd.real {b₁} < ((posterior κ μ) x).snd.real {b₂} ↔ ∑ a : A, μ.real {(a, b₁)} * (κ (a, b₁)).real {x} < ∑ a : A, μ.real {(a, b₂)} * (κ (a, b₂)).real {x}

Marginal listener preference over the latent component of a product parameter space, on reals: the states pool.

theorem ProbabilityTheory.comp_uniformOn_univ_apply_singleton {𝓧 : Type u_1} [MeasurableSpace 𝓧] [MeasurableSingletonClass 𝓧] {W : Type u_2} [MeasurableSpace W] [MeasurableSingletonClass W] [Fintype W] (κ : Kernel W 𝓧) (x : 𝓧) : ((uniformOn Set.univ).bind ⇑κ) {x} = (↑(Fintype.card W))⁻¹ * ∑ w : W, (κ w) {x}

The observation marginal of a kernel against the uniform prior: the mean likelihood.

theorem ProbabilityTheory.posterior_uniformOn_univ_apply_singleton {𝓧 : Type u_1} [MeasurableSpace 𝓧] [MeasurableSingletonClass 𝓧] {W : Type u_2} [MeasurableSpace W] [MeasurableSingletonClass W] [StandardBorelSpace W] [Fintype W] [Nonempty W] (κ : Kernel W 𝓧) [IsFiniteKernel κ] {x : 𝓧} (hx : ∑ w : W, (κ w) {x} ≠ 0) (w : W) : ((posterior κ (uniformOn Set.univ)) x) {w} = (κ w) {x} / ∑ w' : W, (κ w') {x}

Bayes against the uniform prior: the posterior at a state is its likelihood of the observation normalized over the states, the prior cancelling.