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.

Notation

• X ⟂ᵢ[Z, hZ; μ] Y for CondIndepFun (MeasurableSpace.comap Z inferInstance) hZ.comap_le X Y μ, independence of X and Y given Z.
• X ⟂ᵢ[Z, hZ] Y for the cases of μ = volume.

These notations are scoped in the ProbabilityTheory namespace.

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' f μ = ProbabilityTheory.Kernel.iIndepFun 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. We use the notation X ⟂ᵢ[Z, hZ; μ] Y to write that X and Y are conditionally independent given (the σ-algebra generated by) Z (scoped in ProbabilityTheory).

Equations

• ProbabilityTheory.CondIndepFun m' hm' f g μ = ProbabilityTheory.Kernel.IndepFun f g (ProbabilityTheory.condExpKernel μ m') (μ.trim hm')

def ProbabilityTheory.«term_⟂ᵢ[_,_;_]_» : Lean.TrailingParserDescr

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. We use the notation X ⟂ᵢ[Z, hZ; μ] Y to write that X and Y are conditionally independent given (the σ-algebra generated by) Z (scoped in ProbabilityTheory).

Equations

• One or more equations did not get rendered due to their size.

def ProbabilityTheory.«term_⟂ᵢ[_,_]_» : Lean.TrailingParserDescr

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. We use the notation X ⟂ᵢ[Z, hZ; μ] Y to write that X and Y are conditionally independent given (the σ-algebra generated by) Z (scoped in ProbabilityTheory).

Equations

• One or more equations did not get rendered due to their size.

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 μ] : iCondIndepSets m' hm' π μ ↔ ∀ (s : Finset ι) {f : ι → Set Ω}, (∀ i ∈ s, f i ∈ π i) → μ[(⋂ i ∈ s, f i).indicator fun (ω : Ω) => 1|m'] =ᵐ[μ] ∏ i ∈ s, μ[(f i).indicator fun (ω : Ω) => 1|m']

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 μ] : CondIndepSets m' hm' s1 s2 μ ↔ ∀ (t1 t2 : Set Ω), t1 ∈ s1 → t2 ∈ s2 → μ[(t1 ∩ t2).indicator fun (ω : Ω) => 1|m'] =ᵐ[μ] μ[t1.indicator fun (ω : Ω) => 1|m'] * μ[t2.indicator fun (ω : Ω) => 1|m']

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 μ] : iCondIndepSets m' hm' (fun (i : ι) => {s i}) μ ↔ ∀ (S : Finset ι), μ[(⋂ i ∈ S, s i).indicator fun (ω : Ω) => 1|m'] =ᵐ[μ] ∏ i ∈ S, μ[(s i).indicator fun (ω : Ω) => 1|m']

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) : CondIndepSets m' hm' {s} {t} μ ↔ μ[(s ∩ t).indicator fun (ω : Ω) => 1|m'] =ᵐ[μ] μ[s.indicator fun (ω : Ω) => 1|m'] * μ[t.indicator fun (ω : Ω) => 1|m']

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 μ] : iCondIndep m' hm' m μ ↔ 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 μ] : iCondIndep m' hm' m μ ↔ ∀ (s : Finset ι) {f : ι → Set Ω}, (∀ i ∈ s, MeasurableSet (f i)) → μ[(⋂ i ∈ s, f i).indicator fun (ω : Ω) => 1|m'] =ᵐ[μ] ∏ i ∈ s, μ[(f i).indicator fun (ω : Ω) => 1|m']

