A predicate for having a specified conditional distribution #
We introduce a predicate HasCondDistrib Y X κ P stating that the conditional distribution of Y
given X under the measure P is equal to the kernel κ.
The statement uses HasLaw to express that the law of the pair (X, Y) under P is equal to
(P.map X) ⊗ₘ κ, the product of the law of X under P and the kernel κ.
The use of HasLaw also implies that Y and X are a.e. measurable.
Main definitions #
HasCondDistrib Y X κ P: predicate stating that the conditional distribution ofYgivenXunder the measurePis equal to the kernelκ.
def
ProbabilityTheory.HasCondDistrib
{Ω : Type u_1}
{𝓧 : Type u_2}
{𝓨 : Type u_3}
{mΩ : MeasurableSpace Ω}
{m𝓧 : MeasurableSpace 𝓧}
{m𝓨 : MeasurableSpace 𝓨}
(Y : Ω → 𝓨)
(X : Ω → 𝓧)
(κ : Kernel 𝓧 𝓨)
(P : MeasureTheory.Measure Ω)
:
Predicate stating that the conditional distribution of Y given X under the measure P
is equal to the kernel κ.
Equations
- ProbabilityTheory.HasCondDistrib Y X κ P = ProbabilityTheory.HasLaw (fun (ω : Ω) => (X ω, Y ω)) ((MeasureTheory.Measure.map X P).compProd κ) P
Instances For
theorem
ProbabilityTheory.HasCondDistrib.aemeasurable_fst
{Ω : Type u_1}
{𝓧 : Type u_2}
{𝓨 : Type u_3}
{mΩ : MeasurableSpace Ω}
{m𝓧 : MeasurableSpace 𝓧}
{m𝓨 : MeasurableSpace 𝓨}
{P : MeasureTheory.Measure Ω}
{X : Ω → 𝓧}
{Y : Ω → 𝓨}
{κ : Kernel 𝓧 𝓨}
(h : HasCondDistrib Y X κ P)
:
AEMeasurable X P
theorem
ProbabilityTheory.HasCondDistrib.aemeasurable_snd
{Ω : Type u_1}
{𝓧 : Type u_2}
{𝓨 : Type u_3}
{mΩ : MeasurableSpace Ω}
{m𝓧 : MeasurableSpace 𝓧}
{m𝓨 : MeasurableSpace 𝓨}
{P : MeasureTheory.Measure Ω}
{X : Ω → 𝓧}
{Y : Ω → 𝓨}
{κ : Kernel 𝓧 𝓨}
(h : HasCondDistrib Y X κ P)
:
AEMeasurable Y P
theorem
ProbabilityTheory.HasLaw.prodMk_of_hasCondDistrib
{Ω : Type u_1}
{𝓧 : Type u_2}
{𝓨 : Type u_3}
{mΩ : MeasurableSpace Ω}
{m𝓧 : MeasurableSpace 𝓧}
{m𝓨 : MeasurableSpace 𝓨}
{P : MeasureTheory.Measure Ω}
{X : Ω → 𝓧}
{Y : Ω → 𝓨}
{κ : Kernel 𝓧 𝓨}
{Q : MeasureTheory.Measure 𝓧}
[IsSFiniteKernel κ]
(h1 : HasLaw X Q P)
(h2 : HasCondDistrib Y X κ P)
:
theorem
ProbabilityTheory.HasCondDistrib.hasLaw_of_const
{Ω : Type u_1}
{𝓧 : Type u_2}
{𝓨 : Type u_3}
{mΩ : MeasurableSpace Ω}
{m𝓧 : MeasurableSpace 𝓧}
{m𝓨 : MeasurableSpace 𝓨}
{P : MeasureTheory.Measure Ω}
{X : Ω → 𝓧}
{Y : Ω → 𝓨}
[MeasureTheory.IsProbabilityMeasure P]
{Q : MeasureTheory.Measure 𝓨}
[MeasureTheory.SFinite Q]
(h : HasCondDistrib Y X (Kernel.const 𝓧 Q) P)
:
HasLaw Y Q P
theorem
ProbabilityTheory.HasCondDistrib.comp_left
{Ω : Type u_1}
{𝓧 : Type u_2}
{𝓨 : Type u_3}
{𝓩 : Type u_4}
{mΩ : MeasurableSpace Ω}
{m𝓧 : MeasurableSpace 𝓧}
{m𝓨 : MeasurableSpace 𝓨}
{m𝓩 : MeasurableSpace 𝓩}
{P : MeasureTheory.Measure Ω}
{X : Ω → 𝓧}
{Y : Ω → 𝓨}
{κ : Kernel 𝓧 𝓨}
[MeasureTheory.SFinite P]
[IsSFiniteKernel κ]
(h : HasCondDistrib Y X κ P)
{f : 𝓨 → 𝓩}
(hf : Measurable f)
:
HasCondDistrib (f ∘ Y) X (κ.map f) P
theorem
ProbabilityTheory.HasCondDistrib.fst
{Ω : Type u_1}
{𝓧 : Type u_2}
{𝓨 : Type u_3}
{𝓩 : Type u_4}
{mΩ : MeasurableSpace Ω}
{m𝓧 : MeasurableSpace 𝓧}
{m𝓨 : MeasurableSpace 𝓨}
{m𝓩 : MeasurableSpace 𝓩}
{P : MeasureTheory.Measure Ω}
{X : Ω → 𝓧}
[MeasureTheory.SFinite P]
{Y : Ω → 𝓨 × 𝓩}
{κ : Kernel 𝓧 (𝓨 × 𝓩)}
[IsSFiniteKernel κ]
(h : HasCondDistrib Y X κ P)
:
HasCondDistrib (fun (ω : Ω) => (Y ω).1) X κ.fst P
theorem
ProbabilityTheory.HasCondDistrib.snd
{Ω : Type u_1}
{𝓧 : Type u_2}
{𝓨 : Type u_3}
{𝓩 : Type u_4}
{mΩ : MeasurableSpace Ω}
{m𝓧 : MeasurableSpace 𝓧}
{m𝓨 : MeasurableSpace 𝓨}
{m𝓩 : MeasurableSpace 𝓩}
{P : MeasureTheory.Measure Ω}
{X : Ω → 𝓧}
[MeasureTheory.SFinite P]
{Y : Ω → 𝓨 × 𝓩}
{κ : Kernel 𝓧 (𝓨 × 𝓩)}
[IsSFiniteKernel κ]
(h : HasCondDistrib Y X κ P)
:
HasCondDistrib (fun (ω : Ω) => (Y ω).2) X κ.snd P
theorem
ProbabilityTheory.HasCondDistrib.comp_right
{Ω : Type u_1}
{𝓧 : Type u_2}
{𝓨 : Type u_3}
{𝓩 : Type u_4}
{mΩ : MeasurableSpace Ω}
{m𝓧 : MeasurableSpace 𝓧}
{m𝓨 : MeasurableSpace 𝓨}
{m𝓩 : MeasurableSpace 𝓩}
{P : MeasureTheory.Measure Ω}
{Y : Ω → 𝓨}
{κ : Kernel 𝓧 𝓨}
[MeasureTheory.SFinite P]
[IsSFiniteKernel κ]
{f : 𝓩 → 𝓧}
{hf : Measurable f}
{Z : Ω → 𝓩}
(h : HasCondDistrib Y Z (κ.comap f hf) P)
:
HasCondDistrib Y (f ∘ Z) κ P
theorem
ProbabilityTheory.HasCondDistrib.measurableEquiv_comp_right
{Ω : Type u_1}
{𝓧 : Type u_2}
{𝓨 : Type u_3}
{𝓩 : Type u_4}
{mΩ : MeasurableSpace Ω}
{m𝓧 : MeasurableSpace 𝓧}
{m𝓨 : MeasurableSpace 𝓨}
{m𝓩 : MeasurableSpace 𝓩}
{P : MeasureTheory.Measure Ω}
{X : Ω → 𝓧}
{Y : Ω → 𝓨}
{κ : Kernel 𝓧 𝓨}
[MeasureTheory.SFinite P]
[IsSFiniteKernel κ]
(h : HasCondDistrib Y X κ P)
(f : 𝓧 ≃ᵐ 𝓩)
:
HasCondDistrib Y (⇑f ∘ X) (κ.comap ⇑f.symm ⋯) P
theorem
ProbabilityTheory.HasCondDistrib.of_compProd
{Ω : Type u_1}
{𝓧 : Type u_2}
{𝓨 : Type u_3}
{𝓩 : Type u_4}
{mΩ : MeasurableSpace Ω}
{m𝓧 : MeasurableSpace 𝓧}
{m𝓨 : MeasurableSpace 𝓨}
{m𝓩 : MeasurableSpace 𝓩}
{P : MeasureTheory.Measure Ω}
{X : Ω → 𝓧}
{Y : Ω → 𝓨}
{κ : Kernel 𝓧 𝓨}
[MeasureTheory.SFinite P]
[IsSFiniteKernel κ]
{Z : Ω → 𝓩}
{η : Kernel (𝓧 × 𝓨) 𝓩}
[IsMarkovKernel η]
(h : HasCondDistrib (fun (a : Ω) => (Y a, Z a)) X (κ.compProd η) P)
:
HasCondDistrib Z (fun (a : Ω) => (X a, Y a)) η P