A predicate for having a specified conditional distribution #
structure
ProbabilityTheory.HasCondDistrib
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_4}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mΩ : MeasurableSpace Ω}
[StandardBorelSpace Ω]
[Nonempty Ω]
(Y : α → Ω)
(X : α → β)
(κ : Kernel β Ω)
(μ : MeasureTheory.Measure α)
[MeasureTheory.IsFiniteMeasure μ]
:
Predicate stating that the conditional distribution of Y given X under the measure μ
is equal to the kernel κ.
- aemeasurable_fst : AEMeasurable Y μ
- aemeasurable_snd : AEMeasurable X μ
Instances For
theorem
ProbabilityTheory.hasCondDistrib_fst_prod
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{Ω : Type u_4}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{mΩ : MeasurableSpace Ω}
[StandardBorelSpace Ω]
[Nonempty Ω]
{Y : α → Ω}
{X : α → β}
{κ : Kernel β Ω}
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
{ν : MeasureTheory.Measure γ}
[MeasureTheory.IsProbabilityMeasure ν]
(h : HasCondDistrib Y X κ μ)
:
HasCondDistrib (fun (ω : α × γ) => Y ω.1) (fun (ω : α × γ) => X ω.1) κ (μ.prod ν)
theorem
ProbabilityTheory.HasCondDistrib.comp
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_4}
{Ω' : Type u_5}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mΩ : MeasurableSpace Ω}
[StandardBorelSpace Ω]
[Nonempty Ω]
{mΩ' : MeasurableSpace Ω'}
[StandardBorelSpace Ω']
[Nonempty Ω']
{μ : MeasureTheory.Measure α}
{X : α → β}
{Y : α → Ω}
{κ : Kernel β Ω}
[MeasureTheory.IsFiniteMeasure μ]
(h : HasCondDistrib Y X κ μ)
{f : Ω → Ω'}
(hf : Measurable f)
:
HasCondDistrib (fun (ω : α) => f (Y ω)) X (κ.map f) μ
theorem
ProbabilityTheory.HasCondDistrib.fst
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_4}
{Ω' : Type u_5}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mΩ : MeasurableSpace Ω}
[StandardBorelSpace Ω]
[Nonempty Ω]
{mΩ' : MeasurableSpace Ω'}
[StandardBorelSpace Ω']
[Nonempty Ω']
{μ : MeasureTheory.Measure α}
{X : α → β}
{Y : α → Ω × Ω'}
{κ : Kernel β (Ω × Ω')}
[MeasureTheory.IsFiniteMeasure μ]
(h : HasCondDistrib Y X κ μ)
:
HasCondDistrib (fun (ω : α) => (Y ω).1) X κ.fst μ
theorem
ProbabilityTheory.HasCondDistrib.snd
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_4}
{Ω' : Type u_5}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mΩ : MeasurableSpace Ω}
[StandardBorelSpace Ω]
[Nonempty Ω]
{mΩ' : MeasurableSpace Ω'}
[StandardBorelSpace Ω']
[Nonempty Ω']
{μ : MeasureTheory.Measure α}
{X : α → β}
{Y : α → Ω × Ω'}
{κ : Kernel β (Ω × Ω')}
[MeasureTheory.IsFiniteMeasure μ]
(h : HasCondDistrib Y X κ μ)
:
HasCondDistrib (fun (ω : α) => (Y ω).2) X κ.snd μ
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 Ω}
[StandardBorelSpace Ω]
[Nonempty Ω]
{μ : MeasureTheory.Measure α}
{Y : α → Ω}
{κ : Kernel β Ω}
[MeasureTheory.IsFiniteMeasure μ]
[IsFiniteKernel κ]
{f : γ → β}
(hf : Measurable f)
{Z : α → γ}
(h : HasCondDistrib Y Z (κ.comap f hf) μ)
:
HasCondDistrib Y (f ∘ Z) κ μ
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 Ω}
[StandardBorelSpace Ω]
[Nonempty Ω]
{μ : MeasureTheory.Measure α}
{X : α → β}
{Y : α → Ω}
{κ : Kernel β Ω}
[MeasureTheory.IsFiniteMeasure μ]
[IsFiniteKernel κ]
(h : HasCondDistrib Y X κ μ)
(f : β ≃ᵐ γ)
:
HasCondDistrib Y (⇑f ∘ X) (κ.comap ⇑f.symm ⋯) μ
theorem
ProbabilityTheory.HasCondDistrib.prod_right
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{Ω : Type u_4}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{mΩ : MeasurableSpace Ω}
[StandardBorelSpace Ω]
[Nonempty Ω]
{μ : MeasureTheory.Measure α}
{X : α → β}
{Y : α → Ω}
{κ : Kernel β Ω}
[MeasureTheory.IsFiniteMeasure μ]
[IsFiniteKernel κ]
(h : HasCondDistrib Y X κ μ)
{f : β → γ}
(hf : Measurable f)
:
HasCondDistrib Y (fun (a : α) => (X a, f (X a))) (Kernel.prodMkRight γ κ) μ
theorem
ProbabilityTheory.hasCondDistrib_prod_right_iff
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{Ω : Type u_4}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{mΩ : MeasurableSpace Ω}
[StandardBorelSpace Ω]
[Nonempty Ω]
{μ : MeasureTheory.Measure α}
{κ : Kernel β Ω}
[MeasureTheory.IsFiniteMeasure μ]
[IsFiniteKernel κ]
(X : α → β)
(Y : α → Ω)
{f : β → γ}
(hf : Measurable f)
:
HasCondDistrib Y (fun (a : α) => (X a, f (X a))) (Kernel.prodMkRight γ κ) μ ↔ HasCondDistrib Y X κ μ
theorem
ProbabilityTheory.HasCondDistrib.hasLaw_of_const
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_4}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mΩ : MeasurableSpace Ω}
[StandardBorelSpace Ω]
[Nonempty Ω]
{μ : MeasureTheory.Measure α}
{X : α → β}
{Y : α → Ω}
[MeasureTheory.IsProbabilityMeasure μ]
{Q : MeasureTheory.Measure Ω}
[MeasureTheory.SFinite Q]
(h : HasCondDistrib Y X (Kernel.const β Q) μ)
:
HasLaw Y Q μ
theorem
ProbabilityTheory.HasCondDistrib.indepFun_of_const
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_4}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mΩ : MeasurableSpace Ω}
[StandardBorelSpace Ω]
[Nonempty Ω]
{μ : MeasureTheory.Measure α}
{X : α → β}
{Y : α → Ω}
[MeasureTheory.IsProbabilityMeasure μ]
{Q : MeasureTheory.Measure Ω}
[MeasureTheory.SFinite Q]
(h : HasCondDistrib Y X (Kernel.const β Q) μ)
:
IndepFun X Y μ
theorem
ProbabilityTheory.HasCondDistrib.const_map_of_const
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_4}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mΩ : MeasurableSpace Ω}
[StandardBorelSpace Ω]
[Nonempty Ω]
{μ : MeasureTheory.Measure α}
{X : α → β}
{Y : α → Ω}
[MeasureTheory.IsProbabilityMeasure μ]
{Q : MeasureTheory.Measure Ω}
[MeasureTheory.SFinite Q]
(h : HasCondDistrib Y X (Kernel.const β Q) μ)
[StandardBorelSpace β]
[Nonempty β]
:
HasCondDistrib X Y (Kernel.const Ω (MeasureTheory.Measure.map X μ)) μ
theorem
ProbabilityTheory.HasLaw.prod_of_hasCondDistrib
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_4}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mΩ : MeasurableSpace Ω}
[StandardBorelSpace Ω]
[Nonempty Ω]
{μ : MeasureTheory.Measure α}
{X : α → β}
{Y : α → Ω}
{κ : Kernel β Ω}
{P : MeasureTheory.Measure β}
[MeasureTheory.IsFiniteMeasure μ]
[IsSFiniteKernel κ]
(h1 : HasLaw X P μ)
(h2 : HasCondDistrib Y X κ μ)
:
theorem
ProbabilityTheory.HasCondDistrib.of_compProd
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_4}
{Ω' : Type u_5}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mΩ : MeasurableSpace Ω}
[StandardBorelSpace Ω]
[Nonempty Ω]
{mΩ' : MeasurableSpace Ω'}
[StandardBorelSpace Ω']
[Nonempty Ω']
{μ : MeasureTheory.Measure α}
{X : α → β}
{Y : α → Ω}
{κ : Kernel β Ω}
[MeasureTheory.IsFiniteMeasure μ]
[IsFiniteKernel κ]
{Z : α → Ω'}
{η : Kernel (β × Ω) Ω'}
[IsMarkovKernel η]
(h : HasCondDistrib (fun (a : α) => (Y a, Z a)) X (κ.compProd η) μ)
:
HasCondDistrib Z (fun (a : α) => (X a, Y a)) η μ
theorem
ProbabilityTheory.HasCondDistrib.prod
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_4}
{Ω' : Type u_5}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mΩ : MeasurableSpace Ω}
[StandardBorelSpace Ω]
[Nonempty Ω]
{mΩ' : MeasurableSpace Ω'}
[StandardBorelSpace Ω']
[Nonempty Ω']
{μ : MeasureTheory.Measure α}
{X : α → β}
{Y : α → Ω}
{κ : Kernel β Ω}
[MeasureTheory.IsFiniteMeasure μ]
[IsFiniteKernel κ]
{Z : α → Ω'}
{η : Kernel (β × Ω) Ω'}
[IsFiniteKernel η]
(h1 : HasCondDistrib Y X κ μ)
(h2 : HasCondDistrib Z (fun (ω : α) => (X ω, Y ω)) η μ)
:
HasCondDistrib (fun (ω : α) => (Y ω, Z ω)) X (κ.compProd η) μ
theorem
ProbabilityTheory.HasCondDistrib.hasCondDistrib_sectR
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{Ω : Type u_4}
{Ω' : Type u_5}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{mΩ : MeasurableSpace Ω}
[StandardBorelSpace Ω]
[Nonempty Ω]
{mΩ' : MeasurableSpace Ω'}
[StandardBorelSpace Ω']
[Nonempty Ω']
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
[StandardBorelSpace β]
[Nonempty β]
{W : α → Ω'}
{Z : α → γ}
{f : Ω' → β}
{g : Ω' → Ω}
{η : Kernel (γ × β) Ω}
(hf : Measurable f)
(hg : Measurable g)
(hW : AEMeasurable W μ)
(hcd : HasCondDistrib (g ∘ W) (fun (a : α) => (Z a, (f ∘ W) a)) η μ)
:
∀ᵐ (z : γ) ∂MeasureTheory.Measure.map Z μ, HasCondDistrib g f (η.sectR z) (𝓛[W | Z; μ] z)