Documentation

Mathlib.Probability.Kernel.Posterior

Posterior kernel #

For μ : Measure Ω (called prior measure), seen as a measure on a parameter, and a kernel κ : Kernel Ω 𝓧 that gives the conditional distribution of "data" in 𝓧 given the prior parameter, we can get the distribution of the data with κ ∘ₘ μ, and the joint distribution of parameter and data with μ ⊗ₘ κ : Measure (Ω × 𝓧).

The posterior distribution of the parameter given the data is a Markov kernel κ†μ : Kernel 𝓧 Ω such that (κ ∘ₘ μ) ⊗ₘ κ†μ = (μ ⊗ₘ κ).map Prod.swap. That is, the joint distribution of parameter and data can be recovered from the distribution of the data and the posterior.

Main definitions #

Main statements #

Notation #

κ†μ denotes the posterior of κ with respect to μ, posterior κ μ. can be typed as \dag or \dagger.

This notation emphasizes that the posterior is a kind of inverse of κ, which we would want to denote κ†, but we have to also specify the measure μ.

noncomputable def ProbabilityTheory.posterior {Ω : Type u_1} {𝓧 : Type u_2} { : MeasurableSpace Ω} {m𝓧 : MeasurableSpace 𝓧} [StandardBorelSpace Ω] [Nonempty Ω] (κ : Kernel Ω 𝓧) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] [IsFiniteKernel κ] :
Kernel 𝓧 Ω

Posterior of the kernel κ with respect to the measure μ.

Equations

Posterior of the kernel κ with respect to the measure μ.

Equations
  • One or more equations did not get rendered due to their size.

The posterior is a Markov kernel.

The main property of the posterior.

theorem ProbabilityTheory.compProd_posterior_eq_swap_comp {Ω : Type u_1} {𝓧 : Type u_2} { : MeasurableSpace Ω} {m𝓧 : MeasurableSpace 𝓧} {κ : Kernel Ω 𝓧} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] [IsFiniteKernel κ] [StandardBorelSpace Ω] [Nonempty Ω] :
(μ.bind κ).compProd (posterior κ μ) = (μ.compProd κ).bind (Kernel.swap Ω 𝓧)
theorem ProbabilityTheory.swap_compProd_posterior {Ω : Type u_1} {𝓧 : Type u_2} { : MeasurableSpace Ω} {m𝓧 : MeasurableSpace 𝓧} {κ : Kernel Ω 𝓧} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] [IsFiniteKernel κ] [StandardBorelSpace Ω] [Nonempty Ω] :
((μ.bind κ).compProd (posterior κ μ)).bind (Kernel.swap 𝓧 Ω) = μ.compProd κ

The main property of the posterior, as equality of the following diagrams:

         -- id          -- κ
μ -- κ -|        =  μ -|
         -- κ†μ         -- id
theorem ProbabilityTheory.posterior_prod_id_comp {Ω : Type u_1} {𝓧 : Type u_2} { : MeasurableSpace Ω} {m𝓧 : MeasurableSpace 𝓧} {κ : Kernel Ω 𝓧} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] [IsFiniteKernel κ] [StandardBorelSpace Ω] [Nonempty Ω] :
(μ.bind κ).bind ((posterior κ μ).prod Kernel.id) = μ.compProd κ
theorem ProbabilityTheory.ae_eq_posterior_of_compProd_eq {Ω : Type u_1} {𝓧 : Type u_2} { : MeasurableSpace Ω} {m𝓧 : MeasurableSpace 𝓧} {κ : Kernel Ω 𝓧} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] [IsFiniteKernel κ] [StandardBorelSpace Ω] [Nonempty Ω] {η : Kernel 𝓧 Ω} [IsFiniteKernel η] (h : (μ.bind κ).compProd η = MeasureTheory.Measure.map Prod.swap (μ.compProd κ)) :
η =ᵐ[μ.bind κ] (posterior κ μ)

The posterior is unique up to a κ ∘ₘ μ-null set.

theorem ProbabilityTheory.ae_eq_posterior_of_compProd_eq_swap_comp {Ω : Type u_1} {𝓧 : Type u_2} { : MeasurableSpace Ω} {m𝓧 : MeasurableSpace 𝓧} {κ : Kernel Ω 𝓧} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] [IsFiniteKernel κ] [StandardBorelSpace Ω] [Nonempty Ω] (η : Kernel 𝓧 Ω) [IsFiniteKernel η] (h : (μ.bind κ).compProd η = (μ.compProd κ).bind (Kernel.swap Ω 𝓧)) :
η =ᵐ[μ.bind κ] (posterior κ μ)

The posterior is unique up to a κ ∘ₘ μ-null set.

@[simp]
theorem ProbabilityTheory.posterior_comp_self {Ω : Type u_1} {𝓧 : Type u_2} { : MeasurableSpace Ω} {m𝓧 : MeasurableSpace 𝓧} {κ : Kernel Ω 𝓧} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] [IsFiniteKernel κ] [StandardBorelSpace Ω] [Nonempty Ω] [IsMarkovKernel κ] :
(μ.bind κ).bind (posterior κ μ) = μ

The posterior of the identity kernel is the identity kernel.

For a deterministic kernel κ, κ ∘ₖ κ†μ is μ.map f-a.e. equal to the identity kernel.

