feat: extend results on product measures from sigma-finite to s-finit…

…e measures (#8713)

Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>

Mathlib/Analysis/Calculus/Rademacher.lean

@@ -220,7 +220,7 @@ theorem ae_lineDeriv_sum_eq
       ContDiff.lipschitzWith_of_hasCompactSupport g_comp g_smooth le_top
     simp_rw [integral_lineDeriv_mul_eq hf g_lip g_comp]
     simp_rw [(g_smooth.differentiable le_top).differentiableAt.lineDeriv_eq_fderiv]
-    simp only [map_neg, map_sum, SMulHomClass.map_smul, smul_eq_mul, neg_mul]
+    simp only [map_neg, _root_.map_sum, SMulHomClass.map_smul, smul_eq_mul, neg_mul]
     simp only [integral_neg, mul_neg, Finset.sum_neg_distrib, neg_inj]
     exact S2
   suffices B : ∀ i ∈ s, Integrable (fun x ↦ a i * (fderiv ℝ g x (v i) * f x)) μ by

Mathlib/Logic/Function/Basic.lean

@@ -765,27 +765,11 @@ lemma factorsThrough_iff (g : α → γ) [Nonempty γ] : g.FactorsThrough f ↔
   fun h _ _ hf => by rw [Classical.choose_spec h, comp_apply, comp_apply, hf]⟩
 #align function.factors_through_iff Function.factorsThrough_iff
 
-lemma FactorsThrough.apply_extend {δ} {g : α → γ} (hf : FactorsThrough g f)
-    (F : γ → δ) (e' : β → γ) (b : β) :
-    F (extend f g e' b) = extend f (F ∘ g) (F ∘ e') b := by
-  by_cases hb : ∃ a, f a = b
-  case pos =>
-    rcases hb with ⟨a, ha⟩
-    subst b
-    rw [hf.extend_apply, FactorsThrough.extend_apply, comp]
-    case intro.hf =>
-      intro a b h
-      simp only [comp_apply]
-      apply congr_arg
-      exact hf h
-  case neg =>
-    rw [extend_apply' _ _ _ hb, extend_apply' _ _ _ hb, comp]
-#align function.factors_through.apply_extend Function.FactorsThrough.apply_extend
-
-lemma Injective.apply_extend {δ} (hf : Injective f) (F : γ → δ) (g : α → γ) (e' : β → γ) (b : β) :
+lemma apply_extend {δ} {g : α → γ} (F : γ → δ) (f : α → β) (e' : β → γ) (b : β) :
     F (extend f g e' b) = extend f (F ∘ g) (F ∘ e') b :=
-  (hf.factorsThrough g).apply_extend F e' b
-#align function.injective.apply_extend Function.Injective.apply_extend
+  apply_dite F _ _ _
+#align function.factors_through.apply_extend Function.apply_extend
+#align function.injective.apply_extend Function.apply_extend
 
 theorem extend_injective (hf : Injective f) (e' : β → γ) : Injective fun g ↦ extend f g e' := by
   intro g₁ g₂ hg

Mathlib/MeasureTheory/Constructions/Pi.lean

@@ -243,7 +243,7 @@ instance sigmaFinite_tprod (l : List δ) (μ : ∀ i, Measure (π i)) [∀ i, Si
     SigmaFinite (Measure.tprod l μ) := by
   induction l with
   | nil => rw [tprod_nil]; infer_instance
-  | cons i l ih => rw [tprod_cons]; exact @prod.instSigmaFinite _ _ _ _ _ _ ih _
+  | cons i l ih => rw [tprod_cons]; exact @prod.instSigmaFinite _ _ _ _ _ _ _ ih
 #align measure_theory.measure.sigma_finite_tprod MeasureTheory.Measure.sigmaFinite_tprod
 
 theorem tprod_tprod (l : List δ) (μ : ∀ i, Measure (π i)) [∀ i, SigmaFinite (μ i)]

Mathlib/MeasureTheory/Group/Measure.lean

@@ -202,30 +202,26 @@ theorem forall_measure_preimage_mul_right_iff (μ : Measure G) :
 #align measure_theory.forall_measure_preimage_add_right_iff MeasureTheory.forall_measure_preimage_add_right_iff
 
 @[to_additive]
-instance Measure.prod.instIsMulLeftInvariant [IsMulLeftInvariant μ] [SigmaFinite μ] {H : Type*}
+instance Measure.prod.instIsMulLeftInvariant [IsMulLeftInvariant μ] [SFinite μ] {H : Type*}
     [Mul H] {mH : MeasurableSpace H} {ν : Measure H} [MeasurableMul H] [IsMulLeftInvariant ν]
-    [SigmaFinite ν] : IsMulLeftInvariant (μ.prod ν) := by
+    [SFinite ν] : IsMulLeftInvariant (μ.prod ν) := by
   constructor
   rintro ⟨g, h⟩
   change map (Prod.map (g * ·) (h * ·)) (μ.prod ν) = μ.prod ν
   rw [← map_prod_map _ _ (measurable_const_mul g) (measurable_const_mul h),
     map_mul_left_eq_self μ g, map_mul_left_eq_self ν h]
-  · rw [map_mul_left_eq_self μ g]; infer_instance
-  · rw [map_mul_left_eq_self ν h]; infer_instance
 #align measure_theory.measure.prod.measure.is_mul_left_invariant MeasureTheory.Measure.prod.instIsMulLeftInvariant
 #align measure_theory.measure.prod.measure.is_add_left_invariant MeasureTheory.Measure.prod.instIsAddLeftInvariant
 
 @[to_additive]
-instance Measure.prod.instIsMulRightInvariant [IsMulRightInvariant μ] [SigmaFinite μ] {H : Type*}
+instance Measure.prod.instIsMulRightInvariant [IsMulRightInvariant μ] [SFinite μ] {H : Type*}
     [Mul H] {mH : MeasurableSpace H} {ν : Measure H} [MeasurableMul H] [IsMulRightInvariant ν]
-    [SigmaFinite ν] : IsMulRightInvariant (μ.prod ν) := by
+    [SFinite ν] : IsMulRightInvariant (μ.prod ν) := by
   constructor
   rintro ⟨g, h⟩
   change map (Prod.map (· * g) (· * h)) (μ.prod ν) = μ.prod ν
   rw [← map_prod_map _ _ (measurable_mul_const g) (measurable_mul_const h),
     map_mul_right_eq_self μ g, map_mul_right_eq_self ν h]
-  · rw [map_mul_right_eq_self μ g]; infer_instance
-  · rw [map_mul_right_eq_self ν h]; infer_instance
 #align measure_theory.measure.prod.measure.is_mul_right_invariant MeasureTheory.Measure.prod.instIsMulRightInvariant
 #align measure_theory.measure.prod.measure.is_add_right_invariant MeasureTheory.Measure.prod.instIsMulRightInvariant
 
@@ -435,6 +431,10 @@ theorem measurePreserving_inv (μ : Measure G) [IsInvInvariant μ] : MeasurePres
 #align measure_theory.measure.measure_preserving_inv MeasureTheory.Measure.measurePreserving_inv
 #align measure_theory.measure.measure_preserving_neg MeasureTheory.Measure.measurePreserving_neg
 
+@[to_additive]
+instance inv.instSFinite (μ : Measure G) [SFinite μ] : SFinite μ.inv := by
+  rw [Measure.inv]; infer_instance
+
 end Inv
 
 section InvolutiveInv
@@ -954,7 +954,7 @@ instance (priority := 100) IsHaarMeasure.sigmaFinite [SigmaCompactSpace G] : Sig
 @[to_additive]
 instance prod.instIsHaarMeasure {G : Type*} [Group G] [TopologicalSpace G] {_ : MeasurableSpace G}
     {H : Type*} [Group H] [TopologicalSpace H] {_ : MeasurableSpace H} (μ : Measure G)
-    (ν : Measure H) [IsHaarMeasure μ] [IsHaarMeasure ν] [SigmaFinite μ] [SigmaFinite ν]
+    (ν : Measure H) [IsHaarMeasure μ] [IsHaarMeasure ν] [SFinite μ] [SFinite ν]
     [MeasurableMul G] [MeasurableMul H] : IsHaarMeasure (μ.prod ν) where
 #align measure_theory.measure.prod.is_haar_measure MeasureTheory.Measure.prod.instIsHaarMeasure
 #align measure_theory.measure.prod.is_add_haar_measure MeasureTheory.Measure.prod.instIsAddHaarMeasure

Mathlib/MeasureTheory/Measure/AEMeasurable.lean

@@ -15,7 +15,6 @@ function. This property, called `AEMeasurable f μ`, is defined in the file `Mea
 We discuss several of its properties that are analogous to properties of measurable functions.
 -/
 
-
 open MeasureTheory MeasureTheory.Measure Filter Set Function Classical ENNReal
 
 variable {ι α β γ δ R : Type*} {m0 : MeasurableSpace α} [MeasurableSpace β] [MeasurableSpace γ]
@@ -447,3 +446,24 @@ lemma MeasureTheory.NullMeasurable.aemeasurable_of_aerange {f : α → β} {t :
     lift f' to α → t using hf't
     replace hf'm : NullMeasurable f' μ := hf'm.measurable'.subtype_mk
     exact (measurable_subtype_coe.comp_aemeasurable hf'm.aemeasurable).congr hff'.symm
+
+namespace MeasureTheory
+namespace Measure
+
+lemma map_sum {ι : Type*} {m : ι → Measure α} {f : α → β} (hf : AEMeasurable f (Measure.sum m)) :
+    Measure.map f (Measure.sum m) = Measure.sum (fun i ↦ Measure.map f (m i)) := by
+  ext s hs
+  rw [map_apply_of_aemeasurable hf hs, sum_apply₀ _ (hf.nullMeasurable hs), sum_apply _ hs]
+  have M i : AEMeasurable f (m i) := hf.mono_measure (le_sum m i)
+  simp_rw [map_apply_of_aemeasurable (M _) hs]
+
+instance (μ : Measure α) (f : α → β) [SFinite μ] : SFinite (μ.map f) := by
+  by_cases H : AEMeasurable f μ
+  · rw [← sum_sFiniteSeq μ] at H ⊢
+    rw [map_sum H]
+    infer_instance
+  · rw [map_of_not_aemeasurable H]
+    infer_instance
+
+end Measure
+end MeasureTheory

Mathlib/MeasureTheory/Measure/Haar/OfBasis.lean

@@ -54,7 +54,7 @@ theorem image_parallelepiped (f : E →ₗ[ℝ] F) (v : ι → E) :
     f '' parallelepiped v = parallelepiped (f ∘ v) := by
   simp only [parallelepiped, ← image_comp]
   congr 1 with t
-  simp only [Function.comp_apply, map_sum, LinearMap.map_smulₛₗ, RingHom.id_apply]
+  simp only [Function.comp_apply, _root_.map_sum, LinearMap.map_smulₛₗ, RingHom.id_apply]
 #align image_parallelepiped image_parallelepiped
 
 /-- Reindexing a family of vectors does not change their parallelepiped. -/

Mathlib/MeasureTheory/Measure/MeasureSpace.lean

@@ -452,7 +452,7 @@ theorem measure_iUnion_eq_iSup [Countable ι] {s : ι → Set α} (hd : Directed
   generalize ht : Function.extend Encodable.encode s ⊥ = t
   replace hd : Directed (· ⊆ ·) t := ht ▸ hd.extend_bot Encodable.encode_injective
   suffices μ (⋃ n, t n) = ⨆ n, μ (t n) by
-    simp only [← ht, Encodable.encode_injective.apply_extend μ, ← iSup_eq_iUnion,
+    simp only [← ht, Function.apply_extend μ, ← iSup_eq_iUnion,
       iSup_extend_bot Encodable.encode_injective, (· ∘ ·), Pi.bot_apply, bot_eq_empty,
       measure_empty] at this
     exact this.trans (iSup_extend_bot Encodable.encode_injective _)
@@ -478,7 +478,6 @@ theorem measure_iUnion_eq_iSup [Countable ι] {s : ι → Set α} (hd : Directed
         _ = μ (⋃ n ∈ I, t n) := (measure_biUnion_toMeasurable I.countable_toSet _)
         _ ≤ μ (t N) := (measure_mono (iUnion₂_subset hN))
         _ ≤ ⨆ n, μ (t n) := le_iSup (μ ∘ t) N
-
 #align measure_theory.measure_Union_eq_supr MeasureTheory.measure_iUnion_eq_iSup
 
 theorem measure_biUnion_eq_iSup {s : ι → Set α} {t : Set ι} (ht : t.Countable)
@@ -1407,7 +1406,8 @@ theorem le_sum_apply (f : ι → Measure α) (s : Set α) : ∑' i, f i s ≤ su
 #align measure_theory.measure.le_sum_apply MeasureTheory.Measure.le_sum_apply
 
 @[simp]
-theorem sum_apply (f : ι → Measure α) {s : Set α} (hs : MeasurableSet s) : sum f s = ∑' i, f i s :=
+theorem sum_apply (f : ι → Measure α) {s : Set α} (hs : MeasurableSet s) :
+    sum f s = ∑' i, f i s :=
   toMeasure_apply _ _ hs
 #align measure_theory.measure.sum_apply MeasureTheory.Measure.sum_apply
 
@@ -1420,6 +1420,23 @@ theorem sum_apply₀ (f : ι → Measure α) {s : Set α} (hs : NullMeasurableSe
   _ = ∑' i, f i t := sum_apply _ t_meas
   _ ≤ ∑' i, f i s := ENNReal.tsum_le_tsum (fun i ↦ measure_mono ts)
 
+/-! For the next theorem, the countability assumption is necessary. For a counterexample, consider
+an uncountable space, with a distinguished point `x₀`, and the sigma-algebra made of countable sets
+not containing `x₀`, and their complements. All points but `x₀` are measurable.
+Consider the sum of the Dirac masses at points different from `x₀`, and `s = x₀`. For any Dirac mass
+`δ_x`, we have `δ_x (x₀) = 0`, so `∑' x, δ_x (x₀) = 0`. On the other hand, the measure `sum δ_x`
+gives mass one to each point different from `x₀`, so it gives infinite mass to any measurable set
+containing `x₀` (as such a set is uncountable), and by outer regularity one get `sum δ_x {x₀} = ∞`.
+-/
+theorem sum_apply_of_countable [Countable ι] (f : ι → Measure α) (s : Set α) :
+    sum f s = ∑' i, f i s := by
+  apply le_antisymm ?_ (le_sum_apply _ _)
+  rcases exists_measurable_superset_forall_eq f s with ⟨t, hst, htm, ht⟩
+  calc
+  sum f s ≤ sum f t := measure_mono hst
+  _ = ∑' i, f i t := sum_apply _ htm
+  _ = ∑' i, f i s := by simp [ht]
+
 theorem le_sum (μ : ι → Measure α) (i : ι) : μ i ≤ sum μ := fun s hs => by
   simpa only [sum_apply μ hs] using ENNReal.le_tsum i
 #align measure_theory.measure.le_sum MeasureTheory.Measure.le_sum
@@ -1441,6 +1458,11 @@ theorem sum_apply_eq_zero' {μ : ι → Measure α} {s : Set α} (hs : Measurabl
     sum μ s = 0 ↔ ∀ i, μ i s = 0 := by simp [hs]
 #align measure_theory.measure.sum_apply_eq_zero' MeasureTheory.Measure.sum_apply_eq_zero'
 
+theorem sum_sum {ι' : Type*} (μ : ι → ι' → Measure α) :
+    (sum fun n => sum (μ n)) = sum (fun (p : ι × ι') ↦ μ p.1 p.2) := by
+  ext1 s hs
+  simp [sum_apply _ hs, ENNReal.tsum_prod']
+
 theorem sum_comm {ι' : Type*} (μ : ι → ι' → Measure α) :
     (sum fun n => sum (μ n)) = sum fun m => sum fun n => μ n m := by
   ext1 s hs
@@ -1502,12 +1524,21 @@ theorem sum_congr {μ ν : ℕ → Measure α} (h : ∀ n, μ n = ν n) : sum μ
   congr_arg sum (funext h)
 #align measure_theory.measure.sum_congr MeasureTheory.Measure.sum_congr
 
-theorem sum_add_sum (μ ν : ℕ → Measure α) : sum μ + sum ν = sum fun n => μ n + ν n := by
+theorem sum_add_sum {ι : Type*} (μ ν : ι → Measure α) : sum μ + sum ν = sum fun n => μ n + ν n := by
   ext1 s hs
   simp only [add_apply, sum_apply _ hs, Pi.add_apply, coe_add,
     tsum_add ENNReal.summable ENNReal.summable]
 #align measure_theory.measure.sum_add_sum MeasureTheory.Measure.sum_add_sum
 
+@[simp] lemma sum_comp_equiv {ι ι' : Type*} (e : ι' ≃ ι) (m : ι → Measure α) :
+    sum (m ∘ e) = sum m := by
+  ext s hs
+  simpa [hs, sum_apply] using e.tsum_eq (fun n ↦ m n s)
+
+@[simp] lemma sum_extend_zero {ι ι' : Type*} {f : ι → ι'} (hf : Injective f) (m : ι → Measure α) :
+    sum (Function.extend f m 0) = sum m := by
+  ext s hs
+  simp [*, Function.apply_extend (fun μ : Measure α ↦ μ s)]
 end Sum
 
 /-! ### Absolute continuity -/

Mathlib/MeasureTheory/Measure/Restrict.lean

@@ -519,6 +519,12 @@ theorem restrict_sum (μ : ι → Measure α) {s : Set α} (hs : MeasurableSet s
   ext fun t ht => by simp only [sum_apply, restrict_apply, ht, ht.inter hs]
 #align measure_theory.measure.restrict_sum MeasureTheory.Measure.restrict_sum
 
+@[simp]
+theorem restrict_sum_of_countable [Countable ι] (μ : ι → Measure α) (s : Set α) :
+    (sum μ).restrict s = sum fun i => (μ i).restrict s := by
+  ext t ht
+  simp_rw [sum_apply _ ht, restrict_apply ht, sum_apply_of_countable]
+
 lemma AbsolutelyContinuous.restrict (h : μ ≪ ν) (s : Set α) : μ.restrict s ≪ ν.restrict s := by
   refine Measure.AbsolutelyContinuous.mk (fun t ht htν ↦ ?_)
   rw [restrict_apply ht] at htν ⊢

Mathlib/MeasureTheory/Measure/Typeclasses.lean

@@ -494,7 +494,27 @@ instance isFiniteMeasure_sFiniteSeq [h : SFinite μ] (n : ℕ) : IsFiniteMeasure
 lemma sum_sFiniteSeq (μ : Measure α) [h : SFinite μ] : sum (sFiniteSeq μ) = μ :=
   h.1.choose_spec.2.symm
 
+/-- A countable sum of finite measures is s-finite.
+This lemma is superseeded by the instance below. -/
+lemma sfinite_sum_of_countable {ι : Type*} [Countable ι]
+    (m : ι → Measure α) [∀ n, IsFiniteMeasure (m n)] : SFinite (Measure.sum m) := by
+  classical
+  obtain ⟨f, hf⟩ : ∃ f : ι → ℕ, Function.Injective f := Countable.exists_injective_nat ι
+  refine ⟨_, fun n ↦ ?_, (sum_extend_zero hf m).symm⟩
+  rcases em (n ∈ range f) with ⟨i, rfl⟩ | hn
+  · rw [hf.extend_apply]
+    infer_instance
+  · rw [Function.extend_apply' _ _ _ hn, Pi.zero_apply]
+    infer_instance
+
+instance {ι : Type*} [Countable ι] (m : ι → Measure α) [∀ n, SFinite (m n)] :
+    SFinite (Measure.sum m) := by
+  change SFinite (Measure.sum (fun i ↦ m i))
+  simp_rw [← sum_sFiniteSeq (m _), Measure.sum_sum]
+  apply sfinite_sum_of_countable
+
 end SFinite
+
 /-- A measure `μ` is called σ-finite if there is a countable collection of sets
  `{ A i | i ∈ ℕ }` such that `μ (A i) < ∞` and `⋃ i, A i = s`. -/
 class SigmaFinite {m0 : MeasurableSpace α} (μ : Measure α) : Prop where

Mathlib/Topology/Algebra/InfiniteSum/Basic.lean

@@ -619,6 +619,11 @@ theorem tsum_eq_tsum_of_ne_zero_bij {g : γ → α} (i : support g → β)
   tsum_eq_tsum_of_hasSum_iff_hasSum (hasSum_iff_hasSum_of_ne_zero_bij i hi hf hfg)
 #align tsum_eq_tsum_of_ne_zero_bij tsum_eq_tsum_of_ne_zero_bij
 
+@[simp]
+lemma tsum_extend_zero {γ : Type*} {g : γ → β} (hg : Injective g) (f : γ → α) :
+    ∑' y, extend g f 0 y = ∑' x, f x :=
+  tsum_eq_tsum_of_hasSum_iff_hasSum <| hasSum_extend_zero hg
+
 /-! ### `tsum` on subsets -/
 
 theorem tsum_subtype (s : Set β) (f : β → α) : ∑' x : s, f x = ∑' x, s.indicator f x :=