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>

docs/undergrad.yaml

@@ -531,9 +531,9 @@ Probability Theory:
   Definitions of a probability space:
     probability measure: 'measure_theory.probability_measure'
     events:
-    independent events:
+    independent events: 'probability_theory.Indep_set'
     sigma-algebra: 'measurable_space'
-    independent sigma-algebra:
+    independent sigma-algebra: 'probability_theory.Indep'
     $0$-$1$ law:
     Borel-Cantelli lemma (easy direction): 'measure_theory.measure_limsup_eq_zero'
     Borel-Cantelli lemma (difficult direction):
@@ -544,7 +544,7 @@ Probability Theory:
     absolute continuity of probability laws:
     probability density function:
     law of joint probability:
-    independence of random variables:
+    independence of random variables: 'probability_theory.Indep_fun'
     mean and variance of a real-valued random variable:
     transfer theorem:
     moments:

src/measure_theory/measure_space.lean

@@ -1698,6 +1698,15 @@ lemma measure.finite_at_nhds [topological_space α] (μ : measure α)
   μ.finite_at_filter (𝓝 x) :=
 locally_finite_measure.finite_at_nhds x
 
+lemma measure.smul_finite {α : Type*} [measurable_space α] (μ : measure α) [finite_measure μ]
+  {c : ennreal} (hc : c < ⊤) :
+  finite_measure (c • μ) :=
+begin
+  refine ⟨_⟩,
+  rw measure.smul_apply,
+  exact ennreal.mul_lt_top hc (measure_lt_top μ set.univ),
+end
+
 lemma measure.exists_is_open_measure_lt_top [topological_space α] (μ : measure α)
   [locally_finite_measure μ] (x : α) :
   ∃ s : set α, x ∈ s ∧ is_open s ∧ μ s < ⊤ :=
@@ -1716,18 +1725,39 @@ begin
   rwa sUnion_image
 end
 
+/-- If two finite measures give the same mass to the whole space and coincide on a π-system made
+of measurable sets, then they coincide on all sets in the σ-algebra generated by the π-system. -/
+lemma ext_on_measurable_space_of_generate_finite {α} (m₀ : measurable_space α)
+  {μ ν : measure α} [finite_measure μ]
+  (C : set (set α)) (hμν : ∀ s ∈ C, μ s = ν s) {m : measurable_space α}
+  (h : m ≤ m₀) (hA : m = measurable_space.generate_from C) (hC : is_pi_system C)
+  (h_univ : μ set.univ = ν set.univ) {s : set α} (hs : m.is_measurable' s) :
+  μ s = ν s :=
+begin
+  haveI : @finite_measure _ m₀ ν := begin
+     constructor,
+     rw ← h_univ,
+     apply finite_measure.measure_univ_lt_top,
+  end,
+  refine induction_on_inter hA hC (by simp) hμν _ _ hs,
+  { intros t h1t h2t,
+    have h1t_ : @is_measurable α m₀ t, from h _ h1t,
+    rw [@measure_compl α m₀ μ t h1t_ (@measure_lt_top α m₀ μ _ t),
+      @measure_compl α m₀ ν t h1t_ (@measure_lt_top α m₀ ν _ t), h_univ, h2t], },
+  { intros f h1f h2f h3f,
+    have h2f_ : ∀ (i : ℕ), @is_measurable α m₀ (f i), from (λ i, h _ (h2f i)),
+    have h_Union : @is_measurable α m₀ (⋃ (i : ℕ), f i),from @is_measurable.Union α ℕ m₀ _ f h2f_,
+    simp [measure_Union, h_Union, h1f, h3f, h2f_], },
+end
+
 /-- Two finite measures are equal if they are equal on the π-system generating the σ-algebra
   (and `univ`). -/
 lemma ext_of_generate_finite (C : set (set α)) (hA : _inst_1 = generate_from C)
-  (hC : is_pi_system C) {μ ν : measure α}
-  [finite_measure μ] [finite_measure ν] (hμν : ∀ s ∈ C, μ s = ν s) (h_univ : μ univ = ν univ) :
+  (hC : is_pi_system C) {μ ν : measure α} [finite_measure μ]
+  (hμν : ∀ s ∈ C, μ s = ν s) (h_univ : μ univ = ν univ) :
   μ = ν :=
-begin
-  ext1 s hs,
-  refine induction_on_inter hA hC (by simp) hμν _ _ hs,
-  { rintros t h1t h2t, change is_measurable t at h1t, simp [measure_compl, measure_lt_top, *] },
-  { rintros f h1f h2f h3f, simp [measure_Union, is_measurable.Union, *] }
-end
+measure.ext (λ s hs,
+  ext_on_measurable_space_of_generate_finite _inst_1 C hμν (le_refl _inst_1) hA hC h_univ hs)
 
 namespace measure
 

src/probability_theory/independence.lean

@@ -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