Conditional Independence

We define conditional independence of sets/σ-algebras/functions with respect to a σ-algebra.

Two σ-algebras m₁ and m₂ are conditionally independent given a third σ-algebra m' if for all m₁-measurable sets t₁ and m₂-measurable sets t₂, μ⟦t₁ ∩ t₂ | m'⟧ =ᵐ[μ] μ⟦t₁ | m'⟧ * μ⟦t₂ | m'⟧.

On standard Borel spaces, the conditional expectation with respect to m' defines a kernel ProbabilityTheory.condexpKernel, and the definition above is equivalent to ∀ᵐ ω ∂μ, condexpKernel μ m' ω (t₁ ∩ t₂) = condexpKernel μ m' ω t₁ * condexpKernel μ m' ω t₂. We use this property as the definition of conditional independence.

Main definitions

We provide four definitions of conditional independence:

• iCondIndepSets: conditional independence of a family of sets of sets pi : ι → Set (Set Ω). This is meant to be used with π-systems.
• iCondIndep: conditional independence of a family of measurable space structures m : ι → MeasurableSpace Ω,
• iCondIndepSet: conditional independence of a family of sets s : ι → Set Ω,
• iCondIndepFun: conditional independence of a family of functions. For measurable spaces m : Π (i : ι), MeasurableSpace (β i), we consider functions f : Π (i : ι), Ω → β i.

Additionally, we provide four corresponding statements for two measurable space structures (resp. sets of sets, sets, functions) instead of a family. These properties are denoted by the same names as for a family, but without the starting i, for example CondIndepFun is the version of iCondIndepFun for two functions.

Main statements

• ProbabilityTheory.iCondIndepSets.iCondIndep: if π-systems are conditionally independent as sets of sets, then the measurable space structures they generate are conditionally independent.
• ProbabilityTheory.condIndepSets.condIndep: variant with two π-systems.

Implementation notes

The definitions of conditional independence in this file are a particular case of independence with respect to a kernel and a measure, as defined in the file Probability/Independence/Kernel.lean. The kernel used is ProbabilityTheory.condexpKernel.

