# Independence of sets of sets and measure spaces (σ-algebras) #

• A family of sets of sets π : ι → Set (Set Ω) is independent 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, μ (⋂ i in s, f i) = ∏ i ∈ s, μ (f i). It will be used for families of π-systems.
• A family of measurable space structures (i.e. of σ-algebras) is independent with respect to a measure μ (typically defined on a finer σ-algebra) if the family of sets of measurable sets they define is independent. I.e., m : ι → MeasurableSpace Ω is independent with respect to a 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) = ∏ i ∈ s, μ (f i).
• Independence of sets (or events in probabilistic parlance) is defined as independence of the measurable space structures they generate: a set s generates the measurable space structure with measurable sets ∅, s, sᶜ, univ.
• Independence of functions (or random variables) is also defined as independence of the measurable space structures they generate: a function f for which we have a measurable space m on the codomain generates MeasurableSpace.comap f m.

## Main statements #

• iIndepSets.iIndep: if π-systems are independent as sets of sets, then the measurable space structures they generate are independent.
• IndepSets.indep: variant with two π-systems.

## Implementation notes #

The definitions of independence in this file are a particular case of independence with respect to a kernel and a measure, as defined in the file Kernel.lean.

We provide four definitions of independence:

• iIndepSets: independence of a family of sets of sets pi : ι → Set (Set Ω). This is meant to be used with π-systems.
• iIndep: independence of a family of measurable space structures m : ι → MeasurableSpace Ω,
• iIndepSet: independence of a family of sets s : ι → Set Ω,
• iIndepFun: 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 IndepFun is the version of iIndepFun for two functions.

The definition of independence for iIndepSets uses finite sets (Finset). See ProbabilityTheory.kernel.iIndepSets. An alternative and equivalent way of defining independence would have been to use countable sets.

Most of the definitions and lemmas in this file list all variables instead of using the variable keyword at the beginning of a section, for example lemma Indep.symm {Ω} {m₁ m₂ : MeasurableSpace Ω} {_mΩ : MeasurableSpace Ω} {μ : measure Ω} ... . This is intentional, to be able to control the order of the MeasurableSpace variables. Indeed when defining μ in the example above, the measurable space used is the last one defined, here {_mΩ : MeasurableSpace Ω}, and not m₁ or m₂.

## References #

• Williams, David. Probability with martingales. Cambridge university press, 1991. Part A, Chapter 4.
def ProbabilityTheory.iIndepSets {Ω : Type u_1} {ι : Type u_2} {_mΩ : } (π : ιSet (Set Ω)) (μ : ) :

A family of sets of sets π : ι → Set (Set Ω) is independent 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) = ∏ i ∈ s, μ (f i) . It will be used for families of pi_systems.

Equations
Instances For
def ProbabilityTheory.IndepSets {Ω : Type u_1} {_mΩ : } (s1 : Set (Set Ω)) (s2 : Set (Set Ω)) (μ : ) :

Two sets of sets s₁, s₂ are independent with respect to a measure μ if for any sets t₁ ∈ p₁, t₂ ∈ s₂, then μ (t₁ ∩ t₂) = μ (t₁) * μ (t₂)

Equations
Instances For
def ProbabilityTheory.iIndep {Ω : Type u_1} {ι : Type u_2} (m : ι) {_mΩ : } (μ : ) :

A family of measurable space structures (i.e. of σ-algebras) is independent 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 independent 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) = ∏ i ∈ s, μ (f i).

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

Two measurable space structures (or σ-algebras) m₁, m₂ are independent with respect to a measure μ (defined on a third σ-algebra) if for any sets t₁ ∈ m₁, t₂ ∈ m₂, μ (t₁ ∩ t₂) = μ (t₁) * μ (t₂)

