feat(MeasureTheory): additive contents on rings of sets (#20977)

Two main results: - a function on a ring of sets which is additive on pairs of disjoint sets defines an additive content - if an additive content is continuous at `∅`, then its value on a countable disjoint union is the sum of the values Co-authored-by: Peter Pfaffelhuber Co-authored-by: Sébastien Gouëzel Part of the formalization of Kolmogorov's extension theorem. Co-authored-by: Remy Degenne <[email protected]>
leanprover-community · Jan 24, 2025 · 8a9bd06 · 8a9bd06
1 parent 5fb85e0
commit 8a9bd06
Show file tree

Hide file tree

Showing 5 changed files with 142 additions and 10 deletions.
diff --git a/Mathlib/Data/Nat/Lattice.lean b/Mathlib/Data/Nat/Lattice.lean
@@ -3,6 +3,7 @@ Copyright (c) 2018 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Floris van Doorn, Gabriel Ebner, Yury Kudryashov
 -/
+import Mathlib.Data.Set.Accumulate
 import Mathlib.Order.ConditionallyCompleteLattice.Finset
 import Mathlib.Order.Interval.Finset.Nat
 
@@ -235,4 +236,7 @@ theorem biInter_le_succ (u : ℕ → Set α) (n : ℕ) : ⋂ k ≤ n + 1, u k =
 theorem biInter_le_succ' (u : ℕ → Set α) (n : ℕ) : ⋂ k ≤ n + 1, u k = u 0 ∩ ⋂ k ≤ n, u (k + 1) :=
   Nat.iInf_le_succ' u n
 
+theorem accumulate_succ (u : ℕ → Set α) (n : ℕ) :
+    Accumulate u (n + 1) = Accumulate u n ∪ u (n + 1) := biUnion_le_succ u n
+
 end Set
diff --git a/Mathlib/Data/Set/Accumulate.lean b/Mathlib/Data/Set/Accumulate.lean
@@ -52,4 +52,16 @@ theorem iUnion_accumulate [Preorder α] : ⋃ x, Accumulate s x = ⋃ x, s x :=
     exact ⟨x', hz⟩
   · exact iUnion_mono fun i => subset_accumulate
 
+@[simp]
+lemma accumulate_zero_nat (s : ℕ → Set β) : Accumulate s 0 = s 0 := by
+  simp [accumulate_def]
+
+open Function in
+theorem disjoint_accumulate [Preorder α] (hs : Pairwise (Disjoint on s)) {i j : α} (hij : i < j) :
+    Disjoint (Accumulate s i) (s j) := by
+  apply disjoint_left.2 (fun x hx ↦ ?_)
+  simp only [Accumulate, mem_iUnion, exists_prop] at hx
+  rcases hx with ⟨k, hk, hx⟩
+  exact disjoint_left.1 (hs (hk.trans_lt hij).ne) hx
+
 end Set
diff --git a/Mathlib/MeasureTheory/Measure/AddContent.lean b/Mathlib/MeasureTheory/Measure/AddContent.lean
@@ -3,9 +3,9 @@ Copyright (c) 2024 Rémy Degenne. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Rémy Degenne, Peter Pfaffelhuber
 -/
-import Mathlib.Algebra.BigOperators.Group.Finset.Basic
-import Mathlib.Data.ENNReal.Basic
 import Mathlib.MeasureTheory.SetSemiring
+import Mathlib.Topology.Algebra.InfiniteSum.Defs
+import Mathlib.Topology.Instances.ENNReal.Lemmas
 
 /-!
 # Additive Contents
@@ -37,12 +37,16 @@ If `C` is a set ring (`MeasureTheory.IsSetRing C`), we have, for `s, t ∈ C`,
 
 * `MeasureTheory.addContent_union_le`: `m (s ∪ t) ≤ m s + m t`
 * `MeasureTheory.addContent_le_diff`: `m s - m t ≤ m (s \ t)`
+* `IsSetRing.addContent_of_union`: a function on a ring of sets which is additive on pairs of
+disjoint sets defines an additive content
+* `addContent_iUnion_eq_sum_of_tendsto_zero`: if an additive content is continuous at `∅`, then
+its value on a countable disjoint union is the sum of the values
 
 -/
 
-open Set Finset
+open Set Finset Function Filter
 
-open scoped ENNReal
+open scoped ENNReal Topology
 
 namespace MeasureTheory
 
@@ -157,9 +161,10 @@ lemma addContent_biUnion_le {ι : Type*} (hC : IsSetRing C) {s : ι → Set α}
     {S : Finset ι} (hs : ∀ n ∈ S, s n ∈ C) :
     m (⋃ i ∈ S, s i) ≤ ∑ i ∈ S, m (s i) := by
   classical
-  induction' S using Finset.induction with i S hiS h hs
-  · simp
-  · rw [Finset.sum_insert hiS]
+  induction S using Finset.induction with
+  | empty => simp
+  | @insert i S hiS h =>
+    rw [Finset.sum_insert hiS]
     simp_rw [← Finset.mem_coe, Finset.coe_insert, Set.biUnion_insert]
     simp only [Finset.mem_insert, forall_eq_or_imp] at hs
     refine (addContent_union_le hC hs.1 (hC.biUnion_mem S hs.2)).trans ?_
@@ -173,6 +178,82 @@ lemma le_addContent_diff (m : AddContent C) (hC : IsSetRing C) (hs : s ∈ C) (h
   rw [tsub_eq_zero_of_le
     (addContent_mono hC.isSetSemiring (hC.inter_mem hs ht) ht inter_subset_right), add_zero]
 
+lemma addContent_diff_of_ne_top (m : AddContent C) (hC : IsSetRing C)
+    (hm_ne_top : ∀ s ∈ C, m s ≠ ∞)
+    {s t : Set α} (hs : s ∈ C) (ht : t ∈ C) (hts : t ⊆ s) :
+    m (s \ t) = m s - m t := by
+  have h_union : m (t ∪ s \ t) = m t + m (s \ t) :=
+    addContent_union hC ht (hC.diff_mem hs ht) disjoint_sdiff_self_right
+  simp_rw [Set.union_diff_self, Set.union_eq_right.mpr hts] at h_union
+  rw [h_union, ENNReal.add_sub_cancel_left (hm_ne_top _ ht)]
+
+lemma addContent_accumulate (m : AddContent C) (hC : IsSetRing C)
+    {s : ℕ → Set α} (hs_disj : Pairwise (Disjoint on s)) (hsC : ∀ i, s i ∈ C) (n : ℕ) :
+      m (Set.Accumulate s n) = ∑ i in Finset.range (n + 1), m (s i) := by
+  induction n with
+  | zero => simp
+  | succ n hn =>
+    rw [Finset.sum_range_succ, ← hn, Set.accumulate_succ, addContent_union hC _ (hsC _)]
+    · exact Set.disjoint_accumulate hs_disj (Nat.lt_succ_self n)
+    · exact hC.accumulate_mem hsC n
+
+/-- A function which is additive on disjoint elements in a ring of sets `C` defines an
+additive content on `C`. -/
+def IsSetRing.addContent_of_union (m : Set α → ℝ≥0∞) (hC : IsSetRing C) (m_empty : m ∅ = 0)
+    (m_add : ∀ {s t : Set α} (_hs : s ∈ C) (_ht : t ∈ C), Disjoint s t → m (s ∪ t) = m s + m t) :
+    AddContent C where
+  toFun := m
+  empty' := m_empty
+  sUnion' I h_ss h_dis h_mem := by
+    classical
+    induction I using Finset.induction with
+    | empty => simp only [Finset.coe_empty, Set.sUnion_empty, Finset.sum_empty, m_empty]
+    | @insert s I hsI h =>
+      rw [Finset.coe_insert] at *
+      rw [Set.insert_subset_iff] at h_ss
+      rw [Set.pairwiseDisjoint_insert_of_not_mem] at h_dis
+      swap; · exact hsI
+      have h_sUnion_mem : ⋃₀ ↑I ∈ C := by
+        rw [Set.sUnion_eq_biUnion]
+        apply hC.biUnion_mem
+        intro n hn
+        exact h_ss.2 hn
+      rw [Set.sUnion_insert, m_add h_ss.1 h_sUnion_mem (Set.disjoint_sUnion_right.mpr h_dis.2),
+        Finset.sum_insert hsI, h h_ss.2 h_dis.1]
+      rwa [Set.sUnion_insert] at h_mem
+
+/-- In a ring of sets, continuity of an additive content at `∅` implies σ-additivity.
+This is not true in general in semirings, or without the hypothesis that `m` is finite. See the
+examples 7 and 8 in Halmos' book Measure Theory (1974), page 40. -/
+theorem addContent_iUnion_eq_sum_of_tendsto_zero (hC : IsSetRing C) (m : AddContent C)
+    (hm_ne_top : ∀ s ∈ C, m s ≠ ∞)
+    (hm_tendsto : ∀ ⦃s : ℕ → Set α⦄ (_ : ∀ n, s n ∈ C),
+      Antitone s → (⋂ n, s n) = ∅ → Tendsto (fun n ↦ m (s n)) atTop (𝓝 0))
+    ⦃f : ℕ → Set α⦄ (hf : ∀ i, f i ∈ C) (hUf : (⋃ i, f i) ∈ C)
+    (h_disj : Pairwise (Disjoint on f)) :
+    m (⋃ i, f i) = ∑' i, m (f i) := by
+  -- We use the continuity of `m` at `∅` on the sequence `n ↦ (⋃ i, f i) \ (set.accumulate f n)`
+  let s : ℕ → Set α := fun n ↦ (⋃ i, f i) \ Set.Accumulate f n
+  have hCs n : s n ∈ C := hC.diff_mem hUf (hC.accumulate_mem hf n)
+  have h_tendsto : Tendsto (fun n ↦ m (s n)) atTop (𝓝 0) := by
+    refine hm_tendsto hCs ?_ ?_
+    · intro i j hij x hxj
+      rw [Set.mem_diff] at hxj ⊢
+      exact ⟨hxj.1, fun hxi ↦ hxj.2 (Set.monotone_accumulate hij hxi)⟩
+    · simp_rw [s, Set.diff_eq]
+      rw [Set.iInter_inter_distrib, Set.iInter_const, ← Set.compl_iUnion, Set.iUnion_accumulate]
+      exact Set.inter_compl_self _
+  have hmsn n : m (s n) = m (⋃ i, f i) - ∑ i in Finset.range (n + 1), m (f i) := by
+    rw [addContent_diff_of_ne_top m hC hm_ne_top hUf (hC.accumulate_mem hf n)
+      (Set.accumulate_subset_iUnion _), addContent_accumulate m hC h_disj hf n]
+  simp_rw [hmsn] at h_tendsto
+  refine tendsto_nhds_unique ?_ (ENNReal.tendsto_nat_tsum fun i ↦ m (f i))
+  refine (Filter.tendsto_add_atTop_iff_nat 1).mp ?_
+  rwa [ENNReal.tendsto_const_sub_nhds_zero_iff (hm_ne_top _ hUf) (fun n ↦ ?_)] at h_tendsto
+  rw [← addContent_accumulate m hC h_disj hf]
+  exact addContent_mono hC.isSetSemiring (hC.accumulate_mem hf n) hUf
+    (Set.accumulate_subset_iUnion _)
+
 end IsSetRing
 
 end MeasureTheory
diff --git a/Mathlib/MeasureTheory/SetSemiring.lean b/Mathlib/MeasureTheory/SetSemiring.lean
@@ -3,6 +3,8 @@ Copyright (c) 2023 Rémy Degenne. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Rémy Degenne, Peter Pfaffelhuber
 -/
+import Mathlib.Data.Nat.Lattice
+import Mathlib.Data.Set.Accumulate
 import Mathlib.Data.Set.Pairwise.Lattice
 import Mathlib.MeasureTheory.PiSystem
 
@@ -303,9 +305,10 @@ lemma biUnion_mem {ι : Type*} (hC : IsSetRing C) {s : ι → Set α}
     (S : Finset ι) (hs : ∀ n ∈ S, s n ∈ C) :
     ⋃ i ∈ S, s i ∈ C := by
   classical
-  induction' S using Finset.induction with i S _ h hs
-  · simp [hC.empty_mem]
-  · simp_rw [← Finset.mem_coe, Finset.coe_insert, Set.biUnion_insert]
+  induction S using Finset.induction with
+  | empty => simp [hC.empty_mem]
+  | @insert i S _ h =>
+    simp_rw [← Finset.mem_coe, Finset.coe_insert, Set.biUnion_insert]
     refine hC.union_mem (hs i (mem_insert_self i S)) ?_
     exact h (fun n hnS ↦ hs n (mem_insert_of_mem hnS))
 
@@ -341,6 +344,24 @@ lemma disjointed_mem {ι : Type*} [Preorder ι] [LocallyFiniteOrderBot ι]
     disjointed s i ∈ C :=
   disjointedRec (fun _ j ht ↦ hC.diff_mem ht <| hs j) (hs i)
 
+theorem iUnion_le_mem (hC : IsSetRing C) {s : ℕ → Set α} (hs : ∀ n, s n ∈ C) (n : ℕ) :
+    (⋃ i ≤ n, s i) ∈ C := by
+  induction n with
+  | zero => simp [hs 0]
+  | succ n hn => rw [biUnion_le_succ]; exact hC.union_mem hn (hs _)
+
+theorem iInter_le_mem (hC : IsSetRing C) {s : ℕ → Set α} (hs : ∀ n, s n ∈ C) (n : ℕ) :
+    (⋂ i ≤ n, s i) ∈ C := by
+  induction n with
+  | zero => simp [hs 0]
+  | succ n hn => rw [biInter_le_succ]; exact hC.inter_mem hn (hs _)
+
+theorem accumulate_mem (hC : IsSetRing C) {s : ℕ → Set α} (hs : ∀ i, s i ∈ C) (n : ℕ) :
+    Accumulate s n ∈ C := by
+  induction n with
+  | zero => simp [hs 0]
+  | succ n hn => rw [accumulate_succ]; exact hC.union_mem hn (hs _)
+
 end IsSetRing
 
 end MeasureTheory
diff --git a/Mathlib/Topology/Instances/ENNReal/Lemmas.lean b/Mathlib/Topology/Instances/ENNReal/Lemmas.lean
@@ -237,6 +237,20 @@ protected theorem tendsto_nhds_zero {f : Filter α} {u : α → ℝ≥0∞} :
     Tendsto u f (𝓝 0) ↔ ∀ ε > 0, ∀ᶠ x in f, u x ≤ ε :=
   nhds_zero_basis_Iic.tendsto_right_iff
 
+theorem tendsto_const_sub_nhds_zero_iff {l : Filter α} {f : α → ℝ≥0∞} {a : ℝ≥0∞} (ha : a ≠ ∞)
+    (hfa : ∀ n, f n ≤ a) :
+    Tendsto (fun n ↦ a - f n) l (𝓝 0) ↔ Tendsto (fun n ↦ f n) l (𝓝 a) := by
+  rw [ENNReal.tendsto_nhds_zero, ENNReal.tendsto_nhds ha]
+  refine ⟨fun h ε hε ↦ ?_, fun h ε hε ↦ ?_⟩
+  · filter_upwards [h ε hε] with n hn
+    refine ⟨?_, (hfa n).trans (le_add_right le_rfl)⟩
+    rw [tsub_le_iff_right] at hn ⊢
+    rwa [add_comm]
+  · filter_upwards [h ε hε] with n hn
+    have hN_left := hn.1
+    rw [tsub_le_iff_right] at hN_left ⊢
+    rwa [add_comm]
+
 protected theorem tendsto_atTop [Nonempty β] [SemilatticeSup β] {f : β → ℝ≥0∞} {a : ℝ≥0∞}
     (ha : a ≠ ∞) : Tendsto f atTop (𝓝 a) ↔ ∀ ε > 0, ∃ N, ∀ n ≥ N, f n ∈ Icc (a - ε) (a + ε) :=
   .trans (atTop_basis.tendsto_iff (hasBasis_nhds_of_ne_top ha)) (by simp only [true_and]; rfl)