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 in 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 in 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 Ω} [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 [MeasurableSpace Ω], and not m₁ or m₂.

References #

Williams, David. Probability with martingales. Cambridge university press, 1991. Part A, Chapter 4.

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

Main statements #

Implementation notes #

References #

Deducing Indep from iIndep #

π-system lemma #

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

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

Independence of measurable sets #

Independence of random variables #

Deducing `Indep` from `iIndep` #