Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
feat(measure_theory/independence): define independence of sets of set…
…s, measurable spaces, sets, functions (#5848) This first PR about independence contains definitions, a few lemmas about independence of unions/intersections of sets of sets, and a proof that two measurable spaces are independent iff generating pi-systems are independent (included in this PR to demonstrate usability of the definitions). Co-authored-by: Rémy Degenne <remydegenne@gmail.com> Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
- Loading branch information
1 parent
e5f9409
commit 78a518a
Showing
3 changed files
with
353 additions
and
11 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,312 @@ | ||
/- | ||
Copyright (c) 2021 Rémy Degenne. All rights reserved. | ||
Released under Apache 2.0 license as described in the file LICENSE. | ||
Author: Rémy Degenne | ||
-/ | ||
import measure_theory.measure_space | ||
import algebra.big_operators.intervals | ||
import data.finset.intervals | ||
|
||
/-! | ||
# 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 : ι → measurable_space α` 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 `measurable_space.comap f m`. | ||
## Main statements | ||
* TODO: `Indep_of_Indep_sets`: if π-systems are independent as sets of sets, then the | ||
measurable space structures they generate are independent. | ||
* `indep_of_indep_sets`: variant with two π-systems. | ||
## Implementation notes | ||
We provide one main definition of independence: | ||
* `Indep_sets`: independence of a family of sets of sets `pi : ι → set (set α)`. | ||
Three other independence notions are defined using `Indep_sets`: | ||
* `Indep`: independence of a family of measurable space structures `m : ι → measurable_space α`, | ||
* `Indep_set`: independence of a family of sets `s : ι → set α`, | ||
* `Indep_fun`: independence of a family of functions. For measurable spaces | ||
`m : Π (i : ι), measurable_space (β 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 a capital letter, for example `indep_fun` is the version of `Indep_fun` | ||
for two functions. | ||
The definition of independence for `Indep_sets` uses finite sets (`finset`). An alternative and | ||
equivalent way of defining independence would have been to use countable sets. | ||
TODO: prove that equivalence. | ||
Most of the definitions and lemma in this file list all variables instead of using the `variables` | ||
keyword at the beginning of a section, for example | ||
`lemma indep.symm {α} {m₁ m₂ : measurable_space α} [measurable_space α] {μ : measure α} ...` . | ||
This is intentional, to be able to control the order of the `measurable_space` variables. Indeed | ||
when defining `μ` in the example above, the measurable space used is the last one defined, here | ||
`[measurable_space α]`, and not `m₁` or `m₂`. | ||
## References | ||
* Williams, David. Probability with martingales. Cambridge university press, 1991. | ||
Part A, Chapter 4. | ||
-/ | ||
|
||
open measure_theory measurable_space | ||
open_locale big_operators classical | ||
|
||
namespace probability_theory | ||
|
||
section definitions | ||
|
||
/-- 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 in s, μ (f i) `. | ||
It will be used for families of pi_systems. -/ | ||
def Indep_sets {α ι} [measurable_space α] (π : ι → set (set α)) (μ : measure α . volume_tac) : | ||
Prop := | ||
∀ (s : finset ι) {f : ι → set α} (H : ∀ i, i ∈ s → f i ∈ π i), μ (⋂ i ∈ s, f i) = ∏ i in s, μ (f i) | ||
|
||
/-- 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₂)` -/ | ||
def indep_sets {α} [measurable_space α] (s1 s2 : set (set α)) (μ : measure α . volume_tac) : Prop := | ||
∀ t1 t2 : set α, t1 ∈ s1 → t2 ∈ s2 → μ (t1 ∩ t2) = μ t1 * μ t2 | ||
|
||
/-- 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 : ι → measurable_space α` 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 in s, μ (f i) `. -/ | ||
def Indep {α ι} (m : ι → measurable_space α) [measurable_space α] (μ : measure α . volume_tac) : | ||
Prop := | ||
Indep_sets (λ x, (m x).is_measurable') μ | ||
|
||
/-- 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₂)` -/ | ||
def indep {α} (m₁ m₂ : measurable_space α) [measurable_space α] (μ : measure α . volume_tac) : | ||
Prop := | ||
indep_sets (m₁.is_measurable') (m₂.is_measurable') μ | ||
|
||
/-- 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`. -/ | ||
def Indep_set {α ι} [measurable_space α] (s : ι → set α) (μ : measure α . volume_tac) : Prop := | ||
Indep (λ i, generate_from {s i}) μ | ||
|
||
/-- 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`. -/ | ||
def indep_set {α} [measurable_space α] {s t : set α} (μ : measure α . volume_tac) : Prop := | ||
indep (generate_from {s}) (generate_from {t}) μ | ||
|
||
/-- 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 `measurable_space.comap g m`. -/ | ||
def Indep_fun {α ι} [measurable_space α] {β : ι → Type*} (m : Π (x : ι), measurable_space (β x)) | ||
(f : Π (x : ι), α → β x) (μ : measure α . volume_tac) : Prop := | ||
Indep (λ x, measurable_space.comap (f x) (m x)) μ | ||
|
||
/-- 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 `measurable_space.comap f m`. -/ | ||
def indep_fun {α β γ} [measurable_space α] (mβ : measurable_space β) (mγ : measurable_space γ) | ||
{f : α → β} {g : α → γ} (μ : measure α . volume_tac) : Prop := | ||
indep (measurable_space.comap f mβ) (measurable_space.comap g mγ) μ | ||
|
||
end definitions | ||
|
||
section indep | ||
|
||
lemma indep_sets.symm {α} {s₁ s₂ : set (set α)} [measurable_space α] {μ : measure α} | ||
(h : indep_sets s₁ s₂ μ) : | ||
indep_sets s₂ s₁ μ := | ||
by { intros t1 t2 ht1 ht2, rw [set.inter_comm, mul_comm], exact h t2 t1 ht2 ht1, } | ||
|
||
lemma indep.symm {α} {m₁ m₂ : measurable_space α} [measurable_space α] {μ : measure α} | ||
(h : indep m₁ m₂ μ) : | ||
indep m₂ m₁ μ := | ||
indep_sets.symm h | ||
|
||
lemma indep_sets_of_indep_sets_of_le_left {α} {s₁ s₂ s₃: set (set α)} [measurable_space α] | ||
{μ : measure α} (h_indep : indep_sets s₁ s₂ μ) (h31 : s₃ ⊆ s₁) : | ||
indep_sets s₃ s₂ μ := | ||
λ t1 t2 ht1 ht2, h_indep t1 t2 (set.mem_of_subset_of_mem h31 ht1) ht2 | ||
|
||
lemma indep_sets_of_indep_sets_of_le_right {α} {s₁ s₂ s₃: set (set α)} [measurable_space α] | ||
{μ : measure α} (h_indep : indep_sets s₁ s₂ μ) (h32 : s₃ ⊆ s₂) : | ||
indep_sets s₁ s₃ μ := | ||
λ t1 t2 ht1 ht2, h_indep t1 t2 ht1 (set.mem_of_subset_of_mem h32 ht2) | ||
|
||
lemma indep_of_indep_of_le_left {α} {m₁ m₂ m₃: measurable_space α} [measurable_space α] | ||
{μ : measure α} (h_indep : indep m₁ m₂ μ) (h31 : m₃ ≤ m₁) : | ||
indep m₃ m₂ μ := | ||
λ t1 t2 ht1 ht2, h_indep t1 t2 (h31 _ ht1) ht2 | ||
|
||
lemma indep_of_indep_of_le_right {α} {m₁ m₂ m₃: measurable_space α} [measurable_space α] | ||
{μ : measure α} (h_indep : indep m₁ m₂ μ) (h32 : m₃ ≤ m₂) : | ||
indep m₁ m₃ μ := | ||
λ t1 t2 ht1 ht2, h_indep t1 t2 ht1 (h32 _ ht2) | ||
|
||
lemma indep_sets.union {α} [measurable_space α] {s₁ s₂ s' : set (set α)} {μ : measure α} | ||
(h₁ : indep_sets s₁ s' μ) (h₂ : indep_sets s₂ s' μ) : | ||
indep_sets (s₁ ∪ s₂) s' μ := | ||
begin | ||
intros t1 t2 ht1 ht2, | ||
cases (set.mem_union _ _ _).mp ht1 with ht1₁ ht1₂, | ||
{ exact h₁ t1 t2 ht1₁ ht2, }, | ||
{ exact h₂ t1 t2 ht1₂ ht2, }, | ||
end | ||
|
||
@[simp] lemma indep_sets.union_iff {α} [measurable_space α] {s₁ s₂ s' : set (set α)} | ||
{μ : measure α} : | ||
indep_sets (s₁ ∪ s₂) s' μ ↔ indep_sets s₁ s' μ ∧ indep_sets s₂ s' μ := | ||
⟨λ h, ⟨indep_sets_of_indep_sets_of_le_left h (set.subset_union_left s₁ s₂), | ||
indep_sets_of_indep_sets_of_le_left h (set.subset_union_right s₁ s₂)⟩, | ||
λ h, indep_sets.union h.left h.right⟩ | ||
|
||
lemma indep_sets.Union {α ι} [measurable_space α] {s : ι → set (set α)} {s' : set (set α)} | ||
{μ : measure α} (hyp : ∀ n, indep_sets (s n) s' μ) : | ||
indep_sets (⋃ n, s n) s' μ := | ||
begin | ||
intros t1 t2 ht1 ht2, | ||
rw set.mem_Union at ht1, | ||
cases ht1 with n ht1, | ||
exact hyp n t1 t2 ht1 ht2, | ||
end | ||
|
||
lemma indep_sets.inter {α} [measurable_space α] {s₁ s' : set (set α)} (s₂ : set (set α)) | ||
{μ : measure α} (h₁ : indep_sets s₁ s' μ) : | ||
indep_sets (s₁ ∩ s₂) s' μ := | ||
λ t1 t2 ht1 ht2, h₁ t1 t2 ((set.mem_inter_iff _ _ _).mp ht1).left ht2 | ||
|
||
lemma indep_sets.Inter {α ι} [measurable_space α] {s : ι → set (set α)} {s' : set (set α)} | ||
{μ : measure α} (h : ∃ n, indep_sets (s n) s' μ) : | ||
indep_sets (⋂ n, s n) s' μ := | ||
by {intros t1 t2 ht1 ht2, cases h with n h, exact h t1 t2 (set.mem_Inter.mp ht1 n) ht2 } | ||
|
||
end indep | ||
|
||
/-! ### Deducing `indep` from `Indep` -/ | ||
section from_Indep_to_indep | ||
|
||
lemma Indep_sets.indep_sets {α ι} {s : ι → set (set α)} [measurable_space α] {μ : measure α} | ||
(h_indep : Indep_sets s μ) {i j : ι} (hij : i ≠ j) : | ||
indep_sets (s i) (s j) μ := | ||
begin | ||
intros t₁ t₂ ht₁ ht₂, | ||
have hf_m : ∀ (x : ι), x ∈ {i, j} → (ite (x=i) t₁ t₂) ∈ s x, | ||
{ intros x hx, | ||
cases finset.mem_insert.mp hx with hx hx, | ||
{ simp [hx, ht₁], }, | ||
{ simp [finset.mem_singleton.mp hx, hij.symm, ht₂], }, }, | ||
have h1 : t₁ = ite (i = i) t₁ t₂, by simp only [if_true, eq_self_iff_true], | ||
have h2 : t₂ = ite (j = i) t₁ t₂, by simp only [hij.symm, if_false], | ||
have h_inter : (⋂ (t : ι) (H : t ∈ ({i, j} : finset ι)), ite (t = i) t₁ t₂) | ||
= (ite (i = i) t₁ t₂) ∩ (ite (j = i) t₁ t₂), | ||
by simp only [finset.set_bInter_singleton, finset.set_bInter_insert], | ||
have h_prod : (∏ (t : ι) in ({i, j} : finset ι), μ (ite (t = i) t₁ t₂)) | ||
= μ (ite (i = i) t₁ t₂) * μ (ite (j = i) t₁ t₂), | ||
by simp only [hij, finset.prod_singleton, finset.prod_insert, not_false_iff, | ||
finset.mem_singleton], | ||
rw h1, | ||
nth_rewrite 1 h2, | ||
nth_rewrite 3 h2, | ||
rw [←h_inter, ←h_prod, h_indep {i, j} hf_m], | ||
end | ||
|
||
lemma Indep.indep {α ι} {m : ι → measurable_space α} [measurable_space α] {μ : measure α} | ||
(h_indep : Indep m μ) {i j : ι} (hij : i ≠ j) : | ||
indep (m i) (m j) μ := | ||
begin | ||
change indep_sets ((λ x, (m x).is_measurable') i) ((λ x, (m x).is_measurable') j) μ, | ||
exact Indep_sets.indep_sets h_indep hij, | ||
end | ||
|
||
end from_Indep_to_indep | ||
|
||
/-! | ||
## π-system lemma | ||
Independence of measurable spaces is equivalent to independence of generating π-systems. | ||
-/ | ||
|
||
section from_measurable_spaces_to_sets_of_sets | ||
/-! ### Independence of measurable space structures implies independence of generating π-systems -/ | ||
|
||
lemma Indep.Indep_sets {α ι} [measurable_space α] {μ : measure α} {m : ι → measurable_space α} | ||
{s : ι → set (set α)} (hms : ∀ n, m n = measurable_space.generate_from (s n)) | ||
(h_indep : Indep m μ) : | ||
Indep_sets s μ := | ||
begin | ||
refine (λ S f hfs, h_indep S (λ x hxS, _)), | ||
simp_rw hms x, | ||
exact is_measurable_generate_from (hfs x hxS), | ||
end | ||
|
||
lemma indep.indep_sets {α} [measurable_space α] {μ : measure α} {s1 s2 : set (set α)} | ||
(h_indep : indep (generate_from s1) (generate_from s2) μ) : | ||
indep_sets s1 s2 μ := | ||
λ t1 t2 ht1 ht2, h_indep t1 t2 (is_measurable_generate_from ht1) (is_measurable_generate_from ht2) | ||
|
||
end from_measurable_spaces_to_sets_of_sets | ||
|
||
section from_pi_systems_to_measurable_spaces | ||
/-! ### Independence of generating π-systems implies independence of measurable space structures -/ | ||
|
||
private lemma indep_sets.indep_aux {α} {m2 : measurable_space α} | ||
{m : measurable_space α} {μ : measure α} [probability_measure μ] {p1 p2 : set (set α)} | ||
(h2 : m2 ≤ m) (hp2 : is_pi_system p2) (hpm2 : m2 = generate_from p2) | ||
(hyp : indep_sets p1 p2 μ) {t1 t2 : set α} (ht1 : t1 ∈ p1) (ht2m : m2.is_measurable' t2) : | ||
μ (t1 ∩ t2) = μ t1 * μ t2 := | ||
begin | ||
let μ_inter := μ.restrict t1, | ||
let ν := (μ t1) • μ, | ||
have h_univ : μ_inter set.univ = ν set.univ, | ||
by rw [measure.restrict_apply_univ, measure.smul_apply, measure_univ, mul_one], | ||
haveI : finite_measure μ_inter := @restrict.finite_measure α _ t1 μ (measure_lt_top μ t1), | ||
rw [set.inter_comm, ←@measure.restrict_apply α _ μ t1 t2 (h2 t2 ht2m)], | ||
refine ext_on_measurable_space_of_generate_finite m p2 (λ t ht, _) h2 hpm2 hp2 h_univ ht2m, | ||
have ht2 : m.is_measurable' t, | ||
{ refine h2 _ _, | ||
rw hpm2, | ||
exact is_measurable_generate_from ht, }, | ||
rw [measure.restrict_apply ht2, measure.smul_apply, set.inter_comm], | ||
exact hyp t1 t ht1 ht, | ||
end | ||
|
||
lemma indep_sets.indep {α} {m1 m2 : measurable_space α} {m : measurable_space α} | ||
{μ : measure α} [probability_measure μ] {p1 p2 : set (set α)} (h1 : m1 ≤ m) (h2 : m2 ≤ m) | ||
(hp1 : is_pi_system p1) (hp2 : is_pi_system p2) (hpm1 : m1 = generate_from p1) | ||
(hpm2 : m2 = generate_from p2) (hyp : indep_sets p1 p2 μ) : | ||
indep m1 m2 μ := | ||
begin | ||
intros t1 t2 ht1 ht2, | ||
let μ_inter := μ.restrict t2, | ||
let ν := (μ t2) • μ, | ||
have h_univ : μ_inter set.univ = ν set.univ, | ||
by rw [measure.restrict_apply_univ, measure.smul_apply, measure_univ, mul_one], | ||
haveI : finite_measure μ_inter := @restrict.finite_measure α _ t2 μ (measure_lt_top μ t2), | ||
rw [mul_comm, ←@measure.restrict_apply α _ μ t2 t1 (h1 t1 ht1)], | ||
refine ext_on_measurable_space_of_generate_finite m p1 (λ t ht, _) h1 hpm1 hp1 h_univ ht1, | ||
have ht1 : m.is_measurable' t, | ||
{ refine h1 _ _, | ||
rw hpm1, | ||
exact is_measurable_generate_from ht, }, | ||
rw [measure.restrict_apply ht1, measure.smul_apply, mul_comm], | ||
exact indep_sets.indep_aux h2 hp2 hpm2 hyp ht ht2, | ||
end | ||
|
||
end from_pi_systems_to_measurable_spaces | ||
|
||
end probability_theory |