theorem ProbabilityTheory.absolutelyContinuous_posterior {Ω : Type u_1} {𝓧 : Type u_2} { : MeasurableSpace Ω} {m𝓧 : MeasurableSpace 𝓧} {κ : Kernel Ω 𝓧} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] [IsFiniteKernel κ] [StandardBorelSpace Ω] [Nonempty Ω] {ν : MeasureTheory.Measure 𝓧} [MeasureTheory.SFinite ν] (h_ac : ∀ᵐ (ω : Ω) μ, (κ ω).AbsolutelyContinuous ν) :
∀ᵐ (b : 𝓧) μ.bind κ, ((posterior κ μ) b).AbsolutelyContinuous μ
theorem ProbabilityTheory.posterior_posterior {Ω : Type u_1} {𝓧 : Type u_2} { : MeasurableSpace Ω} {m𝓧 : MeasurableSpace 𝓧} {κ : Kernel Ω 𝓧} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] [IsFiniteKernel κ] [StandardBorelSpace Ω] [Nonempty Ω] [StandardBorelSpace 𝓧] [Nonempty 𝓧] [IsMarkovKernel κ] :
(posterior (posterior κ μ) (μ.bind κ)) =ᵐ[μ] κ

The posterior is involutive (up to μ-a.e. equality).

theorem ProbabilityTheory.posterior_comp {Ω : Type u_1} {𝓧 : Type u_2} {𝓨 : Type u_3} { : MeasurableSpace Ω} {m𝓧 : MeasurableSpace 𝓧} {m𝓨 : MeasurableSpace 𝓨} {κ : Kernel Ω 𝓧} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] [IsFiniteKernel κ] [StandardBorelSpace Ω] [Nonempty Ω] [StandardBorelSpace 𝓧] [Nonempty 𝓧] {η : Kernel 𝓧 𝓨} [IsFiniteKernel η] :
(posterior (η.comp κ) μ) =ᵐ[(μ.bind κ).bind η] ((posterior κ μ).comp (posterior η (μ.bind κ)))

The posterior is contravariant.

theorem ProbabilityTheory.rnDeriv_posterior_ae_prod {Ω : Type u_1} {𝓧 : Type u_2} { : MeasurableSpace Ω} {m𝓧 : MeasurableSpace 𝓧} {κ : Kernel Ω 𝓧} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] [IsFiniteKernel κ] [StandardBorelSpace Ω] [Nonempty Ω] [MeasurableSpace.CountableOrCountablyGenerated Ω 𝓧] (h_ac : ∀ᵐ (ω : Ω) μ, (κ ω).AbsolutelyContinuous (μ.bind κ)) :
∀ᵐ (p : Ω × 𝓧) μ.prod (μ.bind κ), (posterior κ μ).rnDeriv (Kernel.const 𝓧 μ) p.2 p.1 = κ.rnDeriv (Kernel.const Ω (μ.bind κ)) p.1 p.2
theorem ProbabilityTheory.rnDeriv_posterior {Ω : Type u_1} {𝓧 : Type u_2} { : MeasurableSpace Ω} {m𝓧 : MeasurableSpace 𝓧} {κ : Kernel Ω 𝓧} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] [IsFiniteKernel κ] [StandardBorelSpace Ω] [Nonempty Ω] [MeasurableSpace.CountableOrCountablyGenerated Ω 𝓧] (h_ac : ∀ᵐ (ω : Ω) μ, (κ ω).AbsolutelyContinuous (μ.bind κ)) :
∀ᵐ (ω : Ω) μ, ∀ᵐ (x : 𝓧) μ.bind κ, (posterior κ μ).rnDeriv (Kernel.const 𝓧 μ) x ω = κ.rnDeriv (Kernel.const Ω (μ.bind κ)) ω x
theorem ProbabilityTheory.rnDeriv_posterior_symm {Ω : Type u_1} {𝓧 : Type u_2} { : MeasurableSpace Ω} {m𝓧 : MeasurableSpace 𝓧} {κ : Kernel Ω 𝓧} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] [IsFiniteKernel κ] [StandardBorelSpace Ω] [Nonempty Ω] [MeasurableSpace.CountableOrCountablyGenerated Ω 𝓧] (h_ac : ∀ᵐ (ω : Ω) μ, (κ ω).AbsolutelyContinuous (μ.bind κ)) :
∀ᵐ (x : 𝓧) μ.bind κ, ∀ᵐ (ω : Ω) μ, (posterior κ μ).rnDeriv (Kernel.const 𝓧 μ) x ω = κ.rnDeriv (Kernel.const Ω (μ.bind κ)) ω x
theorem ProbabilityTheory.posterior_eq_withDensity {Ω : Type u_1} {𝓧 : Type u_2} { : MeasurableSpace Ω} {m𝓧 : MeasurableSpace 𝓧} {κ : Kernel Ω 𝓧} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] [IsFiniteKernel κ] [StandardBorelSpace Ω] [Nonempty Ω] [MeasurableSpace.CountableOrCountablyGenerated Ω 𝓧] (h_ac : ∀ᵐ (ω : Ω) μ, (κ ω).AbsolutelyContinuous (μ.bind κ)) :
∀ᵐ (x : 𝓧) μ.bind κ, (posterior κ μ) x = μ.withDensity fun (ω : Ω) => κ.rnDeriv (Kernel.const Ω (μ.bind κ)) ω x

If κ ω ≪ κ ∘ₘ μ for μ-almost every ω, then for κ ∘ₘ μ-almost every x, κ†μ x = μ.withDensity (fun ω ↦ κ.rnDeriv (Kernel.const _ (κ ∘ₘ μ)) ω x). This is a form of Bayes' theorem. The condition is true for example for countable Ω.