# Independence with respect to a kernel and a measure #

A family of sets of sets π : ι → Set (Set Ω) is independent with respect to a kernel κ : kernel α Ω and a measure μ on α 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 for μ-almost every a : α, κ a (⋂ i in s, f i) = ∏ i ∈ s, κ a (f i).

This notion of independence is a generalization of both independence and conditional independence. For conditional independence, κ is the conditional kernel ProbabilityTheory.condexpKernel and μ is the ambiant measure. For (non-conditional) independence, κ = kernel.const Unit μ and the measure is the Dirac measure on Unit.

The main purpose of this file is to prove only once the properties that hold for both conditional and non-conditional independence.

## Main definitions #

• ProbabilityTheory.kernel.iIndepSets: independence of a family of sets of sets. Variant for two sets of sets: ProbabilityTheory.kernel.IndepSets.
• ProbabilityTheory.kernel.iIndep: independence of a family of σ-algebras. Variant for two σ-algebras: Indep.
• ProbabilityTheory.kernel.iIndepSet: independence of a family of sets. Variant for two sets: ProbabilityTheory.kernel.IndepSet.
• ProbabilityTheory.kernel.iIndepFun: independence of a family of functions (random variables). Variant for two functions: ProbabilityTheory.kernel.IndepFun.

See the file Mathlib/Probability/Kernel/Basic.lean for a more detailed discussion of these definitions in the particular case of the usual independence notion.

## Main statements #

• ProbabilityTheory.kernel.iIndepSets.iIndep: if π-systems are independent as sets of sets, then the measurable space structures they generate are independent.
• ProbabilityTheory.kernel.IndepSets.Indep: variant with two π-systems.
def ProbabilityTheory.kernel.iIndepSets {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : } {_mΩ : } (π : ιSet (Set Ω)) (κ : ()) (μ : ) :

A family of sets of sets π : ι → Set (Set Ω) is independent with respect to a kernel κ and 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 ∀ᵐ a ∂μ, κ a (⋂ i in s, f i) = ∏ i ∈ s, κ a (f i). It will be used for families of pi_systems.

Equations
• = ∀ (s : ) {f : ιSet Ω}, (is, f i π i)∀ᵐ (a : α) ∂μ, (κ a) (is, f i) = is, (κ a) (f i)
Instances For
def ProbabilityTheory.kernel.IndepSets {α : Type u_1} {Ω : Type u_2} {_mα : } {_mΩ : } (s1 : Set (Set Ω)) (s2 : Set (Set Ω)) (κ : ()) (μ : ) :

Two sets of sets s₁, s₂ are independent with respect to a kernel κ and a measure μ if for any sets t₁ ∈ s₁, t₂ ∈ s₂, then ∀ᵐ a ∂μ, κ a (t₁ ∩ t₂) = κ a (t₁) * κ a (t₂)

Equations
• = ∀ (t1 t2 : Set Ω), t1 s1t2 s2∀ᵐ (a : α) ∂μ, (κ a) (t1 t2) = (κ a) t1 * (κ a) t2
Instances For
def ProbabilityTheory.kernel.iIndep {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : } (m : ι) {_mΩ : } (κ : ()) (μ : ) :

A family of measurable space structures (i.e. of σ-algebras) is independent with respect to a kernel κ and a measure μ if the family of sets of measurable sets they define is independent.

Equations
Instances For
def ProbabilityTheory.kernel.Indep {α : Type u_1} {Ω : Type u_2} {_mα : } (m₁ : ) (m₂ : ) {_mΩ : } (κ : ()) (μ : ) :

Two measurable space structures (or σ-algebras) m₁, m₂ are independent with respect to a kernel κ and a measure μ if for any sets t₁ ∈ m₁, t₂ ∈ m₂, ∀ᵐ a ∂μ, κ a (t₁ ∩ t₂) = κ a (t₁) * κ a (t₂)

Equations
Instances For
def ProbabilityTheory.kernel.iIndepSet {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : } {_mΩ : } (s : ιSet Ω) (κ : ()) (μ : ) :

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

Equations
Instances For
def ProbabilityTheory.kernel.IndepSet {α : Type u_1} {Ω : Type u_2} {_mα : } {_mΩ : } (s : Set Ω) (t : Set Ω) (κ : ()) (μ : ) :

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

Equations
Instances For
def ProbabilityTheory.kernel.iIndepFun {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : } {_mΩ : } {β : ιType u_4} (m : (x : ι) → MeasurableSpace (β x)) (f : (x : ι) → Ωβ x) (κ : ()) (μ : ) :

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

Equations
Instances For
def ProbabilityTheory.kernel.IndepFun {α : Type u_1} {Ω : Type u_2} {_mα : } {β : Type u_4} {γ : Type u_5} {_mΩ : } [mβ : ] [mγ : ] (f : Ωβ) (g : Ωγ) (κ : ()) (μ : ) :

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

