feat(Measure/Typeclasses): rename sFiniteSeq (#17423)

Moves:
- MeasureTheory.*sFiniteSeq* -> MeasureTheory.*sfiniteSeq*

Author: urkud

Mathlib/MeasureTheory/Constructions/Prod/Basic.lean

@@ -163,7 +163,7 @@ theorem measurable_measure_prod_mk_left_finite [IsFiniteMeasure ν] {s : Set (α
   is a measurable function. -/
 theorem measurable_measure_prod_mk_left [SFinite ν] {s : Set (α × β)} (hs : MeasurableSet s) :
     Measurable fun x => ν (Prod.mk x ⁻¹' s) := by
-  rw [← sum_sFiniteSeq ν]
+  rw [← sum_sfiniteSeq ν]
   simp_rw [Measure.sum_apply_of_countable]
   exact Measurable.ennreal_tsum (fun i ↦ measurable_measure_prod_mk_left_finite hs)
 
@@ -573,8 +573,8 @@ instance prod.instSFinite {α β : Type*} {_ : MeasurableSpace α} {μ : Measure
     [SFinite μ] {_ : MeasurableSpace β} {ν : Measure β} [SFinite ν] :
     SFinite (μ.prod ν) := by
   have : μ.prod ν =
-      Measure.sum (fun (p : ℕ × ℕ) ↦ (sFiniteSeq μ p.1).prod (sFiniteSeq ν p.2)) := by
-    conv_lhs => rw [← sum_sFiniteSeq μ, ← sum_sFiniteSeq ν]
+      Measure.sum (fun (p : ℕ × ℕ) ↦ (sfiniteSeq μ p.1).prod (sfiniteSeq ν p.2)) := by
+    conv_lhs => rw [← sum_sfiniteSeq μ, ← sum_sfiniteSeq ν]
     apply prod_sum
   rw [this]
   infer_instance
@@ -620,12 +620,12 @@ theorem prod_eq {μ : Measure α} [SigmaFinite μ] {ν : Measure β} [SigmaFinit
 variable [SFinite μ]
 
 theorem prod_swap : map Prod.swap (μ.prod ν) = ν.prod μ := by
-  have : sum (fun (i : ℕ × ℕ) ↦ map Prod.swap ((sFiniteSeq μ i.1).prod (sFiniteSeq ν i.2)))
-       = sum (fun (i : ℕ × ℕ) ↦ map Prod.swap ((sFiniteSeq μ i.2).prod (sFiniteSeq ν i.1))) := by
+  have : sum (fun (i : ℕ × ℕ) ↦ map Prod.swap ((sfiniteSeq μ i.1).prod (sfiniteSeq ν i.2)))
+       = sum (fun (i : ℕ × ℕ) ↦ map Prod.swap ((sfiniteSeq μ i.2).prod (sfiniteSeq ν i.1))) := by
     ext s hs
     rw [sum_apply _ hs, sum_apply _ hs]
     exact ((Equiv.prodComm ℕ ℕ).tsum_eq _).symm
-  rw [← sum_sFiniteSeq μ, ← sum_sFiniteSeq ν, prod_sum, prod_sum,
+  rw [← sum_sfiniteSeq μ, ← sum_sfiniteSeq ν, prod_sum, prod_sum,
     map_sum measurable_swap.aemeasurable, this]
   congr 1
   ext1 i
@@ -687,19 +687,19 @@ lemma nullMeasurableSet_prod {s : Set α} {t : Set β} :
 theorem prodAssoc_prod [SFinite τ] :
     map MeasurableEquiv.prodAssoc ((μ.prod ν).prod τ) = μ.prod (ν.prod τ) := by
   have : sum (fun (p : ℕ × ℕ × ℕ) ↦
-        (sFiniteSeq μ p.1).prod ((sFiniteSeq ν p.2.1).prod (sFiniteSeq τ p.2.2)))
+        (sfiniteSeq μ p.1).prod ((sfiniteSeq ν p.2.1).prod (sfiniteSeq τ p.2.2)))
       = sum (fun (p : (ℕ × ℕ) × ℕ) ↦
-        (sFiniteSeq μ p.1.1).prod ((sFiniteSeq ν p.1.2).prod (sFiniteSeq τ p.2))) := by
+        (sfiniteSeq μ p.1.1).prod ((sfiniteSeq ν p.1.2).prod (sfiniteSeq τ p.2))) := by
     ext s hs
     rw [sum_apply _ hs, sum_apply _ hs, ← (Equiv.prodAssoc _ _ _).tsum_eq]
     simp only [Equiv.prodAssoc_apply]
-  rw [← sum_sFiniteSeq μ, ← sum_sFiniteSeq ν, ← sum_sFiniteSeq τ, prod_sum, prod_sum,
+  rw [← sum_sfiniteSeq μ, ← sum_sfiniteSeq ν, ← sum_sfiniteSeq τ, prod_sum, prod_sum,
     map_sum MeasurableEquiv.prodAssoc.measurable.aemeasurable, prod_sum, prod_sum, this]
   congr
   ext1 i
   refine (prod_eq_generateFrom generateFrom_measurableSet generateFrom_prod
-    isPiSystem_measurableSet isPiSystem_prod ((sFiniteSeq μ i.1.1)).toFiniteSpanningSetsIn
-    ((sFiniteSeq ν i.1.2).toFiniteSpanningSetsIn.prod (sFiniteSeq τ i.2).toFiniteSpanningSetsIn)
+    isPiSystem_measurableSet isPiSystem_prod ((sfiniteSeq μ i.1.1)).toFiniteSpanningSetsIn
+    ((sfiniteSeq ν i.1.2).toFiniteSpanningSetsIn.prod (sfiniteSeq τ i.2).toFiniteSpanningSetsIn)
       ?_).symm
   rintro s hs _ ⟨t, ht, u, hu, rfl⟩; rw [mem_setOf_eq] at hs ht hu
   simp_rw [map_apply (MeasurableEquiv.measurable _) (hs.prod (ht.prod hu)),
@@ -710,7 +710,7 @@ theorem prodAssoc_prod [SFinite τ] :
 
 theorem prod_restrict (s : Set α) (t : Set β) :
     (μ.restrict s).prod (ν.restrict t) = (μ.prod ν).restrict (s ×ˢ t) := by
-  rw [← sum_sFiniteSeq μ, ← sum_sFiniteSeq ν, restrict_sum_of_countable, restrict_sum_of_countable,
+  rw [← sum_sfiniteSeq μ, ← sum_sfiniteSeq ν, restrict_sum_of_countable, restrict_sum_of_countable,
     prod_sum, prod_sum, restrict_sum_of_countable]
   congr 1
   ext1 i
@@ -725,35 +725,35 @@ theorem restrict_prod_eq_prod_univ (s : Set α) :
 
 theorem prod_dirac (y : β) : μ.prod (dirac y) = map (fun x => (x, y)) μ := by
   classical
-  rw [← sum_sFiniteSeq μ, prod_sum_left, map_sum measurable_prod_mk_right.aemeasurable]
+  rw [← sum_sfiniteSeq μ, prod_sum_left, map_sum measurable_prod_mk_right.aemeasurable]
   congr
   ext1 i
   refine prod_eq fun s t hs ht => ?_
   simp_rw [map_apply measurable_prod_mk_right (hs.prod ht), mk_preimage_prod_left_eq_if, measure_if,
-    dirac_apply' _ ht, ← indicator_mul_right _ fun _ => sFiniteSeq μ i s, Pi.one_apply, mul_one]
+    dirac_apply' _ ht, ← indicator_mul_right _ fun _ => sfiniteSeq μ i s, Pi.one_apply, mul_one]
 
 theorem dirac_prod (x : α) : (dirac x).prod ν = map (Prod.mk x) ν := by
   classical
-  rw [← sum_sFiniteSeq ν, prod_sum_right, map_sum measurable_prod_mk_left.aemeasurable]
+  rw [← sum_sfiniteSeq ν, prod_sum_right, map_sum measurable_prod_mk_left.aemeasurable]
   congr
   ext1 i
   refine prod_eq fun s t hs ht => ?_
   simp_rw [map_apply measurable_prod_mk_left (hs.prod ht), mk_preimage_prod_right_eq_if, measure_if,
-    dirac_apply' _ hs, ← indicator_mul_left _ _ fun _ => sFiniteSeq ν i t, Pi.one_apply, one_mul]
+    dirac_apply' _ hs, ← indicator_mul_left _ _ fun _ => sfiniteSeq ν i t, Pi.one_apply, one_mul]
 
 theorem dirac_prod_dirac {x : α} {y : β} : (dirac x).prod (dirac y) = dirac (x, y) := by
   rw [prod_dirac, map_dirac measurable_prod_mk_right]
 
 theorem prod_add (ν' : Measure β) [SFinite ν'] : μ.prod (ν + ν') = μ.prod ν + μ.prod ν' := by
-  simp_rw [← sum_sFiniteSeq ν, ← sum_sFiniteSeq ν', sum_add_sum, ← sum_sFiniteSeq μ, prod_sum,
+  simp_rw [← sum_sfiniteSeq ν, ← sum_sfiniteSeq ν', sum_add_sum, ← sum_sfiniteSeq μ, prod_sum,
     sum_add_sum]
   congr
   ext1 i
   refine prod_eq fun s t _ _ => ?_
   simp_rw [add_apply, prod_prod, left_distrib]
 
 theorem add_prod (μ' : Measure α) [SFinite μ'] : (μ + μ').prod ν = μ.prod ν + μ'.prod ν := by
-  simp_rw [← sum_sFiniteSeq μ, ← sum_sFiniteSeq μ', sum_add_sum, ← sum_sFiniteSeq ν, prod_sum,
+  simp_rw [← sum_sfiniteSeq μ, ← sum_sfiniteSeq μ', sum_add_sum, ← sum_sfiniteSeq ν, prod_sum,
     sum_add_sum]
   congr
   ext1 i
@@ -771,7 +771,7 @@ theorem prod_zero (μ : Measure α) : μ.prod (0 : Measure β) = 0 := by simp [M
 theorem map_prod_map {δ} [MeasurableSpace δ] {f : α → β} {g : γ → δ} (μa : Measure α)
     (μc : Measure γ) [SFinite μa] [SFinite μc] (hf : Measurable f) (hg : Measurable g) :
     (map f μa).prod (map g μc) = map (Prod.map f g) (μa.prod μc) := by
-  simp_rw [← sum_sFiniteSeq μa, ← sum_sFiniteSeq μc, map_sum hf.aemeasurable,
+  simp_rw [← sum_sfiniteSeq μa, ← sum_sfiniteSeq μc, map_sum hf.aemeasurable,
     map_sum hg.aemeasurable, prod_sum, map_sum (hf.prod_map hg).aemeasurable]
   congr
   ext1 i

Mathlib/MeasureTheory/Decomposition/Lebesgue.lean

@@ -922,7 +922,7 @@ then the same is true for any s-finite measure. -/
 theorem HaveLebesgueDecomposition.sfinite_of_isFiniteMeasure [SFinite μ]
     (_h : ∀ (μ : Measure α) [IsFiniteMeasure μ], HaveLebesgueDecomposition μ ν) :
     HaveLebesgueDecomposition μ ν :=
-  sum_sFiniteSeq μ ▸ sum_left _
+  sum_sfiniteSeq μ ▸ sum_left _
 
 attribute [local instance] haveLebesgueDecomposition_of_finiteMeasure
 

Mathlib/MeasureTheory/Integral/Lebesgue.lean

@@ -1836,9 +1836,9 @@ theorem exists_measurable_le_forall_setLIntegral_eq [SFinite μ] (f : α → ℝ
   · exact ⟨g, hgm, hgle, fun s ↦ (hleg s).antisymm (lintegral_mono hgle)⟩
   -- Without loss of generality, `μ` is a finite measure.
   wlog h : IsFiniteMeasure μ generalizing μ
-  · choose g hgm hgle hgint using fun n ↦ @this (sFiniteSeq μ n) _ inferInstance
+  · choose g hgm hgle hgint using fun n ↦ @this (sfiniteSeq μ n) _ inferInstance
     refine ⟨fun x ↦ ⨆ n, g n x, measurable_iSup hgm, fun x ↦ iSup_le (hgle · x), fun s ↦ ?_⟩
-    rw [← sum_sFiniteSeq μ, Measure.restrict_sum_of_countable,
+    rw [← sum_sfiniteSeq μ, Measure.restrict_sum_of_countable,
       lintegral_sum_measure, lintegral_sum_measure]
     exact ENNReal.tsum_le_tsum fun n ↦ (hgint n s).trans (lintegral_mono fun x ↦ le_iSup (g · x) _)
   -- According to `exists_measurable_le_lintegral_eq`, for any natural `n`

Mathlib/MeasureTheory/Measure/AEMeasurable.lean

@@ -413,7 +413,7 @@ lemma map_sum {ι : Type*} {m : ι → Measure α} {f : α → β} (hf : AEMeasu
 
 instance (μ : Measure α) (f : α → β) [SFinite μ] : SFinite (μ.map f) := by
   by_cases H : AEMeasurable f μ
-  · rw [← sum_sFiniteSeq μ] at H ⊢
+  · rw [← sum_sfiniteSeq μ] at H ⊢
     rw [map_sum H]
     infer_instance
   · rw [map_of_not_aemeasurable H]

Mathlib/MeasureTheory/Measure/Typeclasses.lean

@@ -548,24 +548,36 @@ section SFinite
 class SFinite (μ : Measure α) : Prop where
   out' : ∃ m : ℕ → Measure α, (∀ n, IsFiniteMeasure (m n)) ∧ μ = Measure.sum m
 
-/-- A sequence of finite measures such that `μ = sum (sFiniteSeq μ)` (see `sum_sFiniteSeq`). -/
-noncomputable
-def sFiniteSeq (μ : Measure α) [h : SFinite μ] : ℕ → Measure α := h.1.choose
+/-- A sequence of finite measures such that `μ = sum (sfiniteSeq μ)` (see `sum_sfiniteSeq`). -/
+noncomputable def sfiniteSeq (μ : Measure α) [h : SFinite μ] : ℕ → Measure α := h.1.choose
 
-instance isFiniteMeasure_sFiniteSeq [h : SFinite μ] (n : ℕ) : IsFiniteMeasure (sFiniteSeq μ n) :=
+@[deprecated (since := "2024-10-11")] alias sFiniteSeq := sfiniteSeq
+
+instance isFiniteMeasure_sfiniteSeq [h : SFinite μ] (n : ℕ) : IsFiniteMeasure (sfiniteSeq μ n) :=
   h.1.choose_spec.1 n
 
-lemma sum_sFiniteSeq (μ : Measure α) [h : SFinite μ] : sum (sFiniteSeq μ) = μ :=
+set_option linter.deprecated false in
+@[deprecated (since := "2024-10-11")]
+instance isFiniteMeasure_sFiniteSeq [SFinite μ] (n : ℕ) : IsFiniteMeasure (sFiniteSeq μ n) :=
+  isFiniteMeasure_sfiniteSeq n
+
+lemma sum_sfiniteSeq (μ : Measure α) [h : SFinite μ] : sum (sfiniteSeq μ) = μ :=
   h.1.choose_spec.2.symm
 
-lemma sFiniteSeq_le (μ : Measure α) [SFinite μ] (n : ℕ) : sFiniteSeq μ n ≤ μ :=
-  (le_sum _ n).trans (sum_sFiniteSeq μ).le
+@[deprecated (since := "2024-10-11")] alias sum_sFiniteSeq := sum_sfiniteSeq
+
+lemma sfiniteSeq_le (μ : Measure α) [SFinite μ] (n : ℕ) : sfiniteSeq μ n ≤ μ :=
+  (le_sum _ n).trans (sum_sfiniteSeq μ).le
+
+@[deprecated (since := "2024-10-11")] alias sFiniteSeq_le := sfiniteSeq_le
 
 instance : SFinite (0 : Measure α) := ⟨fun _ ↦ 0, inferInstance, by rw [Measure.sum_zero]⟩
 
 @[simp]
-lemma sFiniteSeq_zero (n : ℕ) : sFiniteSeq (0 : Measure α) n = 0 :=
-  bot_unique <| sFiniteSeq_le _ _
+lemma sfiniteSeq_zero (n : ℕ) : sfiniteSeq (0 : Measure α) n = 0 :=
+  bot_unique <| sfiniteSeq_le _ _
+
+@[deprecated (since := "2024-10-11")] alias sFiniteSeq_zero := sfiniteSeq_zero
 
 /-- A countable sum of finite measures is s-finite.
 This lemma is superseded by the instance below. -/
@@ -582,29 +594,29 @@ lemma sfinite_sum_of_countable [Countable ι]
 
 instance [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]
+  simp_rw [← sum_sfiniteSeq (m _), Measure.sum_sum]
   apply sfinite_sum_of_countable
 
 instance [SFinite μ] [SFinite ν] : SFinite (μ + ν) := by
   have : ∀ b : Bool, SFinite (cond b μ ν) := by simp [*]
   simpa using inferInstanceAs (SFinite (.sum (cond · μ ν)))
 
 instance [SFinite μ] (s : Set α) : SFinite (μ.restrict s) :=
-  ⟨fun n ↦ (sFiniteSeq μ n).restrict s, fun n ↦ inferInstance,
-    by rw [← restrict_sum_of_countable, sum_sFiniteSeq]⟩
+  ⟨fun n ↦ (sfiniteSeq μ n).restrict s, fun n ↦ inferInstance,
+    by rw [← restrict_sum_of_countable, sum_sfiniteSeq]⟩
 
 variable (μ) in
 /-- For an s-finite measure `μ`, there exists a finite measure `ν`
 such that each of `μ` and `ν` is absolutely continuous with respect to the other.
 -/
 theorem exists_isFiniteMeasure_absolutelyContinuous [SFinite μ] :
     ∃ ν : Measure α, IsFiniteMeasure ν ∧ μ ≪ ν ∧ ν ≪ μ := by
-  rcases ENNReal.exists_pos_tsum_mul_lt_of_countable top_ne_zero (sFiniteSeq μ · univ)
+  rcases ENNReal.exists_pos_tsum_mul_lt_of_countable top_ne_zero (sfiniteSeq μ · univ)
     fun _ ↦ measure_ne_top _ _ with ⟨c, hc₀, hc⟩
-  have {s : Set α} : sum (fun n ↦ c n • sFiniteSeq μ n) s = 0 ↔ μ s = 0 := by
-    conv_rhs => rw [← sum_sFiniteSeq μ, sum_apply_of_countable]
+  have {s : Set α} : sum (fun n ↦ c n • sfiniteSeq μ n) s = 0 ↔ μ s = 0 := by
+    conv_rhs => rw [← sum_sfiniteSeq μ, sum_apply_of_countable]
     simp [(hc₀ _).ne']
-  refine ⟨.sum fun n ↦ c n • sFiniteSeq μ n, ⟨?_⟩, fun _ ↦ this.1, fun _ ↦ this.2⟩
+  refine ⟨.sum fun n ↦ c n • sfiniteSeq μ n, ⟨?_⟩, fun _ ↦ this.1, fun _ ↦ this.2⟩
   simpa [mul_comm] using hc
 
 variable (μ) in
@@ -791,9 +803,9 @@ theorem countable_meas_pos_of_disjoint_iUnion₀ {ι : Type*} {_ : MeasurableSpa
     [SFinite μ] {As : ι → Set α} (As_mble : ∀ i : ι, NullMeasurableSet (As i) μ)
     (As_disj : Pairwise (AEDisjoint μ on As)) :
     Set.Countable { i : ι | 0 < μ (As i) } := by
-  rw [← sum_sFiniteSeq μ] at As_disj As_mble ⊢
-  have obs : { i : ι | 0 < sum (sFiniteSeq μ) (As i) }
-      ⊆ ⋃ n, { i : ι | 0 < sFiniteSeq μ n (As i) } := by
+  rw [← sum_sfiniteSeq μ] at As_disj As_mble ⊢
+  have obs : { i : ι | 0 < sum (sfiniteSeq μ) (As i) }
+      ⊆ ⋃ n, { i : ι | 0 < sfiniteSeq μ n (As i) } := by
     intro i hi
     by_contra con
     simp only [mem_iUnion, mem_setOf_eq, not_exists, not_lt, nonpos_iff_eq_zero] at *
@@ -939,7 +951,7 @@ This only holds when `μ` is s-finite -- for example for σ-finite measures. For
 this assumption (but requiring that `t` has finite measure), see `measure_toMeasurable_inter`. -/
 theorem measure_toMeasurable_inter_of_sFinite [SFinite μ] {s : Set α} (hs : MeasurableSet s)
     (t : Set α) : μ (toMeasurable μ t ∩ s) = μ (t ∩ s) :=
-  measure_toMeasurable_inter_of_sum hs (fun _ ↦ measure_ne_top _ t) (sum_sFiniteSeq μ).symm
+  measure_toMeasurable_inter_of_sum hs (fun _ ↦ measure_ne_top _ t) (sum_sfiniteSeq μ).symm
 
 @[simp]
 theorem restrict_toMeasurable_of_sFinite [SFinite μ] (s : Set α) :

Mathlib/MeasureTheory/Measure/WithDensity.lean

@@ -615,8 +615,8 @@ instance Measure.withDensity.instSFinite [SFinite μ] {f : α → ℝ≥0∞} :
   · rcases exists_measurable_le_withDensity_eq μ f with ⟨g, hgm, -, h⟩
     exact h ▸ this hgm
   wlog hμ : IsFiniteMeasure μ generalizing μ
-  · rw [← sum_sFiniteSeq μ, withDensity_sum]
-    have (n : ℕ) : SFinite ((sFiniteSeq μ n).withDensity f) := this inferInstance
+  · rw [← sum_sfiniteSeq μ, withDensity_sum]
+    have (n : ℕ) : SFinite ((sfiniteSeq μ n).withDensity f) := this inferInstance
     infer_instance
   set s := {x | f x = ∞}
   have hs : MeasurableSet s := hfm (measurableSet_singleton _)

Mathlib/MeasureTheory/Measure/WithDensityFinite.lean

@@ -100,9 +100,12 @@ instance [SFinite μ] [NeZero μ] : IsProbabilityMeasure μ.toFinite := by
 lemma absolutelyContinuous_toFinite (μ : Measure α) [SFinite μ] : μ ≪ μ.toFinite :=
   Measure.ae_le_iff_absolutelyContinuous.mp ae_toFinite.ge
 
-lemma sFiniteSeq_absolutelyContinuous_toFinite (μ : Measure α) [SFinite μ] (n : ℕ) :
-    sFiniteSeq μ n ≪ μ.toFinite :=
-  (sFiniteSeq_le μ n).absolutelyContinuous.trans (absolutelyContinuous_toFinite μ)
+lemma sfiniteSeq_absolutelyContinuous_toFinite (μ : Measure α) [SFinite μ] (n : ℕ) :
+    sfiniteSeq μ n ≪ μ.toFinite :=
+  (sfiniteSeq_le μ n).absolutelyContinuous.trans (absolutelyContinuous_toFinite μ)
+
+@[deprecated (since := "2024-10-11")]
+alias sFiniteSeq_absolutelyContinuous_toFinite := sfiniteSeq_absolutelyContinuous_toFinite
 
 lemma toFinite_absolutelyContinuous (μ : Measure α) [SFinite μ] : μ.toFinite ≪ μ :=
   Measure.ae_le_iff_absolutelyContinuous.mp ae_toFinite.le

Mathlib/Probability/Kernel/Basic.lean

@@ -124,7 +124,7 @@ instance const.instIsFiniteKernel {μβ : Measure β} [IsFiniteMeasure μβ] :
 
 instance const.instIsSFiniteKernel {μβ : Measure β} [SFinite μβ] :
     IsSFiniteKernel (const α μβ) :=
-  ⟨fun n ↦ const α (sFiniteSeq μβ n), fun n ↦ inferInstance, by rw [sum_const, sum_sFiniteSeq]⟩
+  ⟨fun n ↦ const α (sfiniteSeq μβ n), fun n ↦ inferInstance, by rw [sum_const, sum_sfiniteSeq]⟩
 
 instance const.instIsMarkovKernel {μβ : Measure β} [hμβ : IsProbabilityMeasure μβ] :
     IsMarkovKernel (const α μβ) :=