theorem ProbabilityTheory.condIndep_iff_condIndepSets {Ω : Type u_1} (m' m₁ m₂ : MeasurableSpace Ω) {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] (hm' : m' ≤ mΩ) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] : CondIndep m' m₁ m₂ hm' μ ↔ 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 μ] : CondIndep m' m₁ m₂ hm' μ ↔ ∀ (t1 t2 : Set Ω), MeasurableSet t1 → MeasurableSet t2 → μ[(t1 ∩ t2).indicator fun (ω : Ω) => 1|m'] =ᵐ[μ] μ[t1.indicator fun (ω : Ω) => 1|m'] * μ[t2.indicator fun (ω : Ω) => 1|m']

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 μ] : iCondIndepSet m' hm' s μ ↔ 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 μ] : iCondIndepSet m' hm' s μ ↔ 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 μ] : iCondIndepSet m' hm' s μ ↔ ∀ (S : Finset ι), μ[(⋂ i ∈ S, s i).indicator fun (ω : Ω) => 1|m'] =ᵐ[μ] ∏ i ∈ S, μ[(s i).indicator fun (ω : Ω) => 1|m']

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

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 μ] : iCondIndepFun m' hm' f μ ↔ 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 μ] : iCondIndepFun m' hm' f μ ↔ ∀ (s : Finset ι) {g : ι → Set Ω}, (∀ i ∈ s, MeasurableSet (g i)) → μ[(⋂ i ∈ s, g i).indicator fun (ω : Ω) => 1|m'] =ᵐ[μ] ∏ i ∈ s, μ[(g i).indicator fun (ω : Ω) => 1|m']

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 μ] : CondIndepFun m' hm' f g μ ↔ 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 μ] : CondIndepFun m' hm' f g μ ↔ ∀ (t1 t2 : Set Ω), MeasurableSet t1 → MeasurableSet t2 → μ[(t1 ∩ t2).indicator fun (ω : Ω) => 1|m'] =ᵐ[μ] μ[t1.indicator fun (ω : Ω) => 1|m'] * μ[t2.indicator fun (ω : Ω) => 1|m']

theorem ProbabilityTheory.CondIndepSets.symm {Ω : Type u_1} {m' mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {s₁ s₂ : Set (Set Ω)} (h : CondIndepSets m' hm' s₁ s₂ μ) : 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 : CondIndepSets m' hm' s₁ s₂ μ) (h31 : s₃ ⊆ s₁) : 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 : CondIndepSets m' hm' s₁ s₂ μ) (h32 : s₃ ⊆ s₂) : 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₁ : CondIndepSets m' hm' s₁ s' μ) (h₂ : CondIndepSets m' hm' s₂ s' μ) : 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 Ω)} : CondIndepSets m' hm' (s₁ ∪ s₂) s' μ ↔ CondIndepSets m' hm' s₁ s' μ ∧ 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 : ι), CondIndepSets m' hm' (s n) s' μ) : 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, CondIndepSets m' hm' (s n) s' μ) : 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₁ : CondIndepSets m' hm' s₁ s' μ) : 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 : ι), CondIndepSets m' hm' (s n) s' μ) : 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, CondIndepSets m' hm' (s n) s' μ) : 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 Ω) : 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 Ω) : 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 : CondIndep m' m₁ m₂ hm' μ) : 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 μ] : 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 μ] : 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 : CondIndep m' m₁ m₂ hm' μ) (h31 : m₃ ≤ m₁) : 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 : CondIndep m' m₁ m₂ hm' μ) (h32 : m₃ ≤ m₂) : 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 : iCondIndepSets m' hm' s μ) {i j : ι} (hij : i ≠ j) : 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 : iCondIndep m' hm' m μ) {i j : ι} (hij : i ≠ j) : 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 : iCondIndepFun m' hm' f μ) {i j : ι} (hij : i ≠ j) : 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 : 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 : CondIndep m' (MeasurableSpace.generateFrom s1) (MeasurableSpace.generateFrom s2) hm' μ) : 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 : CondIndepSets m' hm' p1 p2 μ) : 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 : CondIndepSets m' hm' p1 p2 μ) : 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 : iCondIndepSets m' hm' s μ) (hST : Disjoint S T) : 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 : iCondIndepSet m' hm' s μ) (S T : Set ι) (hST : Disjoint S T) : 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 : iCondIndep m' hm' m μ) {S T : Set ι} (hST : Disjoint S T) : 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 : ι), 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) : 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 : iCondIndepSet m' hm' s μ) (i : ι) : 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 μ] [Preorder ι] {s : ι → Set Ω} (hsm : ∀ (n : ι), MeasurableSet (s n)) (hs : iCondIndepSet m' hm' s μ) (i : ι) {k : ι} (hk : i < k) : 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 : iCondIndepSet m' hm' s μ) (n : ℕ) : 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 : ι), CondIndep m' (m i) m₁ hm' μ) (h_le : ∀ (i : ι), m i ≤ mΩ) (h_le' : m₁ ≤ mΩ) (hm : Monotone m) : 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 : ι), CondIndep m' (m i) m₁ hm' μ) (h_le : ∀ (i : ι), m i ≤ mΩ) (h_le' : m₁ ≤ mΩ) (hm : Antitone m) : CondIndep m' (⨆ (i : ι), m i) m₁ hm' μ

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

