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

• posterior κ μ: posterior of a kernel κ for a prior measure μ.

Main statements

• compProd_posterior_eq_map_swap: the main property of the posterior, (κ ∘ₘ μ) ⊗ₘ κ†μ = (μ ⊗ₘ κ).map Prod.swap.

• ae_eq_posterior_of_compProd_eq

• posterior_comp_self: κ†μ ∘ₘ κ ∘ₘ μ = μ

• posterior_posterior: (κ†μ)†(κ ∘ₘ μ) =ᵐ[μ] κ

• posterior_comp: (η ∘ₖ κ)†μ =ᵐ[η ∘ₘ κ ∘ₘ μ] κ†μ ∘ₖ η†(κ ∘ₘ μ)

• posterior_eq_withDensity: If κ ω ≪ κ ∘ₘ μ for μ-almost every ω, then for κ ∘ₘ μ-almost every x, κ†μ x = μ.withDensity (fun ω ↦ κ.rnDeriv (Kernel.const _ (κ ∘ₘ μ)) ω x). The condition is true for countable Ω: see absolutelyContinuous_comp_of_countable.

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} {mΩ : MeasurableSpace Ω} {m𝓧 : MeasurableSpace 𝓧} [StandardBorelSpace Ω] [Nonempty Ω] (κ : Kernel Ω 𝓧) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] [IsFiniteKernel κ] : Kernel 𝓧 Ω

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

Equations

• ProbabilityTheory.posterior κ μ = (MeasureTheory.Measure.map Prod.swap (μ.compProd κ)).condKernel

def ProbabilityTheory.«term_†_» : Lean.TrailingParserDescr

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

Equations

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

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

The posterior is a Markov kernel.

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

The main property of the posterior.

theorem ProbabilityTheory.compProd_posterior_eq_swap_comp {Ω : Type u_1} {𝓧 : Type u_2} {mΩ : 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} {mΩ : MeasurableSpace Ω} {m𝓧 : MeasurableSpace 𝓧} {κ : Kernel Ω 𝓧} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] [IsFiniteKernel κ] [StandardBorelSpace Ω] [Nonempty Ω] : ((μ.bind ⇑κ).compProd (posterior κ μ)).bind ⇑(Kernel.swap 𝓧 Ω) = μ.compProd κ

theorem ProbabilityTheory.parallelProd_posterior_comp_copy_comp {Ω : Type u_1} {𝓧 : Type u_2} {mΩ : MeasurableSpace Ω} {m𝓧 : MeasurableSpace 𝓧} {κ : Kernel Ω 𝓧} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] [IsFiniteKernel κ] [StandardBorelSpace Ω] [Nonempty Ω] : ((μ.bind ⇑κ).bind ⇑(Kernel.copy 𝓧)).bind ⇑(Kernel.id.parallelComp (posterior κ μ)) = (μ.bind ⇑(Kernel.copy Ω)).bind ⇑(κ.parallelComp Kernel.id)

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} {mΩ : 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} {mΩ : 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} {mΩ : 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} {mΩ : MeasurableSpace Ω} {m𝓧 : MeasurableSpace 𝓧} {κ : Kernel Ω 𝓧} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] [IsFiniteKernel κ] [StandardBorelSpace Ω] [Nonempty Ω] [IsMarkovKernel κ] : (μ.bind ⇑κ).bind ⇑(posterior κ μ) = μ

theorem ProbabilityTheory.posterior_id {Ω : Type u_1} {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] [Nonempty Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] : ⇑(posterior Kernel.id μ) =ᵐ[μ] ⇑Kernel.id

The posterior of the identity kernel is the identity kernel.

theorem ProbabilityTheory.deterministic_comp_posterior {Ω : Type u_1} {𝓧 : Type u_2} {mΩ : MeasurableSpace Ω} {m𝓧 : MeasurableSpace 𝓧} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] [StandardBorelSpace Ω] [Nonempty Ω] [MeasurableSpace.CountablyGenerated 𝓧] {f : Ω → 𝓧} (hf : Measurable f) : ⇑((Kernel.deterministic f hf).comp (posterior (Kernel.deterministic f hf) μ)) =ᵐ[MeasureTheory.Measure.map f μ] ⇑Kernel.id

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

theorem ProbabilityTheory.absolutelyContinuous_posterior {Ω : Type u_1} {𝓧 : Type u_2} {mΩ : 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} {mΩ : 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} {mΩ : 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.absolutelyContinuous_of_posterior {Ω : Type u_1} {𝓧 : Type u_2} {mΩ : MeasurableSpace Ω} {m𝓧 : MeasurableSpace 𝓧} {κ : Kernel Ω 𝓧} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] [IsFiniteKernel κ] [StandardBorelSpace Ω] [Nonempty Ω] [MeasurableSpace.CountableOrCountablyGenerated Ω 𝓧] (h_ac : ∀ᵐ (b : 𝓧) ∂μ.bind ⇑κ, ((posterior κ μ) b).AbsolutelyContinuous μ) : ∀ᵐ (ω : Ω) ∂μ, (κ ω).AbsolutelyContinuous (μ.bind ⇑κ)

theorem ProbabilityTheory.absolutelyContinuous_posterior_iff {Ω : Type u_1} {𝓧 : Type u_2} {mΩ : MeasurableSpace Ω} {m𝓧 : MeasurableSpace 𝓧} {κ : Kernel Ω 𝓧} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] [IsFiniteKernel κ] [StandardBorelSpace Ω] [Nonempty Ω] [MeasurableSpace.CountableOrCountablyGenerated Ω 𝓧] : (∀ᵐ (b : 𝓧) ∂μ.bind ⇑κ, ((posterior κ μ) b).AbsolutelyContinuous μ) ↔ ∀ᵐ (ω : Ω) ∂μ, (κ ω).AbsolutelyContinuous (μ.bind ⇑κ)

theorem ProbabilityTheory.Kernel.absolutelyContinuous_comp_of_absolutelyContinuous {Ω : Type u_1} {𝓧 : Type u_2} {mΩ : MeasurableSpace Ω} {m𝓧 : MeasurableSpace 𝓧} {κ : Kernel Ω 𝓧} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] [IsFiniteKernel κ] [StandardBorelSpace Ω] [Nonempty Ω] [MeasurableSpace.CountableOrCountablyGenerated Ω 𝓧] {ν : MeasureTheory.Measure 𝓧} [MeasureTheory.SFinite ν] (h_ac : ∀ᵐ (ω : Ω) ∂μ, (κ ω).AbsolutelyContinuous ν) : ∀ᵐ (ω : Ω) ∂μ, (κ ω).AbsolutelyContinuous (μ.bind ⇑κ)

theorem ProbabilityTheory.rnDeriv_posterior_ae_prod {Ω : Type u_1} {𝓧 : Type u_2} {mΩ : 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} {mΩ : 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} {mΩ : 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} {mΩ : 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 Ω.