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 α}
{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.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.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 η) μ