|
| 1 | +/- |
| 2 | +Copyright (c) 2025 Oliver Butterley. All rights reserved. |
| 3 | +Released under Apache 2.0 license as described in the file LICENSE. |
| 4 | +Authors: Oliver Butterley, Yoh Tanimoto |
| 5 | +-/ |
| 6 | +module |
| 7 | + |
| 8 | +public import Mathlib.Analysis.Normed.Group.Basic |
| 9 | +public import Mathlib.MeasureTheory.VectorMeasure.Basic |
| 10 | +public import Mathlib.Order.Partition.Finpartition |
| 11 | + |
| 12 | +/-! |
| 13 | +# Pre-variation of a subadditive set function |
| 14 | +
|
| 15 | +Given a σ-subadditive `ℝ≥0∞`-valued set function `f`, we define the pre-variation as the supremum |
| 16 | +over finite measurable partitions of the sum of `f` on the parts. This construction yields a |
| 17 | +measure. |
| 18 | +
|
| 19 | +## Main definitions |
| 20 | +
|
| 21 | +* `IsSigmaSubadditiveSetFun f` — `f` is σ-subadditive on measurable sets |
| 22 | +* `ennrealPreVariation f` — the `VectorMeasure X ℝ≥0∞` built from a σ-subadditive function |
| 23 | +* `preVariation f` — the `Measure X` built from a σ-subadditive function |
| 24 | +
|
| 25 | +## References |
| 26 | +
|
| 27 | +* [Walter Rudin, Real and Complex Analysis.][Rud87] |
| 28 | +
|
| 29 | +-/ |
| 30 | + |
| 31 | +@[expose] public section |
| 32 | + |
| 33 | +variable {X : Type*} [MeasurableSpace X] |
| 34 | + |
| 35 | +open MeasureTheory BigOperators NNReal ENNReal Function |
| 36 | + |
| 37 | +namespace MeasureTheory |
| 38 | + |
| 39 | +/-! |
| 40 | +## Pre-variation of a subadditive `ℝ≥0∞`-valued function |
| 41 | +
|
| 42 | +Given a set function `f : Set X → ℝ≥0∞` we can define another set function by taking the supremum |
| 43 | +over all finite partitions of measurable sets `E i` of the sum of `∑ i, f (E i)`. If `f` is |
| 44 | +σ-subadditive then the function defined is an `ℝ≥0∞`-valued measure. |
| 45 | +-/ |
| 46 | + |
| 47 | +section |
| 48 | + |
| 49 | +variable (f : Set X → ℝ≥0∞) |
| 50 | + |
| 51 | +open Classical in |
| 52 | +/-- If `s` is measurable then `preVariationFun f s` is the supremum over partitions `P` of `s` of |
| 53 | +the quantity `∑ p ∈ P.parts, f p`. If `s` is not measurable then it is set to `0`. -/ |
| 54 | +noncomputable def preVariationFun (s : Set X) : ℝ≥0∞ := |
| 55 | + if h : MeasurableSet s then |
| 56 | + ⨆ (P : Finpartition (⟨s, h⟩ : Subtype MeasurableSet)), ∑ p ∈ P.parts, f p |
| 57 | + else 0 |
| 58 | + |
| 59 | +end |
| 60 | + |
| 61 | +namespace preVariation |
| 62 | + |
| 63 | +variable (f : Set X → ℝ≥0∞) |
| 64 | + |
| 65 | +/-- `preVariationFun` of the empty set is equal to zero. -/ |
| 66 | +lemma empty : preVariationFun f ∅ = 0 := by simp [preVariationFun] |
| 67 | + |
| 68 | +lemma sum_le {s : Set X} (hs : MeasurableSet s) |
| 69 | + (P : Finpartition (⟨s, hs⟩ : Subtype MeasurableSet)) : |
| 70 | + ∑ p ∈ P.parts, f p ≤ preVariationFun f s := by |
| 71 | + simpa [preVariationFun, hs, le_iSup_iff] using fun _ a ↦ a P |
| 72 | + |
| 73 | +open Classical in |
| 74 | +/-- If `P` is a partition of `s₁` and `s₁ ⊆ s₂` then |
| 75 | +`∑ p ∈ P.parts, f p ≤ preVariationFun f s₂`. -/ |
| 76 | +lemma sum_le_preVariationFun_of_subset {s₁ s₂ : Set X} (hs₁ : MeasurableSet s₁) |
| 77 | + (hs₂ : MeasurableSet s₂) (h : s₁ ⊆ s₂) (P : Finpartition (⟨s₁, hs₁⟩ : Subtype MeasurableSet)) : |
| 78 | + ∑ p ∈ P.parts, f p ≤ preVariationFun f s₂ := by |
| 79 | + by_cases heq : s₁ = s₂ |
| 80 | + · rw [← heq]; exact sum_le f hs₁ P |
| 81 | + · let b : Subtype MeasurableSet := ⟨s₂ \ s₁, hs₂.diff hs₁⟩ |
| 82 | + have hb : b ≠ ⊥ := fun hc => heq (h.antisymm (Set.diff_eq_empty.mp (congrArg (·.1) hc))) |
| 83 | + have hab : Disjoint (⟨s₁, hs₁⟩ : Subtype MeasurableSet) b := by |
| 84 | + simp only [b, disjoint_iff, Subtype.ext_iff] |
| 85 | + exact Set.inter_diff_self s₁ s₂ |
| 86 | + have hc : (⟨s₁, hs₁⟩ : Subtype MeasurableSet) ⊔ b = ⟨s₂, hs₂⟩ := |
| 87 | + Subtype.ext (Set.union_diff_cancel h) |
| 88 | + calc ∑ p ∈ P.parts, f p |
| 89 | + _ ≤ ∑ p ∈ (P.extend hb hab hc).parts, f p := |
| 90 | + Finset.sum_le_sum_of_subset fun _ hx => Finset.mem_insert_of_mem hx |
| 91 | + _ ≤ preVariationFun f s₂ := sum_le f hs₂ _ |
| 92 | + |
| 93 | +/-- `preVariationFun` is monotone in terms of the (measurable) set. -/ |
| 94 | +lemma mono {s₁ s₂ : Set X} (hs₂ : MeasurableSet s₂) (h : s₁ ⊆ s₂) : |
| 95 | + preVariationFun f s₁ ≤ preVariationFun f s₂ := by |
| 96 | + by_cases hs₁ : MeasurableSet s₁ |
| 97 | + · have := sum_le_preVariationFun_of_subset f hs₁ hs₂ h |
| 98 | + simp_all [preVariationFun] |
| 99 | + · simp [preVariationFun, hs₁] |
| 100 | + |
| 101 | +lemma exists_Finpartition_sum_gt {s : Set X} (hs : MeasurableSet s) {a : ℝ≥0∞} |
| 102 | + (ha : a < preVariationFun f s) : ∃ P : Finpartition (⟨s, hs⟩ : Subtype MeasurableSet), |
| 103 | + a < ∑ p ∈ P.parts, f p := by |
| 104 | + simp_all [preVariationFun, lt_iSup_iff] |
| 105 | + |
| 106 | +lemma exists_Finpartition_sum_ge {s : Set X} (hs : MeasurableSet s) {ε : ℝ≥0} (hε : 0 < ε) |
| 107 | + (h : preVariationFun f s ≠ ⊤) : |
| 108 | + ∃ P : Finpartition (⟨s, hs⟩ : Subtype MeasurableSet), |
| 109 | + preVariationFun f s ≤ ∑ p ∈ P.parts, f p + ε := by |
| 110 | + let ε' := min ε (preVariationFun f s).toNNReal |
| 111 | + have hε' : ε' ≤ preVariationFun f s := by simp_all [ε'] |
| 112 | + have : ε' ≤ ε := by simp_all [ε'] |
| 113 | + obtain hw | hw : preVariationFun f s ≠ 0 ∨ preVariationFun f s = 0 := ne_or_eq _ _ |
| 114 | + · have : 0 < ε' := by |
| 115 | + simp only [lt_inf_iff, ε'] |
| 116 | + exact ⟨hε, toNNReal_pos hw h⟩ |
| 117 | + let a := preVariationFun f s - ε' |
| 118 | + have ha : a < preVariationFun f s := ENNReal.sub_lt_self h hw (by positivity) |
| 119 | + obtain ⟨P, hP⟩ := exists_Finpartition_sum_gt f hs ha |
| 120 | + use P |
| 121 | + calc preVariationFun f s |
| 122 | + _ = a + ε' := (tsub_add_cancel_of_le hε').symm |
| 123 | + _ ≤ ∑ p ∈ P.parts, f p + ε' := by |
| 124 | + exact (ENNReal.add_le_add_iff_right coe_ne_top).mpr (le_of_lt hP) |
| 125 | + _ ≤ ∑ p ∈ P.parts, f p + ε := by gcongr |
| 126 | + · simp [*] |
| 127 | + |
| 128 | +open Classical in |
| 129 | +/-- The sup of measurable set subtypes over a finset equals the biUnion of the underlying sets. -/ |
| 130 | +lemma Finset.sup_measurableSetSubtype_eq_biUnion {ι : Type*} |
| 131 | + (s : ι → Subtype (@MeasurableSet X _)) (I : Finset ι) : |
| 132 | + ((I.sup s : Subtype MeasurableSet) : Set X) = ⋃ i ∈ I, (s i).val := by |
| 133 | + refine I.induction_on (by simp) ?_ |
| 134 | + intro _ _ _ h |
| 135 | + simp [← h] |
| 136 | + |
| 137 | +open Classical in |
| 138 | +lemma sum_le_preVariationFun_iUnion' {s : ℕ → Set X} (hs : ∀ i, MeasurableSet (s i)) |
| 139 | + (hs' : Pairwise (Disjoint on s)) |
| 140 | + (P : ∀ (i : ℕ), Finpartition (⟨s i, hs i⟩ : Subtype MeasurableSet)) (n : ℕ) : |
| 141 | + ∑ i ∈ Finset.range n, ∑ p ∈ (P i).parts, f p ≤ preVariationFun f (⋃ i, s i) := by |
| 142 | + let s' (i : ℕ) : Subtype MeasurableSet := ⟨s i, hs i⟩ |
| 143 | + have hs_disj : Set.PairwiseDisjoint (Finset.range n : Set ℕ) s' := fun i _ j _ hij => by |
| 144 | + simp only [Function.onFun, disjoint_iff, Subtype.ext_iff] |
| 145 | + exact Set.disjoint_iff_inter_eq_empty.mp (hs' hij) |
| 146 | + let Q := Finpartition.combine P hs_disj |
| 147 | + have hQ_le : (Finset.range n).sup s' ≤ ⟨⋃ i, s i, MeasurableSet.iUnion hs⟩ := by |
| 148 | + rw [← Subtype.coe_le_coe, Finset.sup_measurableSetSubtype_eq_biUnion s'] |
| 149 | + exact Set.iUnion₂_subset fun i _ => Set.subset_iUnion s i |
| 150 | + let R := Q.extendOfLE hQ_le |
| 151 | + calc ∑ i ∈ Finset.range n, ∑ p ∈ (P i).parts, f p |
| 152 | + _ = ∑ p ∈ Q.parts, f p := (Finpartition.sum_combine P hs_disj (fun p => f p)).symm |
| 153 | + _ ≤ ∑ p ∈ R.parts, f p := Finset.sum_le_sum_of_subset (Q.parts_subset_extendOfLE hQ_le) |
| 154 | + _ ≤ preVariationFun f (⋃ i, s i) := sum_le f (MeasurableSet.iUnion hs) R |
| 155 | + |
| 156 | +lemma sum_le_preVariationFun_iUnion {s : ℕ → Set X} (hs : ∀ i, MeasurableSet (s i)) |
| 157 | + (hs' : Pairwise (Disjoint on s)) : |
| 158 | + ∑' i, preVariationFun f (s i) ≤ preVariationFun f (⋃ i, s i) := by |
| 159 | + refine ENNReal.tsum_le_of_sum_range_le fun n ↦ ?_ |
| 160 | + by_cases hn : n = 0 |
| 161 | + · simp [hn] |
| 162 | + refine ENNReal.le_of_forall_pos_le_add fun ε' hε' hsnetop ↦ ?_ |
| 163 | + let ε := ε' / n |
| 164 | + have hε : 0 < ε := by positivity |
| 165 | + have hs'' i : preVariationFun f (s i) ≠ ⊤ := lt_top_iff_ne_top.mp <| |
| 166 | + (mono f (MeasurableSet.iUnion hs) (Set.subset_iUnion s i)).trans_lt hsnetop |
| 167 | + -- For each set `s i` we choose a Finpartition `P i` such that, for each `i`, |
| 168 | + -- `preVariationFun f (s i) ≤ ∑ p ∈ (P i), f p + ε`. |
| 169 | + choose P hP using fun i ↦ exists_Finpartition_sum_ge f (hs i) (hε) (hs'' i) |
| 170 | + calc ∑ i ∈ Finset.range n, preVariationFun f (s i) |
| 171 | + _ ≤ ∑ i ∈ Finset.range n, (∑ p ∈ (P i).parts, f p + ε) := Finset.sum_le_sum fun i _ => hP i |
| 172 | + _ = ∑ i ∈ Finset.range n, ∑ p ∈ (P i).parts, f p + ε' := by |
| 173 | + rw [Finset.sum_add_distrib]; norm_cast |
| 174 | + simp [show n * ε = ε' by rw [mul_div_cancel₀ _ (by positivity)]] |
| 175 | + _ ≤ preVariationFun f (⋃ i, s i) + ε' := by |
| 176 | + gcongr; exact sum_le_preVariationFun_iUnion' f hs hs' P n |
| 177 | + |
| 178 | +end preVariation |
| 179 | + |
| 180 | +/-- A set function is σ-subadditive on measurable sets if the value assigned to the union of a |
| 181 | +countable disjoint family of measurable sets is bounded above by the sum of values on the family. -/ |
| 182 | +def IsSigmaSubadditiveSetFun (f : Set X → ℝ≥0∞) : Prop := |
| 183 | + ∀ (s : ℕ → {t : Set X // MeasurableSet t}), Pairwise (Disjoint on (Subtype.val ∘ s)) → |
| 184 | + f (⋃ i, (s i).val) ≤ ∑' i, f (s i) |
| 185 | + |
| 186 | +namespace preVariation |
| 187 | + |
| 188 | +variable {f : Set X → ℝ≥0∞} |
| 189 | + |
| 190 | +open Classical in |
| 191 | +/-- Additivity of `preVariationFun` for disjoint measurable sets. -/ |
| 192 | +lemma iUnion (hf : IsSigmaSubadditiveSetFun f) (hf' : f ∅ = 0) (s : ℕ → Set X) |
| 193 | + (hs : ∀ i, MeasurableSet (s i)) (hs' : Pairwise (Disjoint on s)) : |
| 194 | + HasSum (fun i ↦ preVariationFun f (s i)) (preVariationFun f (⋃ i, s i)) := by |
| 195 | + refine ENNReal.summable.hasSum_iff.mpr (le_antisymm (sum_le_preVariationFun_iUnion f hs hs') ?_) |
| 196 | + refine ENNReal.le_tsum_of_forall_lt_exists_sum fun b hb ↦ ?_ |
| 197 | + simp only [preVariationFun, MeasurableSet.iUnion hs, reduceDIte, lt_iSup_iff] at hb |
| 198 | + obtain ⟨Q, hQ⟩ := hb |
| 199 | + let s' (i : ℕ) : Subtype MeasurableSet := ⟨s i, hs i⟩ |
| 200 | + let P (i : ℕ) := Q.restrict (b := s' i) (Set.subset_iUnion s i) |
| 201 | + have splitting : ∑ q ∈ Q.parts, f q ≤ ∑' i, ∑ p ∈ (P i).parts, f p := by |
| 202 | + calc ∑ q ∈ Q.parts, f q |
| 203 | + _ ≤ ∑ q ∈ Q.parts, ∑' i, f (q ⊓ s' i) := by |
| 204 | + apply Finset.sum_le_sum fun q hq => ?_ |
| 205 | + have hq_eq : q.val = ⋃ i, q.val ∩ s i := by |
| 206 | + rw [← Set.inter_iUnion]; exact (Set.inter_eq_left.mpr (Q.le hq)).symm |
| 207 | + let t (i : ℕ) : Subtype MeasurableSet := ⟨q.val ∩ s i, q.2.inter (hs i)⟩ |
| 208 | + have ht_disj : Pairwise (Disjoint on (Subtype.val ∘ t)) := |
| 209 | + fun i j hij => (hs' hij).mono Set.inter_subset_right Set.inter_subset_right |
| 210 | + calc f q |
| 211 | + _ = f (⋃ i, q.val ∩ s i) := congrArg f hq_eq |
| 212 | + _ = f (⋃ i, (t i).val) := rfl |
| 213 | + _ ≤ ∑' i, f (t i) := hf t ht_disj |
| 214 | + _ = ∑' i, f (q ⊓ s' i) := rfl |
| 215 | + _ = ∑' i, ∑ q ∈ Q.parts, f (q ⊓ s' i) := |
| 216 | + (Summable.tsum_finsetSum (fun _ _ ↦ ENNReal.summable)).symm |
| 217 | + _ = ∑' i, ∑ p ∈ (P i).parts, f p := by |
| 218 | + congr 1; funext i |
| 219 | + exact (Q.sum_restrict _ (fun p => f p) hf').symm |
| 220 | + obtain ⟨n, hn⟩ := lt_iSup_iff.mp <| ENNReal.tsum_eq_iSup_nat ▸ lt_of_lt_of_le hQ splitting |
| 221 | + have bound (i : ℕ) : ∑ p ∈ (P i).parts, f p ≤ preVariationFun f (s i) := sum_le f (hs i) (P i) |
| 222 | + exact ⟨Finset.range n, lt_of_lt_of_le hn (Finset.sum_le_sum fun i _ => bound i)⟩ |
| 223 | + |
| 224 | +end preVariation |
| 225 | + |
| 226 | +/-! |
| 227 | +## Construction of measures from σ-subadditive functions |
| 228 | +-/ |
| 229 | + |
| 230 | +variable (f : Set X → ℝ≥0∞) |
| 231 | + |
| 232 | +/-- The `VectorMeasure X ℝ≥0∞` built from a σ-subadditive function. -/ |
| 233 | +noncomputable def ennrealPreVariation (hf : IsSigmaSubadditiveSetFun f) (hf' : f ∅ = 0) : |
| 234 | + VectorMeasure X ℝ≥0∞ where |
| 235 | + measureOf' := preVariationFun f |
| 236 | + empty' := preVariation.empty f |
| 237 | + not_measurable' _ h := by simp [preVariationFun, h] |
| 238 | + m_iUnion' := preVariation.iUnion hf hf' |
| 239 | + |
| 240 | +/-- The `Measure X` built from a σ-subadditive function. -/ |
| 241 | +noncomputable def preVariation (hf : IsSigmaSubadditiveSetFun f) (hf' : f ∅ = 0) : Measure X := |
| 242 | + (ennrealPreVariation f hf hf').ennrealToMeasure |
| 243 | + |
| 244 | +end MeasureTheory |
0 commit comments