@[deprecated ProbabilityTheory.iCondIndepSets.piiUnionInter_of_notMem (since := "2025-05-23")]

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 : iCondIndepSets m' hm' π μ) (haS : a ∉ S) : CondIndepSets m' hm' (piiUnionInter π ↑S) (π a) μ

Alias of ProbabilityTheory.iCondIndepSets.piiUnionInter_of_notMem.

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 : 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 : CondIndepSets m' hm' S T μ) : 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 : CondIndep m' m₁ m₂ hm' μ) {s t : Set Ω} (hs : MeasurableSet s) (ht : MeasurableSet t) : 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 μ] : CondIndep m' m₁ m₂ hm' μ ↔ ∀ (s t : Set Ω), MeasurableSet s → MeasurableSet t → 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) : CondIndepFun m' hm' f g μ ↔ ∀ (s : Set β) (t : Set β'), MeasurableSet s → MeasurableSet t → μ[(f ⁻¹' s ∩ g ⁻¹' t).indicator fun (ω : Ω) => 1|m'] =ᵐ[μ] fun (ω : Ω) => μ[(f ⁻¹' s).indicator fun (ω : Ω) => 1|m'] ω * μ[(g ⁻¹' t).indicator fun (ω : Ω) => 1|m'] ω

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)) : iCondIndepFun m' hm' f μ ↔ ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)}, (∀ i ∈ S, MeasurableSet (sets i)) → μ[(⋂ i ∈ S, f i ⁻¹' sets i).indicator fun (ω : Ω) => 1|m'] =ᵐ[μ] ∏ i ∈ S, μ[(f i ⁻¹' sets i).indicator fun (ω : Ω) => 1|m']

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) : CondIndepFun m' hm' f g μ ↔ ∀ (s : Set β) (t : Set β'), MeasurableSet s → MeasurableSet t → CondIndepSet m' hm' (f ⁻¹' s) (g ⁻¹' t) μ

theorem ProbabilityTheory.CondIndepFun.symm {Ω : Type u_1} {β : Type u_3} {β' : Type u_4} {m' mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'} {f : Ω → β} {g : Ω → β'} (hfg : CondIndepFun m' hm' f g μ) : 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 : CondIndepFun m' hm' f g μ) (hφ : Measurable φ) (hψ : Measurable ψ) : CondIndepFun m' hm' (φ ∘ f) (ψ ∘ g) μ

theorem ProbabilityTheory.condIndepFun_const_left {Ω : Type u_1} {β : Type u_3} {β' : Type u_4} {m' mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'} (c : β) (X : Ω → β') : CondIndepFun m' hm' (fun (x : Ω) => c) X μ

theorem ProbabilityTheory.condIndepFun_const_right {Ω : Type u_1} {β : Type u_3} {β' : Type u_4} {m' mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'} (X : Ω → β) (c : β') : CondIndepFun m' hm' X (fun (x : Ω) => c) μ

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 : CondIndepFun m' hm' f g μ) : 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 : CondIndepFun m' hm' f g μ) : CondIndepFun m' hm' (-f) g μ