Equations
Instances For
def ProbabilityTheory.iIndepSet {Ω : Type u_1} {ι : Type u_2} {_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.IndepSet {Ω : Type u_1} {_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.iIndepFun {Ω : Type u_1} {ι : Type u_2} {_mΩ : } {β : ιType u_6} (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.IndepFun {Ω : Type u_1} {β : Type u_6} {γ : Type u_7} {_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.iIndepSets_iff {Ω : Type u_1} {ι : Type u_2} :
∀ {x : } (π : ιSet (Set Ω)) (μ : ), ∀ (s : ) {f : ιSet Ω}, (is, f i π i)μ (is, f i) = is, μ (f i)
theorem ProbabilityTheory.iIndepSets.meas_biInter {Ω : Type u_1} {ι : Type u_2} {π : ιSet (Set Ω)} :
∀ {x : } {μ : }, ∀ (s : ) {f : ιSet Ω}, (is, f i π i)μ (is, f i) = is, μ (f i)
theorem ProbabilityTheory.iIndepSets.meas_iInter {Ω : Type u_1} {ι : Type u_2} {π : ιSet (Set Ω)} :
∀ {x : } {μ : } {s : ιSet Ω} [inst : ], (∀ (i : ι), s i π i)μ (⋂ (i : ι), s i) = i : ι, μ (s i)
theorem ProbabilityTheory.IndepSets_iff {Ω : Type u_1} :
∀ {x : } (s1 s2 : Set (Set Ω)) (μ : ), ∀ (t1 t2 : Set Ω), t1 s1t2 s2μ (t1 t2) = μ t1 * μ t2
theorem ProbabilityTheory.iIndep_iff_iIndepSets {Ω : Type u_1} {ι : Type u_2} (m : ι) {_mΩ : } (μ : ) :
ProbabilityTheory.iIndepSets (fun (x : ι) => {s : Set Ω | }) μ
theorem ProbabilityTheory.iIndep.iIndepSets' {Ω : Type u_1} {ι : Type u_2} {m : ι} :
∀ {x : } {μ : }, ProbabilityTheory.iIndepSets (fun (x : ι) => {s : Set Ω | }) μ
theorem ProbabilityTheory.iIndep_iff {Ω : Type u_1} {ι : Type u_2} (m : ι) {_mΩ : } (μ : ) :
∀ (s : ) {f : ιSet Ω}, (is, MeasurableSet (f i))μ (is, f i) = is, μ (f i)
theorem ProbabilityTheory.iIndep.meas_biInter {Ω : Type u_1} {ι : Type u_2} {m : ι} :
∀ {x : } {μ : } {S : } {s : ιSet Ω}, (iS, MeasurableSet (s i))μ (iS, s i) = iS, μ (s i)
theorem ProbabilityTheory.iIndep.meas_iInter {Ω : Type u_1} {ι : Type u_2} {m : ι} :
∀ {x : } {μ : } {s : ιSet Ω} [inst : ], (∀ (i : ι), MeasurableSet (s i))μ (⋂ (i : ι), s i) = i : ι, μ (s i)
theorem ProbabilityTheory.Indep_iff_IndepSets {Ω : Type u_1} (m₁ : ) (m₂ : ) {_mΩ : } (μ : ) :
ProbabilityTheory.IndepSets {s : Set Ω | } {s : Set Ω | } μ
theorem ProbabilityTheory.Indep_iff {Ω : Type u_1} (m₁ : ) (m₂ : ) {_mΩ : } (μ : ) :
∀ (t1 t2 : Set Ω), μ (t1 t2) = μ t1 * μ t2
theorem ProbabilityTheory.iIndepSet_iff_iIndep {Ω : Type u_1} {ι : Type u_2} :
∀ {x : } (s : ιSet Ω) (μ : ), ProbabilityTheory.iIndep (fun (i : ι) => ) μ
theorem ProbabilityTheory.iIndepSet_iff {Ω : Type u_1} {ι : Type u_2} :
∀ {x : } (s : ιSet Ω) (μ : ), ∀ (s' : ) {f : ιSet Ω}, (is', MeasurableSet (f i))μ (is', f i) = is', μ (f i)
theorem ProbabilityTheory.IndepSet_iff_Indep {Ω : Type u_1} :
∀ {x : } (s t : Set Ω) (μ : ),
theorem ProbabilityTheory.IndepSet_iff {Ω : Type u_1} :
∀ {x : } (s t : Set Ω) (μ : ), ∀ (t1 t2 : Set Ω), μ (t1 t2) = μ t1 * μ t2
theorem ProbabilityTheory.iIndepFun_iff_iIndep {Ω : Type u_1} {ι : Type u_2} :
∀ {x : } {β : ιType u_6} (m : (x : ι) → MeasurableSpace (β x)) (f : (x : ι) → Ωβ x) (μ : ), ProbabilityTheory.iIndep (fun (x : ι) => MeasurableSpace.comap (f x) (m x)) μ
theorem ProbabilityTheory.iIndepFun.iIndep {Ω : Type u_1} {ι : Type u_2} {κ : ιType u_5} :
∀ {x : } {μ : } {m : (i : ι) → MeasurableSpace (κ i)} {f : (x : ι) → Ωκ x}, ProbabilityTheory.iIndep (fun (x : ι) => MeasurableSpace.comap (f x) (m x)) μ
theorem ProbabilityTheory.iIndepFun_iff {Ω : Type u_1} {ι : Type u_2} :
∀ {x : } {β : ιType u_6} (m : (x : ι) → MeasurableSpace (β x)) (f : (x : ι) → Ωβ x) (μ : ), ∀ (s : ) {f' : ιSet Ω}, (is, MeasurableSet (f' i))μ (is, f' i) = is, μ (f' i)
theorem ProbabilityTheory.iIndepFun.meas_biInter {Ω : Type u_1} {ι : Type u_2} {κ : ιType u_5} :
∀ {x : } {μ : } {S : } {s : ιSet Ω} {m : (i : ι) → MeasurableSpace (κ i)} {f : (x : ι) → Ωκ x}, (iS, MeasurableSet (s i))μ (iS, s i) = iS, μ (s i)
theorem ProbabilityTheory.iIndepFun.meas_iInter {Ω : Type u_1} {ι : Type u_2} {κ : ιType u_5} :
∀ {x : } {μ : } {s : ιSet Ω} [inst : ] {m : (i : ι) → MeasurableSpace (κ i)} {f : (x : ι) → Ωκ x}, (∀ (i : ι), MeasurableSet (s i))μ (⋂ (i : ι), s i) = i : ι, μ (s i)
theorem ProbabilityTheory.IndepFun_iff_Indep {Ω : Type u_1} {β : Type u_3} {γ : Type u_4} :
∀ {x : } [ : ] [ : ] (f : Ωβ) (g : Ωγ) (μ : ),
theorem ProbabilityTheory.IndepFun_iff {Ω : Type u_1} :
∀ {x : } {β : Type u_6} {γ : Type u_7} [ : ] [ : ] (f : Ωβ) (g : Ωγ) (μ : ), ∀ (t1 t2 : Set Ω), μ (t1 t2) = μ t1 * μ t2
theorem ProbabilityTheory.IndepFun.meas_inter {Ω : Type u_1} {β : Type u_3} {γ : Type u_4} :
∀ {x : } {μ : } [ : ] [ : ] {f : Ωβ} {g : Ωγ}, ∀ {s t : Set Ω}, μ (s t) = μ s * μ t
theorem ProbabilityTheory.IndepSets.symm {Ω : Type u_1} {_mΩ : } {μ : } {s₁ : Set (Set Ω)} {s₂ : Set (Set Ω)} (h : ) :
theorem ProbabilityTheory.Indep.symm {Ω : Type u_1} {m₁ : } {m₂ : } {_mΩ : } {μ : } (h : ) :
theorem ProbabilityTheory.indep_bot_right {Ω : Type u_1} (m' : ) {_mΩ : } {μ : } :
theorem ProbabilityTheory.indep_bot_left {Ω : Type u_1} (m' : ) {_mΩ : } {μ : } :
theorem ProbabilityTheory.indepSet_empty_right {Ω : Type u_1} {_mΩ : } {μ : } (s : Set Ω) :
theorem ProbabilityTheory.indepSet_empty_left {Ω : Type u_1} {_mΩ : } {μ : } (s : Set Ω) :
theorem ProbabilityTheory.indepSets_of_indepSets_of_le_left {Ω : Type u_1} {_mΩ : } {μ : } {s₁ : Set (Set Ω)} {s₂ : Set (Set Ω)} {s₃ : Set (Set Ω)} (h_indep : ) (h31 : s₃ s₁) :
theorem ProbabilityTheory.indepSets_of_indepSets_of_le_right {Ω : Type u_1} {_mΩ : } {μ : } {s₁ : Set (Set Ω)} {s₂ : Set (Set Ω)} {s₃ : Set (Set Ω)} (h_indep : ) (h32 : s₃ s₂) :
theorem ProbabilityTheory.indep_of_indep_of_le_left {Ω : Type u_1} {m₁ : } {m₂ : } {m₃ : } {_mΩ : } {μ : } (h_indep : ) (h31 : m₃ m₁) :
theorem ProbabilityTheory.indep_of_indep_of_le_right {Ω : Type u_1} {m₁ : } {m₂ : } {m₃ : } {_mΩ : } {μ : } (h_indep : ) (h32 : m₃ m₂) :
theorem ProbabilityTheory.IndepSets.union {Ω : Type u_1} {_mΩ : } {μ : } {s₁ : Set (Set Ω)} {s₂ : Set (Set Ω)} {s' : Set (Set Ω)} (h₁ : ) (h₂ : ) :
@[simp]
theorem ProbabilityTheory.IndepSets.union_iff {Ω : Type u_1} {_mΩ : } {μ : } {s₁ : Set (Set Ω)} {s₂ : Set (Set Ω)} {s' : Set (Set Ω)} :
theorem ProbabilityTheory.IndepSets.iUnion {Ω : Type u_1} {ι : Type u_2} {_mΩ : } {μ : } {s : ιSet (Set Ω)} {s' : Set (Set Ω)} (hyp : ∀ (n : ι), ProbabilityTheory.IndepSets (s n) s' μ) :
ProbabilityTheory.IndepSets (⋃ (n : ι), s n) s' μ
theorem ProbabilityTheory.IndepSets.bUnion {Ω : Type u_1} {ι : Type u_2} {_mΩ : } {μ : } {s : ιSet (Set Ω)} {s' : Set (Set Ω)} {u : Set ι} (hyp : nu, ProbabilityTheory.IndepSets (s n) s' μ) :
ProbabilityTheory.IndepSets (nu, s n) s' μ
theorem ProbabilityTheory.IndepSets.inter {Ω : Type u_1} {_mΩ : } {μ : } {s₁ : Set (Set Ω)} {s' : Set (Set Ω)} (s₂ : Set (Set Ω)) (h₁ : ) :
theorem ProbabilityTheory.IndepSets.iInter {Ω : Type u_1} {ι : Type u_2} {_mΩ : } {μ : } {s : ιSet (Set Ω)} {s' : Set (Set Ω)} (h : ∃ (n : ι), ProbabilityTheory.IndepSets (s n) s' μ) :
ProbabilityTheory.IndepSets (⋂ (n : ι), s n) s' μ
theorem ProbabilityTheory.IndepSets.bInter {Ω : Type u_1} {ι : Type u_2} {_mΩ : } {μ : } {s : ιSet (Set Ω)} {s' : Set (Set Ω)} {u : Set ι} (h : nu, ProbabilityTheory.IndepSets (s n) s' μ) :
ProbabilityTheory.IndepSets (nu, s n) s' μ
theorem ProbabilityTheory.indepSets_singleton_iff {Ω : Type u_1} {_mΩ : } {μ : } {s : Set Ω} {t : Set Ω} :
ProbabilityTheory.IndepSets {s} {t} μ μ (s t) = μ s * μ t

### Deducing Indep from iIndep#

theorem ProbabilityTheory.iIndepSets.indepSets {Ω : Type u_1} {ι : Type u_2} {_mΩ : } {μ : } {s : ιSet (Set Ω)} (h_indep : ) {i : ι} {j : ι} (hij : i j) :
theorem ProbabilityTheory.iIndep.indep {Ω : Type u_1} {ι : Type u_2} {m : ι} {_mΩ : } {μ : } (h_indep : ) {i : ι} {j : ι} (hij : i j) :
theorem ProbabilityTheory.iIndepFun.indepFun {Ω : Type u_1} {ι : Type u_2} {_mΩ : } {μ : } {β : ιType u_6} {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.iIndep.iIndepSets {Ω : Type u_1} {ι : Type u_2} {m : ι} {_mΩ : } {μ : } {s : ιSet (Set Ω)} (hms : ∀ (n : ι), m n = ) (h_indep : ) :
theorem ProbabilityTheory.Indep.indepSets {Ω : Type u_1} {_mΩ : } {μ : } {s1 : Set (Set Ω)} {s2 : Set (Set Ω)} (h_indep : ) :

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

theorem ProbabilityTheory.IndepSets.indep {Ω : Type u_1} {m1 : } {m2 : } {_mΩ : } {μ : } {p1 : Set (Set Ω)} {p2 : Set (Set Ω)} (h1 : m1 _mΩ) (h2 : m2 _mΩ) (hp1 : ) (hp2 : ) (hpm1 : ) (hpm2 : ) (hyp : ) :
theorem ProbabilityTheory.IndepSets.indep' {Ω : Type u_1} {_mΩ : } {μ : } {p1 : Set (Set Ω)} {p2 : Set (Set Ω)} (hp1m : sp1, ) (hp2m : sp2, ) (hp1 : ) (hp2 : ) (hyp : ) :
theorem ProbabilityTheory.indepSets_piiUnionInter_of_disjoint {Ω : Type u_1} {ι : Type u_2} {_mΩ : } {μ : } {s : ιSet (Set Ω)} {S : Set ι} {T : Set ι} (h_indep : ) (hST : Disjoint S T) :
theorem ProbabilityTheory.iIndepSet.indep_generateFrom_of_disjoint {Ω : Type u_1} {ι : Type u_2} {_mΩ : } {μ : } {s : ιSet Ω} (hsm : ∀ (n : ι), MeasurableSet (s n)) (hs : ) (S : Set ι) (T : Set ι) (hST : Disjoint S T) :
ProbabilityTheory.Indep (MeasurableSpace.generateFrom {t : Set Ω | nS, s n = t}) (MeasurableSpace.generateFrom {t : Set Ω | kT, s k = t}) μ
theorem ProbabilityTheory.indep_iSup_of_disjoint {Ω : Type u_1} {ι : Type u_2} {m : ι} {_mΩ : } {μ : } (h_le : ∀ (i : ι), m i _mΩ) (h_indep : ) {S : Set ι} {T : Set ι} (hST : Disjoint S T) :
ProbabilityTheory.Indep (iS, m i) (iT, m i) μ
theorem ProbabilityTheory.indep_iSup_of_directed_le {Ω : Type u_1} {ι : Type u_2} {m : ι} {m1 : } {_mΩ : } {μ : } (h_indep : ∀ (i : ι), ProbabilityTheory.Indep (m i) m1 μ) (h_le : ∀ (i : ι), m i _mΩ) (h_le' : m1 _mΩ) (hm : Directed (fun (x x_1 : ) => x x_1) m) :
ProbabilityTheory.Indep (⨆ (i : ι), m i) m1 μ
theorem ProbabilityTheory.iIndepSet.indep_generateFrom_lt {Ω : Type u_1} {ι : Type u_2} {_mΩ : } {μ : } [] {s : ιSet Ω} (hsm : ∀ (n : ι), MeasurableSet (s n)) (hs : ) (i : ι) :
ProbabilityTheory.Indep () (MeasurableSpace.generateFrom {t : Set Ω | j < i, s j = t}) μ
theorem ProbabilityTheory.iIndepSet.indep_generateFrom_le {Ω : Type u_1} {ι : Type u_2} {_mΩ : } {μ : } [] {s : ιSet Ω} (hsm : ∀ (n : ι), MeasurableSet (s n)) (hs : ) (i : ι) {k : ι} (hk : i < k) :
ProbabilityTheory.Indep () (MeasurableSpace.generateFrom {t : Set Ω | ji, s j = t}) μ
theorem ProbabilityTheory.iIndepSet.indep_generateFrom_le_nat {Ω : Type u_1} {_mΩ : } {μ : } {s : Set Ω} (hsm : ∀ (n : ), MeasurableSet (s n)) (hs : ) (n : ) :
theorem ProbabilityTheory.indep_iSup_of_monotone {Ω : Type u_1} {ι : Type u_2} {m : ι} {m1 : } {_mΩ : } {μ : } [] (h_indep : ∀ (i : ι), ProbabilityTheory.Indep (m i) m1 μ) (h_le : ∀ (i : ι), m i _mΩ) (h_le' : m1 _mΩ) (hm : ) :
ProbabilityTheory.Indep (⨆ (i : ι), m i) m1 μ
theorem ProbabilityTheory.indep_iSup_of_antitone {Ω : Type u_1} {ι : Type u_2} {m : ι} {m1 : } {_mΩ : } {μ : } [] (h_indep : ∀ (i : ι), ProbabilityTheory.Indep (m i) m1 μ) (h_le : ∀ (i : ι), m i _mΩ) (h_le' : m1 _mΩ) (hm : ) :
ProbabilityTheory.Indep (⨆ (i : ι), m i) m1 μ
theorem ProbabilityTheory.iIndepSets.piiUnionInter_of_not_mem {Ω : Type u_1} {ι : Type u_2} {_mΩ : } {μ : } {π : ιSet (Set Ω)} {a : ι} {S : } (hp_ind : ) (haS : aS) :
theorem ProbabilityTheory.iIndepSets.iIndep {Ω : Type u_1} {ι : Type u_2} {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 μ ↔ μ (s ∩ t) = μ s * μ t,
• IndepSet s t μ ↔ IndepSets {s} {t} μ.
theorem ProbabilityTheory.indepSet_iff_indepSets_singleton {Ω : Type u_1} {_mΩ : } {s : Set Ω} {t : Set Ω} (hs_meas : ) (ht_meas : ) (μ : ) :
theorem ProbabilityTheory.indepSet_iff_measure_inter_eq_mul {Ω : Type u_1} {_mΩ : } {s : Set Ω} {t : Set Ω} (hs_meas : ) (ht_meas : ) (μ : ) :
μ (s t) = μ s * μ t
theorem ProbabilityTheory.IndepSets.indepSet_of_mem {Ω : Type u_1} {_mΩ : } {s : Set Ω} {t : Set Ω} (S : Set (Set Ω)) (T : Set (Set Ω)) (hs : s S) (ht : t T) (hs_meas : ) (ht_meas : ) (μ : ) (h_indep : ) :
theorem ProbabilityTheory.Indep.indepSet_of_measurableSet {Ω : Type u_1} {m₁ : } {m₂ : } {_mΩ : } {μ : } (h_indep : ) {s : Set Ω} {t : Set Ω} (hs : ) (ht : ) :
theorem ProbabilityTheory.indep_iff_forall_indepSet {Ω : Type u_1} {m₁ : } {m₂ : } {_mΩ : } (μ : ) :
∀ (s t : Set Ω),
theorem ProbabilityTheory.iIndep_comap_mem_iff {Ω : Type u_1} {ι : Type u_2} {_mΩ : } {μ : } {f : ιSet Ω} :
ProbabilityTheory.iIndep (fun (i : ι) => MeasurableSpace.comap (fun (x : Ω) => x f i) ) μ
theorem ProbabilityTheory.iIndepSet.iIndep_comap_mem {Ω : Type u_1} {ι : Type u_2} {_mΩ : } {μ : } {f : ιSet Ω} :
ProbabilityTheory.iIndep (fun (i : ι) => MeasurableSpace.comap (fun (x : Ω) => x f i) ) μ

Alias of the reverse direction of ProbabilityTheory.iIndep_comap_mem_iff.

theorem ProbabilityTheory.iIndepSets_singleton_iff {Ω : Type u_1} {ι : Type u_2} {_mΩ : } {μ : } {s : ιSet Ω} :
ProbabilityTheory.iIndepSets (fun (i : ι) => {s i}) μ ∀ (t : ), μ (it, s i) = it, μ (s i)
theorem ProbabilityTheory.iIndepSet_iff_iIndepSets_singleton {Ω : Type u_1} {ι : Type u_2} {_mΩ : } {μ : } {f : ιSet Ω} (hf : ∀ (i : ι), MeasurableSet (f i)) :
ProbabilityTheory.iIndepSets (fun (i : ι) => {f i}) μ
theorem ProbabilityTheory.iIndepSet_iff_meas_biInter {Ω : Type u_1} {ι : Type u_2} {_mΩ : } {μ : } {f : ιSet Ω} (hf : ∀ (i : ι), MeasurableSet (f i)) :
∀ (s : ), μ (is, f i) = is, μ (f i)
theorem ProbabilityTheory.iIndepSets.iIndepSet_of_mem {Ω : Type u_1} {ι : Type u_2} {_mΩ : } {μ : } {π : ιSet (Set Ω)} {f : ιSet Ω} (hfπ : ∀ (i : ι), f i π i) (hf : ∀ (i : ι), MeasurableSet (f i)) (hπ : ) :

### Independence of random variables #

theorem ProbabilityTheory.indepFun_iff_measure_inter_preimage_eq_mul {Ω : Type u_1} {β : Type u_6} {β' : Type u_7} {_mΩ : } {μ : } {f : Ωβ} {g : Ωβ'} {mβ : } {mβ' : } :
∀ (s : Set β) (t : Set β'), μ (f ⁻¹' s g ⁻¹' t) = μ (f ⁻¹' s) * μ (g ⁻¹' t)
theorem ProbabilityTheory.iIndepFun_iff_measure_inter_preimage_eq_mul {Ω : Type u_1} {_mΩ : } {μ : } {ι : Type u_10} {β : ιType u_11} (m : (x : ι) → MeasurableSpace (β x)) (f : (i : ι) → Ωβ i) :
∀ (S : ) {sets : (i : ι) → Set (β i)}, (iS, MeasurableSet (sets i))μ (iS, f i ⁻¹' sets i) = iS, μ (f i ⁻¹' sets i)
theorem ProbabilityTheory.indepFun_iff_indepSet_preimage {Ω : Type u_1} {β : Type u_6} {β' : Type u_7} {_mΩ : } {μ : } {f : Ωβ} {g : Ωβ'} {mβ : } {mβ' : } (hf : ) (hg : ) :
∀ (s : Set β) (t : Set β'), ProbabilityTheory.IndepSet (f ⁻¹' s) (g ⁻¹' t) μ
theorem ProbabilityTheory.indepFun_iff_map_prod_eq_prod_map_map {Ω : Type u_1} {β : Type u_6} {β' : Type u_7} {_mΩ : } {μ : } {f : Ωβ} {g : Ωβ'} {mβ : } {mβ' : } (hf : ) (hg : ) :
MeasureTheory.Measure.map (fun (ω : Ω) => (f ω, g ω)) μ = .prod
theorem ProbabilityTheory.IndepFun.symm {Ω : Type u_1} {β : Type u_6} {β' : Type u_7} {_mΩ : } {μ : } {f : Ωβ} {g : Ωβ'} :
∀ {x : } {x_1 : },
theorem ProbabilityTheory.IndepFun.ae_eq {Ω : Type u_1} {β : Type u_6} {β' : Type u_7} {_mΩ : } {μ : } {f : Ωβ} {g : Ωβ'} {mβ : } {mβ' : } {f' : Ωβ} {g' : Ωβ'} (hfg : ) (hf : f =ᵐ[μ] f') (hg : g =ᵐ[μ] g') :
theorem ProbabilityTheory.IndepFun.comp {Ω : Type u_1} {β : Type u_6} {β' : Type u_7} {γ : Type u_8} {γ' : Type u_9} {_mΩ : } {μ : } {f : Ωβ} {g : Ωβ'} {_mβ : } {_mβ' : } {_mγ : } {_mγ' : } {φ : βγ} {ψ : β'γ'} (hfg : ) (hφ : ) (hψ : ) :
theorem ProbabilityTheory.IndepFun.neg_right {Ω : Type u_1} {β : Type u_6} {β' : Type u_7} {_mΩ : } {μ : } {f : Ωβ} {g : Ωβ'} {_mβ : } {_mβ' : } [Neg β'] [] (hfg : ) :
theorem ProbabilityTheory.IndepFun.neg_left {Ω : Type u_1} {β : Type u_6} {β' : Type u_7} {_mΩ : } {μ : } {f : Ωβ} {g : Ωβ'} {_mβ : } {_mβ' : } [Neg β] [] (hfg : ) :
theorem ProbabilityTheory.iIndepFun.of_subsingleton {Ω : Type u_1} {ι : Type u_2} {_mΩ : } {μ : } {β : ιType u_10} {m : (i : ι) → MeasurableSpace (β i)} {f : (i : ι) → Ωβ i} [] :
theorem ProbabilityTheory.iIndepFun.isProbabilityMeasure {Ω : Type u_1} {ι : Type u_2} {_mΩ : } {μ : } {β : ιType u_10} {m : (i : ι) → MeasurableSpace (β i)} {f : (i : ι) → Ωβ i} (h : ) :
theorem ProbabilityTheory.iIndepFun.indepFun_finset {Ω : Type u_1} {ι : Type u_2} {_mΩ : } {μ : } {β : ιType u_10} {m : (i : ι) → MeasurableSpace (β i)} {f : (i : ι) → Ωβ i} (S : ) (T : ) (hST : Disjoint S T) (hf_Indep : ) (hf_meas : ∀ (i : ι), Measurable (f i)) :
ProbabilityTheory.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.iIndepFun.indepFun_prod_mk {Ω : Type u_1} {ι : Type u_2} {_mΩ : } {μ : } {β : ιType u_10} {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.IndepFun (fun (a : Ω) => (f i a, f j a)) (f k) μ
theorem ProbabilityTheory.iIndepFun.indepFun_prod_mk_prod_mk {Ω : Type u_1} {ι : Type u_2} {_mΩ : } {μ : } {β : ιType u_10} {m : (i : ι) → MeasurableSpace (β i)} {f : (i : ι) → Ωβ i} (h_indep : ) (hf : ∀ (i : ι), Measurable (f i)) (i : ι) (j : ι) (k : ι) (l : ι) (hik : i k) (hil : i l) (hjk : j k) (hjl : j l) :
ProbabilityTheory.IndepFun (fun (a : Ω) => (f i a, f j a)) (fun (a : Ω) => (f k a, f l a)) μ
theorem ProbabilityTheory.iIndepFun.indepFun_add_left {Ω : Type u_1} {ι : Type u_2} {_mΩ : } {μ : } {β : Type u_10} {m : } [Add β] [] {f : ιΩβ} (hf_indep : ProbabilityTheory.iIndepFun (fun (x : ι) => m) f μ) (hf_meas : ∀ (i : ι), Measurable (f i)) (i : ι) (j : ι) (k : ι) (hik : i k) (hjk : j k) :
ProbabilityTheory.IndepFun (f i + f j) (f k) μ
theorem ProbabilityTheory.iIndepFun.indepFun_mul_left {Ω : Type u_1} {ι : Type u_2} {_mΩ : } {μ : } {β : Type u_10} {m : } [Mul β] [] {f : ιΩβ} (hf_indep : ProbabilityTheory.iIndepFun (fun (x : ι) => m) f μ) (hf_meas : ∀ (i : ι), Measurable (f i)) (i : ι) (j : ι) (k : ι) (hik : i k) (hjk : j k) :
ProbabilityTheory.IndepFun (f i * f j) (f k) μ
theorem ProbabilityTheory.iIndepFun.indepFun_add_right {Ω : Type u_1} {ι : Type u_2} {_mΩ : } {μ : } {β : Type u_10} {m : } [Add β] [] {f : ιΩβ} (hf_indep : ProbabilityTheory.iIndepFun (fun (x : ι) => m) f μ) (hf_meas : ∀ (i : ι), Measurable (f i)) (i : ι) (j : ι) (k : ι) (hij : i j) (hik : i k) :
ProbabilityTheory.IndepFun (f i) (f j + f k) μ
theorem ProbabilityTheory.iIndepFun.indepFun_mul_right {Ω : Type u_1} {ι : Type u_2} {_mΩ : } {μ : } {β : Type u_10} {m : } [Mul β] [] {f : ιΩβ} (hf_indep : ProbabilityTheory.iIndepFun (fun (x : ι) => m) f μ) (hf_meas : ∀ (i : ι), Measurable (f i)) (i : ι) (j : ι) (k : ι) (hij : i j) (hik : i k) :
ProbabilityTheory.IndepFun (f i) (f j * f k) μ
theorem ProbabilityTheory.iIndepFun.indepFun_add_add {Ω : Type u_1} {ι : Type u_2} {_mΩ : } {μ : } {β : Type u_10} {m : } [Add β] [] {f : ιΩβ} (hf_indep : ProbabilityTheory.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.IndepFun (f i + f j) (f k + f l) μ
theorem ProbabilityTheory.iIndepFun.indepFun_mul_mul {Ω : Type u_1} {ι : Type u_2} {_mΩ : } {μ : } {β : Type u_10} {m : } [Mul β] [] {f : ιΩβ} (hf_indep : ProbabilityTheory.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.IndepFun (f i * f j) (f k * f l) μ
theorem ProbabilityTheory.iIndepFun.indepFun_sub_left {Ω : Type u_1} {ι : Type u_2} {_mΩ : } {μ : } {β : Type u_10} {m : } [Sub β] [] {f : ιΩβ} (hf_indep : ProbabilityTheory.iIndepFun (fun (x : ι) => m) f μ) (hf_meas : ∀ (i : ι), Measurable (f i)) (i : ι) (j : ι) (k : ι) (hik : i k) (hjk : j k) :
ProbabilityTheory.IndepFun (f i - f j) (f k) μ
theorem ProbabilityTheory.iIndepFun.indepFun_div_left {Ω : Type u_1} {ι : Type u_2} {_mΩ : } {μ : } {β : Type u_10} {m : } [Div β] [] {f : ιΩβ} (hf_indep : ProbabilityTheory.iIndepFun (fun (x : ι) => m) f μ) (hf_meas : ∀ (i : ι), Measurable (f i)) (i : ι) (j : ι) (k : ι) (hik : i k) (hjk : j k) :
ProbabilityTheory.IndepFun (f i / f j) (f k) μ
theorem ProbabilityTheory.iIndepFun.indepFun_sub_right {Ω : Type u_1} {ι : Type u_2} {_mΩ : } {μ : } {β : Type u_10} {m : } [Sub β] [] {f : ιΩβ} (hf_indep : ProbabilityTheory.iIndepFun (fun (x : ι) => m) f μ) (hf_meas : ∀ (i : ι), Measurable (f i)) (i : ι) (j : ι) (k : ι) (hij : i j) (hik : i k) :
ProbabilityTheory.IndepFun (f i) (f j - f k) μ
theorem ProbabilityTheory.iIndepFun.indepFun_div_right {Ω : Type u_1} {ι : Type u_2} {_mΩ : } {μ : } {β : Type u_10} {m : } [Div β] [] {f : ιΩβ} (hf_indep : ProbabilityTheory.iIndepFun (fun (x : ι) => m) f μ) (hf_meas : ∀ (i : ι), Measurable (f i)) (i : ι) (j : ι) (k : ι) (hij : i j) (hik : i k) :
ProbabilityTheory.IndepFun (f i) (f j / f k) μ
theorem ProbabilityTheory.iIndepFun.indepFun_sub_sub {Ω : Type u_1} {ι : Type u_2} {_mΩ : } {μ : } {β : Type u_10} {m : } [Sub β] [] {f : ιΩβ} (hf_indep : ProbabilityTheory.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.IndepFun (f i - f j) (f k - f l) μ
theorem ProbabilityTheory.iIndepFun.indepFun_div_div {Ω : Type u_1} {ι : Type u_2} {_mΩ : } {μ : } {β : Type u_10} {m : } [Div β] [] {f : ιΩβ} (hf_indep : ProbabilityTheory.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.IndepFun (f i / f j) (f k / f l) μ
theorem ProbabilityTheory.iIndepFun.indepFun_finset_sum_of_not_mem {Ω : Type u_1} {ι : Type u_2} {_mΩ : } {μ : } {β : Type u_10} {m : } [] [] {f : ιΩβ} (hf_Indep : ProbabilityTheory.iIndepFun (fun (x : ι) => m) f μ) (hf_meas : ∀ (i : ι), Measurable (f i)) {s : } {i : ι} (hi : is) :
ProbabilityTheory.IndepFun (js, f j) (f i) μ
theorem ProbabilityTheory.iIndepFun.indepFun_finset_prod_of_not_mem {Ω : Type u_1} {ι : Type u_2} {_mΩ : } {μ : } {β : Type u_10} {m : } [] [] {f : ιΩβ} (hf_Indep : ProbabilityTheory.iIndepFun (fun (x : ι) => m) f μ) (hf_meas : ∀ (i : ι), Measurable (f i)) {s : } {i : ι} (hi : is) :
ProbabilityTheory.IndepFun (js, f j) (f i) μ
theorem ProbabilityTheory.iIndepFun.indepFun_sum_range_succ {Ω : Type u_1} {_mΩ : } {μ : } {β : Type u_10} {m : } [] [] {f : Ωβ} (hf_Indep : ProbabilityTheory.iIndepFun (fun (x : ) => m) f μ) (hf_meas : ∀ (i : ), Measurable (f i)) (n : ) :
ProbabilityTheory.IndepFun (j, f j) (f n) μ
theorem ProbabilityTheory.iIndepFun.indepFun_prod_range_succ {Ω : Type u_1} {_mΩ : } {μ : } {β : Type u_10} {m : } [] [] {f : Ωβ} (hf_Indep : ProbabilityTheory.iIndepFun (fun (x : ) => m) f μ) (hf_meas : ∀ (i : ), Measurable (f i)) (n : ) :
ProbabilityTheory.IndepFun (j, f j) (f n) μ
theorem ProbabilityTheory.iIndepSet.iIndepFun_indicator {Ω : Type u_1} {ι : Type u_2} {β : Type u_6} {_mΩ : } {μ : } [Zero β] [One β] {m : } {s : ιSet Ω} (hs : ) :
ProbabilityTheory.iIndepFun (fun (_n : ι) => m) (fun (n : ι) => (s n).indicator fun ( : Ω) => 1) μ