def ProbabilityTheory.iCondIndepSets {Ω : Type u_1} {ι : Type u_2} (m' : MeasurableSpace Ω) [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] (hm' : m' ≤ mΩ) (π : ι → Set (Set Ω)) (μ : autoParam (MeasureTheory.Measure Ω) _auto✝) [MeasureTheory.IsFiniteMeasure μ] : Prop

A family of sets of sets π : ι → Set (Set Ω) is conditionally independent given m' with respect to a measure μ if for any finite set of indices s = {i_1, ..., i_n}, for any sets f i_1 ∈ π i_1, ..., f i_n ∈ π i_n, then μ⟦⋂ i in s, f i | m'⟧ =ᵐ[μ] ∏ i in s, μ⟦f i | m'⟧. See ProbabilityTheory.iCondIndepSets_iff. It will be used for families of pi_systems.

Equations

• ProbabilityTheory.iCondIndepSets m' hm' π = ProbabilityTheory.kernel.iIndepSets π (ProbabilityTheory.condexpKernel μ m')

def ProbabilityTheory.CondIndepSets {Ω : Type u_1} (m' : MeasurableSpace Ω) [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] (hm' : m' ≤ mΩ) (s1 : Set (Set Ω)) (s2 : Set (Set Ω)) (μ : autoParam (MeasureTheory.Measure Ω) _auto✝) [MeasureTheory.IsFiniteMeasure μ] : Prop

Two sets of sets s₁, s₂ are conditionally independent given m' with respect to a measure μ if for any sets t₁ ∈ s₁, t₂ ∈ s₂, then μ⟦t₁ ∩ t₂ | m'⟧ =ᵐ[μ] μ⟦t₁ | m'⟧ * μ⟦t₂ | m'⟧. See ProbabilityTheory.condIndepSets_iff.

Equations

• ProbabilityTheory.CondIndepSets m' hm' s1 s2 = ProbabilityTheory.kernel.IndepSets s1 s2 (ProbabilityTheory.condexpKernel μ m')

def ProbabilityTheory.iCondIndep {Ω : Type u_1} {ι : Type u_2} (m' : MeasurableSpace Ω) [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] (hm' : m' ≤ mΩ) (m : ι → MeasurableSpace Ω) (μ : autoParam (MeasureTheory.Measure Ω) _auto✝) [MeasureTheory.IsFiniteMeasure μ] : Prop

A family of measurable space structures (i.e. of σ-algebras) is conditionally independent given m' with respect to a measure μ (typically defined on a finer σ-algebra) if the family of sets of measurable sets they define is independent. m : ι → MeasurableSpace Ω is conditionally independent given m' with respect to measure μ if for any finite set of indices s = {i_1, ..., i_n}, for any sets f i_1 ∈ m i_1, ..., f i_n ∈ m i_n, then μ⟦⋂ i in s, f i | m'⟧ =ᵐ[μ] ∏ i in s, μ⟦f i | m'⟧ . See ProbabilityTheory.iCondIndep_iff.

Equations

• ProbabilityTheory.iCondIndep m' hm' m = ProbabilityTheory.kernel.iIndep m (ProbabilityTheory.condexpKernel μ m')

def ProbabilityTheory.CondIndep {Ω : Type u_1} (m' : MeasurableSpace Ω) (m₁ : MeasurableSpace Ω) (m₂ : MeasurableSpace Ω) [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] (hm' : m' ≤ mΩ) (μ : autoParam (MeasureTheory.Measure Ω) _auto✝) [MeasureTheory.IsFiniteMeasure μ] : Prop

Two measurable space structures (or σ-algebras) m₁, m₂ are conditionally independent given m' with respect to a measure μ (defined on a third σ-algebra) if for any sets t₁ ∈ m₁, t₂ ∈ m₂, μ⟦t₁ ∩ t₂ | m'⟧ =ᵐ[μ] μ⟦t₁ | m'⟧ * μ⟦t₂ | m'⟧. See ProbabilityTheory.condIndep_iff.

Equations

• ProbabilityTheory.CondIndep m' m₁ m₂ hm' = ProbabilityTheory.kernel.Indep m₁ m₂ (ProbabilityTheory.condexpKernel μ m')

def ProbabilityTheory.iCondIndepSet {Ω : Type u_1} {ι : Type u_2} (m' : MeasurableSpace Ω) [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] (hm' : m' ≤ mΩ) (s : ι → Set Ω) (μ : autoParam (MeasureTheory.Measure Ω) _auto✝) [MeasureTheory.IsFiniteMeasure μ] : Prop

A family of sets is conditionally independent if the family of measurable space structures they generate is conditionally independent. For a set s, the generated measurable space has measurable sets ∅, s, sᶜ, univ. See ProbabilityTheory.iCondIndepSet_iff.

Equations

• ProbabilityTheory.iCondIndepSet m' hm' s = ProbabilityTheory.kernel.iIndepSet s (ProbabilityTheory.condexpKernel μ m')

def ProbabilityTheory.CondIndepSet {Ω : Type u_1} (m' : MeasurableSpace Ω) [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] (hm' : m' ≤ mΩ) (s : Set Ω) (t : Set Ω) (μ : autoParam (MeasureTheory.Measure Ω) _auto✝) [MeasureTheory.IsFiniteMeasure μ] : Prop

Two sets are conditionally independent if the two measurable space structures they generate are conditionally independent. For a set s, the generated measurable space structure has measurable sets ∅, s, sᶜ, univ. See ProbabilityTheory.condIndepSet_iff.

Equations

• ProbabilityTheory.CondIndepSet m' hm' s t = ProbabilityTheory.kernel.IndepSet s t (ProbabilityTheory.condexpKernel μ m')

def ProbabilityTheory.iCondIndepFun {Ω : Type u_1} {ι : Type u_2} (m' : MeasurableSpace Ω) [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] (hm' : m' ≤ mΩ) {β : ι → Type u_3} (m : (x : ι) → MeasurableSpace (β x)) (f : (x : ι) → Ω → β x) (μ : autoParam (MeasureTheory.Measure Ω) _auto✝) [MeasureTheory.IsFiniteMeasure μ] : Prop

A family of functions defined on the same space Ω and taking values in possibly different spaces, each with a measurable space structure, is conditionally independent if the family of measurable space structures they generate on Ω is conditionally independent. For a function g with codomain having measurable space structure m, the generated measurable space structure is m.comap g. See ProbabilityTheory.iCondIndepFun_iff.

Equations

• ProbabilityTheory.iCondIndepFun m' hm' m f = ProbabilityTheory.kernel.iIndepFun m f (ProbabilityTheory.condexpKernel μ m')

def ProbabilityTheory.CondIndepFun {Ω : Type u_1} (m' : MeasurableSpace Ω) [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] (hm' : m' ≤ mΩ) {β : Type u_3} {γ : Type u_4} [MeasurableSpace β] [MeasurableSpace γ] (f : Ω → β) (g : Ω → γ) (μ : autoParam (MeasureTheory.Measure Ω) _auto✝) [MeasureTheory.IsFiniteMeasure μ] : Prop

Two functions are conditionally independent if the two measurable space structures they generate are conditionally independent. For a function f with codomain having measurable space structure m, the generated measurable space structure is m.comap f. See ProbabilityTheory.condIndepFun_iff.

Equations

• ProbabilityTheory.CondIndepFun m' hm' f g = ProbabilityTheory.kernel.IndepFun f g (ProbabilityTheory.condexpKernel μ m')

theorem ProbabilityTheory.iCondIndepSets_iff {Ω : Type u_1} {ι : Type u_2} (m' : MeasurableSpace Ω) [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] (hm' : m' ≤ mΩ) (π : ι → Set (Set Ω)) (hπ : ∀ (i : ι), ∀ s ∈ π i, MeasurableSet s) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] : ProbabilityTheory.iCondIndepSets m' hm' π ↔ ∀ (s : Finset ι) {f : ι → Set Ω}, (∀ i ∈ s, f i ∈ π i) → MeasureTheory.condexp m' μ (Set.indicator (⋂ i ∈ s, f i) fun (ω : Ω) => 1) =ᶠ[MeasureTheory.Measure.ae μ] Finset.prod s fun (i : ι) => MeasureTheory.condexp m' μ (Set.indicator (f i) fun (ω : Ω) => 1)

theorem ProbabilityTheory.condIndepSets_iff {Ω : Type u_1} (m' : MeasurableSpace Ω) [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] (hm' : m' ≤ mΩ) (s1 : Set (Set Ω)) (s2 : Set (Set Ω)) (hs1 : ∀ s ∈ s1, MeasurableSet s) (hs2 : ∀ s ∈ s2, MeasurableSet s) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] : ProbabilityTheory.CondIndepSets m' hm' s1 s2 ↔ ∀ (t1 t2 : Set Ω), t1 ∈ s1 → t2 ∈ s2 → MeasureTheory.condexp m' μ (Set.indicator (t1 ∩ t2) fun (ω : Ω) => 1) =ᶠ[MeasureTheory.Measure.ae μ] MeasureTheory.condexp m' μ (Set.indicator t1 fun (ω : Ω) => 1) * MeasureTheory.condexp m' μ (Set.indicator t2 fun (ω : Ω) => 1)

theorem ProbabilityTheory.iCondIndepSets_singleton_iff {Ω : Type u_1} {ι : Type u_2} (m' : MeasurableSpace Ω) [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] (hm' : m' ≤ mΩ) (s : ι → Set Ω) (hπ : ∀ (i : ι), MeasurableSet (s i)) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] : (ProbabilityTheory.iCondIndepSets m' hm' fun (i : ι) => {s i}) ↔ ∀ (S : Finset ι), MeasureTheory.condexp m' μ (Set.indicator (⋂ i ∈ S, s i) fun (ω : Ω) => 1) =ᶠ[MeasureTheory.Measure.ae μ] Finset.prod S fun (i : ι) => MeasureTheory.condexp m' μ (Set.indicator (s i) fun (ω : Ω) => 1)

theorem ProbabilityTheory.condIndepSets_singleton_iff {Ω : Type u_1} (m' : MeasurableSpace Ω) [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] (hm' : m' ≤ mΩ) {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {s : Set Ω} {t : Set Ω} (hs : MeasurableSet s) (ht : MeasurableSet t) : ProbabilityTheory.CondIndepSets m' hm' {s} {t} ↔ MeasureTheory.condexp m' μ (Set.indicator (s ∩ t) fun (ω : Ω) => 1) =ᶠ[MeasureTheory.Measure.ae μ] MeasureTheory.condexp m' μ (Set.indicator s fun (ω : Ω) => 1) * MeasureTheory.condexp m' μ (Set.indicator t fun (ω : Ω) => 1)

theorem ProbabilityTheory.iCondIndep_iff_iCondIndepSets {Ω : Type u_1} {ι : Type u_2} (m' : MeasurableSpace Ω) [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] (hm' : m' ≤ mΩ) (m : ι → MeasurableSpace Ω) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] : ProbabilityTheory.iCondIndep m' hm' m ↔ ProbabilityTheory.iCondIndepSets m' hm' fun (x : ι) => {s : Set Ω | MeasurableSet s}

theorem ProbabilityTheory.iCondIndep_iff {Ω : Type u_1} {ι : Type u_2} (m' : MeasurableSpace Ω) [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] (hm' : m' ≤ mΩ) (m : ι → MeasurableSpace Ω) (hm : ∀ (i : ι), m i ≤ mΩ) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] : ProbabilityTheory.iCondIndep m' hm' m ↔ ∀ (s : Finset ι) {f : ι → Set Ω}, (∀ i ∈ s, MeasurableSet (f i)) → MeasureTheory.condexp m' μ (Set.indicator (⋂ i ∈ s, f i) fun (ω : Ω) => 1) =ᶠ[MeasureTheory.Measure.ae μ] Finset.prod s fun (i : ι) => MeasureTheory.condexp m' μ (Set.indicator (f i) fun (ω : Ω) => 1)

theorem ProbabilityTheory.condIndep_iff_condIndepSets {Ω : Type u_1} (m' : MeasurableSpace Ω) (m₁ : MeasurableSpace Ω) (m₂ : MeasurableSpace Ω) [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] (hm' : m' ≤ mΩ) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] : ProbabilityTheory.CondIndep m' m₁ m₂ hm' ↔ ProbabilityTheory.CondIndepSets m' hm' {s : Set Ω | MeasurableSet s} {s : Set Ω | MeasurableSet s}

theorem ProbabilityTheory.condIndep_iff {Ω : Type u_1} (m' : MeasurableSpace Ω) (m₁ : MeasurableSpace Ω) (m₂ : MeasurableSpace Ω) [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] (hm' : m' ≤ mΩ) (hm₁ : m₁ ≤ mΩ) (hm₂ : m₂ ≤ mΩ) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] : ProbabilityTheory.CondIndep m' m₁ m₂ hm' ↔ ∀ (t1 t2 : Set Ω), MeasurableSet t1 → MeasurableSet t2 → MeasureTheory.condexp m' μ (Set.indicator (t1 ∩ t2) fun (ω : Ω) => 1) =ᶠ[MeasureTheory.Measure.ae μ] MeasureTheory.condexp m' μ (Set.indicator t1 fun (ω : Ω) => 1) * MeasureTheory.condexp m' μ (Set.indicator t2 fun (ω : Ω) => 1)

theorem ProbabilityTheory.iCondIndepSet_iff_iCondIndep {Ω : Type u_1} {ι : Type u_2} (m' : MeasurableSpace Ω) [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] (hm' : m' ≤ mΩ) (s : ι → Set Ω) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] : ProbabilityTheory.iCondIndepSet m' hm' s ↔ ProbabilityTheory.iCondIndep m' hm' fun (i : ι) => MeasurableSpace.generateFrom {s i}

theorem ProbabilityTheory.iCondIndepSet_iff_iCondIndepSets_singleton {Ω : Type u_1} {ι : Type u_2} (m' : MeasurableSpace Ω) [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] (hm' : m' ≤ mΩ) (s : ι → Set Ω) (hs : ∀ (i : ι), MeasurableSet (s i)) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] : ProbabilityTheory.iCondIndepSet m' hm' s ↔ ProbabilityTheory.iCondIndepSets m' hm' fun (i : ι) => {s i}

theorem ProbabilityTheory.iCondIndepSet_iff {Ω : Type u_1} {ι : Type u_2} (m' : MeasurableSpace Ω) [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] (hm' : m' ≤ mΩ) (s : ι → Set Ω) (hs : ∀ (i : ι), MeasurableSet (s i)) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] : ProbabilityTheory.iCondIndepSet m' hm' s ↔ ∀ (S : Finset ι), MeasureTheory.condexp m' μ (Set.indicator (⋂ i ∈ S, s i) fun (ω : Ω) => 1) =ᶠ[MeasureTheory.Measure.ae μ] Finset.prod S fun (i : ι) => MeasureTheory.condexp m' μ (Set.indicator (s i) fun (ω : Ω) => 1)

theorem ProbabilityTheory.condIndepSet_iff_condIndep {Ω : Type u_1} (m' : MeasurableSpace Ω) [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] (hm' : m' ≤ mΩ) (s : Set Ω) (t : Set Ω) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] : ProbabilityTheory.CondIndepSet m' hm' s t ↔ ProbabilityTheory.CondIndep m' (MeasurableSpace.generateFrom {s}) (MeasurableSpace.generateFrom {t}) hm'

theorem ProbabilityTheory.condIndepSet_iff_condIndepSets_singleton {Ω : Type u_1} (m' : MeasurableSpace Ω) [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] (hm' : m' ≤ mΩ) {s : Set Ω} {t : Set Ω} (hs_meas : MeasurableSet s) (ht_meas : MeasurableSet t) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] : ProbabilityTheory.CondIndepSet m' hm' s t ↔ ProbabilityTheory.CondIndepSets m' hm' {s} {t}

theorem ProbabilityTheory.condIndepSet_iff {Ω : Type u_1} (m' : MeasurableSpace Ω) [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] (hm' : m' ≤ mΩ) (s : Set Ω) (t : Set Ω) (hs : MeasurableSet s) (ht : MeasurableSet t) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] : ProbabilityTheory.CondIndepSet m' hm' s t ↔ MeasureTheory.condexp m' μ (Set.indicator (s ∩ t) fun (ω : Ω) => 1) =ᶠ[MeasureTheory.Measure.ae μ] MeasureTheory.condexp m' μ (Set.indicator s fun (ω : Ω) => 1) * MeasureTheory.condexp m' μ (Set.indicator t fun (ω : Ω) => 1)

theorem ProbabilityTheory.iCondIndepFun_iff_iCondIndep {Ω : Type u_1} {ι : Type u_2} (m' : MeasurableSpace Ω) [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] (hm' : m' ≤ mΩ) {β : ι → Type u_3} (m : (x : ι) → MeasurableSpace (β x)) (f : (x : ι) → Ω → β x) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] : ProbabilityTheory.iCondIndepFun m' hm' m f ↔ ProbabilityTheory.iCondIndep m' hm' fun (x : ι) => MeasurableSpace.comap (f x) (m x)

theorem ProbabilityTheory.iCondIndepFun_iff {Ω : Type u_1} {ι : Type u_2} (m' : MeasurableSpace Ω) [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] (hm' : m' ≤ mΩ) {β : ι → Type u_3} (m : (x : ι) → MeasurableSpace (β x)) (f : (x : ι) → Ω → β x) (hf : ∀ (i : ι), Measurable (f i)) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] : ProbabilityTheory.iCondIndepFun m' hm' m f ↔ ∀ (s : Finset ι) {g : ι → Set Ω}, (∀ i ∈ s, MeasurableSet (g i)) → MeasureTheory.condexp m' μ (Set.indicator (⋂ i ∈ s, g i) fun (ω : Ω) => 1) =ᶠ[MeasureTheory.Measure.ae μ] Finset.prod s fun (i : ι) => MeasureTheory.condexp m' μ (Set.indicator (g i) fun (ω : Ω) => 1)

theorem ProbabilityTheory.condIndepFun_iff_condIndep {Ω : Type u_1} (m' : MeasurableSpace Ω) [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] (hm' : m' ≤ mΩ) {β : Type u_3} {γ : Type u_4} [mβ : MeasurableSpace β] [mγ : MeasurableSpace γ] (f : Ω → β) (g : Ω → γ) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] : ProbabilityTheory.CondIndepFun m' hm' f g ↔ ProbabilityTheory.CondIndep m' (MeasurableSpace.comap f mβ) (MeasurableSpace.comap g mγ) hm'

theorem ProbabilityTheory.condIndepFun_iff {Ω : Type u_1} (m' : MeasurableSpace Ω) [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] (hm' : m' ≤ mΩ) {β : Type u_3} {γ : Type u_4} [mβ : MeasurableSpace β] [mγ : MeasurableSpace γ] (f : Ω → β) (g : Ω → γ) (hf : Measurable f) (hg : Measurable g) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] : ProbabilityTheory.CondIndepFun m' hm' f g ↔ ∀ (t1 t2 : Set Ω), MeasurableSet t1 → MeasurableSet t2 → MeasureTheory.condexp m' μ (Set.indicator (t1 ∩ t2) fun (ω : Ω) => 1) =ᶠ[MeasureTheory.Measure.ae μ] MeasureTheory.condexp m' μ (Set.indicator t1 fun (ω : Ω) => 1) * MeasureTheory.condexp m' μ (Set.indicator t2 fun (ω : Ω) => 1)

theorem ProbabilityTheory.CondIndepSets.symm {Ω : Type u_1} {m' : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {s₁ : Set (Set Ω)} {s₂ : Set (Set Ω)} (h : ProbabilityTheory.CondIndepSets m' hm' s₁ s₂) : ProbabilityTheory.CondIndepSets m' hm' s₂ s₁

theorem ProbabilityTheory.condIndepSets_of_condIndepSets_of_le_left {Ω : Type u_1} {m' : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {s₁ : Set (Set Ω)} {s₂ : Set (Set Ω)} {s₃ : Set (Set Ω)} (h_indep : ProbabilityTheory.CondIndepSets m' hm' s₁ s₂) (h31 : s₃ ⊆ s₁) : ProbabilityTheory.CondIndepSets m' hm' s₃ s₂

theorem ProbabilityTheory.condIndepSets_of_condIndepSets_of_le_right {Ω : Type u_1} {m' : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {s₁ : Set (Set Ω)} {s₂ : Set (Set Ω)} {s₃ : Set (Set Ω)} (h_indep : ProbabilityTheory.CondIndepSets m' hm' s₁ s₂) (h32 : s₃ ⊆ s₂) : ProbabilityTheory.CondIndepSets m' hm' s₁ s₃

theorem ProbabilityTheory.CondIndepSets.union {Ω : Type u_1} {m' : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {s₁ : Set (Set Ω)} {s₂ : Set (Set Ω)} {s' : Set (Set Ω)} (h₁ : ProbabilityTheory.CondIndepSets m' hm' s₁ s') (h₂ : ProbabilityTheory.CondIndepSets m' hm' s₂ s') : ProbabilityTheory.CondIndepSets m' hm' (s₁ ∪ s₂) s'

@[simp]

theorem ProbabilityTheory.CondIndepSets.union_iff {Ω : Type u_1} {m' : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {s₁ : Set (Set Ω)} {s₂ : Set (Set Ω)} {s' : Set (Set Ω)} : ProbabilityTheory.CondIndepSets m' hm' (s₁ ∪ s₂) s' ↔ ProbabilityTheory.CondIndepSets m' hm' s₁ s' ∧ ProbabilityTheory.CondIndepSets m' hm' s₂ s'

theorem ProbabilityTheory.CondIndepSets.iUnion {Ω : Type u_1} {ι : Type u_2} {m' : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {s : ι → Set (Set Ω)} {s' : Set (Set Ω)} (hyp : ∀ (n : ι), ProbabilityTheory.CondIndepSets m' hm' (s n) s') : ProbabilityTheory.CondIndepSets m' hm' (⋃ (n : ι), s n) s'

theorem ProbabilityTheory.CondIndepSets.bUnion {Ω : Type u_1} {ι : Type u_2} {m' : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {s : ι → Set (Set Ω)} {s' : Set (Set Ω)} {u : Set ι} (hyp : ∀ n ∈ u, ProbabilityTheory.CondIndepSets m' hm' (s n) s') : ProbabilityTheory.CondIndepSets m' hm' (⋃ n ∈ u, s n) s'

theorem ProbabilityTheory.CondIndepSets.inter {Ω : Type u_1} {m' : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {s₁ : Set (Set Ω)} {s' : Set (Set Ω)} (s₂ : Set (Set Ω)) (h₁ : ProbabilityTheory.CondIndepSets m' hm' s₁ s') : ProbabilityTheory.CondIndepSets m' hm' (s₁ ∩ s₂) s'

theorem ProbabilityTheory.CondIndepSets.iInter {Ω : Type u_1} {ι : Type u_2} {m' : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {s : ι → Set (Set Ω)} {s' : Set (Set Ω)} (h : ∃ (n : ι), ProbabilityTheory.CondIndepSets m' hm' (s n) s') : ProbabilityTheory.CondIndepSets m' hm' (⋂ (n : ι), s n) s'

theorem ProbabilityTheory.CondIndepSets.bInter {Ω : Type u_1} {ι : Type u_2} {m' : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {s : ι → Set (Set Ω)} {s' : Set (Set Ω)} {u : Set ι} (h : ∃ n ∈ u, ProbabilityTheory.CondIndepSets m' hm' (s n) s') : ProbabilityTheory.CondIndepSets m' hm' (⋂ n ∈ u, s n) s'

theorem ProbabilityTheory.condIndepSet_empty_right {Ω : Type u_1} {m' : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] (s : Set Ω) : ProbabilityTheory.CondIndepSet m' hm' s ∅

theorem ProbabilityTheory.condIndepSet_empty_left {Ω : Type u_1} {m' : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] (s : Set Ω) : ProbabilityTheory.CondIndepSet m' hm' ∅ s

theorem ProbabilityTheory.CondIndep.symm {Ω : Type u_1} {m' : MeasurableSpace Ω} {m₁ : MeasurableSpace Ω} {m₂ : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] (h : ProbabilityTheory.CondIndep m' m₁ m₂ hm') : ProbabilityTheory.CondIndep m' m₂ m₁ hm'

theorem ProbabilityTheory.condIndep_bot_right {Ω : Type u_1} (m₁ : MeasurableSpace Ω) {m' : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] : ProbabilityTheory.CondIndep m' m₁ ⊥ hm'

theorem ProbabilityTheory.condIndep_bot_left {Ω : Type u_1} (m₁ : MeasurableSpace Ω) {m' : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] : ProbabilityTheory.CondIndep m' ⊥ m₁ hm'

theorem ProbabilityTheory.condIndep_of_condIndep_of_le_left {Ω : Type u_1} {m' : MeasurableSpace Ω} {m₁ : MeasurableSpace Ω} {m₂ : MeasurableSpace Ω} {m₃ : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] (h_indep : ProbabilityTheory.CondIndep m' m₁ m₂ hm') (h31 : m₃ ≤ m₁) : ProbabilityTheory.CondIndep m' m₃ m₂ hm'

theorem ProbabilityTheory.condIndep_of_condIndep_of_le_right {Ω : Type u_1} {m' : MeasurableSpace Ω} {m₁ : MeasurableSpace Ω} {m₂ : MeasurableSpace Ω} {m₃ : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] (h_indep : ProbabilityTheory.CondIndep m' m₁ m₂ hm') (h32 : m₃ ≤ m₂) : ProbabilityTheory.CondIndep m' m₁ m₃ hm'

Deducing CondIndep from iCondIndep

theorem ProbabilityTheory.iCondIndepSets.condIndepSets {Ω : Type u_1} {ι : Type u_2} {m' : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {s : ι → Set (Set Ω)} (h_indep : ProbabilityTheory.iCondIndepSets m' hm' s) {i : ι} {j : ι} (hij : i ≠ j) : ProbabilityTheory.CondIndepSets m' hm' (s i) (s j)

theorem ProbabilityTheory.iCondIndep.condIndep {Ω : Type u_1} {ι : Type u_2} {m' : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {m : ι → MeasurableSpace Ω} (h_indep : ProbabilityTheory.iCondIndep m' hm' m) {i : ι} {j : ι} (hij : i ≠ j) : ProbabilityTheory.CondIndep m' (m i) (m j) hm'

theorem ProbabilityTheory.iCondIndepFun.condIndepFun {Ω : Type u_1} {ι : Type u_2} {m' : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {β : ι → Type u_3} {m : (x : ι) → MeasurableSpace (β x)} {f : (i : ι) → Ω → β i} (hf_Indep : ProbabilityTheory.iCondIndepFun m' hm' m f) {i : ι} {j : ι} (hij : i ≠ j) : ProbabilityTheory.CondIndepFun m' hm' (f i) (f j)

π-system lemma

Conditional independence of measurable spaces is equivalent to conditional independence of generating π-systems.

Conditional independence of σ-algebras implies conditional independence of

generating π-systems

theorem ProbabilityTheory.iCondIndep.iCondIndepSets {Ω : Type u_1} {ι : Type u_2} {m' : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {m : ι → MeasurableSpace Ω} {s : ι → Set (Set Ω)} (hms : ∀ (n : ι), m n = MeasurableSpace.generateFrom (s n)) (h_indep : ProbabilityTheory.iCondIndep m' hm' m) : ProbabilityTheory.iCondIndepSets m' hm' s

theorem ProbabilityTheory.CondIndep.condIndepSets {Ω : Type u_1} {m' : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {s1 : Set (Set Ω)} {s2 : Set (Set Ω)} (h_indep : ProbabilityTheory.CondIndep m' (MeasurableSpace.generateFrom s1) (MeasurableSpace.generateFrom s2) hm') : ProbabilityTheory.CondIndepSets m' hm' s1 s2

Conditional independence of generating π-systems implies conditional independence of

σ-algebras

theorem ProbabilityTheory.CondIndepSets.condIndep {Ω : Type u_1} {m' : MeasurableSpace Ω} {m₁ : MeasurableSpace Ω} {m₂ : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {p1 : Set (Set Ω)} {p2 : Set (Set Ω)} (h1 : m₁ ≤ mΩ) (h2 : m₂ ≤ mΩ) (hp1 : IsPiSystem p1) (hp2 : IsPiSystem p2) (hpm1 : m₁ = MeasurableSpace.generateFrom p1) (hpm2 : m₂ = MeasurableSpace.generateFrom p2) (hyp : ProbabilityTheory.CondIndepSets m' hm' p1 p2) : ProbabilityTheory.CondIndep m' m₁ m₂ hm'

theorem ProbabilityTheory.CondIndepSets.condIndep' {Ω : Type u_1} {m' : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {p1 : Set (Set Ω)} {p2 : Set (Set Ω)} (hp1m : ∀ s ∈ p1, MeasurableSet s) (hp2m : ∀ s ∈ p2, MeasurableSet s) (hp1 : IsPiSystem p1) (hp2 : IsPiSystem p2) (hyp : ProbabilityTheory.CondIndepSets m' hm' p1 p2) : ProbabilityTheory.CondIndep m' (MeasurableSpace.generateFrom p1) (MeasurableSpace.generateFrom p2) hm'

theorem ProbabilityTheory.condIndepSets_piiUnionInter_of_disjoint {Ω : Type u_1} {ι : Type u_2} {m' : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {s : ι → Set (Set Ω)} {S : Set ι} {T : Set ι} (h_indep : ProbabilityTheory.iCondIndepSets m' hm' s) (hST : Disjoint S T) : ProbabilityTheory.CondIndepSets m' hm' (piiUnionInter s S) (piiUnionInter s T)

theorem ProbabilityTheory.iCondIndepSet.condIndep_generateFrom_of_disjoint {Ω : Type u_1} {ι : Type u_2} {m' : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {s : ι → Set Ω} (hsm : ∀ (n : ι), MeasurableSet (s n)) (hs : ProbabilityTheory.iCondIndepSet m' hm' s) (S : Set ι) (T : Set ι) (hST : Disjoint S T) : ProbabilityTheory.CondIndep m' (MeasurableSpace.generateFrom {t : Set Ω | ∃ n ∈ S, s n = t}) (MeasurableSpace.generateFrom {t : Set Ω | ∃ k ∈ T, s k = t}) hm'

theorem ProbabilityTheory.condIndep_iSup_of_disjoint {Ω : Type u_1} {ι : Type u_2} {m' : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {m : ι → MeasurableSpace Ω} (h_le : ∀ (i : ι), m i ≤ mΩ) (h_indep : ProbabilityTheory.iCondIndep m' hm' m) {S : Set ι} {T : Set ι} (hST : Disjoint S T) : ProbabilityTheory.CondIndep m' (⨆ i ∈ S, m i) (⨆ i ∈ T, m i) hm'

theorem ProbabilityTheory.condIndep_iSup_of_directed_le {Ω : Type u_1} {ι : Type u_2} {m' : MeasurableSpace Ω} {m₁ : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {m : ι → MeasurableSpace Ω} (h_indep : ∀ (i : ι), ProbabilityTheory.CondIndep m' (m i) m₁ hm') (h_le : ∀ (i : ι), m i ≤ mΩ) (h_le' : m₁ ≤ mΩ) (hm : Directed (fun (x x_1 : MeasurableSpace Ω) => x ≤ x_1) m) : ProbabilityTheory.CondIndep m' (⨆ (i : ι), m i) m₁ hm'

theorem ProbabilityTheory.iCondIndepSet.condIndep_generateFrom_lt {Ω : Type u_1} {ι : Type u_2} {m' : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] [Preorder ι] {s : ι → Set Ω} (hsm : ∀ (n : ι), MeasurableSet (s n)) (hs : ProbabilityTheory.iCondIndepSet m' hm' s) (i : ι) : ProbabilityTheory.CondIndep m' (MeasurableSpace.generateFrom {s i}) (MeasurableSpace.generateFrom {t : Set Ω | ∃ j < i, s j = t}) hm'

theorem ProbabilityTheory.iCondIndepSet.condIndep_generateFrom_le {Ω : Type u_1} {ι : Type u_2} {m' : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] [LinearOrder ι] {s : ι → Set Ω} (hsm : ∀ (n : ι), MeasurableSet (s n)) (hs : ProbabilityTheory.iCondIndepSet m' hm' s) (i : ι) {k : ι} (hk : i < k) : ProbabilityTheory.CondIndep m' (MeasurableSpace.generateFrom {s k}) (MeasurableSpace.generateFrom {t : Set Ω | ∃ j ≤ i, s j = t}) hm'

theorem ProbabilityTheory.iCondIndepSet.condIndep_generateFrom_le_nat {Ω : Type u_1} {m' : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {s : ℕ → Set Ω} (hsm : ∀ (n : ℕ), MeasurableSet (s n)) (hs : ProbabilityTheory.iCondIndepSet m' hm' s) (n : ℕ) : ProbabilityTheory.CondIndep m' (MeasurableSpace.generateFrom {s (n + 1)}) (MeasurableSpace.generateFrom {t : Set Ω | ∃ k ≤ n, s k = t}) hm'

theorem ProbabilityTheory.condIndep_iSup_of_monotone {Ω : Type u_1} {ι : Type u_2} {m' : MeasurableSpace Ω} {m₁ : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] [SemilatticeSup ι] {m : ι → MeasurableSpace Ω} (h_indep : ∀ (i : ι), ProbabilityTheory.CondIndep m' (m i) m₁ hm') (h_le : ∀ (i : ι), m i ≤ mΩ) (h_le' : m₁ ≤ mΩ) (hm : Monotone m) : ProbabilityTheory.CondIndep m' (⨆ (i : ι), m i) m₁ hm'

theorem ProbabilityTheory.condIndep_iSup_of_antitone {Ω : Type u_1} {ι : Type u_2} {m' : MeasurableSpace Ω} {m₁ : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] [SemilatticeInf ι] {m : ι → MeasurableSpace Ω} (h_indep : ∀ (i : ι), ProbabilityTheory.CondIndep m' (m i) m₁ hm') (h_le : ∀ (i : ι), m i ≤ mΩ) (h_le' : m₁ ≤ mΩ) (hm : Antitone m) : ProbabilityTheory.CondIndep m' (⨆ (i : ι), m i) m₁ hm'

theorem ProbabilityTheory.iCondIndepSets.piiUnionInter_of_not_mem {Ω : Type u_1} {ι : Type u_2} {m' : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {π : ι → Set (Set Ω)} {a : ι} {S : Finset ι} (hp_ind : ProbabilityTheory.iCondIndepSets m' hm' π) (haS : a ∉ S) : ProbabilityTheory.CondIndepSets m' hm' (piiUnionInter π ↑S) (π a)

theorem ProbabilityTheory.iCondIndepSets.iCondIndep {Ω : Type u_1} {ι : Type u_2} {m' : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] (m : ι → MeasurableSpace Ω) (h_le : ∀ (i : ι), m i ≤ mΩ) (π : ι → Set (Set Ω)) (h_pi : ∀ (n : ι), IsPiSystem (π n)) (h_generate : ∀ (i : ι), m i = MeasurableSpace.generateFrom (π i)) (h_ind : ProbabilityTheory.iCondIndepSets m' hm' π) : ProbabilityTheory.iCondIndep m' hm' m

The σ-algebras generated by conditionally independent pi-systems are conditionally independent.

Conditional independence of measurable sets

theorem ProbabilityTheory.CondIndepSets.condIndepSet_of_mem {Ω : Type u_1} {m' : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' ≤ mΩ} {s : Set Ω} {t : Set Ω} (S : Set (Set Ω)) (T : Set (Set Ω)) (hs : s ∈ S) (ht : t ∈ T) (hs_meas : MeasurableSet s) (ht_meas : MeasurableSet t) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] (h_indep : ProbabilityTheory.CondIndepSets m' hm' S T) : ProbabilityTheory.CondIndepSet m' hm' s t

theorem ProbabilityTheory.CondIndep.condIndepSet_of_measurableSet {Ω : Type u_1} {m' : MeasurableSpace Ω} {m₁ : MeasurableSpace Ω} {m₂ : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] (h_indep : ProbabilityTheory.CondIndep m' m₁ m₂ hm') {s : Set Ω} {t : Set Ω} (hs : MeasurableSet s) (ht : MeasurableSet t) : ProbabilityTheory.CondIndepSet m' hm' s t

theorem ProbabilityTheory.condIndep_iff_forall_condIndepSet {Ω : Type u_1} {m' : MeasurableSpace Ω} {m₁ : MeasurableSpace Ω} {m₂ : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' ≤ mΩ} (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] : ProbabilityTheory.CondIndep m' m₁ m₂ hm' ↔ ∀ (s t : Set Ω), MeasurableSet s → MeasurableSet t → ProbabilityTheory.CondIndepSet m' hm' s t

Conditional independence of random variables

theorem ProbabilityTheory.condIndepFun_iff_condexp_inter_preimage_eq_mul {Ω : Type u_1} {β : Type u_3} {β' : Type u_4} {m' : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {f : Ω → β} {g : Ω → β'} {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'} (hf : Measurable f) (hg : Measurable g) : ProbabilityTheory.CondIndepFun m' hm' f g ↔ ∀ (s : Set β) (t : Set β'), MeasurableSet s → MeasurableSet t → MeasureTheory.condexp m' μ (Set.indicator (f ⁻¹' s ∩ g ⁻¹' t) fun (ω : Ω) => 1) =ᶠ[MeasureTheory.Measure.ae μ] fun (ω : Ω) => MeasureTheory.condexp m' μ (Set.indicator (f ⁻¹' s) fun (ω : Ω) => 1) ω * MeasureTheory.condexp m' μ (Set.indicator (g ⁻¹' t) fun (ω : Ω) => 1) ω

theorem ProbabilityTheory.iCondIndepFun_iff_condexp_inter_preimage_eq_mul {Ω : Type u_1} {ι : Type u_2} {m' : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {β : ι → Type u_5} (m : (x : ι) → MeasurableSpace (β x)) (f : (i : ι) → Ω → β i) (hf : ∀ (i : ι), Measurable (f i)) : ProbabilityTheory.iCondIndepFun m' hm' m f ↔ ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)}, (∀ i ∈ S, MeasurableSet (sets i)) → MeasureTheory.condexp m' μ (Set.indicator (⋂ i ∈ S, f i ⁻¹' sets i) fun (ω : Ω) => 1) =ᶠ[MeasureTheory.Measure.ae μ] Finset.prod S fun (i : ι) => MeasureTheory.condexp m' μ (Set.indicator (f i ⁻¹' sets i) fun (ω : Ω) => 1)

theorem ProbabilityTheory.condIndepFun_iff_condIndepSet_preimage {Ω : Type u_1} {β : Type u_3} {β' : Type u_4} {m' : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {f : Ω → β} {g : Ω → β'} {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'} (hf : Measurable f) (hg : Measurable g) : ProbabilityTheory.CondIndepFun m' hm' f g ↔ ∀ (s : Set β) (t : Set β'), MeasurableSet s → MeasurableSet t → ProbabilityTheory.CondIndepSet m' hm' (f ⁻¹' s) (g ⁻¹' t)

theorem ProbabilityTheory.CondIndepFun.symm {Ω : Type u_1} {β : Type u_3} {m' : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] : ∀ {x : MeasurableSpace β} {f g : Ω → β}, ProbabilityTheory.CondIndepFun m' hm' f g → ProbabilityTheory.CondIndepFun m' hm' g f

theorem ProbabilityTheory.CondIndepFun.comp {Ω : Type u_1} {β : Type u_3} {β' : Type u_4} {m' : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {f : Ω → β} {g : Ω → β'} {γ : Type u_5} {γ' : Type u_6} {_mβ : MeasurableSpace β} {_mβ' : MeasurableSpace β'} {_mγ : MeasurableSpace γ} {_mγ' : MeasurableSpace γ'} {φ : β → γ} {ψ : β' → γ'} (hfg : ProbabilityTheory.CondIndepFun m' hm' f g) (hφ : Measurable φ) (hψ : Measurable ψ) : ProbabilityTheory.CondIndepFun m' hm' (φ ∘ f) (ψ ∘ g)

theorem ProbabilityTheory.iCondIndepFun.of_subsingleton {Ω : Type u_1} {ι : Type u_2} {m' : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {β : ι → Type u_5} {m : (i : ι) → MeasurableSpace (β i)} {f : (i : ι) → Ω → β i} [Subsingleton ι] : ProbabilityTheory.iCondIndepFun m' hm' m f

theorem ProbabilityTheory.iCondIndepFun.condIndepFun_finset {Ω : Type u_1} {ι : Type u_2} {m' : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {β : ι → Type u_6} {m : (i : ι) → MeasurableSpace (β i)} {f : (i : ι) → Ω → β i} (S : Finset ι) (T : Finset ι) (hST : Disjoint S T) (hf_Indep : ProbabilityTheory.iCondIndepFun m' hm' m f) (hf_meas : ∀ (i : ι), Measurable (f i)) : ProbabilityTheory.CondIndepFun m' hm' (fun (a : Ω) (i : { x : ι // x ∈ S }) => f (↑i) a) fun (a : Ω) (i : { x : ι // x ∈ T }) => f (↑i) a

If f is a family of mutually conditionally independent random variables (iCondIndepFun m' hm' m f μ) and S, T are two disjoint finite index sets, then the tuple formed by f i for i ∈ S is conditionally independent of the tuple (f i)_i for i ∈ T.

theorem ProbabilityTheory.iCondIndepFun.condIndepFun_prod_mk {Ω : Type u_1} {ι : Type u_2} {m' : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {β : ι → Type u_6} {m : (i : ι) → MeasurableSpace (β i)} {f : (i : ι) → Ω → β i} (hf_Indep : ProbabilityTheory.iCondIndepFun m' hm' m f) (hf_meas : ∀ (i : ι), Measurable (f i)) (i : ι) (j : ι) (k : ι) (hik : i ≠ k) (hjk : j ≠ k) : ProbabilityTheory.CondIndepFun m' hm' (fun (a : Ω) => (f i a, f j a)) (f k)

theorem ProbabilityTheory.iCondIndepFun.condIndepFun_prod_mk_prod_mk {Ω : Type u_1} {ι : Type u_2} {m' : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {β : ι → Type u_5} {m : (i : ι) → MeasurableSpace (β i)} {f : (i : ι) → Ω → β i} (h_indep : ProbabilityTheory.iCondIndepFun m' hm' m f) (hf : ∀ (i : ι), Measurable (f i)) (i : ι) (j : ι) (k : ι) (l : ι) (hik : i ≠ k) (hil : i ≠ l) (hjk : j ≠ k) (hjl : j ≠ l) : ProbabilityTheory.CondIndepFun m' hm' (fun (a : Ω) => (f i a, f j a)) fun (a : Ω) => (f k a, f l a)

theorem ProbabilityTheory.iCondIndepFun.indepFun_add_left {Ω : Type u_1} {ι : Type u_2} {m' : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {β : Type u_5} {m : MeasurableSpace β} [Add β] [MeasurableAdd₂ β] {f : ι → Ω → β} (hf_indep : ProbabilityTheory.iCondIndepFun m' hm' (fun (x : ι) => m) f) (hf_meas : ∀ (i : ι), Measurable (f i)) (i : ι) (j : ι) (k : ι) (hik : i ≠ k) (hjk : j ≠ k) : ProbabilityTheory.CondIndepFun m' hm' (f i + f j) (f k)

theorem ProbabilityTheory.iCondIndepFun.indepFun_mul_left {Ω : Type u_1} {ι : Type u_2} {m' : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {β : Type u_5} {m : MeasurableSpace β} [Mul β] [MeasurableMul₂ β] {f : ι → Ω → β} (hf_indep : ProbabilityTheory.iCondIndepFun m' hm' (fun (x : ι) => m) f) (hf_meas : ∀ (i : ι), Measurable (f i)) (i : ι) (j : ι) (k : ι) (hik : i ≠ k) (hjk : j ≠ k) : ProbabilityTheory.CondIndepFun m' hm' (f i * f j) (f k)

theorem ProbabilityTheory.iCondIndepFun.indepFun_add_right {Ω : Type u_1} {ι : Type u_2} {m' : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {β : Type u_5} {m : MeasurableSpace β} [Add β] [MeasurableAdd₂ β] {f : ι → Ω → β} (hf_indep : ProbabilityTheory.iCondIndepFun m' hm' (fun (x : ι) => m) f) (hf_meas : ∀ (i : ι), Measurable (f i)) (i : ι) (j : ι) (k : ι) (hij : i ≠ j) (hik : i ≠ k) : ProbabilityTheory.CondIndepFun m' hm' (f i) (f j + f k)

theorem ProbabilityTheory.iCondIndepFun.indepFun_mul_right {Ω : Type u_1} {ι : Type u_2} {m' : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {β : Type u_5} {m : MeasurableSpace β} [Mul β] [MeasurableMul₂ β] {f : ι → Ω → β} (hf_indep : ProbabilityTheory.iCondIndepFun m' hm' (fun (x : ι) => m) f) (hf_meas : ∀ (i : ι), Measurable (f i)) (i : ι) (j : ι) (k : ι) (hij : i ≠ j) (hik : i ≠ k) : ProbabilityTheory.CondIndepFun m' hm' (f i) (f j * f k)

theorem ProbabilityTheory.iCondIndepFun.indepFun_add_add {Ω : Type u_1} {ι : Type u_2} {m' : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {β : Type u_5} {m : MeasurableSpace β} [Add β] [MeasurableAdd₂ β] {f : ι → Ω → β} (hf_indep : ProbabilityTheory.iCondIndepFun m' hm' (fun (x : ι) => m) f) (hf_meas : ∀ (i : ι), Measurable (f i)) (i : ι) (j : ι) (k : ι) (l : ι) (hik : i ≠ k) (hil : i ≠ l) (hjk : j ≠ k) (hjl : j ≠ l) : ProbabilityTheory.CondIndepFun m' hm' (f i + f j) (f k + f l)

theorem ProbabilityTheory.iCondIndepFun.indepFun_mul_mul {Ω : Type u_1} {ι : Type u_2} {m' : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {β : Type u_5} {m : MeasurableSpace β} [Mul β] [MeasurableMul₂ β] {f : ι → Ω → β} (hf_indep : ProbabilityTheory.iCondIndepFun m' hm' (fun (x : ι) => m) f) (hf_meas : ∀ (i : ι), Measurable (f i)) (i : ι) (j : ι) (k : ι) (l : ι) (hik : i ≠ k) (hil : i ≠ l) (hjk : j ≠ k) (hjl : j ≠ l) : ProbabilityTheory.CondIndepFun m' hm' (f i * f j) (f k * f l)

theorem ProbabilityTheory.iCondIndepFun.indepFun_sub_left {Ω : Type u_1} {ι : Type u_2} {m' : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {β : Type u_5} {m : MeasurableSpace β} [Sub β] [MeasurableSub₂ β] {f : ι → Ω → β} (hf_indep : ProbabilityTheory.iCondIndepFun m' hm' (fun (x : ι) => m) f) (hf_meas : ∀ (i : ι), Measurable (f i)) (i : ι) (j : ι) (k : ι) (hik : i ≠ k) (hjk : j ≠ k) : ProbabilityTheory.CondIndepFun m' hm' (f i - f j) (f k)

theorem ProbabilityTheory.iCondIndepFun.indepFun_div_left {Ω : Type u_1} {ι : Type u_2} {m' : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {β : Type u_5} {m : MeasurableSpace β} [Div β] [MeasurableDiv₂ β] {f : ι → Ω → β} (hf_indep : ProbabilityTheory.iCondIndepFun m' hm' (fun (x : ι) => m) f) (hf_meas : ∀ (i : ι), Measurable (f i)) (i : ι) (j : ι) (k : ι) (hik : i ≠ k) (hjk : j ≠ k) : ProbabilityTheory.CondIndepFun m' hm' (f i / f j) (f k)

theorem ProbabilityTheory.iCondIndepFun.indepFun_sub_right {Ω : Type u_1} {ι : Type u_2} {m' : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {β : Type u_5} {m : MeasurableSpace β} [Sub β] [MeasurableSub₂ β] {f : ι → Ω → β} (hf_indep : ProbabilityTheory.iCondIndepFun m' hm' (fun (x : ι) => m) f) (hf_meas : ∀ (i : ι), Measurable (f i)) (i : ι) (j : ι) (k : ι) (hij : i ≠ j) (hik : i ≠ k) : ProbabilityTheory.CondIndepFun m' hm' (f i) (f j - f k)

theorem ProbabilityTheory.iCondIndepFun.indepFun_div_right {Ω : Type u_1} {ι : Type u_2} {m' : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {β : Type u_5} {m : MeasurableSpace β} [Div β] [MeasurableDiv₂ β] {f : ι → Ω → β} (hf_indep : ProbabilityTheory.iCondIndepFun m' hm' (fun (x : ι) => m) f) (hf_meas : ∀ (i : ι), Measurable (f i)) (i : ι) (j : ι) (k : ι) (hij : i ≠ j) (hik : i ≠ k) : ProbabilityTheory.CondIndepFun m' hm' (f i) (f j / f k)

theorem ProbabilityTheory.iCondIndepFun.indepFun_sub_sub {Ω : Type u_1} {ι : Type u_2} {m' : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {β : Type u_5} {m : MeasurableSpace β} [Sub β] [MeasurableSub₂ β] {f : ι → Ω → β} (hf_indep : ProbabilityTheory.iCondIndepFun m' hm' (fun (x : ι) => m) f) (hf_meas : ∀ (i : ι), Measurable (f i)) (i : ι) (j : ι) (k : ι) (l : ι) (hik : i ≠ k) (hil : i ≠ l) (hjk : j ≠ k) (hjl : j ≠ l) : ProbabilityTheory.CondIndepFun m' hm' (f i - f j) (f k - f l)

theorem ProbabilityTheory.iCondIndepFun.indepFun_div_div {Ω : Type u_1} {ι : Type u_2} {m' : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {β : Type u_5} {m : MeasurableSpace β} [Div β] [MeasurableDiv₂ β] {f : ι → Ω → β} (hf_indep : ProbabilityTheory.iCondIndepFun m' hm' (fun (x : ι) => m) f) (hf_meas : ∀ (i : ι), Measurable (f i)) (i : ι) (j : ι) (k : ι) (l : ι) (hik : i ≠ k) (hil : i ≠ l) (hjk : j ≠ k) (hjl : j ≠ l) : ProbabilityTheory.CondIndepFun m' hm' (f i / f j) (f k / f l)

theorem ProbabilityTheory.iCondIndepFun.condIndepFun_finset_sum_of_not_mem {Ω : Type u_1} {ι : Type u_2} {m' : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {β : Type u_5} {m : MeasurableSpace β} [AddCommMonoid β] [MeasurableAdd₂ β] {f : ι → Ω → β} (hf_Indep : ProbabilityTheory.iCondIndepFun m' hm' (fun (x : ι) => m) f) (hf_meas : ∀ (i : ι), Measurable (f i)) {s : Finset ι} {i : ι} (hi : i ∉ s) : ProbabilityTheory.CondIndepFun m' hm' (Finset.sum s fun (j : ι) => f j) (f i)

theorem ProbabilityTheory.iCondIndepFun.condIndepFun_finset_prod_of_not_mem {Ω : Type u_1} {ι : Type u_2} {m' : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {β : Type u_5} {m : MeasurableSpace β} [CommMonoid β] [MeasurableMul₂ β] {f : ι → Ω → β} (hf_Indep : ProbabilityTheory.iCondIndepFun m' hm' (fun (x : ι) => m) f) (hf_meas : ∀ (i : ι), Measurable (f i)) {s : Finset ι} {i : ι} (hi : i ∉ s) : ProbabilityTheory.CondIndepFun m' hm' (Finset.prod s fun (j : ι) => f j) (f i)

theorem ProbabilityTheory.iCondIndepFun.condIndepFun_sum_range_succ {Ω : Type u_1} {m' : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {β : Type u_5} {m : MeasurableSpace β} [AddCommMonoid β] [MeasurableAdd₂ β] {f : ℕ → Ω → β} (hf_Indep : ProbabilityTheory.iCondIndepFun m' hm' (fun (x : ℕ) => m) f) (hf_meas : ∀ (i : ℕ), Measurable (f i)) (n : ℕ) : ProbabilityTheory.CondIndepFun m' hm' (Finset.sum (Finset.range n) fun (j : ℕ) => f j) (f n)

theorem ProbabilityTheory.iCondIndepFun.condIndepFun_prod_range_succ {Ω : Type u_1} {m' : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {β : Type u_5} {m : MeasurableSpace β} [CommMonoid β] [MeasurableMul₂ β] {f : ℕ → Ω → β} (hf_Indep : ProbabilityTheory.iCondIndepFun m' hm' (fun (x : ℕ) => m) f) (hf_meas : ∀ (i : ℕ), Measurable (f i)) (n : ℕ) : ProbabilityTheory.CondIndepFun m' hm' (Finset.prod (Finset.range n) fun (j : ℕ) => f j) (f n)

theorem ProbabilityTheory.iCondIndepSet.iCondIndepFun_indicator {Ω : Type u_1} {ι : Type u_2} {β : Type u_3} {m' : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] [Zero β] [One β] {m : MeasurableSpace β} {s : ι → Set Ω} (hs : ProbabilityTheory.iCondIndepSet m' hm' s) : ProbabilityTheory.iCondIndepFun m' hm' (fun (_n : ι) => m) fun (n : ι) => Set.indicator (s n) fun (_ω : Ω) => 1