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 Ω] (hm' : m' ≤ mΩ) (π : ι → Set (Set Ω)) (μ : MeasureTheory.Measure Ω := by volume_tac) [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 ∈ 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') (μ.trim hm')

def ProbabilityTheory.CondIndepSets {Ω : Type u_1} (m' : MeasurableSpace Ω) {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] (hm' : m' ≤ mΩ) (s1 s2 : Set (Set Ω)) (μ : MeasureTheory.Measure Ω := by volume_tac) [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') (μ.trim hm')

def ProbabilityTheory.iCondIndep {Ω : Type u_1} {ι : Type u_2} (m' : MeasurableSpace Ω) {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] (hm' : m' ≤ mΩ) (m : ι → MeasurableSpace Ω) (μ : MeasureTheory.Measure Ω := by volume_tac) [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 ∈ s, μ⟦f i | m'⟧ . See ProbabilityTheory.iCondIndep_iff.

Equations

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

def ProbabilityTheory.CondIndep {Ω : Type u_1} (m' m₁ m₂ : MeasurableSpace Ω) {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] (hm' : m' ≤ mΩ) (μ : MeasureTheory.Measure Ω := by volume_tac) [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') (μ.trim hm')

def ProbabilityTheory.iCondIndepSet {Ω : Type u_1} {ι : Type u_2} (m' : MeasurableSpace Ω) {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] (hm' : m' ≤ mΩ) (s : ι → Set Ω) (μ : MeasureTheory.Measure Ω := by volume_tac) [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') (μ.trim hm')

def ProbabilityTheory.CondIndepSet {Ω : Type u_1} (m' : MeasurableSpace Ω) {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] (hm' : m' ≤ mΩ) (s t : Set Ω) (μ : MeasureTheory.Measure Ω := by volume_tac) [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') (μ.trim hm')

def ProbabilityTheory.iCondIndepFun {Ω : Type u_1} {ι : Type u_2} (m' : MeasurableSpace Ω) {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] (hm' : m' ≤ mΩ) {β : ι → Type u_3} (m : (x : ι) → MeasurableSpace (β x)) (f : (x : ι) → Ω → β x) (μ : MeasureTheory.Measure Ω := by volume_tac) [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') (μ.trim hm')

def ProbabilityTheory.CondIndepFun {Ω : Type u_1} (m' : MeasurableSpace Ω) {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] (hm' : m' ≤ mΩ) {β : Type u_3} {γ : Type u_4} [MeasurableSpace β] [MeasurableSpace γ] (f : Ω → β) (g : Ω → γ) (μ : MeasureTheory.Measure Ω := by volume_tac) [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') (μ.trim hm')

theorem ProbabilityTheory.iCondIndepSets_iff {Ω : Type u_1} {ι : Type u_2} (m' : MeasurableSpace Ω) {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] (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' μ ((⋂ i ∈ s, f i).indicator fun (ω : Ω) => 1) =ᵐ[μ] ∏ i ∈ s, MeasureTheory.condexp m' μ ((f i).indicator fun (ω : Ω) => 1)

theorem ProbabilityTheory.condIndepSets_iff {Ω : Type u_1} (m' : MeasurableSpace Ω) {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] (hm' : m' ≤ mΩ) (s1 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' μ ((t1 ∩ t2).indicator fun (ω : Ω) => 1) =ᵐ[μ] MeasureTheory.condexp m' μ (t1.indicator fun (ω : Ω) => 1) * MeasureTheory.condexp m' μ (t2.indicator fun (ω : Ω) => 1)

theorem ProbabilityTheory.iCondIndepSets_singleton_iff {Ω : Type u_1} {ι : Type u_2} (m' : MeasurableSpace Ω) {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] (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' μ ((⋂ i ∈ S, s i).indicator fun (ω : Ω) => 1) =ᵐ[μ] ∏ i ∈ S, MeasureTheory.condexp m' μ ((s i).indicator fun (ω : Ω) => 1)

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

theorem ProbabilityTheory.iCondIndep_iff_iCondIndepSets {Ω : Type u_1} {ι : Type u_2} (m' : MeasurableSpace Ω) {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] (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 Ω] (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' μ ((⋂ i ∈ s, f i).indicator fun (ω : Ω) => 1) =ᵐ[μ] ∏ i ∈ s, MeasureTheory.condexp m' μ ((f i).indicator fun (ω : Ω) => 1)

theorem ProbabilityTheory.condIndep_iff_condIndepSets {Ω : Type u_1} (m' m₁ m₂ : MeasurableSpace Ω) {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] (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' m₁ m₂ : MeasurableSpace Ω) {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] (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' μ ((t1 ∩ t2).indicator fun (ω : Ω) => 1) =ᵐ[μ] MeasureTheory.condexp m' μ (t1.indicator fun (ω : Ω) => 1) * MeasureTheory.condexp m' μ (t2.indicator fun (ω : Ω) => 1)

theorem ProbabilityTheory.iCondIndepSet_iff_iCondIndep {Ω : Type u_1} {ι : Type u_2} (m' : MeasurableSpace Ω) {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] (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 Ω] (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 Ω] (hm' : m' ≤ mΩ) (s : ι → Set Ω) (hs : ∀ (i : ι), MeasurableSet (s i)) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] : ProbabilityTheory.iCondIndepSet m' hm' s μ ↔ ∀ (S : Finset ι), MeasureTheory.condexp m' μ ((⋂ i ∈ S, s i).indicator fun (ω : Ω) => 1) =ᵐ[μ] ∏ i ∈ S, MeasureTheory.condexp m' μ ((s i).indicator fun (ω : Ω) => 1)

theorem ProbabilityTheory.condIndepSet_iff_condIndep {Ω : Type u_1} (m' : MeasurableSpace Ω) {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] (hm' : m' ≤ mΩ) (s 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 Ω] (hm' : m' ≤ mΩ) {s 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 Ω] (hm' : m' ≤ mΩ) (s t : Set Ω) (hs : MeasurableSet s) (ht : MeasurableSet t) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] : ProbabilityTheory.CondIndepSet m' hm' s t μ ↔ MeasureTheory.condexp m' μ ((s ∩ t).indicator fun (ω : Ω) => 1) =ᵐ[μ] MeasureTheory.condexp m' μ (s.indicator fun (ω : Ω) => 1) * MeasureTheory.condexp m' μ (t.indicator fun (ω : Ω) => 1)

theorem ProbabilityTheory.iCondIndepFun_iff_iCondIndep {Ω : Type u_1} {ι : Type u_2} (m' : MeasurableSpace Ω) {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] (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 Ω] (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' μ ((⋂ i ∈ s, g i).indicator fun (ω : Ω) => 1) =ᵐ[μ] ∏ i ∈ s, MeasureTheory.condexp m' μ ((g i).indicator fun (ω : Ω) => 1)

theorem ProbabilityTheory.condIndepFun_iff_condIndep {Ω : Type u_1} (m' : MeasurableSpace Ω) {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] (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 Ω] (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' μ ((t1 ∩ t2).indicator fun (ω : Ω) => 1) =ᵐ[μ] MeasureTheory.condexp m' μ (t1.indicator fun (ω : Ω) => 1) * MeasureTheory.condexp m' μ (t2.indicator fun (ω : Ω) => 1)

theorem ProbabilityTheory.CondIndepSets.symm {Ω : Type u_1} {m' mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {s₁ 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' mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {s₁ s₂ 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' mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {s₁ s₂ 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' mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {s₁ s₂ 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' mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {s₁ s₂ 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' mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] {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' mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] {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' mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {s₁ 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' mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] {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' mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] {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' mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] (s : Set Ω) : ProbabilityTheory.CondIndepSet m' hm' s ∅ μ

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

theorem ProbabilityTheory.CondIndep.symm {Ω : Type u_1} {m' m₁ m₂ mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] {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' mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] : ProbabilityTheory.CondIndep m' m₁ ⊥ hm' μ

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

theorem ProbabilityTheory.condIndep_of_condIndep_of_le_left {Ω : Type u_1} {m' m₁ m₂ m₃ mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] {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' m₁ m₂ m₃ mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] {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' mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] {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' mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] {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' mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] {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' mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] {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' mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {s1 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' m₁ m₂ mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {p1 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' mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {p1 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' mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {s : ι → Set (Set Ω)} {S 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' mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {s : ι → Set Ω} (hsm : ∀ (n : ι), MeasurableSet (s n)) (hs : ProbabilityTheory.iCondIndepSet m' hm' s μ) (S 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' mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {m : ι → MeasurableSpace Ω} (h_le : ∀ (i : ι), m i ≤ mΩ) (h_indep : ProbabilityTheory.iCondIndep m' hm' m μ) {S 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' m₁ mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] {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 (x1 x2 : MeasurableSpace Ω) => x1 ≤ x2) m) : ProbabilityTheory.CondIndep m' (⨆ (i : ι), m i) m₁ hm' μ

theorem ProbabilityTheory.iCondIndepSet.condIndep_generateFrom_lt {Ω : Type u_1} {ι : Type u_2} {m' mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] {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' mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] {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' mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] {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' m₁ mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] {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' m₁ mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] {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' mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] {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' mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] {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' mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] {hm' : m' ≤ mΩ} {s t : Set Ω} (S 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' m₁ m₂ mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] (h_indep : ProbabilityTheory.CondIndep m' m₁ m₂ hm' μ) {s t : Set Ω} (hs : MeasurableSet s) (ht : MeasurableSet t) : ProbabilityTheory.CondIndepSet m' hm' s t μ

theorem ProbabilityTheory.condIndep_iff_forall_condIndepSet {Ω : Type u_1} {m' m₁ m₂ mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] {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' mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] {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' μ ((f ⁻¹' s ∩ g ⁻¹' t).indicator fun (ω : Ω) => 1) =ᵐ[μ] fun (ω : Ω) => MeasureTheory.condexp m' μ ((f ⁻¹' s).indicator fun (ω : Ω) => 1) ω * MeasureTheory.condexp m' μ ((g ⁻¹' t).indicator fun (ω : Ω) => 1) ω

theorem ProbabilityTheory.iCondIndepFun_iff_condexp_inter_preimage_eq_mul {Ω : Type u_1} {ι : Type u_2} {m' mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] {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' μ ((⋂ i ∈ S, f i ⁻¹' sets i).indicator fun (ω : Ω) => 1) =ᵐ[μ] ∏ i ∈ S, MeasureTheory.condexp m' μ ((f i ⁻¹' sets i).indicator fun (ω : Ω) => 1)

theorem ProbabilityTheory.condIndepFun_iff_condIndepSet_preimage {Ω : Type u_1} {β : Type u_3} {β' : Type u_4} {m' mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] {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' mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {x✝ : MeasurableSpace β} {f g : Ω → β} (hfg : 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' mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] {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.CondIndepFun.neg_right {Ω : Type u_1} {β : Type u_3} {β' : Type u_4} {m' mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {f : Ω → β} {g : Ω → β'} {_mβ : MeasurableSpace β} {_mβ' : MeasurableSpace β'} [Neg β'] [MeasurableNeg β'] (hfg : ProbabilityTheory.CondIndepFun m' hm' f g μ) : ProbabilityTheory.CondIndepFun m' hm' f (-g) μ

theorem ProbabilityTheory.CondIndepFun.neg_left {Ω : Type u_1} {β : Type u_3} {β' : Type u_4} {m' mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {f : Ω → β} {g : Ω → β'} {_mβ : MeasurableSpace β} {_mβ' : MeasurableSpace β'} [Neg β] [MeasurableNeg β] (hfg : ProbabilityTheory.CondIndepFun m' hm' f g μ) : ProbabilityTheory.CondIndepFun m' hm' (-f) g μ

theorem ProbabilityTheory.iCondIndepFun.of_subsingleton {Ω : Type u_1} {ι : Type u_2} {m' mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] {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' mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {β : ι → Type u_6} {m : (i : ι) → MeasurableSpace (β i)} {f : (i : ι) → Ω → β i} (S 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' mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] {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' mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] {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_mul_left {Ω : Type u_1} {ι : Type u_2} {β : Type u_3} {m' mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {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_left {Ω : Type u_1} {ι : Type u_2} {β : Type u_3} {m' mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {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_right {Ω : Type u_1} {ι : Type u_2} {β : Type u_3} {m' mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {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_right {Ω : Type u_1} {ι : Type u_2} {β : Type u_3} {m' mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {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_mul {Ω : Type u_1} {ι : Type u_2} {β : Type u_3} {m' mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {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_add_add {Ω : Type u_1} {ι : Type u_2} {β : Type u_3} {m' mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {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_div_left {Ω : Type u_1} {ι : Type u_2} {β : Type u_3} {m' mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {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_left {Ω : Type u_1} {ι : Type u_2} {β : Type u_3} {m' mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {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_right {Ω : Type u_1} {ι : Type u_2} {β : Type u_3} {m' mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {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_right {Ω : Type u_1} {ι : Type u_2} {β : Type u_3} {m' mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {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_div {Ω : Type u_1} {ι : Type u_2} {β : Type u_3} {m' mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {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.indepFun_sub_sub {Ω : Type u_1} {ι : Type u_2} {β : Type u_3} {m' mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {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.condIndepFun_finset_prod_of_not_mem {Ω : Type u_1} {ι : Type u_2} {β : Type u_3} {m' mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {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' (∏ j ∈ s, f j) (f i) μ

theorem ProbabilityTheory.iCondIndepFun.condIndepFun_finset_sum_of_not_mem {Ω : Type u_1} {ι : Type u_2} {β : Type u_3} {m' mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {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' (∑ j ∈ s, f j) (f i) μ

theorem ProbabilityTheory.iCondIndepFun.condIndepFun_prod_range_succ {Ω : Type u_1} {β : Type u_3} {m' mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {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' (∏ j ∈ Finset.range n, f j) (f n) μ

theorem ProbabilityTheory.iCondIndepFun.condIndepFun_sum_range_succ {Ω : Type u_1} {β : Type u_3} {m' mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {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' (∑ j ∈ Finset.range n, f j) (f n) μ

theorem ProbabilityTheory.iCondIndepSet.iCondIndepFun_indicator {Ω : Type u_1} {ι : Type u_2} {β : Type u_3} {m' mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] {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 : ι) => (s n).indicator fun (_ω : Ω) => 1) μ