Bayesian inverse (or posterior) #
Main definitions #
bayesInv: Bayesian inverse of a kernel
Main statements #
Notation #
κ†μ denotes the Bayesian inverse of κ with respect to μ, bayesInv κ μ.
Implementation details #
noncomputable def
ProbabilityTheory.bayesInv
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
[StandardBorelSpace α]
[Nonempty α]
(κ : ProbabilityTheory.Kernel α β)
(μ : MeasureTheory.Measure α)
[MeasureTheory.IsFiniteMeasure μ]
[ProbabilityTheory.IsFiniteKernel κ]
:
Bayesian inverse of the kernel κ with respect to the measure μ.
Equations
- ProbabilityTheory.bayesInv κ μ = (MeasureTheory.Measure.map Prod.swap (μ.compProd κ)).condKernel
Instances For
Bayesian inverse of the kernel κ with respect to the measure μ.
Equations
- ProbabilityTheory.«term_†_» = Lean.ParserDescr.trailingNode `ProbabilityTheory.term_†_ 1022 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "†") (Lean.ParserDescr.cat `term 0))
Instances For
instance
ProbabilityTheory.instIsMarkovKernelBayesInv
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{κ : ProbabilityTheory.Kernel α β}
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
[ProbabilityTheory.IsFiniteKernel κ]
[StandardBorelSpace α]
[Nonempty α]
:
The Bayesian inverse is a Markov kernel.
Equations
- ⋯ = ⋯
theorem
ProbabilityTheory.compProd_bayesInv
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
[StandardBorelSpace α]
[Nonempty α]
(κ : ProbabilityTheory.Kernel α β)
(μ : MeasureTheory.Measure α)
[MeasureTheory.IsFiniteMeasure μ]
[ProbabilityTheory.IsFiniteKernel κ]
:
(μ.bind ⇑κ).compProd (ProbabilityTheory.bayesInv κ μ) = MeasureTheory.Measure.map Prod.swap (μ.compProd κ)
The main property of the Bayesian inverse.
theorem
ProbabilityTheory.compProd_bayesInv'
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
[StandardBorelSpace α]
[Nonempty α]
(κ : ProbabilityTheory.Kernel α β)
(μ : MeasureTheory.Measure α)
[MeasureTheory.IsFiniteMeasure μ]
[ProbabilityTheory.IsFiniteKernel κ]
:
(μ.bind ⇑κ).bind ⇑(ProbabilityTheory.Kernel.id.prod (ProbabilityTheory.bayesInv κ μ)) = MeasureTheory.Measure.map Prod.swap (μ.bind ⇑(ProbabilityTheory.Kernel.id.prod κ))
theorem
ProbabilityTheory.compProd_bayesInv''
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
[StandardBorelSpace α]
[Nonempty α]
(κ : ProbabilityTheory.Kernel α β)
(μ : MeasureTheory.Measure α)
[MeasureTheory.IsFiniteMeasure μ]
[ProbabilityTheory.IsFiniteKernel κ]
:
((μ.bind ⇑κ).bind ⇑(ProbabilityTheory.Kernel.copy β)).bind
⇑(ProbabilityTheory.Kernel.id.parallelComp (ProbabilityTheory.bayesInv κ μ)) = (μ.bind ⇑(ProbabilityTheory.Kernel.copy α)).bind ⇑(κ.parallelComp ProbabilityTheory.Kernel.id)
theorem
ProbabilityTheory.compProd_bayesInv'''
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
[StandardBorelSpace α]
[Nonempty α]
(κ : ProbabilityTheory.Kernel α β)
(μ : MeasureTheory.Measure α)
[MeasureTheory.IsFiniteMeasure μ]
[ProbabilityTheory.IsFiniteKernel κ]
:
(μ.bind ⇑κ).compProd (ProbabilityTheory.bayesInv κ μ) = (μ.compProd κ).bind ⇑(ProbabilityTheory.Kernel.swap α β)
theorem
ProbabilityTheory.bayesInv_prod_id_comp
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
[StandardBorelSpace α]
[Nonempty α]
(κ : ProbabilityTheory.Kernel α β)
(μ : MeasureTheory.Measure α)
[MeasureTheory.IsFiniteMeasure μ]
[ProbabilityTheory.IsFiniteKernel κ]
:
(μ.bind ⇑κ).bind ⇑((ProbabilityTheory.bayesInv κ μ).prod ProbabilityTheory.Kernel.id) = μ.compProd κ
theorem
ProbabilityTheory.eq_bayesInv_of_compProd_eq
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{κ : ProbabilityTheory.Kernel α β}
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
[ProbabilityTheory.IsFiniteKernel κ]
[StandardBorelSpace α]
[Nonempty α]
(η : ProbabilityTheory.Kernel β α)
[ProbabilityTheory.IsFiniteKernel η]
(h : (μ.bind ⇑κ).compProd η = MeasureTheory.Measure.map Prod.swap (μ.compProd κ))
:
∀ᵐ (a : β) ∂μ.bind ⇑κ, η a = (ProbabilityTheory.bayesInv κ μ) a
The Bayesian inverse is unique up to a μ ∘ₘ κ-null set.
@[simp]
theorem
ProbabilityTheory.bayesInv_comp_self
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{κ : ProbabilityTheory.Kernel α β}
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
[ProbabilityTheory.IsFiniteKernel κ]
[StandardBorelSpace α]
[Nonempty α]
[ProbabilityTheory.IsMarkovKernel κ]
:
(μ.bind ⇑κ).bind ⇑(ProbabilityTheory.bayesInv κ μ) = μ
theorem
ProbabilityTheory.bayesInv_bayesInv
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{κ : ProbabilityTheory.Kernel α β}
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
[ProbabilityTheory.IsFiniteKernel κ]
[StandardBorelSpace α]
[Nonempty α]
[StandardBorelSpace β]
[Nonempty β]
[ProbabilityTheory.IsMarkovKernel κ]
:
∀ᵐ (a : α) ∂μ, (ProbabilityTheory.bayesInv (ProbabilityTheory.bayesInv κ μ) (μ.bind ⇑κ)) a = κ a
The Bayesian inverse is involutive (up to μ-a.e. equality).
theorem
ProbabilityTheory.bayesInv_id
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
[StandardBorelSpace α]
[Nonempty α]
:
∀ᵐ (a : α) ∂μ, (ProbabilityTheory.bayesInv ProbabilityTheory.Kernel.id μ) a = ProbabilityTheory.Kernel.id a
The Bayesian inverse of the identity kernel is the identity kernel.
theorem
ProbabilityTheory.bayesInv_comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{κ : ProbabilityTheory.Kernel α β}
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
[ProbabilityTheory.IsFiniteKernel κ]
[StandardBorelSpace α]
[Nonempty α]
[StandardBorelSpace β]
[Nonempty β]
{η : ProbabilityTheory.Kernel β γ}
[ProbabilityTheory.IsFiniteKernel η]
:
∀ᵐ (c : γ) ∂(μ.bind ⇑κ).bind ⇑η,
(ProbabilityTheory.bayesInv (η.comp κ) μ) c = ((ProbabilityTheory.bayesInv κ μ).comp (ProbabilityTheory.bayesInv η (μ.bind ⇑κ))) c
The Bayesian inverse is contravariant.