theorem
ProbabilityTheory.IndepFun.identDistrib_cond
{Ω : Type u_1}
{α : Type u_2}
{β : Type u_3}
:
∀ {x : MeasurableSpace Ω} {x_1 : MeasurableSpace α} {x_2 : MeasurableSpace β} {μ : MeasureTheory.Measure Ω} {A : Ω → α}
{B : Ω → β} [inst : MeasureTheory.IsProbabilityMeasure μ],
ProbabilityTheory.IndepFun A B μ →
∀ {s : Set β},
MeasurableSet s →
Measurable A →
Measurable B → μ (B ⁻¹' s) ≠ 0 → ProbabilityTheory.IdentDistrib A A μ (ProbabilityTheory.cond μ (B ⁻¹' s))
If A is independent from B, then conditioning on an event given by B does not change
the distribution of A.
theorem
ProbabilityTheory.IndepFun.cond_left
{Ω : Type u_1}
{α : Type u_2}
{β : Type u_3}
:
∀ {x : MeasurableSpace Ω} {x_1 : MeasurableSpace α} {x_2 : MeasurableSpace β} {μ : MeasureTheory.Measure Ω} {A : Ω → α}
{B : Ω → β},
ProbabilityTheory.IndepFun A B μ →
∀ {s : Set α}, MeasurableSet s → Measurable A → ProbabilityTheory.IndepFun A B (ProbabilityTheory.cond μ (A ⁻¹' s))
If A is independent of B, then they remain independent when conditioning on an event
of the form A ∈ s of positive probability.
theorem
ProbabilityTheory.IndepFun.cond_right
{Ω : Type u_1}
{α : Type u_2}
{β : Type u_3}
:
∀ {x : MeasurableSpace Ω} {x_1 : MeasurableSpace α} {x_2 : MeasurableSpace β} {μ : MeasureTheory.Measure Ω} {A : Ω → α}
{B : Ω → β},
ProbabilityTheory.IndepFun A B μ →
∀ {t : Set β}, MeasurableSet t → Measurable B → ProbabilityTheory.IndepFun A B (ProbabilityTheory.cond μ (B ⁻¹' t))
If A is independent of B, then they remain independent when conditioning on an event
of the form B ∈ t of positive probability.
theorem
ProbabilityTheory.IndepFun.cond
{Ω : Type u_1}
{α : Type u_2}
{β : Type u_3}
:
∀ {x : MeasurableSpace Ω} {x_1 : MeasurableSpace α} {x_2 : MeasurableSpace β} {μ : MeasureTheory.Measure Ω} {A : Ω → α}
{B : Ω → β},
ProbabilityTheory.IndepFun A B μ →
∀ {s : Set α} {t : Set β},
MeasurableSet s →
MeasurableSet t →
Measurable A → Measurable B → ProbabilityTheory.IndepFun A B (ProbabilityTheory.cond μ (A ⁻¹' s ∩ B ⁻¹' t))
If A is independent of B, then they remain independent when conditioning on an event
of the form A ∈ s ∩ B ∈ t of positive probability.
def
ProbabilityTheory.CondIndepFun
{Ω : Type u_1}
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
[MeasurableSpace Ω]
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSpace γ]
(f : Ω → α)
(g : Ω → β)
(h : Ω → γ)
(μ : autoParam (MeasureTheory.Measure Ω) _auto✝)
:
The assertion that f and g are conditionally independent relative to h.
Equations
- ProbabilityTheory.CondIndepFun f g h μ = ∀ᵐ (z : γ) ∂MeasureTheory.Measure.map h μ, ProbabilityTheory.IndepFun f g (ProbabilityTheory.cond μ (h ⁻¹' {z}))
Instances For
theorem
ProbabilityTheory.condIndepFun_iff
{Ω : Type u_1}
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
[MeasurableSpace Ω]
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSpace γ]
{μ : MeasureTheory.Measure Ω}
{f : Ω → α}
{g : Ω → β}
{h : Ω → γ}
:
ProbabilityTheory.CondIndepFun f g h μ ↔ ∀ᵐ (z : γ) ∂MeasureTheory.Measure.map h μ, ProbabilityTheory.IndepFun f g (ProbabilityTheory.cond μ (h ⁻¹' {z}))
theorem
ProbabilityTheory.CondIndepFun.comp_right
{Ω : Type u_1}
{Ω' : Type u_2}
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
[MeasurableSpace Ω]
[MeasurableSpace Ω']
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSpace γ]
{μ : MeasureTheory.Measure Ω}
{f : Ω → α}
{g : Ω → β}
{h : Ω → γ}
[MeasurableSingletonClass γ]
{i : Ω' → Ω}
(hi : MeasurableEmbedding i)
(hi' : ∀ᵐ (a : Ω) ∂μ, a ∈ Set.range i)
(hf : Measurable f)
(hg : Measurable g)
(hh : Measurable h)
(hfg : ProbabilityTheory.CondIndepFun f g h μ)
:
ProbabilityTheory.CondIndepFun (f ∘ i) (g ∘ i) (h ∘ i) (MeasureTheory.Measure.comap i μ)
Composing independent functions with a measurable embedding of conull range gives independent functions.
theorem
ProbabilityTheory.condIndep_copies
{Ω : Type u_1}
{α : Type u}
{β : Type u}
[MeasurableSpace Ω]
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSingletonClass β]
[Countable β]
(X : Ω → α)
(Y : Ω → β)
(hX : Measurable X)
(hY : Measurable Y)
[finY : FiniteRange Y]
(μ : MeasureTheory.Measure Ω)
[MeasureTheory.IsProbabilityMeasure μ]
:
∃ (Ω' : Type u) (x : MeasurableSpace Ω') (X₁ : Ω' → α) (X₂ : Ω' → α) (Y' : Ω' → β) (ν : MeasureTheory.Measure Ω'),
MeasureTheory.IsProbabilityMeasure ν ∧ Measurable X₁ ∧ Measurable X₂ ∧ Measurable Y' ∧ ProbabilityTheory.CondIndepFun X₁ X₂ Y' ν ∧ ProbabilityTheory.IdentDistrib (⟨X₁, Y'⟩) (⟨X, Y⟩) ν μ ∧ ProbabilityTheory.IdentDistrib (⟨X₂, Y'⟩) (⟨X, Y⟩) ν μ
For X, Y random variables, there exist conditionally independent trials X_1, X_2, Y'.
theorem
ProbabilityTheory.condIndep_copies'
{Ω : Type u_1}
{α : Type u}
{β : Type u}
[MeasurableSpace Ω]
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSingletonClass β]
[Countable β]
(X : Ω → α)
(Y : Ω → β)
(hX : Measurable X)
(hY : Measurable Y)
[FiniteRange Y]
(μ : MeasureTheory.Measure Ω)
[MeasureTheory.IsProbabilityMeasure μ]
(p : α → β → Prop)
(hp : Measurable (Function.uncurry p))
(hp' : ∀ᵐ (ω : Ω) ∂μ, p (X ω) (Y ω))
:
∃ (Ω' : Type u) (x : MeasurableSpace Ω') (X₁ : Ω' → α) (X₂ : Ω' → α) (Y' : Ω' → β) (ν : MeasureTheory.Measure Ω'),
MeasureTheory.IsProbabilityMeasure ν ∧ Measurable X₁ ∧ Measurable X₂ ∧ Measurable Y' ∧ ProbabilityTheory.CondIndepFun X₁ X₂ Y' ν ∧ ProbabilityTheory.IdentDistrib (⟨X₁, Y'⟩) (⟨X, Y⟩) ν μ ∧ ProbabilityTheory.IdentDistrib (⟨X₂, Y'⟩) (⟨X, Y⟩) ν μ ∧ (∀ (ω : Ω'), p (X₁ ω) (Y' ω)) ∧ ∀ (ω : Ω'), p (X₂ ω) (Y' ω)
For X, Y random variables, there exist conditionally independent trials X₁, X₂, Y'.