|
| 1 | +/- |
| 2 | +Copyright (c) 2026 Etienne Marion. All rights reserved. |
| 3 | +Released under Apache 2.0 license as described in the file LICENSE. |
| 4 | +Authors: Etienne Marion |
| 5 | +-/ |
| 6 | +module |
| 7 | + |
| 8 | +public import Mathlib.MeasureTheory.Integral.Bochner.Basic |
| 9 | + |
| 10 | +import Mathlib.Analysis.Normed.Module.FiniteDimension |
| 11 | + |
| 12 | +/-! |
| 13 | +# Integral with respect to a sum of measures |
| 14 | +
|
| 15 | +In this file we prove that a function `f` is integrable with respect to a countable sum of measures |
| 16 | +`Measure.sum μ` if and only if `f` is integrable with respect to each `μ i` and the sequence |
| 17 | +`fun i ↦ ∫ x, ‖f x‖ ∂μ i` is summable. We then show that under this integrability condition, |
| 18 | +`∫ x, f x ∂Measure.sum μ = ∑' i, ∫ f x ∂μ i`. |
| 19 | +
|
| 20 | +We specialize these results to the case where each measure is a Dirac mass, |
| 21 | +i.e. `μ i = (c i) • .dirac (x i)`. |
| 22 | +
|
| 23 | +Finally we compute integrals over countable and finite spaces or sets. |
| 24 | +
|
| 25 | +## Main statements |
| 26 | +
|
| 27 | +* `integrable_sum_measure_iff`: A function `f` is integrable with respect to a countable sum |
| 28 | + of measures `Measure.sum μ` if and only if `f` is integrable with respect to each `μ i` and the |
| 29 | + sequence `fun i ↦ ∫ x, ‖f x‖ ∂μ i` is summable. |
| 30 | +* `integrable_sum_dirac_iff`: A function `f` is integrable with respect to a countable sum |
| 31 | + of Dirac masses `Measure.sum (fun i ↦ (c i) • Measure.dirac (x i))` if and only if |
| 32 | + the sequence `fun i ↦ (c i).toReal * ‖f (x i)‖` is summable. |
| 33 | +* `hasSum_integral_measure`: If `f` is integrable with respect to `Measure.sum μ`, |
| 34 | + then the sequence `fun i ↦ ∫ x, f x ∂μ i` is summable and its sum is `∫ x, f x ∂Measure.sum μ`. |
| 35 | +* `integral_sum_dirac_eq_tsum`: If the sequence `fun i ↦ (c i).toReal * ‖f (x i)‖` is summable, |
| 36 | + then `∑' i, (c i).toReal • f (x i) = ∫ x, f x, ∂Measure.sum (fun i ↦ (c i) • .dirac (x i))`. |
| 37 | +
|
| 38 | +## Tags |
| 39 | +
|
| 40 | +sum of measures, integral, Dirac mass |
| 41 | +-/ |
| 42 | + |
| 43 | +public section |
| 44 | + |
| 45 | +open Filter Set |
| 46 | +open scoped ENNReal NNReal Topology |
| 47 | + |
| 48 | +namespace MeasureTheory |
| 49 | + |
| 50 | +variable {ι X E : Type*} [Countable ι] {mX : MeasurableSpace X} [NormedAddCommGroup E] |
| 51 | + {μ : ι → Measure X} {f : X → E} |
| 52 | + |
| 53 | +section Integrable |
| 54 | + |
| 55 | +lemma integrable_sum_measure |
| 56 | + (hf : ∀ i, Integrable f (μ i)) (h : Summable (fun i ↦ ∫ x, ‖f x‖ ∂μ i)) : |
| 57 | + Integrable f (Measure.sum μ) := by |
| 58 | + refine ⟨aestronglyMeasurable_sum_measure_iff.mpr fun i ↦ (hf i).aestronglyMeasurable, ?_⟩ |
| 59 | + · rw [HasFiniteIntegral, lintegral_sum_measure] |
| 60 | + convert h.tsum_ofReal_lt_top with i |
| 61 | + rw [ofReal_integral_eq_lintegral_ofReal (hf i).norm] |
| 62 | + · simp_rw [ofReal_norm_eq_enorm] |
| 63 | + · exact ae_of_all _ fun _ ↦ by positivity |
| 64 | + |
| 65 | +omit [Countable ι] in |
| 66 | +lemma Integrable.summable_integral (hf : Integrable f (Measure.sum μ)) : |
| 67 | + Summable (fun i ↦ ∫ x, ‖f x‖ ∂μ i) := by |
| 68 | + convert ENNReal.summable_toReal (f := fun i ↦ ∫⁻ x, ‖f x‖ₑ ∂μ i) ?_ with i |
| 69 | + · rw [← integral_toReal ?_ (by simp)] |
| 70 | + · simp |
| 71 | + · exact (hf.aestronglyMeasurable.mono_measure (Measure.le_sum _ i)).enorm |
| 72 | + rw [← lintegral_sum_measure] |
| 73 | + exact hf.2.ne |
| 74 | + |
| 75 | +/-- A function `f` is integrable with respect to a countable sum of measures `Measure.sum μ` |
| 76 | +if and only if `f` is integrable with respect to each `μ i` and |
| 77 | +the sequence `fun i ↦ ∫ x, ‖f x‖ ∂μ i` is summable. -/ |
| 78 | +lemma integrable_sum_measure_iff : |
| 79 | + Integrable f (Measure.sum μ) ↔ |
| 80 | + (∀ i, Integrable f (μ i)) ∧ Summable (fun i ↦ ∫ x, ‖f x‖ ∂μ i) where |
| 81 | + mp h := ⟨fun i ↦ h.mono_measure (Measure.le_sum _ i), h.summable_integral⟩ |
| 82 | + mpr h := integrable_sum_measure h.1 h.2 |
| 83 | + |
| 84 | +section Dirac |
| 85 | + |
| 86 | +variable [MeasurableSingletonClass X] {x : ι → X} {c : ι → ℝ≥0∞} |
| 87 | + |
| 88 | +lemma integrable_sum_dirac (hc : ∀ i, c i ≠ ∞) (h : Summable (fun i ↦ (c i).toReal * ‖f (x i)‖)) : |
| 89 | + Integrable f (Measure.sum (fun i ↦ (c i) • .dirac (x i))) := |
| 90 | + integrable_sum_measure (fun i ↦ (integrable_dirac (by simp)).smul_measure (hc i)) |
| 91 | + (by simpa using h) |
| 92 | + |
| 93 | +omit [Countable ι] in |
| 94 | +lemma Integrable.summable_of_dirac |
| 95 | + (hf : Integrable f (Measure.sum (fun i ↦ (c i) • .dirac (x i)))) : |
| 96 | + Summable (fun i ↦ (c i).toReal * ‖f (x i)‖) := by |
| 97 | + simpa using hf.summable_integral |
| 98 | + |
| 99 | +/-- A function `f` is integrable with respect to a countable sum of |
| 100 | +Dirac masses `Measure.sum (fun i ↦ (c i) • Measure.dirac (x i))` if and only if |
| 101 | +the sequence `fun i ↦ (c i).toReal * ‖f (x i)‖` is summable. -/ |
| 102 | +lemma integrable_sum_dirac_iff (hc : ∀ i, c i ≠ ∞) : |
| 103 | + Integrable f (Measure.sum (fun i ↦ (c i) • .dirac (x i))) ↔ |
| 104 | + Summable (fun i ↦ (c i).toReal * ‖f (x i)‖) where |
| 105 | + mp h := h.summable_of_dirac |
| 106 | + mpr h := integrable_sum_dirac hc h |
| 107 | + |
| 108 | +end Dirac |
| 109 | + |
| 110 | +end Integrable |
| 111 | + |
| 112 | +section Integral |
| 113 | + |
| 114 | +variable [NormedSpace ℝ E] |
| 115 | + |
| 116 | +omit [Countable ι] in |
| 117 | +/-- If `f` is integrable with respect to `Measure.sum μ`, then the sequence |
| 118 | +`fun i ↦ ∫ x, f x ∂μ i` is summable and its sum is `∫ x, f x ∂Measure.sum μ`. -/ |
| 119 | +theorem hasSum_integral_measure (hf : Integrable f (Measure.sum μ)) : |
| 120 | + HasSum (fun i ↦ ∫ x, f x ∂μ i) (∫ x, f x ∂Measure.sum μ) := by |
| 121 | + have hfi : ∀ i, Integrable f (μ i) := fun i ↦ hf.mono_measure (Measure.le_sum _ _) |
| 122 | + simp only [HasSum, ← integral_finset_sum_measure fun i _ ↦ hfi i] |
| 123 | + refine Metric.nhds_basis_ball.tendsto_right_iff.mpr fun ε ε0 ↦ ?_ |
| 124 | + lift ε to ℝ≥0 using ε0.le |
| 125 | + have hf_lt : (∫⁻ x, ‖f x‖ₑ ∂Measure.sum μ) < ∞ := hf.2 |
| 126 | + have hmem : ∀ᶠ y in 𝓝 (∫⁻ x, ‖f x‖ₑ ∂Measure.sum μ), (∫⁻ x, ‖f x‖ₑ ∂Measure.sum μ) < y + ε := by |
| 127 | + refine tendsto_id.add tendsto_const_nhds (lt_mem_nhds (α := ℝ≥0∞) <| ENNReal.lt_add_right ?_ ?_) |
| 128 | + exacts [hf_lt.ne, ENNReal.coe_ne_zero.2 (NNReal.coe_ne_zero.1 ε0.ne')] |
| 129 | + refine ((hasSum_lintegral_measure (fun x ↦ ‖f x‖ₑ) μ).eventually hmem).mono fun s hs ↦ ?_ |
| 130 | + obtain ⟨ν, hν⟩ : ∃ ν, (∑ i ∈ s, μ i) + ν = Measure.sum μ := by |
| 131 | + refine ⟨Measure.sum fun i : ↥(sᶜ : Set ι) ↦ μ i, ?_⟩ |
| 132 | + simpa only [← Measure.sum_coe_finset] using Measure.sum_add_sum_compl (s : Set ι) μ |
| 133 | + rw [Metric.mem_ball, ← coe_nndist, NNReal.coe_lt_coe, ← ENNReal.coe_lt_coe, ← hν] |
| 134 | + rw [← hν, integrable_add_measure] at hf |
| 135 | + refine (nndist_integral_add_measure_le_lintegral hf.1 hf.2).trans_lt ?_ |
| 136 | + rw [← hν, lintegral_add_measure, lintegral_finset_sum_measure] at hs |
| 137 | + exact lt_of_add_lt_add_left hs |
| 138 | + |
| 139 | +omit [Countable ι] in |
| 140 | +theorem integral_sum_measure (hf : Integrable f (Measure.sum μ)) : |
| 141 | + ∫ x, f x ∂Measure.sum μ = ∑' i, ∫ x, f x ∂μ i := |
| 142 | + (hasSum_integral_measure hf).tsum_eq.symm |
| 143 | + |
| 144 | +section Dirac |
| 145 | + |
| 146 | +variable [MeasurableSingletonClass X] {x : ι → X} {c : ι → ℝ≥0∞} |
| 147 | + |
| 148 | +lemma integral_sum_dirac [FiniteDimensional ℝ E] (hc : ∀ i, c i ≠ ∞) : |
| 149 | + ∫ x, f x ∂Measure.sum (fun i ↦ (c i) • .dirac (x i)) = ∑' i, (c i).toReal • f (x i) := by |
| 150 | + by_cases hf : Integrable f (.sum (fun i ↦ (c i) • .dirac (x i))) |
| 151 | + · rw [integral_sum_measure hf] |
| 152 | + congr with i |
| 153 | + rw [integral_smul_measure, integral_dirac] |
| 154 | + · rw [integral_undef hf, tsum_eq_zero_of_not_summable] |
| 155 | + apply mt Summable.norm |
| 156 | + convert mt (integrable_sum_dirac hc) hf |
| 157 | + simp [norm_smul] |
| 158 | + |
| 159 | +lemma hasSum_integral_sum_dirac [CompleteSpace E] (hc : ∀ i, c i ≠ ∞) |
| 160 | + (hf : Summable (fun i ↦ (c i).toReal * ‖f (x i)‖)) : |
| 161 | + HasSum (fun i ↦ (c i).toReal • f (x i)) |
| 162 | + (∫ x, f x ∂Measure.sum (fun i ↦ (c i) • .dirac (x i))) := by |
| 163 | + simpa using hasSum_integral_measure (integrable_sum_dirac hc hf) |
| 164 | + |
| 165 | +/-- If the sequence `fun i ↦ (c i).toReal * ‖f (x i)‖` is summable, then |
| 166 | +`∫ x, f x, ∂Measure.sum (fun i ↦ (c i) • .dirac (x i)) = ∑' i, (c i).toReal • f (x i)`. -/ |
| 167 | +lemma integral_sum_dirac_eq_tsum [CompleteSpace E] (hc : ∀ i, c i ≠ ∞) |
| 168 | + (hf : Summable (fun i ↦ (c i).toReal * ‖f (x i)‖)) : |
| 169 | + ∫ x, f x ∂Measure.sum (fun i ↦ (c i) • .dirac (x i)) = ∑' i, (c i).toReal • f (x i) := |
| 170 | + (hasSum_integral_sum_dirac hc hf).tsum_eq.symm |
| 171 | + |
| 172 | +end Dirac |
| 173 | + |
| 174 | +section DiscreteSpace |
| 175 | + |
| 176 | +variable [CompleteSpace E] [MeasurableSingletonClass X] {μ : Measure X} |
| 177 | + |
| 178 | +theorem integral_countable [Countable X] (hf : Integrable f μ) : |
| 179 | + ∫ x, f x ∂μ = ∑' x, μ.real {x} • f x := by |
| 180 | + rw [← Measure.sum_smul_dirac μ] at hf |
| 181 | + rw [← Measure.sum_smul_dirac μ, integral_sum_measure hf] |
| 182 | + congr 1 with a : 1 |
| 183 | + rw [integral_smul_measure, integral_dirac, Measure.sum_smul_dirac, measureReal_def] |
| 184 | + |
| 185 | +@[deprecated (since := "2026-03-09")] alias integral_countable' := integral_countable |
| 186 | + |
| 187 | +theorem setIntegral_countable (f : X → E) {s : Set X} (hs : s.Countable) (hf : IntegrableOn f s μ) : |
| 188 | + ∫ x in s, f x ∂μ = ∑' x : s, μ.real {(x : X)} • f x := by |
| 189 | + have hi : Countable { x // x ∈ s } := Iff.mpr countable_coe_iff hs |
| 190 | + have hf' : Integrable (fun (x : s) ↦ f x) (Measure.comap Subtype.val μ) := by |
| 191 | + rw [IntegrableOn, ← map_comap_subtype_coe, integrable_map_measure] at hf |
| 192 | + · apply hf |
| 193 | + · exact Integrable.aestronglyMeasurable hf |
| 194 | + · exact Measurable.aemeasurable measurable_subtype_coe |
| 195 | + · exact Countable.measurableSet hs |
| 196 | + rw [← integral_subtype_comap hs.measurableSet, integral_countable hf'] |
| 197 | + congr 1 with a : 1 |
| 198 | + rw [measureReal_def, Measure.comap_apply Subtype.val Subtype.coe_injective |
| 199 | + (fun s' hs' ↦ MeasurableSet.subtype_image (Countable.measurableSet hs) hs') _ |
| 200 | + (MeasurableSet.singleton a)] |
| 201 | + simp [measureReal_def] |
| 202 | + |
| 203 | +theorem setIntegral_finset (s : Finset X) (hf : IntegrableOn f s μ) : |
| 204 | + ∫ x in s, f x ∂μ = ∑ x ∈ s, μ.real {x} • f x := by |
| 205 | + rw [setIntegral_countable _ s.countable_toSet hf, ← Finset.tsum_subtype'] |
| 206 | + |
| 207 | +@[deprecated (since := "2026-03-09")] alias integral_finset := setIntegral_finset |
| 208 | + |
| 209 | +theorem integral_fintype [Fintype X] (hf : Integrable f μ) : |
| 210 | + ∫ x, f x ∂μ = ∑ x, μ.real {x} • f x := by |
| 211 | + -- NB: Integrable f does not follow from Fintype, because the measure itself could be non-finite |
| 212 | + rw [← setIntegral_finset .univ, Finset.coe_univ, Measure.restrict_univ] |
| 213 | + simp [Finset.coe_univ, hf] |
| 214 | + |
| 215 | +@[simp] lemma integral_count [Fintype X] (f : X → E) : |
| 216 | + ∫ x, f x ∂.count = ∑ a, f a := by simp [integral_fintype] |
| 217 | + |
| 218 | +end DiscreteSpace |
| 219 | + |
| 220 | +end Integral |
| 221 | + |
| 222 | +end MeasureTheory |
0 commit comments