A predicate for having a specified conditional distribution #
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 Ω}
{Y : α → Ω}
{X : α → β}
{κ : Kernel β Ω}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure γ}
[MeasureTheory.IsProbabilityMeasure ν]
(h : HasCondDistrib Y X κ μ)
:
HasCondDistrib (fun (ω : α × γ) => Y ω.1) (fun (ω : α × γ) => X ω.1) κ (μ.prod ν)
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 Ω}
{μ : 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 Ω}
{μ : 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.indepFun_of_const
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_4}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mΩ : MeasurableSpace Ω}
{μ : MeasureTheory.Measure α}
{X : α → β}
{Y : α → Ω}
[MeasureTheory.IsProbabilityMeasure μ]
{Q : MeasureTheory.Measure Ω}
[MeasureTheory.SFinite Q]
(h : HasCondDistrib Y X (Kernel.const β Q) μ)
:
IndepFun X Y μ
theorem
ProbabilityTheory.IndepFun.hasCondDistrib_const
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_4}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mΩ : MeasurableSpace Ω}
{μ : MeasureTheory.Measure α}
{X : α → β}
{Y : α → Ω}
[MeasureTheory.IsFiniteMeasure μ]
{Q : MeasureTheory.Measure Ω}
[MeasureTheory.SFinite Q]
(h : IndepFun X Y μ)
(hX : AEMeasurable X μ)
(hY : HasLaw Y Q μ)
:
HasCondDistrib Y X (Kernel.const β Q) μ
theorem
ProbabilityTheory.hasCondDistrib_self
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{X : α → β}
[MeasureTheory.SFinite μ]
(hX : AEMeasurable X μ)
:
HasCondDistrib X X Kernel.id μ
theorem
ProbabilityTheory.HasCondDistrib.const_map_of_const
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_4}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mΩ : MeasurableSpace Ω}
{μ : MeasureTheory.Measure α}
{X : α → β}
{Y : α → Ω}
[MeasureTheory.IsProbabilityMeasure μ]
{Q : MeasureTheory.Measure Ω}
[MeasureTheory.SFinite Q]
(h : HasCondDistrib Y X (Kernel.const β Q) μ)
:
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 Ω}
{μ : MeasureTheory.Measure α}
{X : α → β}
{Y : α → Ω}
{κ : Kernel β Ω}
{P : MeasureTheory.Measure β}
(h1 : HasLaw X P μ)
(h2 : HasCondDistrib Y X κ μ)
:
theorem
ProbabilityTheory.HasCondDistrib.congr
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_4}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mΩ : MeasurableSpace Ω}
{μ : MeasureTheory.Measure α}
{X : α → β}
{Y : α → Ω}
{κ : Kernel β Ω}
{X' : α → β}
{Y' : α → Ω}
(h : HasCondDistrib Y X κ μ)
(hX : X' =ᵐ[μ] X)
(hY : Y' =ᵐ[μ] Y)
:
HasCondDistrib Y' X' κ μ
HasCondDistrib only depends on the almost everywhere equivalence classes of the two random
variables.
theorem
ProbabilityTheory.HasCondDistrib.hasLaw_comp
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_4}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mΩ : MeasurableSpace Ω}
{μ : MeasureTheory.Measure α}
{X : α → β}
{Y : α → Ω}
{κ : Kernel β Ω}
[MeasureTheory.SFinite μ]
[IsSFiniteKernel κ]
(h : HasCondDistrib Y X κ μ)
:
HasLaw Y ((MeasureTheory.Measure.map X μ).bind ⇑κ) μ
theorem
ProbabilityTheory.HasCondDistrib.prod
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_4}
{Ω' : Type u_5}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mΩ : MeasurableSpace Ω}
{mΩ' : MeasurableSpace Ω'}
{μ : MeasureTheory.Measure α}
{X : α → β}
{Y : α → Ω}
{κ : Kernel β Ω}
{Z : α → Ω'}
{η : Kernel (β × Ω) Ω'}
(h1 : HasCondDistrib Y X κ μ)
(h2 : HasCondDistrib Z (fun (ω : α) => (X ω, Y ω)) η μ)
:
HasCondDistrib (fun (ω : α) => (Y ω, Z ω)) X (κ.compProd η) μ
theorem
ProbabilityTheory.hasCondDistrib_comp_self
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_4}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mΩ : MeasurableSpace Ω}
{μ : MeasureTheory.Measure α}
{X : α → β}
[MeasureTheory.SFinite μ]
{f : β → Ω}
(hf : Measurable f)
(hX : AEMeasurable X μ)
:
HasCondDistrib (f ∘ X) X (Kernel.deterministic f hf) μ
theorem
ProbabilityTheory.ae_eq_of_hasCondDistrib_deterministic
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_4}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mΩ : MeasurableSpace Ω}
{μ : MeasureTheory.Measure α}
{X : α → β}
{Y : α → Ω}
[MeasurableEq Ω]
[MeasureTheory.SFinite μ]
{f : β → Ω}
(hf : Measurable f)
(hX : AEMeasurable X μ)
(hY : AEMeasurable Y μ)
(h : HasCondDistrib Y X (Kernel.deterministic f hf) μ)
:
Y =ᵐ[μ] f ∘ X
theorem
ProbabilityTheory.hasCondDistrib_deterministic_iff
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_4}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mΩ : MeasurableSpace Ω}
{μ : MeasureTheory.Measure α}
{X : α → β}
{Y : α → Ω}
[MeasurableEq Ω]
[MeasureTheory.SFinite μ]
{f : β → Ω}
(hf : Measurable f)
(hX : AEMeasurable X μ)
(hY : AEMeasurable Y μ)
:
theorem
ProbabilityTheory.HasCondDistrib.of_measurableEmbedding_comp_right
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{Ω : Type u_4}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{mΩ : MeasurableSpace Ω}
{μ : MeasureTheory.Measure α}
{X : α → β}
{Y : α → Ω}
[MeasureTheory.SFinite μ]
{f : β → γ}
(hf : MeasurableEmbedding f)
{κ : Kernel γ Ω}
[IsSFiniteKernel κ]
(h : HasCondDistrib Y (f ∘ X) κ μ)
:
HasCondDistrib Y X (κ.comap f ⋯) μ
Converse of HasCondDistrib.comp_right for a measurable embedding.
theorem
ProbabilityTheory.hasCondDistrib_measurableEmbedding_comp_right_iff
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{Ω : Type u_4}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{mΩ : MeasurableSpace Ω}
{μ : MeasureTheory.Measure α}
{X : α → β}
{Y : α → Ω}
[MeasureTheory.SFinite μ]
{f : β → γ}
(hf : MeasurableEmbedding f)
{κ : Kernel γ Ω}
[IsSFiniteKernel κ]
:
HasCondDistrib.comp_right is an equivalence for measurable embeddings.
theorem
ProbabilityTheory.hasCondDistrib_measurableEquiv_comp_right_iff
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{Ω : Type u_4}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{mΩ : MeasurableSpace Ω}
{μ : MeasureTheory.Measure α}
{X : α → β}
{Y : α → Ω}
[MeasureTheory.SFinite μ]
(e : β ≃ᵐ γ)
{κ : Kernel γ Ω}
[IsSFiniteKernel κ]
:
HasCondDistrib.comp_right is an equivalence for measurable equivalences.
theorem
ProbabilityTheory.hasCondDistrib_prodMk_left_unique_iff
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_4}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mΩ : MeasurableSpace Ω}
{μ : MeasureTheory.Measure α}
{X : α → β}
{Y : α → Ω}
{δ : Type u_6}
{mδ : MeasurableSpace δ}
[Unique δ]
[MeasureTheory.SFinite μ]
{U : α → δ}
{η : Kernel (δ × β) Ω}
[IsSFiniteKernel η]
:
Conditioning on a pair whose first component takes values in a type with a unique element is the same as conditioning on the second component.
theorem
ProbabilityTheory.hasCondDistrib_prodMk_right_unique_iff
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_4}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mΩ : MeasurableSpace Ω}
{μ : MeasureTheory.Measure α}
{X : α → β}
{Y : α → Ω}
{δ : Type u_6}
{mδ : MeasurableSpace δ}
[Unique δ]
[MeasureTheory.SFinite μ]
{U : α → δ}
{η : Kernel (β × δ) Ω}
[IsSFiniteKernel η]
:
Conditioning on a pair whose second component takes values in a type with a unique element is the same as conditioning on the first component.
theorem
MeasureTheory.Measure.dirac_compProd
{β : Type u_2}
{Ω : Type u_4}
{mβ : MeasurableSpace β}
{mΩ : MeasurableSpace Ω}
{κ : ProbabilityTheory.Kernel β Ω}
[ProbabilityTheory.IsSFiniteKernel κ]
(b : β)
:
theorem
ProbabilityTheory.hasCondDistrib_const_iff
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_4}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mΩ : MeasurableSpace Ω}
{μ : MeasureTheory.Measure α}
{Y : α → Ω}
{κ : Kernel β Ω}
[MeasureTheory.IsProbabilityMeasure μ]
[IsSFiniteKernel κ]
{b : β}
:
Conditioning on a constant is the same as having law κ b.
theorem
ProbabilityTheory.HasCondDistrib.hasLaw_of_const'
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_4}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mΩ : MeasurableSpace Ω}
{μ : MeasureTheory.Measure α}
{Y : α → Ω}
{κ : Kernel β Ω}
[MeasureTheory.IsProbabilityMeasure μ]
[IsSFiniteKernel κ]
{b : β}
:
HasCondDistrib Y (fun (x : α) => b) κ μ → HasLaw Y (κ b) μ
Alias of the forward direction of ProbabilityTheory.hasCondDistrib_const_iff.
Conditioning on a constant is the same as having law κ b.
theorem
ProbabilityTheory.HasLaw.hasCondDistrib_const
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_4}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mΩ : MeasurableSpace Ω}
{μ : MeasureTheory.Measure α}
{Y : α → Ω}
{κ : Kernel β Ω}
[MeasureTheory.IsProbabilityMeasure μ]
[IsSFiniteKernel κ]
{b : β}
:
HasLaw Y (κ b) μ → HasCondDistrib Y (fun (x : α) => b) κ μ
Alias of the reverse direction of ProbabilityTheory.hasCondDistrib_const_iff.
Conditioning on a constant is the same as having law κ b.
theorem
ProbabilityTheory.HasCondDistrib.measure_inter_preimage_eq_mul_of_eqOn_const
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_4}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mΩ : MeasurableSpace Ω}
{μ : MeasureTheory.Measure α}
{X : α → β}
{Y : α → Ω}
{κ : Kernel β Ω}
[IsSFiniteKernel κ]
[MeasureTheory.SFinite μ]
(h : HasCondDistrib Y X κ μ)
{s : Set β}
(hs : MeasurableSet s)
{η : MeasureTheory.Measure Ω}
(hκ : Set.EqOn (⇑κ) (fun (x : β) => η) s)
{u : Set Ω}
(hu : MeasurableSet u)
:
If the conditional distribution of Y given X is a kernel κ which is constant equal to η
on a measurable set s, then μ (X ⁻¹' s ∩ Y ⁻¹' u) = μ (X ⁻¹' s) * η u for all measurable u.
theorem
ProbabilityTheory.HasCondDistrib.hasLaw_cond
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_4}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mΩ : MeasurableSpace Ω}
{μ : MeasureTheory.Measure α}
{X : α → β}
{Y : α → Ω}
{κ : Kernel β Ω}
[IsSFiniteKernel κ]
[MeasureTheory.IsFiniteMeasure μ]
(h : HasCondDistrib Y X κ μ)
(hY : Measurable Y)
{s : Set β}
(hs : MeasurableSet s)
{η : MeasureTheory.Measure Ω}
(hκ : Set.EqOn (⇑κ) (fun (x : β) => η) s)
(hμs : μ (X ⁻¹' s) ≠ 0)
:
If the conditional distribution of Y given X is a kernel κ which is constant equal to η
on a measurable set s, then the law of Y under μ conditioned on X ∈ s is η.
theorem
ProbabilityTheory.HasCondDistrib.indepFun_cond
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_4}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mΩ : MeasurableSpace Ω}
{μ : MeasureTheory.Measure α}
{X : α → β}
{Y : α → Ω}
{κ : Kernel β Ω}
[IsSFiniteKernel κ]
[MeasureTheory.IsFiniteMeasure μ]
(h : HasCondDistrib Y X κ μ)
(hX : Measurable X)
{s : Set β}
(hs : MeasurableSet s)
{η : MeasureTheory.Measure Ω}
(hκ : Set.EqOn (⇑κ) (fun (x : β) => η) s)
:
If the conditional distribution of Y given X is a kernel κ which is constant on a
measurable set s, then X and Y are independent under μ conditioned on X ∈ s.
theorem
ProbabilityTheory.HasCondDistrib.condDistrib_eq
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_4}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mΩ : MeasurableSpace Ω}
{μ : MeasureTheory.Measure α}
{X : α → β}
{Y : α → Ω}
{κ : Kernel β Ω}
[StandardBorelSpace Ω]
[Nonempty Ω]
[MeasureTheory.IsFiniteMeasure μ]
[IsFiniteKernel κ]
(h : HasCondDistrib Y X κ μ)
:
⇑𝓛[Y | X; μ] =ᵐ[MeasureTheory.Measure.map X μ] ⇑κ
theorem
ProbabilityTheory.hasCondDistrib_of_condDistrib_eq
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_4}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mΩ : MeasurableSpace Ω}
{μ : MeasureTheory.Measure α}
{X : α → β}
{Y : α → Ω}
{κ : Kernel β Ω}
[StandardBorelSpace Ω]
[Nonempty Ω]
[MeasureTheory.IsFiniteMeasure μ]
[IsFiniteKernel κ]
(hX : AEMeasurable X μ)
(hY : AEMeasurable Y μ)
(h : ⇑𝓛[Y | X; μ] =ᵐ[MeasureTheory.Measure.map X μ] ⇑κ)
:
HasCondDistrib Y X κ μ
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 Ω}
{mΩ' : MeasurableSpace Ω'}
{μ : MeasureTheory.Measure α}
[StandardBorelSpace Ω]
[Nonempty Ω]
[StandardBorelSpace Ω']
[Nonempty Ω']
[MeasureTheory.IsFiniteMeasure μ]
[StandardBorelSpace β]
[Nonempty β]
{W : α → Ω'}
{Z : α → γ}
{f : Ω' → β}
{g : Ω' → Ω}
{η : Kernel (γ × β) Ω}
[IsFiniteKernel η]
(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)