Equations
Instances For
theorem ProbabilityTheory.kernel.iIndepSets.meas_biInter {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : } {_mΩ : } {κ : ()} {μ : } {π : ιSet (Set Ω)} (h : ) (s : ) {f : ιSet Ω} (hf : is, f i π i) :
∀ᵐ (a : α) ∂μ, (κ a) (is, f i) = is, (κ a) (f i)
theorem ProbabilityTheory.kernel.iIndepSets.meas_iInter {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : } {_mΩ : } {κ : ()} {μ : } {π : ιSet (Set Ω)} {s : ιSet Ω} [] (h : ) (hs : ∀ (i : ι), s i π i) :
∀ᵐ (a : α) ∂μ, (κ a) (⋂ (i : ι), s i) = i : ι, (κ a) (s i)
theorem ProbabilityTheory.kernel.iIndep.iIndepSets' {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : } {m : ι} {_mΩ : } {κ : ()} {μ : } (hμ : ) :
ProbabilityTheory.kernel.iIndepSets (fun (x : ι) => {s : Set Ω | }) κ μ
theorem ProbabilityTheory.kernel.iIndep.meas_biInter {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : } {m : ι} {_mΩ : } {κ : ()} {μ : } {s : ιSet Ω} {S : } (hμ : ) (hs : iS, MeasurableSet (s i)) :
∀ᵐ (a : α) ∂μ, (κ a) (iS, s i) = iS, (κ a) (s i)
theorem ProbabilityTheory.kernel.iIndep.meas_iInter {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : } {m : ι} {_mΩ : } {κ : ()} {μ : } {s : ιSet Ω} [] (h : ) (hs : ∀ (i : ι), MeasurableSet (s i)) :
∀ᵐ (a : α) ∂μ, (κ a) (⋂ (i : ι), s i) = i : ι, (κ a) (s i)
theorem ProbabilityTheory.kernel.iIndepFun.iIndep {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {β : ιType u_4} {mβ : (i : ι) → MeasurableSpace (β i)} {_mα : } {_mΩ : } {κ : ()} {μ : } {f : (x : ι) → Ωβ x} (hf : ) :
ProbabilityTheory.kernel.iIndep (fun (x : ι) => MeasurableSpace.comap (f x) ( x)) κ μ
theorem ProbabilityTheory.kernel.iIndepFun.meas_biInter {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {β : ιType u_4} {mβ : (i : ι) → MeasurableSpace (β i)} {_mα : } {_mΩ : } {κ : ()} {μ : } {s : ιSet Ω} {S : } {f : (x : ι) → Ωβ x} (hf : ) (hs : iS, MeasurableSet (s i)) :
∀ᵐ (a : α) ∂μ, (κ a) (iS, s i) = iS, (κ a) (s i)
theorem ProbabilityTheory.kernel.iIndepFun.meas_iInter {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {β : ιType u_4} {mβ : (i : ι) → MeasurableSpace (β i)} {_mα : } {_mΩ : } {κ : ()} {μ : } {s : ιSet Ω} {f : (x : ι) → Ωβ x} [] (hf : ) (hs : ∀ (i : ι), MeasurableSet (s i)) :
∀ᵐ (a : α) ∂μ, (κ a) (⋂ (i : ι), s i) = i : ι, (κ a) (s i)
theorem ProbabilityTheory.kernel.IndepFun.meas_inter {α : Type u_1} {Ω : Type u_2} {_mα : } {_mΩ : } {κ : ()} {μ : } {β : Type u_5} {γ : Type u_6} [mβ : ] [mγ : ] {f : Ωβ} {g : Ωγ} (hfg : ) {s : Set Ω} {t : Set Ω} (hs : ) (ht : ) :
∀ᵐ (a : α) ∂μ, (κ a) (s t) = (κ a) s * (κ a) t
theorem ProbabilityTheory.kernel.IndepSets.symm {α : Type u_1} {Ω : Type u_2} {_mα : } {_mΩ : } {κ : ()} {μ : } {s₁ : Set (Set Ω)} {s₂ : Set (Set Ω)} (h : ) :
theorem ProbabilityTheory.kernel.Indep.symm {α : Type u_1} {Ω : Type u_2} {_mα : } {m₁ : } {m₂ : } {_mΩ : } {κ : ()} {μ : } (h : ) :
theorem ProbabilityTheory.kernel.indep_bot_right {α : Type u_1} {Ω : Type u_2} {_mα : } (m' : ) {_mΩ : } {κ : ()} {μ : } :
theorem ProbabilityTheory.kernel.indep_bot_left {α : Type u_1} {Ω : Type u_2} {_mα : } (m' : ) {_mΩ : } {κ : ()} {μ : } :
theorem ProbabilityTheory.kernel.indepSet_empty_right {α : Type u_1} {Ω : Type u_2} {_mα : } {_mΩ : } {κ : ()} {μ : } (s : Set Ω) :
theorem ProbabilityTheory.kernel.indepSet_empty_left {α : Type u_1} {Ω : Type u_2} {_mα : } {_mΩ : } {κ : ()} {μ : } (s : Set Ω) :
theorem ProbabilityTheory.kernel.indepSets_of_indepSets_of_le_left {α : Type u_1} {Ω : Type u_2} {_mα : } {s₁ : Set (Set Ω)} {s₂ : Set (Set Ω)} {s₃ : Set (Set Ω)} {_mΩ : } {κ : ()} {μ : } (h_indep : ) (h31 : s₃ s₁) :
theorem ProbabilityTheory.kernel.indepSets_of_indepSets_of_le_right {α : Type u_1} {Ω : Type u_2} {_mα : } {s₁ : Set (Set Ω)} {s₂ : Set (Set Ω)} {s₃ : Set (Set Ω)} {_mΩ : } {κ : ()} {μ : } (h_indep : ) (h32 : s₃ s₂) :
theorem ProbabilityTheory.kernel.indep_of_indep_of_le_left {α : Type u_1} {Ω : Type u_2} {_mα : } {m₁ : } {m₂ : } {m₃ : } {_mΩ : } {κ : ()} {μ : } (h_indep : ) (h31 : m₃ m₁) :
theorem ProbabilityTheory.kernel.indep_of_indep_of_le_right {α : Type u_1} {Ω : Type u_2} {_mα : } {m₁ : } {m₂ : } {m₃ : } {_mΩ : } {κ : ()} {μ : } (h_indep : ) (h32 : m₃ m₂) :
theorem ProbabilityTheory.kernel.IndepSets.union {α : Type u_1} {Ω : Type u_2} {_mα : } {s₁ : Set (Set Ω)} {s₂ : Set (Set Ω)} {s' : Set (Set Ω)} {_mΩ : } {κ : ()} {μ : } (h₁ : ) (h₂ : ) :
@[simp]
theorem ProbabilityTheory.kernel.IndepSets.union_iff {α : Type u_1} {Ω : Type u_2} {_mα : } {s₁ : Set (Set Ω)} {s₂ : Set (Set Ω)} {s' : Set (Set Ω)} {_mΩ : } {κ : ()} {μ : } :
theorem ProbabilityTheory.kernel.IndepSets.iUnion {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : } {s : ιSet (Set Ω)} {s' : Set (Set Ω)} {_mΩ : } {κ : ()} {μ : } (hyp : ∀ (n : ι), ProbabilityTheory.kernel.IndepSets (s n) s' κ μ) :
ProbabilityTheory.kernel.IndepSets (⋃ (n : ι), s n) s' κ μ
theorem ProbabilityTheory.kernel.IndepSets.bUnion {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : } {s : ιSet (Set Ω)} {s' : Set (Set Ω)} {_mΩ : } {κ : ()} {μ : } {u : Set ι} (hyp : nu, ProbabilityTheory.kernel.IndepSets (s n) s' κ μ) :
ProbabilityTheory.kernel.IndepSets (nu, s n) s' κ μ
theorem ProbabilityTheory.kernel.IndepSets.inter {α : Type u_1} {Ω : Type u_2} {_mα : } {s₁ : Set (Set Ω)} {s' : Set (Set Ω)} (s₂ : Set (Set Ω)) {_mΩ : } {κ : ()} {μ : } (h₁ : ) :
theorem ProbabilityTheory.kernel.IndepSets.iInter {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : } {s : ιSet (Set Ω)} {s' : Set (Set Ω)} {_mΩ : } {κ : ()} {μ : } (h : ∃ (n : ι), ProbabilityTheory.kernel.IndepSets (s n) s' κ μ) :
ProbabilityTheory.kernel.IndepSets (⋂ (n : ι), s n) s' κ μ
theorem ProbabilityTheory.kernel.IndepSets.bInter {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : } {s : ιSet (Set Ω)} {s' : Set (Set Ω)} {_mΩ : } {κ : ()} {μ : } {u : Set ι} (h : nu, ProbabilityTheory.kernel.IndepSets (s n) s' κ μ) :
ProbabilityTheory.kernel.IndepSets (nu, s n) s' κ μ
theorem ProbabilityTheory.kernel.iIndep_comap_mem_iff {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : } {f : ιSet Ω} {_mΩ : } {κ : ()} {μ : } :
ProbabilityTheory.kernel.iIndep (fun (i : ι) => MeasurableSpace.comap (fun (x : Ω) => x f i) ) κ μ
theorem ProbabilityTheory.kernel.iIndepSets_singleton_iff {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : } {s : ιSet Ω} {_mΩ : } {κ : ()} {μ : } :
ProbabilityTheory.kernel.iIndepSets (fun (i : ι) => {s i}) κ μ ∀ (S : ), ∀ᵐ (a : α) ∂μ, (κ a) (iS, s i) = iS, (κ a) (s i)
theorem ProbabilityTheory.kernel.indepSets_singleton_iff {α : Type u_1} {Ω : Type u_2} {_mα : } {s : Set Ω} {t : Set Ω} {_mΩ : } {κ : ()} {μ : } :
∀ᵐ (a : α) ∂μ, (κ a) (s t) = (κ a) s * (κ a) t

### Deducing Indep from iIndep#

theorem ProbabilityTheory.kernel.iIndepSets.indepSets {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : } {s : ιSet (Set Ω)} {_mΩ : } {κ : ()} {μ : } (h_indep : ) {i : ι} {j : ι} (hij : i j) :
theorem ProbabilityTheory.kernel.iIndep.indep {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : } {m : ι} {_mΩ : } {κ : ()} {μ : } (h_indep : ) {i : ι} {j : ι} (hij : i j) :
theorem ProbabilityTheory.kernel.iIndepFun.indepFun {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : } {_mΩ : } {κ : ()} {μ : } {β : ιType u_4} {m : (x : ι) → MeasurableSpace (β x)} {f : (i : ι) → Ωβ i} (hf_Indep : ) {i : ι} {j : ι} (hij : i j) :

## π-system lemma #

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

### Independence of measurable space structures implies independence of generating π-systems #

theorem ProbabilityTheory.kernel.iIndep.iIndepSets {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : } {_mΩ : } {κ : ()} {μ : } {m : ι} {s : ιSet (Set Ω)} (hms : ∀ (n : ι), m n = ) (h_indep : ) :
theorem ProbabilityTheory.kernel.Indep.indepSets {α : Type u_1} {Ω : Type u_2} {_mα : } {_mΩ : } {κ : ()} {μ : } {s1 : Set (Set Ω)} {s2 : Set (Set Ω)} (h_indep : ) :

### Independence of generating π-systems implies independence of measurable space structures #

theorem ProbabilityTheory.kernel.IndepSets.indep_aux {α : Type u_1} {Ω : Type u_2} {_mα : } {m₂ : } {m : } {κ : ()} {μ : } {p1 : Set (Set Ω)} {p2 : Set (Set Ω)} (h2 : m₂ m) (hp2 : ) (hpm2 : ) (hyp : ) {t1 : Set Ω} {t2 : Set Ω} (ht1 : t1 p1) (ht1m : ) (ht2m : ) :
∀ᵐ (a : α) ∂μ, (κ a) (t1 t2) = (κ a) t1 * (κ a) t2
theorem ProbabilityTheory.kernel.IndepSets.indep {α : Type u_1} {Ω : Type u_2} {_mα : } {m1 : } {m2 : } {m : } {κ : ()} {μ : } {p1 : Set (Set Ω)} {p2 : Set (Set Ω)} (h1 : m1 m) (h2 : m2 m) (hp1 : ) (hp2 : ) (hpm1 : ) (hpm2 : ) (hyp : ) :

The measurable space structures generated by independent pi-systems are independent.

theorem ProbabilityTheory.kernel.IndepSets.indep' {α : Type u_1} {Ω : Type u_2} {_mα : } {_mΩ : } {κ : ()} {μ : } {p1 : Set (Set Ω)} {p2 : Set (Set Ω)} (hp1m : sp1, ) (hp2m : sp2, ) (hp1 : ) (hp2 : ) (hyp : ) :
theorem ProbabilityTheory.kernel.indepSets_piiUnionInter_of_disjoint {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : } {_mΩ : } {κ : ()} {μ : } {s : ιSet (Set Ω)} {S : Set ι} {T : Set ι} (h_indep : ) (hST : Disjoint S T) :
theorem ProbabilityTheory.kernel.iIndepSet.indep_generateFrom_of_disjoint {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : } {_mΩ : } {κ : ()} {μ : } {s : ιSet Ω} (hsm : ∀ (n : ι), MeasurableSet (s n)) (hs : ) (S : Set ι) (T : Set ι) (hST : Disjoint S T) :
ProbabilityTheory.kernel.Indep (MeasurableSpace.generateFrom {t : Set Ω | nS, s n = t}) (MeasurableSpace.generateFrom {t : Set Ω | kT, s k = t}) κ μ
theorem ProbabilityTheory.kernel.indep_iSup_of_disjoint {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : } {_mΩ : } {κ : ()} {μ : } {m : ι} (h_le : ∀ (i : ι), m i _mΩ) (h_indep : ) {S : Set ι} {T : Set ι} (hST : Disjoint S T) :
ProbabilityTheory.kernel.Indep (iS, m i) (iT, m i) κ μ
theorem ProbabilityTheory.kernel.indep_iSup_of_directed_le {α : Type u_1} {ι : Type u_3} {_mα : } {Ω : Type u_4} {m : ι} {m' : } {m0 : } {κ : ()} {μ : } (h_indep : ∀ (i : ι), ProbabilityTheory.kernel.Indep (m i) m' κ μ) (h_le : ∀ (i : ι), m i m0) (h_le' : m' m0) (hm : Directed (fun (x x_1 : ) => x x_1) m) :
ProbabilityTheory.kernel.Indep (⨆ (i : ι), m i) m' κ μ
theorem ProbabilityTheory.kernel.iIndepSet.indep_generateFrom_lt {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : } {_mΩ : } {κ : ()} {μ : } [] {s : ιSet Ω} (hsm : ∀ (n : ι), MeasurableSet (s n)) (hs : ) (i : ι) :
ProbabilityTheory.kernel.Indep () (MeasurableSpace.generateFrom {t : Set Ω | j < i, s j = t}) κ μ
theorem ProbabilityTheory.kernel.iIndepSet.indep_generateFrom_le {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : } {_mΩ : } {κ : ()} {μ : } [] {s : ιSet Ω} (hsm : ∀ (n : ι), MeasurableSet (s n)) (hs : ) (i : ι) {k : ι} (hk : i < k) :
ProbabilityTheory.kernel.Indep () (MeasurableSpace.generateFrom {t : Set Ω | ji, s j = t}) κ μ
theorem ProbabilityTheory.kernel.iIndepSet.indep_generateFrom_le_nat {α : Type u_1} {Ω : Type u_2} {_mα : } {_mΩ : } {κ : ()} {μ : } {s : Set Ω} (hsm : ∀ (n : ), MeasurableSet (s n)) (hs : ) (n : ) :
theorem ProbabilityTheory.kernel.indep_iSup_of_monotone {α : Type u_1} {ι : Type u_3} {_mα : } [] {Ω : Type u_4} {m : ι} {m' : } {m0 : } {κ : ()} {μ : } (h_indep : ∀ (i : ι), ProbabilityTheory.kernel.Indep (m i) m' κ μ) (h_le : ∀ (i : ι), m i m0) (h_le' : m' m0) (hm : ) :
ProbabilityTheory.kernel.Indep (⨆ (i : ι), m i) m' κ μ
theorem ProbabilityTheory.kernel.indep_iSup_of_antitone {α : Type u_1} {ι : Type u_3} {_mα : } [] {Ω : Type u_4} {m : ι} {m' : } {m0 : } {κ : ()} {μ : } (h_indep : ∀ (i : ι), ProbabilityTheory.kernel.Indep (m i) m' κ μ) (h_le : ∀ (i : ι), m i m0) (h_le' : m' m0) (hm : ) :
ProbabilityTheory.kernel.Indep (⨆ (i : ι), m i) m' κ μ
theorem ProbabilityTheory.kernel.iIndepSets.piiUnionInter_of_not_mem {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : } {_mΩ : } {κ : ()} {μ : } {π : ιSet (Set Ω)} {a : ι} {S : } (hp_ind : ) (haS : aS) :
theorem ProbabilityTheory.kernel.iIndepSets.iIndep {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : } {_mΩ : } {κ : ()} {μ : } (m : ι) (h_le : ∀ (i : ι), m i _mΩ) (π : ιSet (Set Ω)) (h_pi : ∀ (n : ι), IsPiSystem (π n)) (h_generate : ∀ (i : ι), m i = ) (h_ind : ) :

The measurable space structures generated by independent pi-systems are independent.

### Independence of measurable sets #

We prove the following equivalences on IndepSet, for measurable sets s, t.

• IndepSet s t κ μ ↔ ∀ᵐ a ∂μ, κ a (s ∩ t) = κ a s * κ a t,
• IndepSet s t κ μ ↔ IndepSets {s} {t} κ μ.
theorem ProbabilityTheory.kernel.iIndepSet_iff_iIndepSets_singleton {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : } {_mΩ : } {κ : ()} {μ : } {f : ιSet Ω} (hf : ∀ (i : ι), MeasurableSet (f i)) :
ProbabilityTheory.kernel.iIndepSets (fun (i : ι) => {f i}) κ μ
theorem ProbabilityTheory.kernel.iIndepSet_iff_meas_biInter {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : } {_mΩ : } {κ : ()} {μ : } {f : ιSet Ω} (hf : ∀ (i : ι), MeasurableSet (f i)) :
∀ (s : ), ∀ᵐ (a : α) ∂μ, (κ a) (is, f i) = is, (κ a) (f i)
theorem ProbabilityTheory.kernel.iIndepSets.iIndepSet_of_mem {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : } {_mΩ : } {κ : ()} {μ : } {π : ιSet (Set Ω)} {f : ιSet Ω} (hfπ : ∀ (i : ι), f i π i) (hf : ∀ (i : ι), MeasurableSet (f i)) (hπ : ) :
theorem ProbabilityTheory.kernel.indepSet_iff_indepSets_singleton {α : Type u_1} {Ω : Type u_2} {_mα : } {s : Set Ω} {t : Set Ω} {m0 : } (hs_meas : ) (ht_meas : ) (κ : ()) (μ : ) :
theorem ProbabilityTheory.kernel.indepSet_iff_measure_inter_eq_mul {α : Type u_1} {Ω : Type u_2} {_mα : } {s : Set Ω} {t : Set Ω} {_m0 : } (hs_meas : ) (ht_meas : ) (κ : ()) (μ : ) :
∀ᵐ (a : α) ∂μ, (κ a) (s t) = (κ a) s * (κ a) t
theorem ProbabilityTheory.kernel.IndepSets.indepSet_of_mem {α : Type u_1} {Ω : Type u_2} {_mα : } {s : Set Ω} {t : Set Ω} (S : Set (Set Ω)) (T : Set (Set Ω)) {_m0 : } (hs : s S) (ht : t T) (hs_meas : ) (ht_meas : ) (κ : ()) (μ : ) (h_indep : ) :
theorem ProbabilityTheory.kernel.Indep.indepSet_of_measurableSet {α : Type u_1} {Ω : Type u_2} {_mα : } {m₁ : } {m₂ : } {m0 : } {κ : ()} {μ : } (h_indep : ) {s : Set Ω} {t : Set Ω} (hs : ) (ht : ) :
theorem ProbabilityTheory.kernel.indep_iff_forall_indepSet {α : Type u_1} {Ω : Type u_2} {_mα : } (m₁ : ) (m₂ : ) {_m0 : } (κ : ()) (μ : ) :
∀ (s t : Set Ω),

### Independence of random variables #

theorem ProbabilityTheory.kernel.indepFun_iff_measure_inter_preimage_eq_mul {α : Type u_1} {Ω : Type u_2} {β : Type u_4} {β' : Type u_5} {_mα : } {_mΩ : } {κ : ()} {μ : } {f : Ωβ} {g : Ωβ'} {mβ : } {mβ' : } :
∀ (s : Set β) (t : Set β'), ∀ᵐ (a : α) ∂μ, (κ a) (f ⁻¹' s g ⁻¹' t) = (κ a) (f ⁻¹' s) * (κ a) (g ⁻¹' t)
theorem ProbabilityTheory.kernel.iIndepFun_iff_measure_inter_preimage_eq_mul {α : Type u_1} {Ω : Type u_2} {_mα : } {_mΩ : } {κ : ()} {μ : } {ι : Type u_8} {β : ιType u_9} (m : (x : ι) → MeasurableSpace (β x)) (f : (i : ι) → Ωβ i) :
∀ (S : ) {sets : (i : ι) → Set (β i)}, (iS, MeasurableSet (sets i))∀ᵐ (a : α) ∂μ, (κ a) (iS, f i ⁻¹' sets i) = iS, (κ a) (f i ⁻¹' sets i)
theorem ProbabilityTheory.kernel.indepFun_iff_indepSet_preimage {α : Type u_1} {Ω : Type u_2} {β : Type u_4} {β' : Type u_5} {_mα : } {_mΩ : } {κ : ()} {μ : } {f : Ωβ} {g : Ωβ'} {mβ : } {mβ' : } (hf : ) (hg : ) :
∀ (s : Set β) (t : Set β'), ProbabilityTheory.kernel.IndepSet (f ⁻¹' s) (g ⁻¹' t) κ μ
theorem ProbabilityTheory.kernel.IndepFun.symm {α : Type u_1} {Ω : Type u_2} {β : Type u_4} {β' : Type u_5} {_mα : } {_mΩ : } {κ : ()} {μ : } {f : Ωβ} {g : Ωβ'} :
∀ {x : } {x_1 : },
theorem ProbabilityTheory.kernel.IndepFun.ae_eq {α : Type u_1} {Ω : Type u_2} {β : Type u_4} {β' : Type u_5} {_mα : } {_mΩ : } {κ : ()} {μ : } {f : Ωβ} {g : Ωβ'} {mβ : } {mβ' : } {f' : Ωβ} {g' : Ωβ'} (hfg : ) (hf : ∀ᵐ (a : α) ∂μ, f =ᵐ[κ a] f') (hg : ∀ᵐ (a : α) ∂μ, g =ᵐ[κ a] g') :
theorem ProbabilityTheory.kernel.IndepFun.comp {α : Type u_1} {Ω : Type u_2} {β : Type u_4} {β' : Type u_5} {γ : Type u_6} {γ' : Type u_7} {_mα : } {_mΩ : } {κ : ()} {μ : } {f : Ωβ} {g : Ωβ'} {mβ : } {mβ' : } {mγ : } {mγ' : } {φ : βγ} {ψ : β'γ'} (hfg : ) (hφ : ) (hψ : ) :
theorem ProbabilityTheory.kernel.IndepFun.neg_right {α : Type u_1} {Ω : Type u_2} {β : Type u_4} {β' : Type u_5} {_mα : } {_mΩ : } {κ : ()} {μ : } {f : Ωβ} {g : Ωβ'} {_mβ : } {_mβ' : } [Neg β'] [] (hfg : ) :
theorem ProbabilityTheory.kernel.IndepFun.neg_left {α : Type u_1} {Ω : Type u_2} {β : Type u_4} {β' : Type u_5} {_mα : } {_mΩ : } {κ : ()} {μ : } {f : Ωβ} {g : Ωβ'} {_mβ : } {_mβ' : } [Neg β] [] (hfg : ) :
theorem ProbabilityTheory.kernel.iIndepFun.of_subsingleton {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : } {_mΩ : } {κ : ()} {μ : } {β : ιType u_8} {m : (i : ι) → MeasurableSpace (β i)} {f : (i : ι) → Ωβ i} [] :
theorem ProbabilityTheory.kernel.iIndepFun.ae_isProbabilityMeasure {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : } {_mΩ : } {κ : ()} {μ : } {β : ιType u_8} {m : (i : ι) → MeasurableSpace (β i)} {f : (i : ι) → Ωβ i} (h : ) :
∀ᵐ (a : α) ∂μ,
theorem ProbabilityTheory.kernel.iIndepFun.indepFun_finset {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : } {_mΩ : } {κ : ()} {μ : } {β : ιType u_8} {m : (i : ι) → MeasurableSpace (β i)} {f : (i : ι) → Ωβ i} (S : ) (T : ) (hST : Disjoint S T) (hf_Indep : ) (hf_meas : ∀ (i : ι), Measurable (f i)) :
ProbabilityTheory.kernel.IndepFun (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 independent random variables (iIndepFun m f μ) and S, T are two disjoint finite index sets, then the tuple formed by f i for i ∈ S is independent of the tuple (f i)_i for i ∈ T.

theorem ProbabilityTheory.kernel.iIndepFun.indepFun_prod_mk {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : } {_mΩ : } {κ : ()} {μ : } {β : ιType u_8} {m : (i : ι) → MeasurableSpace (β i)} {f : (i : ι) → Ωβ i} (hf_Indep : ) (hf_meas : ∀ (i : ι), Measurable (f i)) (i : ι) (j : ι) (k : ι) (hik : i k) (hjk : j k) :
ProbabilityTheory.kernel.IndepFun (fun (a : Ω) => (f i a, f j a)) (f k) κ μ
theorem ProbabilityTheory.kernel.iIndepFun.indepFun_prod_mk_prod_mk {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : } {_mΩ : } {κ : ()} {μ : } {β : ιType u_8} {m : (i : ι) → MeasurableSpace (β i)} {f : (i : ι) → Ωβ i} (hf_indep : ) (hf_meas : ∀ (i : ι), Measurable (f i)) (i : ι) (j : ι) (k : ι) (l : ι) (hik : i k) (hil : i l) (hjk : j k) (hjl : j l) :
ProbabilityTheory.kernel.IndepFun (fun (a : Ω) => (f i a, f j a)) (fun (a : Ω) => (f k a, f l a)) κ μ
theorem ProbabilityTheory.kernel.iIndepFun.indepFun_add_left {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : } {_mΩ : } {κ : ()} {μ : } {β : Type u_8} {m : } [Add β] [] {f : ιΩβ} (hf_indep : ProbabilityTheory.kernel.iIndepFun (fun (x : ι) => m) f κ μ) (hf_meas : ∀ (i : ι), Measurable (f i)) (i : ι) (j : ι) (k : ι) (hik : i k) (hjk : j k) :
ProbabilityTheory.kernel.IndepFun (f i + f j) (f k) κ μ
theorem ProbabilityTheory.kernel.iIndepFun.indepFun_mul_left {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : } {_mΩ : } {κ : ()} {μ : } {β : Type u_8} {m : } [Mul β] [] {f : ιΩβ} (hf_indep : ProbabilityTheory.kernel.iIndepFun (fun (x : ι) => m) f κ μ) (hf_meas : ∀ (i : ι), Measurable (f i)) (i : ι) (j : ι) (k : ι) (hik : i k) (hjk : j k) :
ProbabilityTheory.kernel.IndepFun (f i * f j) (f k) κ μ
theorem ProbabilityTheory.kernel.iIndepFun.indepFun_add_right {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : } {_mΩ : } {κ : ()} {μ : } {β : Type u_8} {m : } [Add β] [] {f : ιΩβ} (hf_indep : ProbabilityTheory.kernel.iIndepFun (fun (x : ι) => m) f κ μ) (hf_meas : ∀ (i : ι), Measurable (f i)) (i : ι) (j : ι) (k : ι) (hij : i j) (hik : i k) :
ProbabilityTheory.kernel.IndepFun (f i) (f j + f k) κ μ
theorem ProbabilityTheory.kernel.iIndepFun.indepFun_mul_right {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : } {_mΩ : } {κ : ()} {μ : } {β : Type u_8} {m : } [Mul β] [] {f : ιΩβ} (hf_indep : ProbabilityTheory.kernel.iIndepFun (fun (x : ι) => m) f κ μ) (hf_meas : ∀ (i : ι), Measurable (f i)) (i : ι) (j : ι) (k : ι) (hij : i j) (hik : i k) :
ProbabilityTheory.kernel.IndepFun (f i) (f j * f k) κ μ
theorem ProbabilityTheory.kernel.iIndepFun.indepFun_add_add {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : } {_mΩ : } {κ : ()} {μ : } {β : Type u_8} {m : } [Add β] [] {f : ιΩβ} (hf_indep : ProbabilityTheory.kernel.iIndepFun (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.kernel.IndepFun (f i + f j) (f k + f l) κ μ
theorem ProbabilityTheory.kernel.iIndepFun.indepFun_mul_mul {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : } {_mΩ : } {κ : ()} {μ : } {β : Type u_8} {m : } [Mul β] [] {f : ιΩβ} (hf_indep : ProbabilityTheory.kernel.iIndepFun (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.kernel.IndepFun (f i * f j) (f k * f l) κ μ
theorem ProbabilityTheory.kernel.iIndepFun.indepFun_sub_left {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : } {_mΩ : } {κ : ()} {μ : } {β : Type u_8} {m : } [Sub β] [] {f : ιΩβ} (hf_indep : ProbabilityTheory.kernel.iIndepFun (fun (x : ι) => m) f κ μ) (hf_meas : ∀ (i : ι), Measurable (f i)) (i : ι) (j : ι) (k : ι) (hik : i k) (hjk : j k) :
ProbabilityTheory.kernel.IndepFun (f i - f j) (f k) κ μ
theorem ProbabilityTheory.kernel.iIndepFun.indepFun_div_left {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : } {_mΩ : } {κ : ()} {μ : } {β : Type u_8} {m : } [Div β] [] {f : ιΩβ} (hf_indep : ProbabilityTheory.kernel.iIndepFun (fun (x : ι) => m) f κ μ) (hf_meas : ∀ (i : ι), Measurable (f i)) (i : ι) (j : ι) (k : ι) (hik : i k) (hjk : j k) :
ProbabilityTheory.kernel.IndepFun (f i / f j) (f k) κ μ
theorem ProbabilityTheory.kernel.iIndepFun.indepFun_sub_right {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : } {_mΩ : } {κ : ()} {μ : } {β : Type u_8} {m : } [Sub β] [] {f : ιΩβ} (hf_indep : ProbabilityTheory.kernel.iIndepFun (fun (x : ι) => m) f κ μ) (hf_meas : ∀ (i : ι), Measurable (f i)) (i : ι) (j : ι) (k : ι) (hij : i j) (hik : i k) :
ProbabilityTheory.kernel.IndepFun (f i) (f j - f k) κ μ
theorem ProbabilityTheory.kernel.iIndepFun.indepFun_div_right {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : } {_mΩ : } {κ : ()} {μ : } {β : Type u_8} {m : } [Div β] [] {f : ιΩβ} (hf_indep : ProbabilityTheory.kernel.iIndepFun (fun (x : ι) => m) f κ μ) (hf_meas : ∀ (i : ι), Measurable (f i)) (i : ι) (j : ι) (k : ι) (hij : i j) (hik : i k) :
ProbabilityTheory.kernel.IndepFun (f i) (f j / f k) κ μ
theorem ProbabilityTheory.kernel.iIndepFun.indepFun_sub_sub {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : } {_mΩ : } {κ : ()} {μ : } {β : Type u_8} {m : } [Sub β] [] {f : ιΩβ} (hf_indep : ProbabilityTheory.kernel.iIndepFun (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.kernel.IndepFun (f i - f j) (f k - f l) κ μ
theorem ProbabilityTheory.kernel.iIndepFun.indepFun_div_div {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : } {_mΩ : } {κ : ()} {μ : } {β : Type u_8} {m : } [Div β] [] {f : ιΩβ} (hf_indep : ProbabilityTheory.kernel.iIndepFun (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.kernel.IndepFun (f i / f j) (f k / f l) κ μ
theorem ProbabilityTheory.kernel.iIndepFun.indepFun_finset_sum_of_not_mem {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : } {_mΩ : } {κ : ()} {μ : } {β : Type u_8} {m : } [] [] {f : ιΩβ} (hf_Indep : ProbabilityTheory.kernel.iIndepFun (fun (x : ι) => m) f κ μ) (hf_meas : ∀ (i : ι), Measurable (f i)) {s : } {i : ι} (hi : is) :
ProbabilityTheory.kernel.IndepFun (js, f j) (f i) κ μ
theorem ProbabilityTheory.kernel.iIndepFun.indepFun_finset_prod_of_not_mem {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : } {_mΩ : } {κ : ()} {μ : } {β : Type u_8} {m : } [] [] {f : ιΩβ} (hf_Indep : ProbabilityTheory.kernel.iIndepFun (fun (x : ι) => m) f κ μ) (hf_meas : ∀ (i : ι), Measurable (f i)) {s : } {i : ι} (hi : is) :
ProbabilityTheory.kernel.IndepFun (js, f j) (f i) κ μ
theorem ProbabilityTheory.kernel.iIndepFun.indepFun_sum_range_succ {α : Type u_1} {Ω : Type u_2} {_mα : } {_mΩ : } {κ : ()} {μ : } {β : Type u_8} {m : } [] [] {f : Ωβ} (hf_Indep : ProbabilityTheory.kernel.iIndepFun (fun (x : ) => m) f κ μ) (hf_meas : ∀ (i : ), Measurable (f i)) (n : ) :
ProbabilityTheory.kernel.IndepFun (j, f j) (f n) κ μ
theorem ProbabilityTheory.kernel.iIndepFun.indepFun_prod_range_succ {α : Type u_1} {Ω : Type u_2} {_mα : } {_mΩ : } {κ : ()} {μ : } {β : Type u_8} {m : } [] [] {f : Ωβ} (hf_Indep : ProbabilityTheory.kernel.iIndepFun (fun (x : ) => m) f κ μ) (hf_meas : ∀ (i : ), Measurable (f i)) (n : ) :
ProbabilityTheory.kernel.IndepFun (j, f j) (f n) κ μ
theorem ProbabilityTheory.kernel.iIndepSet.iIndepFun_indicator {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {β : Type u_4} {_mα : } {_mΩ : } {κ : ()} {μ : } [Zero β] [One β] {m : } {s : ιSet Ω} (hs : ) :
ProbabilityTheory.kernel.iIndepFun (fun (_n : ι) => m) (fun (n : ι) => (s n).indicator fun ( : Ω) => 1) κ μ