feat(measure_theory/integral): add integral_sum_measure (#12090)

Also add supporting lemmas about finite and infinite sums of measures.

src/measure_theory/function/l1_space.lean

@@ -456,6 +456,15 @@ h.mono_measure $ measure.le_add_left $ le_rfl
   integrable f (μ + ν) ↔ integrable f μ ∧ integrable f ν :=
 ⟨λ h, ⟨h.left_of_add_measure, h.right_of_add_measure⟩, λ h, h.1.add_measure h.2⟩
 
+@[simp] lemma integrable_zero_measure {m : measurable_space α} {f : α → β} :
+  integrable f (0 : measure α) :=
+⟨ae_measurable_zero_measure, has_finite_integral_zero_measure f⟩
+
+theorem integrable_finset_sum_measure {ι} {m : measurable_space α} {f : α → β}
+  {μ : ι → measure α} {s : finset ι} :
+  integrable f (∑ i in s, μ i) ↔ ∀ i ∈ s, integrable f (μ i) :=
+by induction s using finset.induction_on; simp [*]
+
 lemma integrable.smul_measure {f : α → β} (h : integrable f μ) {c : ℝ≥0∞} (hc : c ≠ ∞) :
   integrable f (c • μ) :=
 ⟨h.ae_measurable.smul_measure c, h.has_finite_integral.smul_measure hc⟩
@@ -979,14 +988,6 @@ end measure_theory
 
 open measure_theory
 
-lemma integrable_zero_measure {m : measurable_space α} [measurable_space β] {f : α → β} :
-  integrable f (0 : measure α) :=
-begin
-  apply (integrable_zero _ _ _).congr,
-  change (0 : measure α) {x | 0 ≠ f x} = 0,
-  refl,
-end
-
 variables {E : Type*} [normed_group E] [measurable_space E] [borel_space E]
           {𝕜 : Type*} [nondiscrete_normed_field 𝕜] [normed_space 𝕜 E]
           {H : Type*} [normed_group H] [normed_space 𝕜 H]

src/measure_theory/group/fundamental_domain.lean

@@ -95,18 +95,23 @@ lemma null_measurable_set_smul {ν : measure α} (h : is_fundamental_domain G s
 variables [smul_invariant_measure G α μ]
 
 @[to_additive] lemma pairwise_ae_disjoint (h : is_fundamental_domain G s μ) :
-  pairwise (λ g₁ g₂ : G, μ (g₁ • s ∩ g₂ • s) = 0) :=
+  pairwise (λ g₁ g₂ : G, ae_disjoint μ (g₁ • s) (g₂ • s)) :=
 λ g₁ g₂ hne,
 calc μ (g₁ • s ∩ g₂ • s) = μ (g₂ • ((g₂⁻¹ * g₁) • s ∩ s)) :
-  by rw [smul_set_inter, ← mul_smul, mul_inv_cancel_left]
+  by rw [smul_set_inter, smul_smul, mul_inv_cancel_left]
 ... = μ ((g₂⁻¹ * g₁) • s ∩ s) : measure_smul_set _ _ _
 ... = 0 : h.ae_disjoint _ $ mt inv_mul_eq_one.1 hne.symm
 
+@[to_additive] lemma pairwise_ae_disjoint_of_ac {ν : measure α} (h : is_fundamental_domain G s μ)
+  (hle : ν ≪ μ) :
+  pairwise (λ g₁ g₂ : G, ae_disjoint ν (g₁ • s) (g₂ • s)) :=
+h.pairwise_ae_disjoint.mono $ λ g₁ g₂ h, hle h
+
 variables [encodable G] {ν : measure α}
 
 @[to_additive] lemma sum_restrict_of_ac (h : is_fundamental_domain G s μ) (hν : ν ≪ μ) :
   sum (λ g : G, ν.restrict (g • s)) = ν :=
-by rw [← restrict_Union_ae (h.pairwise_ae_disjoint.mono $ λ i j h, hν h) h.null_measurable_set_smul,
+by rw [← restrict_Union_ae (h.pairwise_ae_disjoint_of_ac hν) h.null_measurable_set_smul,
   restrict_congr_set (hν h.Union_smul_ae_eq), restrict_univ]
 
 @[to_additive] lemma lintegral_eq_tsum_of_ac (h : is_fundamental_domain G s μ) (hν : ν ≪ μ)
@@ -227,8 +232,8 @@ begin
     calc ∫ x in s, f x ∂μ = ∫ x in ⋃ g : G, g • t, f x ∂(μ.restrict s) :
       by rw [restrict_congr_set (hac ht.Union_smul_ae_eq), restrict_univ]
     ... = ∑' g : G, ∫ x in g • t, f x ∂(μ.restrict s) :
-      integral_Union_of_null_inter (λ g, (ht.measurable_set_smul g).null_measurable_set)
-        (ht.pairwise_ae_disjoint.mono $ λ i j h, hac h) hfs.integrable.integrable_on
+      integral_Union_ae ht.null_measurable_set_smul (ht.pairwise_ae_disjoint_of_ac hac)
+        hfs.integrable.integrable_on
     ... = ∑' g : G, ∫ x in s ∩ g • t, f x ∂μ :
       by simp only [restrict_restrict (ht.measurable_set_smul _), inter_comm]
     ... = ∑' g : G, ∫ x in s ∩ g⁻¹ • t, f x ∂μ : ((equiv.inv G).tsum_eq _).symm
@@ -240,8 +245,8 @@ begin
     ... = ∑' g : G, ∫ x in g • s, f x ∂(μ.restrict t) :
       by simp only [hf, restrict_restrict (hs.measurable_set_smul _)]
     ... = ∫ x in ⋃ g : G, g • s, f x ∂(μ.restrict t) :
-      (integral_Union_of_null_inter (λ g, (hs.measurable_set_smul g).null_measurable_set)
-        (hs.pairwise_ae_disjoint.mono $ λ i j h, hac h) hft.integrable.integrable_on).symm
+      (integral_Union_ae hs.null_measurable_set_smul (hs.pairwise_ae_disjoint_of_ac hac)
+        hft.integrable.integrable_on).symm
     ... = ∫ x in t, f x ∂μ :
       by rw [restrict_congr_set (hac hs.Union_smul_ae_eq), restrict_univ] },
   { rw [integral_undef hfs, integral_undef],

src/measure_theory/integral/bochner.lean

@@ -1208,6 +1208,53 @@ end
   ∫ x, f x ∂(0 : measure α) = 0 :=
 set_to_fun_measure_zero (dominated_fin_meas_additive_weighted_smul _) rfl
 
+theorem integral_finset_sum_measure {ι} {m : measurable_space α} {f : α → E}
+  {μ : ι → measure α} {s : finset ι} (hf : ∀ i ∈ s, integrable f (μ i)) :
+  ∫ a, f a ∂(∑ i in s, μ i) = ∑ i in s, ∫ a, f a ∂μ i :=
+begin
+  classical,
+  refine finset.induction_on' s _ _, -- `induction s using finset.induction_on'` fails
+  { simp },
+  { intros i t hi ht hit iht,
+    simp only [finset.sum_insert hit, ← iht],
+    exact integral_add_measure (hf _ hi) (integrable_finset_sum_measure.2 $ λ j hj, hf j (ht hj)) }
+end
+
+lemma nndist_integral_add_measure_le_lintegral (h₁ : integrable f μ) (h₂ : integrable f ν) :
+  (nndist (∫ x, f x ∂μ) (∫ x, f x ∂(μ + ν)) : ℝ≥0∞) ≤ ∫⁻ x, ∥f x∥₊ ∂ν :=
+begin
+  rw [integral_add_measure h₁ h₂, nndist_comm, nndist_eq_nnnorm, add_sub_cancel'],
+  exact ennnorm_integral_le_lintegral_ennnorm _
+end
+
+theorem has_sum_integral_measure {ι} {m : measurable_space α} {f : α → E} {μ : ι → measure α}
+  (hf : integrable f (measure.sum μ)) :
+  has_sum (λ i, ∫ a, f a ∂μ i) (∫ a, f a ∂measure.sum μ) :=
+begin
+  have hfi : ∀ i, integrable f (μ i) := λ i, hf.mono_measure (measure.le_sum _ _),
+  simp only [has_sum, ← integral_finset_sum_measure (λ i _, hfi i)],
+  refine metric.nhds_basis_ball.tendsto_right_iff.mpr (λ ε ε0, _),
+  lift ε to ℝ≥0 using ε0.le,
+  have hf_lt : ∫⁻ x, ∥f x∥₊ ∂(measure.sum μ) < ∞ := hf.2,
+  have hmem : ∀ᶠ y in 𝓝 ∫⁻ x, ∥f x∥₊ ∂(measure.sum μ), ∫⁻ x, ∥f x∥₊ ∂(measure.sum μ) < y + ε,
+  { refine tendsto_id.add tendsto_const_nhds (lt_mem_nhds $ ennreal.lt_add_right _ _),
+    exacts [hf_lt.ne, ennreal.coe_ne_zero.2 (nnreal.coe_ne_zero.1 ε0.ne')] },
+  refine ((has_sum_lintegral_measure (λ x, ∥f x∥₊) μ).eventually hmem).mono (λ s hs, _),
+  obtain ⟨ν, hν⟩ : ∃ ν, (∑ i in s, μ i) + ν = measure.sum μ,
+  { refine ⟨measure.sum (λ i : ↥(sᶜ : set ι), μ i), _⟩,
+    simpa only [← measure.sum_coe_finset] using measure.sum_add_sum_compl (s : set ι) μ },
+  rw [metric.mem_ball, ← coe_nndist, nnreal.coe_lt_coe, ← ennreal.coe_lt_coe, ← hν],
+  rw [← hν, integrable_add_measure] at hf,
+  refine (nndist_integral_add_measure_le_lintegral hf.1 hf.2).trans_lt _,
+  rw [← hν, lintegral_add_measure, lintegral_finset_sum_measure] at hs,
+  exact lt_of_add_lt_add_left hs
+end
+
+theorem integral_sum_measure {ι} {m : measurable_space α} {f : α → E} {μ : ι → measure α}
+  (hf : integrable f (measure.sum μ)) :
+  ∫ a, f a ∂measure.sum μ = ∑' i, ∫ a, f a ∂μ i :=
+(has_sum_integral_measure hf).tsum_eq.symm
+
 @[simp] lemma integral_smul_measure (f : α → E) (c : ℝ≥0∞) :
   ∫ x, f x ∂(c • μ) = c.to_real • ∫ x, f x ∂μ :=
 begin

src/measure_theory/integral/lebesgue.lean

@@ -1376,10 +1376,19 @@ begin
       (finset.sum_le_sum $ λ j hj, simple_func.lintegral_mono le_sup_right le_rfl)⟩
 end
 
+theorem has_sum_lintegral_measure {ι} {m : measurable_space α} (f : α → ℝ≥0∞) (μ : ι → measure α) :
+  has_sum (λ i, ∫⁻ a, f a ∂(μ i)) (∫⁻ a, f a ∂(measure.sum μ)) :=
+(lintegral_sum_measure f μ).symm ▸ ennreal.summable.has_sum
+
 @[simp] lemma lintegral_add_measure {m : measurable_space α} (f : α → ℝ≥0∞) (μ ν : measure α) :
   ∫⁻ a, f a ∂ (μ + ν) = ∫⁻ a, f a ∂μ + ∫⁻ a, f a ∂ν :=
 by simpa [tsum_fintype] using lintegral_sum_measure f (λ b, cond b μ ν)
 
+@[simp] lemma lintegral_finset_sum_measure {ι} {m : measurable_space α} (s : finset ι)
+  (f : α → ℝ≥0∞) (μ : ι → measure α) :
+  ∫⁻ a, f a ∂(∑ i in s, μ i) = ∑ i in s, ∫⁻ a, f a ∂μ i :=
+by { rw [← measure.sum_coe_finset, lintegral_sum_measure, ← finset.tsum_subtype'], refl }
+
 @[simp] lemma lintegral_zero_measure {m : measurable_space α} (f : α → ℝ≥0∞) :
   ∫⁻ a, f a ∂(0 : measure α) = 0 :=
 bot_unique $ by simp [lintegral]

src/measure_theory/integral/set_integral.lean

@@ -165,40 +165,32 @@ begin
     (hi.2.trans_lt $ ennreal.add_lt_top.2 ⟨hfi', ennreal.coe_lt_top⟩).ne]
 end
 
-lemma has_sum_integral_Union {ι : Type*} [encodable ι] {s : ι → set α} {f : α → E}
-  (hm : ∀ i, measurable_set (s i)) (hd : pairwise (disjoint on s))
+lemma has_sum_integral_Union_ae {ι : Type*} [encodable ι] {s : ι → set α} {f : α → E}
+  (hm : ∀ i, null_measurable_set (s i) μ) (hd : pairwise (ae_disjoint μ on s))
   (hfi : integrable_on f (⋃ i, s i) μ) :
   has_sum (λ n, ∫ a in s n, f a ∂ μ) (∫ a in ⋃ n, s n, f a ∂μ) :=
 begin
-  have hfi' : ∀ i, integrable_on f (s i) μ, from λ i, hfi.mono_set (subset_Union _ _),
-  simp only [has_sum, ← integral_finset_bUnion _ (λ i _, hm i) (hd.set_pairwise _) (λ i _, hfi' i)],
-  rw Union_eq_Union_finset at hfi ⊢,
-  exact tendsto_set_integral_of_monotone (λ t, t.measurable_set_bUnion (λ i _, hm i))
-    (λ t₁ t₂ h, bUnion_subset_bUnion_left h) hfi
+  simp only [integrable_on, measure.restrict_Union_ae hd hm] at hfi ⊢,
+  exact has_sum_integral_measure hfi
 end
 
+lemma has_sum_integral_Union {ι : Type*} [encodable ι] {s : ι → set α} {f : α → E}
+  (hm : ∀ i, measurable_set (s i)) (hd : pairwise (disjoint on s))
+  (hfi : integrable_on f (⋃ i, s i) μ) :
+  has_sum (λ n, ∫ a in s n, f a ∂ μ) (∫ a in ⋃ n, s n, f a ∂μ) :=
+has_sum_integral_Union_ae (λ i, (hm i).null_measurable_set) (hd.mono (λ i j h, h.ae_disjoint)) hfi
+
 lemma integral_Union {ι : Type*} [encodable ι] {s : ι → set α} {f : α → E}
   (hm : ∀ i, measurable_set (s i)) (hd : pairwise (disjoint on s))
   (hfi : integrable_on f (⋃ i, s i) μ) :
   (∫ a in (⋃ n, s n), f a ∂μ) = ∑' n, ∫ a in s n, f a ∂ μ :=
 (has_sum.tsum_eq (has_sum_integral_Union hm hd hfi)).symm
 
-lemma has_sum_integral_Union_of_null_inter {ι : Type*} [encodable ι] {s : ι → set α} {f : α → E}
-  (hm : ∀ i, null_measurable_set (s i) μ) (hd : pairwise (ae_disjoint μ on s))
-  (hfi : integrable_on f (⋃ i, s i) μ) :
-  has_sum (λ n, ∫ a in s n, f a ∂ μ) (∫ a in ⋃ n, s n, f a ∂μ) :=
-begin
-  rcases exists_subordinate_pairwise_disjoint hm hd with ⟨t, ht_sub, ht_eq, htm, htd⟩,
-  have htU_eq : (⋃ i, s i) =ᵐ[μ] ⋃ i, t i := eventually_eq.countable_Union ht_eq,
-  simp only [set_integral_congr_set_ae (ht_eq _), set_integral_congr_set_ae htU_eq, htU_eq],
-  exact has_sum_integral_Union htm htd (hfi.congr_set_ae htU_eq.symm)
-end
-
-lemma integral_Union_of_null_inter {ι : Type*} [encodable ι] {s : ι → set α} {f : α → E}
+lemma integral_Union_ae {ι : Type*} [encodable ι] {s : ι → set α} {f : α → E}
   (hm : ∀ i, null_measurable_set (s i) μ) (hd : pairwise (ae_disjoint μ on s))
   (hfi : integrable_on f (⋃ i, s i) μ) :
   (∫ a in (⋃ n, s n), f a ∂μ) = ∑' n, ∫ a in s n, f a ∂ μ :=
-(has_sum.tsum_eq (has_sum_integral_Union_of_null_inter hm hd hfi)).symm
+(has_sum.tsum_eq (has_sum_integral_Union_ae hm hd hfi)).symm
 
 lemma set_integral_eq_zero_of_forall_eq_zero {f : α → E} (hf : measurable f)
   (ht_eq : ∀ x ∈ t, f x = 0) :

src/measure_theory/measure/measure_space.lean

@@ -626,6 +626,18 @@ instance add_comm_monoid [measurable_space α] : add_comm_monoid (measure α) :=
 to_outer_measure_injective.add_comm_monoid to_outer_measure zero_to_outer_measure
   add_to_outer_measure
 
+/-- Coercion to function as an additive monoid homomorphism. -/
+def coe_add_hom {m : measurable_space α} : measure α →+ (set α → ℝ≥0∞) :=
+⟨coe_fn, coe_zero, coe_add⟩
+
+@[simp] lemma coe_finset_sum {m : measurable_space α} (I : finset ι) (μ : ι → measure α) :
+  ⇑(∑ i in I, μ i) = ∑ i in I, μ i :=
+(@coe_add_hom α m).map_sum _ _
+
+theorem finset_sum_apply {m : measurable_space α} (I : finset ι) (μ : ι → measure α) (s : set α) :
+  (∑ i in I, μ i) s = ∑ i in I, μ i s :=
+by rw [coe_finset_sum, finset.sum_apply]
+
 instance [measurable_space α] : has_scalar ℝ≥0∞ (measure α) :=
 ⟨λ c μ,
   { to_outer_measure := c • μ.to_outer_measure,
@@ -1390,11 +1402,18 @@ lemma ae_sum_iff' {μ : ι → measure α} {p : α → Prop} (h : measurable_set
   (∀ᵐ x ∂(sum μ), p x) ↔ ∀ i, ∀ᵐ x ∂(μ i), p x :=
 sum_apply_eq_zero' h.compl
 
+@[simp] lemma sum_fintype [fintype ι] (μ : ι → measure α) : sum μ = ∑ i, μ i :=
+by { ext1 s hs, simp only [sum_apply, finset_sum_apply, hs, tsum_fintype] }
+
+@[simp] lemma sum_coe_finset (s : finset ι) (μ : ι → measure α) :
+  sum (λ i : s, μ i) = ∑ i in s, μ i :=
+by simpa only [sum_fintype] using @fintype.sum_finset_coe _ _ s μ _
+
 @[simp] lemma ae_sum_eq [encodable ι] (μ : ι → measure α) : (sum μ).ae = ⨆ i, (μ i).ae :=
 filter.ext $ λ s, ae_sum_iff.trans mem_supr.symm
 
 @[simp] lemma sum_bool (f : bool → measure α) : sum f = f tt + f ff :=
-ext $ λ s hs, by simp [hs, tsum_fintype]
+by rw [sum_fintype, fintype.sum_bool]
 
 @[simp] lemma sum_cond (μ ν : measure α) : sum (λ b, cond b μ ν) = μ + ν := sum_bool _
 
@@ -1405,8 +1424,16 @@ ext $ λ t ht, by simp only [sum_apply, restrict_apply, ht, ht.inter hs]
 @[simp] lemma sum_of_empty [is_empty ι] (μ : ι → measure α) : sum μ = 0 :=
 by rw [← measure_univ_eq_zero, sum_apply _ measurable_set.univ, tsum_empty]
 
+lemma sum_add_sum_compl (s : set ι) (μ : ι → measure α) :
+  sum (λ i : s, μ i) + sum (λ i : sᶜ, μ i) = sum μ :=
+begin
+  ext1 t ht,
+  simp only [add_apply, sum_apply _ ht],
+  exact @tsum_add_tsum_compl ℝ≥0∞ ι _ _ _ (λ i, μ i t) _ s ennreal.summable ennreal.summable
+end
+
 lemma sum_congr {μ ν : ℕ → measure α} (h : ∀ n, μ n = ν n) : sum μ = sum ν :=
-by { congr, ext1 n, exact h n }
+congr_arg sum (funext h)
 
 lemma sum_add_sum (μ ν : ℕ → measure α) : sum μ + sum ν = sum (λ n, μ n + ν n) :=
 begin