Independence of a join of σ-algebras #
If m₁ is independent of m and m₂ is independent of m₁ ⊔ m, then the join m₁ ⊔ m₂ is
independent of m. The proof checks independence on the π-system of intersections generating the
join.
Main declarations #
ProbabilityTheory.Indep.sup_left: ifm₁is independent ofmandm₂is independent ofm₁ ⊔ m, thenm₁ ⊔ m₂is independent ofm.
theorem
ProbabilityTheory.Indep.sup_left
{Ω : Type u_1}
{mΩ : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsZeroOrProbabilityMeasure μ]
{m₁ m₂ m : MeasurableSpace Ω}
(h₁ : Indep m₁ m μ)
(h₂ : Indep m₂ (m₁ ⊔ m) μ)
(hm₁ : m₁ ≤ mΩ)
(hm₂ : m₂ ≤ mΩ)
(hm : m ≤ mΩ)
:
Indep (m₁ ⊔ m₂) m μ
If m₁ is independent of m and m₂ is independent of m₁ ⊔ m, then the join m₁ ⊔ m₂ is
independent of m.