theorem ProbabilityTheory.condIndepFun_of_measurable_left {Ω : Type u_1} {β : Type u_3} {β' : Type u_4} {m' mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'} {X : Ω → β} {Y : Ω → β'} (hX : Measurable X) (hY : Measurable Y) : CondIndepFun m' hm' X Y μ

theorem ProbabilityTheory.condIndepFun_of_measurable_right {Ω : Type u_1} {β : Type u_3} {β' : Type u_4} {m' mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'} {X : Ω → β} {Y : Ω → β'} (hX : Measurable X) (hY : Measurable Y) : CondIndepFun m' hm' X Y μ

theorem ProbabilityTheory.condIndepFun_self_left {Ω : Type u_1} {β : Type u_3} {β' : Type u_4} {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'} {X : Ω → β} {Z : Ω → β'} (hX : Measurable X) (hZ : Measurable Z) : CondIndepFun (MeasurableSpace.comap Z inferInstance) ⋯ Z X μ

theorem ProbabilityTheory.condIndepFun_self_right {Ω : Type u_1} {β : Type u_3} {β' : Type u_4} {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'} {X : Ω → β} {Z : Ω → β'} (hX : Measurable X) (hZ : Measurable Z) : CondIndepFun (MeasurableSpace.comap Z inferInstance) ⋯ X Z μ

theorem ProbabilityTheory.condIndepFun_iff_compProd_map_prod_eq_compProd_prod_map_map {Ω : 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) : CondIndepFun m' hm' f g μ ↔ (μ.trim hm').compProd ((condExpKernel μ m').map fun (ω : Ω) => (f ω, g ω)) = (μ.trim hm').compProd (((condExpKernel μ m').map f).prod ((condExpKernel μ m').map g))

Two random variables are conditionally independent iff they satisfy the almost sure equality of conditional expectations μ⟦f ⁻¹' s ∩ g ⁻¹' t | m'⟧ =ᵐ[μ] μ⟦f ⁻¹' s | m'⟧ * μ⟦g ⁻¹' t | m'⟧ for all measurable sets s and t (see condIndepFun_iff_condExp_inter_preimage_eq_mul). Here, this is phrased with Markov kernels associated to the conditional expectations, and the almost sure equality is expressed as equality of the composition-product with the measure, which is equivalent to a.e. equality. See condIndepFun_iff_map_prod_eq_prod_map_map for the a.e. equality version with kernels.

For a random variable f, (condExpKernel μ m').map f is the law of the conditional expectation of f given m': almost surely, (condExpKernel μ m').map f ω s = μ⟦f ⁻¹' s | m'⟧ ω.

theorem ProbabilityTheory.condIndepFun_iff_map_prod_eq_prod_map_map {Ω : 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 β'} [MeasurableSpace.CountableOrCountablyGenerated Ω (β × β')] (hf : Measurable f) (hg : Measurable g) : CondIndepFun m' hm' f g μ ↔ ⇑((condExpKernel μ m').map fun (ω : Ω) => (f ω, g ω)) =ᵐ[μ.trim hm'] ⇑(((condExpKernel μ m').map f).prod ((condExpKernel μ m').map g))

Two random variables are conditionally independent iff they satisfy the almost sure equality of conditional expectations μ⟦f ⁻¹' s ∩ g ⁻¹' t | m'⟧ =ᵐ[μ] μ⟦f ⁻¹' s | m'⟧ * μ⟦g ⁻¹' t | m'⟧ for all measurable sets s and t (see condIndepFun_iff_condExp_inter_preimage_eq_mul). Here, this is phrased with Markov kernels associated to the conditional expectations.

For a random variable f, (condExpKernel μ m').map f is the law of the conditional expectation of f given m': almost surely, (condExpKernel μ m').map f ω s = μ⟦f ⁻¹' s | m'⟧ ω.

theorem ProbabilityTheory.condIndepFun_iff_map_prod_eq_prod_comp_trim {Ω : 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) : CondIndepFun m' hm' f g μ ↔ MeasureTheory.Measure.map (fun (ω : Ω) => (ω, f ω, g ω)) μ = (μ.trim hm').bind ⇑(Kernel.id.prod (((condExpKernel μ m').map f).prod ((condExpKernel μ m').map g)))

Two random variables are conditionally independent with respect to m' iff the law of (id, f, g) under μ, in which the identity is to the space with σ-algebra m', can be written as a product involving the conditional expectations of f and g given m'.

For a random variable f, (condExpKernel μ m').map f is the law of the conditional expectation of f given m': almost surely, (condExpKernel μ m').map f ω s = μ⟦f ⁻¹' s | m'⟧ ω.

theorem ProbabilityTheory.condIndepFun_iff_map_prod_eq_prod_condDistrib_prod_condDistrib {Ω : Type u_1} {β : Type u_3} {β' : Type u_4} {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {f : Ω → β} {g : Ω → β'} {γ : Type u_5} {mγ : MeasurableSpace γ} {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'} [StandardBorelSpace β] [Nonempty β] [StandardBorelSpace β'] [Nonempty β'] (hf : Measurable f) (hg : Measurable g) {k : Ω → γ} (hk : Measurable k) : CondIndepFun (MeasurableSpace.comap k inferInstance) ⋯ f g μ ↔ MeasureTheory.Measure.map (fun (ω : Ω) => (k ω, f ω, g ω)) μ = (MeasureTheory.Measure.map k μ).bind ⇑(Kernel.id.prod ((condDistrib f k μ).prod (condDistrib g k μ)))

Two random variables f, g are conditionally independent given a third k iff the joint distribution of k, f, g factors into a product of their conditional distributions given k.

theorem ProbabilityTheory.condIndepFun_iff_condDistrib_prod_ae_eq_prodMkRight {Ω : Type u_1} {β : Type u_3} {β' : Type u_4} {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {f : Ω → β} {g : Ω → β'} {γ : Type u_5} {mγ : MeasurableSpace γ} {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'} [StandardBorelSpace β] [Nonempty β] [StandardBorelSpace β'] [Nonempty β'] (hf : Measurable f) (hg : Measurable g) {k : Ω → γ} (hk : Measurable k) : CondIndepFun (MeasurableSpace.comap k inferInstance) ⋯ g f μ ↔ ⇑(condDistrib f (fun (ω : Ω) => (k ω, g ω)) μ) =ᵐ[MeasureTheory.Measure.map (fun (ω : Ω) => (k ω, g ω)) μ] ⇑(Kernel.prodMkRight β' (condDistrib f k μ))

Two random variables f, g are conditionally independent given a third k iff the conditional distribution of f given k and g is equal to the conditional distribution of f given k.

@[deprecated ProbabilityTheory.condIndepFun_iff_condDistrib_prod_ae_eq_prodMkRight (since := "2025-10-14")]

theorem ProbabilityTheory.condIndepFun_iff_condDistrib_prod_ae_eq_prodMkLeft {Ω : Type u_1} {β : Type u_3} {β' : Type u_4} {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {f : Ω → β} {g : Ω → β'} {γ : Type u_5} {mγ : MeasurableSpace γ} {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'} [StandardBorelSpace β] [Nonempty β] [StandardBorelSpace β'] [Nonempty β'] (hf : Measurable f) (hg : Measurable g) {k : Ω → γ} (hk : Measurable k) : CondIndepFun (MeasurableSpace.comap k inferInstance) ⋯ g f μ ↔ ⇑(condDistrib f (fun (ω : Ω) => (k ω, g ω)) μ) =ᵐ[MeasureTheory.Measure.map (fun (ω : Ω) => (k ω, g ω)) μ] ⇑(Kernel.prodMkRight β' (condDistrib f k μ))

Alias of ProbabilityTheory.condIndepFun_iff_condDistrib_prod_ae_eq_prodMkRight.

---

Two random variables f, g are conditionally independent given a third k iff the conditional distribution of f given k and g is equal to the conditional distribution of f given k.

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 ι] : iCondIndepFun m' hm' 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 : iCondIndepFun m' hm' f μ) (hf_meas : ∀ (i : ι), Measurable (f i)) : CondIndepFun m' hm' (fun (a : Ω) (i : ↥S) => f (↑i) a) (fun (a : Ω) (i : ↥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_prodMk {Ω : 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 : iCondIndepFun m' hm' f μ) (hf_meas : ∀ (i : ι), Measurable (f i)) (i j k : ι) (hik : i ≠ k) (hjk : j ≠ k) : CondIndepFun m' hm' (fun (a : Ω) => (f i a, f j a)) (f k) μ

@[deprecated ProbabilityTheory.iCondIndepFun.condIndepFun_prodMk (since := "2025-03-05")]

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 : iCondIndepFun m' hm' f μ) (hf_meas : ∀ (i : ι), Measurable (f i)) (i j k : ι) (hik : i ≠ k) (hjk : j ≠ k) : CondIndepFun m' hm' (fun (a : Ω) => (f i a, f j a)) (f k) μ

Alias of ProbabilityTheory.iCondIndepFun.condIndepFun_prodMk.

theorem ProbabilityTheory.iCondIndepFun.condIndepFun_prodMk_prodMk {Ω : 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 : iCondIndepFun m' hm' f μ) (hf : ∀ (i : ι), Measurable (f i)) (i j k l : ι) (hik : i ≠ k) (hil : i ≠ l) (hjk : j ≠ k) (hjl : j ≠ l) : CondIndepFun m' hm' (fun (a : Ω) => (f i a, f j a)) (fun (a : Ω) => (f k a, f l a)) μ

@[deprecated ProbabilityTheory.iCondIndepFun.condIndepFun_prodMk_prodMk (since := "2025-03-05")]

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 : iCondIndepFun m' hm' f μ) (hf : ∀ (i : ι), Measurable (f i)) (i j k l : ι) (hik : i ≠ k) (hil : i ≠ l) (hjk : j ≠ k) (hjl : j ≠ l) : CondIndepFun m' hm' (fun (a : Ω) => (f i a, f j a)) (fun (a : Ω) => (f k a, f l a)) μ

Alias of ProbabilityTheory.iCondIndepFun.condIndepFun_prodMk_prodMk.

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 : iCondIndepFun m' hm' f μ) (hf_meas : ∀ (i : ι), Measurable (f i)) (i j k : ι) (hik : i ≠ k) (hjk : j ≠ k) : 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 : iCondIndepFun m' hm' f μ) (hf_meas : ∀ (i : ι), Measurable (f i)) (i j k : ι) (hik : i ≠ k) (hjk : j ≠ k) : 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 : iCondIndepFun m' hm' f μ) (hf_meas : ∀ (i : ι), Measurable (f i)) (i j k : ι) (hij : i ≠ j) (hik : i ≠ k) : 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 : iCondIndepFun m' hm' f μ) (hf_meas : ∀ (i : ι), Measurable (f i)) (i j k : ι) (hij : i ≠ j) (hik : i ≠ k) : 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 : iCondIndepFun m' hm' f μ) (hf_meas : ∀ (i : ι), Measurable (f i)) (i j k l : ι) (hik : i ≠ k) (hil : i ≠ l) (hjk : j ≠ k) (hjl : j ≠ l) : 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 : iCondIndepFun m' hm' f μ) (hf_meas : ∀ (i : ι), Measurable (f i)) (i j k l : ι) (hik : i ≠ k) (hil : i ≠ l) (hjk : j ≠ k) (hjl : j ≠ l) : 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 : iCondIndepFun m' hm' f μ) (hf_meas : ∀ (i : ι), Measurable (f i)) (i j k : ι) (hik : i ≠ k) (hjk : j ≠ k) : 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 : iCondIndepFun m' hm' f μ) (hf_meas : ∀ (i : ι), Measurable (f i)) (i j k : ι) (hik : i ≠ k) (hjk : j ≠ k) : 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 : iCondIndepFun m' hm' f μ) (hf_meas : ∀ (i : ι), Measurable (f i)) (i j k : ι) (hij : i ≠ j) (hik : i ≠ k) : 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 : iCondIndepFun m' hm' f μ) (hf_meas : ∀ (i : ι), Measurable (f i)) (i j k : ι) (hij : i ≠ j) (hik : i ≠ k) : 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 : iCondIndepFun m' hm' f μ) (hf_meas : ∀ (i : ι), Measurable (f i)) (i j k l : ι) (hik : i ≠ k) (hil : i ≠ l) (hjk : j ≠ k) (hjl : j ≠ l) : 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 : iCondIndepFun m' hm' f μ) (hf_meas : ∀ (i : ι), Measurable (f i)) (i j k l : ι) (hik : i ≠ k) (hil : i ≠ l) (hjk : j ≠ k) (hjl : j ≠ l) : CondIndepFun m' hm' (f i - f j) (f k - f l) μ

