feat(measure_theory/pi_system) lemmas for pi_system, useful for independence. (#6353)

The goal here is to prove that the expectation of a product of an finite number of independent random variables equals the production of the expectations.

See https://github.com/leanprover-community/mathlib/tree/mzinkevi_independent_finite_alt




Co-authored-by: mzinkevi <41597957+mzinkevi@users.noreply.github.com>
Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>

Author: mzinkevi

src/measure_theory/measurable_space.lean

@@ -35,17 +35,6 @@ the equivalence are measurable functions.
 We say that a filter `f` is measurably generated if every set `s ∈ f` includes a measurable
 set `t ∈ f`. This property is useful, e.g., to extract a measurable witness of `filter.eventually`.
 
-## Main statements
-
-The main theorem of this file is Dynkin's π-λ theorem, which appears
-here as an induction principle `induction_on_inter`. Suppose `s` is a
-collection of subsets of `α` such that the intersection of two members
-of `s` belongs to `s` whenever it is nonempty. Let `m` be the σ-algebra
-generated by `s`. In order to check that a predicate `C` holds on every
-member of `m`, it suffices to check that `C` holds on the members of `s` and
-that `C` is preserved by complementation and *disjoint* countable
-unions.
-
 ## Notation
 
 * We write `α ≃ᵐ β` for measurable equivalences between the measurable spaces `α` and `β`.
@@ -1137,198 +1126,6 @@ noncomputable def pi_measurable_equiv_tprod {l : list δ'} (hnd : l.nodup) (h :
 
 end measurable_equiv
 
-/-- A pi-system is a collection of subsets of `α` that is closed under intersections of sets that
-  are not disjoint. Usually it is also required that the collection is nonempty, but we don't do
-  that here. -/
-def is_pi_system {α} (C : set (set α)) : Prop :=
-∀ s t ∈ C, (s ∩ t : set α).nonempty → s ∩ t ∈ C
-
-namespace measurable_space
-
-lemma is_pi_system_measurable_set [measurable_space α] :
-  is_pi_system {s : set α | measurable_set s} :=
-λ s t hs ht _, hs.inter ht
-
-/-- A Dynkin system is a collection of subsets of a type `α` that contains the empty set,
-  is closed under complementation and under countable union of pairwise disjoint sets.
-  The disjointness condition is the only difference with `σ`-algebras.
-
-  The main purpose of Dynkin systems is to provide a powerful induction rule for σ-algebras
-  generated by intersection stable set systems.
-
-  A Dynkin system is also known as a "λ-system" or a "d-system".
--/
-structure dynkin_system (α : Type*) :=
-(has : set α → Prop)
-(has_empty : has ∅)
-(has_compl : ∀ {a}, has a → has aᶜ)
-(has_Union_nat : ∀ {f : ℕ → set α}, pairwise (disjoint on f) → (∀ i, has (f i)) → has (⋃ i, f i))
-
-namespace dynkin_system
-
-@[ext] lemma ext : ∀ {d₁ d₂ : dynkin_system α}, (∀ s : set α, d₁.has s ↔ d₂.has s) → d₁ = d₂
-| ⟨s₁, _, _, _⟩ ⟨s₂, _, _, _⟩ h := have s₁ = s₂, from funext $ assume x, propext $ h x,
-  by subst this
-
-variable (d : dynkin_system α)
-
-lemma has_compl_iff {a} : d.has aᶜ ↔ d.has a :=
-⟨λ h, by simpa using d.has_compl h, λ h, d.has_compl h⟩
-
-lemma has_univ : d.has univ :=
-by simpa using d.has_compl d.has_empty
-
-theorem has_Union {β} [encodable β] {f : β → set α}
-  (hd : pairwise (disjoint on f)) (h : ∀ i, d.has (f i)) : d.has (⋃ i, f i) :=
-by { rw ← encodable.Union_decode2, exact
-  d.has_Union_nat (Union_decode2_disjoint_on hd)
-    (λ n, encodable.Union_decode2_cases d.has_empty h) }
-
-theorem has_union {s₁ s₂ : set α}
-  (h₁ : d.has s₁) (h₂ : d.has s₂) (h : s₁ ∩ s₂ ⊆ ∅) : d.has (s₁ ∪ s₂) :=
-by { rw union_eq_Union, exact
-  d.has_Union (pairwise_disjoint_on_bool.2 h) (bool.forall_bool.2 ⟨h₂, h₁⟩) }
-
-lemma has_diff {s₁ s₂ : set α} (h₁ : d.has s₁) (h₂ : d.has s₂) (h : s₂ ⊆ s₁) : d.has (s₁ \ s₂) :=
-begin
-  apply d.has_compl_iff.1,
-  simp [diff_eq, compl_inter],
-  exact d.has_union (d.has_compl h₁) h₂ (λ x ⟨h₁, h₂⟩, h₁ (h h₂)),
-end
-
-instance : partial_order (dynkin_system α) :=
-{ le          := λ m₁ m₂, m₁.has ≤ m₂.has,
-  le_refl     := assume a b, le_refl _,
-  le_trans    := assume a b c, le_trans,
-  le_antisymm := assume a b h₁ h₂, ext $ assume s, ⟨h₁ s, h₂ s⟩ }
-
-/-- Every measurable space (σ-algebra) forms a Dynkin system -/
-def of_measurable_space (m : measurable_space α) : dynkin_system α :=
-{ has       := m.measurable_set',
-  has_empty := m.measurable_set_empty,
-  has_compl := m.measurable_set_compl,
-  has_Union_nat := assume f _ hf, m.measurable_set_Union f hf }
-
-lemma of_measurable_space_le_of_measurable_space_iff {m₁ m₂ : measurable_space α} :
-  of_measurable_space m₁ ≤ of_measurable_space m₂ ↔ m₁ ≤ m₂ :=
-iff.rfl
-
-/-- The least Dynkin system containing a collection of basic sets.
-  This inductive type gives the underlying collection of sets. -/
-inductive generate_has (s : set (set α)) : set α → Prop
-| basic : ∀ t ∈ s, generate_has t
-| empty : generate_has ∅
-| compl : ∀ {a}, generate_has a → generate_has aᶜ
-| Union : ∀ {f : ℕ → set α}, pairwise (disjoint on f) →
-    (∀ i, generate_has (f i)) → generate_has (⋃ i, f i)
-
-lemma generate_has_compl {C : set (set α)} {s : set α} : generate_has C sᶜ ↔ generate_has C s :=
-by { refine ⟨_, generate_has.compl⟩, intro h, convert generate_has.compl h, simp }
-
-/-- The least Dynkin system containing a collection of basic sets. -/
-def generate (s : set (set α)) : dynkin_system α :=
-{ has := generate_has s,
-  has_empty := generate_has.empty,
-  has_compl := assume a, generate_has.compl,
-  has_Union_nat := assume f, generate_has.Union }
-
-lemma generate_has_def {C : set (set α)} : (generate C).has = generate_has C := rfl
-
-instance : inhabited (dynkin_system α) := ⟨generate univ⟩
-
-/-- If a Dynkin system is closed under binary intersection, then it forms a `σ`-algebra. -/
-def to_measurable_space (h_inter : ∀ s₁ s₂, d.has s₁ → d.has s₂ → d.has (s₁ ∩ s₂)) :=
-{ measurable_space .
-  measurable_set'      := d.has,
-  measurable_set_empty := d.has_empty,
-  measurable_set_compl := assume s h, d.has_compl h,
-  measurable_set_Union := assume f hf,
-    have ∀ n, d.has (disjointed f n),
-      from assume n, disjointed_induct (hf n)
-        (assume t i h, h_inter _ _ h $ d.has_compl $ hf i),
-    have d.has (⋃ n, disjointed f n), from d.has_Union disjoint_disjointed this,
-    by rwa [Union_disjointed] at this }
-
-lemma of_measurable_space_to_measurable_space
-  (h_inter : ∀ s₁ s₂, d.has s₁ → d.has s₂ → d.has (s₁ ∩ s₂)) :
-  of_measurable_space (d.to_measurable_space h_inter) = d :=
-ext $ assume s, iff.rfl
-
-/-- If `s` is in a Dynkin system `d`, we can form the new Dynkin system `{s ∩ t | t ∈ d}`. -/
-def restrict_on {s : set α} (h : d.has s) : dynkin_system α :=
-{ has       := λ t, d.has (t ∩ s),
-  has_empty := by simp [d.has_empty],
-  has_compl := assume t hts,
-    have tᶜ ∩ s = ((t ∩ s)ᶜ) \ sᶜ,
-      from set.ext $ assume x, by { by_cases x ∈ s; simp [h] },
-    by { rw [this], exact d.has_diff (d.has_compl hts) (d.has_compl h)
-      (compl_subset_compl.mpr $ inter_subset_right _ _) },
-  has_Union_nat := assume f hd hf,
-    begin
-      rw [inter_comm, inter_Union],
-      apply d.has_Union_nat,
-      { exact λ i j h x ⟨⟨_, h₁⟩, _, h₂⟩, hd i j h ⟨h₁, h₂⟩ },
-      { simpa [inter_comm] using hf },
-    end }
-
-lemma generate_le {s : set (set α)} (h : ∀ t ∈ s, d.has t) : generate s ≤ d :=
-λ t ht, ht.rec_on h d.has_empty
-  (assume a _ h, d.has_compl h)
-  (assume f hd _ hf, d.has_Union hd hf)
-
-lemma generate_has_subset_generate_measurable {C : set (set α)} {s : set α}
-  (hs : (generate C).has s) : (generate_from C).measurable_set' s :=
-generate_le (of_measurable_space (generate_from C)) (λ t, measurable_set_generate_from) s hs
-
-lemma generate_inter {s : set (set α)}
-  (hs : is_pi_system s) {t₁ t₂ : set α}
-  (ht₁ : (generate s).has t₁) (ht₂ : (generate s).has t₂) : (generate s).has (t₁ ∩ t₂) :=
-have generate s ≤ (generate s).restrict_on ht₂,
-  from generate_le _ $ assume s₁ hs₁,
-  have (generate s).has s₁, from generate_has.basic s₁ hs₁,
-  have generate s ≤ (generate s).restrict_on this,
-    from generate_le _ $ assume s₂ hs₂,
-      show (generate s).has (s₂ ∩ s₁), from
-        (s₂ ∩ s₁).eq_empty_or_nonempty.elim
-        (λ h,  h.symm ▸ generate_has.empty)
-        (λ h, generate_has.basic _ (hs _ _ hs₂ hs₁ h)),
-  have (generate s).has (t₂ ∩ s₁), from this _ ht₂,
-  show (generate s).has (s₁ ∩ t₂), by rwa [inter_comm],
-this _ ht₁
-
-/--
-  If we have a collection of sets closed under binary intersections, then the Dynkin system it
-  generates is equal to the σ-algebra it generates.
-  This result is known as the π-λ theorem.
-  A collection of sets closed under binary intersection is called a "π-system" if it is non-empty.
--/
-lemma generate_from_eq {s : set (set α)} (hs : is_pi_system s) :
-  generate_from s = (generate s).to_measurable_space (assume t₁ t₂, generate_inter hs) :=
-le_antisymm
-  (generate_from_le $ assume t ht, generate_has.basic t ht)
-  (of_measurable_space_le_of_measurable_space_iff.mp $
-    by { rw [of_measurable_space_to_measurable_space],
-    exact (generate_le _ $ assume t ht, measurable_set_generate_from ht) })
-
-end dynkin_system
-
-lemma induction_on_inter {C : set α → Prop} {s : set (set α)} [m : measurable_space α]
-  (h_eq : m = generate_from s)
-  (h_inter : is_pi_system s)
-  (h_empty : C ∅) (h_basic : ∀ t ∈ s, C t) (h_compl : ∀ t, measurable_set t → C t → C tᶜ)
-  (h_union : ∀ f : ℕ → set α, pairwise (disjoint on f) →
-    (∀ i, measurable_set (f i)) → (∀ i, C (f i)) → C (⋃ i, f i)) :
-  ∀ ⦃t⦄, measurable_set t → C t :=
-have eq : measurable_set = dynkin_system.generate_has s,
-  by { rw [h_eq, dynkin_system.generate_from_eq h_inter], refl },
-assume t ht,
-have dynkin_system.generate_has s t, by rwa [eq] at ht,
-this.rec_on h_basic h_empty
-  (assume t ht, h_compl t $ by { rw [eq], exact ht })
-  (assume f hf ht, h_union f hf $ assume i, by { rw [eq], exact ht _ })
-
-end measurable_space
-
 namespace filter
 
 variables [measurable_space α]

src/measure_theory/outer_measure.lean

@@ -5,6 +5,7 @@ Authors: Johannes Hölzl, Mario Carneiro
 -/
 import analysis.specific_limits
 import measure_theory.measurable_space
+import measure_theory.pi_system
 import topology.algebra.infinite_sum
 
 /-!