theorem
ProbabilityTheory.IndepFun.identDistrib_cond
{Ω : Type u_1}
{α : Type u_2}
{β : Type u_3}
{x✝ : MeasurableSpace Ω}
{x✝¹ : MeasurableSpace α}
{x✝² : MeasurableSpace β}
{μ : MeasureTheory.Measure Ω}
{A : Ω → α}
{B : Ω → β}
[MeasureTheory.IsProbabilityMeasure μ]
(hi : IndepFun A B μ)
{s : Set β}
(hs : MeasurableSet s)
(hA : Measurable A)
(hB : Measurable B)
(h : μ (B ⁻¹' s) ≠ 0)
:
IdentDistrib A A μ μ[|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✝¹ : MeasurableSpace α}
{x✝² : MeasurableSpace β}
{μ : MeasureTheory.Measure Ω}
{A : Ω → α}
{B : Ω → β}
(hi : IndepFun A B μ)
{s : Set α}
(hs : MeasurableSet s)
(hA : Measurable A)
:
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✝¹ : MeasurableSpace α}
{x✝² : MeasurableSpace β}
{μ : MeasureTheory.Measure Ω}
{A : Ω → α}
{B : Ω → β}
(h : IndepFun A B μ)
{t : Set β}
(ht : MeasurableSet t)
(hB : Measurable B)
:
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✝¹ : MeasurableSpace α}
{x✝² : MeasurableSpace β}
{μ : MeasureTheory.Measure Ω}
{A : Ω → α}
{B : Ω → β}
(hi : IndepFun A B μ)
{s : Set α}
{t : Set β}
(hs : MeasurableSet s)
(ht : MeasurableSet t)
(hA : Measurable A)
(hB : Measurable B)
:
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 : Ω → γ)
(μ : MeasureTheory.Measure Ω := by volume_tac)
:
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 μ[|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 : Ω → γ}
:
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 : CondIndepFun f g h μ)
:
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}
[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' ∧ CondIndepFun X₁ X₂ Y' ν ∧ IdentDistrib (⟨X₁, Y'⟩) (⟨X, Y⟩) ν μ ∧ 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}
[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' ∧ CondIndepFun X₁ X₂ Y' ν ∧ IdentDistrib (⟨X₁, Y'⟩) (⟨X, Y⟩) ν μ ∧ IdentDistrib (⟨X₂, Y'⟩) (⟨X, Y⟩) ν μ ∧ (∀ (ω : Ω'), p (X₁ ω) (Y' ω)) ∧ ∀ (ω : Ω'), p (X₂ ω) (Y' ω)
For X, Y random variables, there exist conditionally independent trials X₁, X₂, Y'.