theorem ProbabilityTheory.iCondIndepFun.condIndepFun_finset_prod_of_notMem {Ω : 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 : iCondIndepFun m' hm' f μ) (hf_meas : ∀ (i : ι), Measurable (f i)) {s : Finset ι} {i : ι} (hi : i ∉ s) : CondIndepFun m' hm' (∏ j ∈ s, f j) (f i) μ

theorem ProbabilityTheory.iCondIndepFun.condIndepFun_finset_sum_of_notMem {Ω : 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 : iCondIndepFun m' hm' f μ) (hf_meas : ∀ (i : ι), Measurable (f i)) {s : Finset ι} {i : ι} (hi : i ∉ s) : CondIndepFun m' hm' (∑ j ∈ s, f j) (f i) μ

@[deprecated ProbabilityTheory.iCondIndepFun.condIndepFun_finset_sum_of_notMem (since := "2025-05-24")]

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 : iCondIndepFun m' hm' f μ) (hf_meas : ∀ (i : ι), Measurable (f i)) {s : Finset ι} {i : ι} (hi : i ∉ s) : CondIndepFun m' hm' (∑ j ∈ s, f j) (f i) μ

Alias of ProbabilityTheory.iCondIndepFun.condIndepFun_finset_sum_of_notMem.

@[deprecated ProbabilityTheory.iCondIndepFun.condIndepFun_finset_prod_of_notMem (since := "2025-05-24")]

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 : iCondIndepFun m' hm' f μ) (hf_meas : ∀ (i : ι), Measurable (f i)) {s : Finset ι} {i : ι} (hi : i ∉ s) : CondIndepFun m' hm' (∏ j ∈ s, f j) (f i) μ

Alias of ProbabilityTheory.iCondIndepFun.condIndepFun_finset_prod_of_notMem.

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 : iCondIndepFun m' hm' f μ) (hf_meas : ∀ (i : ℕ), Measurable (f i)) (n : ℕ) : 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 : iCondIndepFun m' hm' f μ) (hf_meas : ∀ (i : ℕ), Measurable (f i)) (n : ℕ) : 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 : iCondIndepSet m' hm' s μ) : iCondIndepFun m' hm' (fun (n : ι) => (s n).indicator fun (_ω : Ω) => 1) μ