feat: s-finite measures (#8405)

We define s-finite measures, i.e., measures which can be written as a countable sum of finite measures. We show that sigma-finite measures are s-finite, and extend a few results in the library from the sigma-finite case to the s-finite case.

Mathlib/MeasureTheory/Covering/Differentiation.lean

@@ -767,7 +767,7 @@ theorem ae_tendsto_measure_inter_div (s : Set α) :
   apply hx.congr' _
   filter_upwards [v.eventually_filterAt_measurableSet x] with _ ha
   congr 1
-  exact measure_toMeasurable_inter_of_sigmaFinite ha _
+  exact measure_toMeasurable_inter_of_sFinite ha _
 #align vitali_family.ae_tendsto_measure_inter_div VitaliFamily.ae_tendsto_measure_inter_div
 
 /-! ### Lebesgue differentiation theorem -/

Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.lean

@@ -847,7 +847,7 @@ theorem tendsto_addHaar_inter_smul_one_of_density_one (s : Set E) (x : E)
       exact measure_mono (inter_subset_right _ _)
   refine this.congr fun r => ?_
   congr 1
-  apply measure_toMeasurable_inter_of_sigmaFinite
+  apply measure_toMeasurable_inter_of_sFinite
   simp only [image_add_left, singleton_add]
   apply (continuous_add_left (-x)).measurable (ht.const_smul₀ r)
 #align measure_theory.measure.tendsto_add_haar_inter_smul_one_of_density_one MeasureTheory.Measure.tendsto_addHaar_inter_smul_one_of_density_one

Mathlib/MeasureTheory/Measure/MeasureSpace.lean

@@ -721,7 +721,8 @@ theorem measure_inter_eq_of_measure_eq {s t u : Set α} (hs : MeasurableSet s) (
 /-- The measurable superset `toMeasurable μ t` of `t` (which has the same measure as `t`)
 satisfies, for any measurable set `s`, the equality `μ (toMeasurable μ t ∩ s) = μ (u ∩ s)`.
 Here, we require that the measure of `t` is finite. The conclusion holds without this assumption
-when the measure is sigma_finite, see `measure_toMeasurable_inter_of_sigmaFinite`. -/
+when the measure is s-finite (for example when it is σ-finite),
+see `measure_toMeasurable_inter_of_sFinite`. -/
 theorem measure_toMeasurable_inter {s t : Set α} (hs : MeasurableSet s) (ht : μ t ≠ ∞) :
     μ (toMeasurable μ t ∩ s) = μ (t ∩ s) :=
   (measure_inter_eq_of_measure_eq hs (measure_toMeasurable t).symm (subset_toMeasurable μ t)
@@ -1406,6 +1407,15 @@ theorem sum_apply (f : ι → Measure α) {s : Set α} (hs : MeasurableSet s) :
   toMeasure_apply _ _ hs
 #align measure_theory.measure.sum_apply MeasureTheory.Measure.sum_apply
 
+theorem sum_apply₀ (f : ι → Measure α) {s : Set α} (hs : NullMeasurableSet s (sum f)) :
+    sum f s = ∑' i, f i s := by
+  apply le_antisymm ?_ (le_sum_apply _ _)
+  rcases hs.exists_measurable_subset_ae_eq  with ⟨t, ts, t_meas, ht⟩
+  calc
+  sum f s = sum f t := measure_congr ht.symm
+  _ = ∑' i, f i t := sum_apply _ t_meas
+  _ ≤ ∑' i, f i s := ENNReal.tsum_le_tsum (fun i ↦ measure_mono ts)
+
 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
@@ -1593,6 +1603,15 @@ theorem AbsolutelyContinuous.ae_eq (h : μ ≪ ν) {f g : α → δ} (h' : f =
   h.ae_le h'
 #align measure_theory.measure.absolutely_continuous.ae_eq MeasureTheory.Measure.AbsolutelyContinuous.ae_eq
 
+protected theorem _root_.MeasureTheory.AEDisjoint.of_absolutelyContinuous
+    (h : AEDisjoint μ s t) {ν : Measure α} (h' : ν ≪ μ) :
+    AEDisjoint ν s t := h' h
+
+protected theorem _root_.MeasureTheory.AEDisjoint.of_le
+    (h : AEDisjoint μ s t) {ν : Measure α} (h' : ν ≤ μ) :
+    AEDisjoint ν s t :=
+  h.of_absolutelyContinuous (Measure.absolutelyContinuous_of_le h')
+
 /-! ### Quasi measure preserving maps (a.k.a. non-singular maps) -/
 
 

Mathlib/MeasureTheory/Measure/MeasureSpaceDef.lean

@@ -615,8 +615,8 @@ theorem measure_mono_null_ae (H : s ≤ᵐ[μ] t) (ht : μ t = 0) : μ s = 0 :=
 
 /-- A measurable set `t ⊇ s` such that `μ t = μ s`. It even satisfies `μ (t ∩ u) = μ (s ∩ u)` for
 any measurable set `u` if `μ s ≠ ∞`, see `measure_toMeasurable_inter`.
-(This property holds without the assumption `μ s ≠ ∞` when the space is sigma-finite,
-see `measure_toMeasurable_inter_of_sigmaFinite`).
+(This property holds without the assumption `μ s ≠ ∞` when the space is s-finite -- for example
+σ-finite), see `measure_toMeasurable_inter_of_sFinite`).
 If `s` is a null measurable set, then
 we also have `t =ᵐ[μ] s`, see `NullMeasurableSet.toMeasurable_ae_eq`.
 This notion is sometimes called a "measurable hull" in the literature. -/

Mathlib/MeasureTheory/Measure/Typeclasses.lean

@@ -14,6 +14,7 @@ We introduce the following typeclasses for measures:
 * `IsFiniteMeasure μ`: `μ univ < ∞`;
 * `SigmaFinite μ`: there exists a countable collection of sets that cover `univ`
   where `μ` is finite;
+* `SFinite μ`: the measure `μ` can be written as a countable sum of finite measures;
 * `IsLocallyFiniteMeasure μ` : `∀ x, ∃ s ∈ 𝓝 x, μ s < ∞`;
 * `NoAtoms μ` : `∀ x, μ {x} = 0`; possibly should be redefined as
   `∀ s, 0 < μ s → ∃ t ⊆ s, 0 < μ t ∧ μ t < μ s`.
@@ -477,6 +478,23 @@ end Measure
 
 open Measure
 
+section SFinite
+
+/-- A measure is called s-finite if it is a countable sum of finite measures. -/
+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
+
+instance isFiniteMeasure_sFiniteSeq [h : SFinite μ] (n : ℕ) : IsFiniteMeasure (sFiniteSeq μ n) :=
+  h.1.choose_spec.1 n
+
+lemma sum_sFiniteSeq (μ : Measure α) [h : SFinite μ] : sum (sFiniteSeq μ) = μ :=
+  h.1.choose_spec.2.symm
+
+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
@@ -576,6 +594,18 @@ theorem eventually_mem_spanningSets (μ : Measure α) [SigmaFinite μ] (x : α)
   eventually_atTop.2 ⟨spanningSetsIndex μ x, fun _ => mem_spanningSets_of_index_le μ x⟩
 #align measure_theory.eventually_mem_spanning_sets MeasureTheory.eventually_mem_spanningSets
 
+theorem sum_restrict_disjointed_spanningSets (μ : Measure α) [SigmaFinite μ] :
+    sum (fun n ↦ μ.restrict (disjointed (spanningSets μ) n)) = μ := by
+  rw [← restrict_iUnion (disjoint_disjointed _)
+      (MeasurableSet.disjointed (measurable_spanningSets _)),
+    iUnion_disjointed, iUnion_spanningSets, restrict_univ]
+
+instance (priority := 100) [SigmaFinite μ] : SFinite μ := by
+  have : ∀ n, Fact (μ (disjointed (spanningSets μ) n) < ∞) :=
+    fun n ↦ ⟨(measure_mono (disjointed_subset _ _)).trans_lt (measure_spanningSets_lt_top μ n)⟩
+  exact ⟨⟨fun n ↦ μ.restrict (disjointed (spanningSets μ) n), fun n ↦ by infer_instance,
+    (sum_restrict_disjointed_spanningSets μ).symm⟩⟩
+
 namespace Measure
 
 theorem iSup_restrict_spanningSets [SigmaFinite μ] (hs : MeasurableSet s) :
@@ -651,7 +681,7 @@ theorem _root_.Set.Infinite.meas_eq_top [MeasurableSingletonClass α]
 
 /-- If the union of a.e.-disjoint null-measurable sets has finite measure, then there are only
 countably many members of the union whose measure is positive. -/
-theorem countable_meas_pos_of_disjoint_of_meas_iUnion_ne_top₀ {ι : Type*} [MeasurableSpace α]
+theorem countable_meas_pos_of_disjoint_of_meas_iUnion_ne_top₀ {ι : Type*} {_ : MeasurableSpace α}
     (μ : Measure α) {As : ι → Set α} (As_mble : ∀ i : ι, NullMeasurableSet (As i) μ)
     (As_disj : Pairwise (AEDisjoint μ on As)) (Union_As_finite : μ (⋃ i, As i) ≠ ∞) :
     Set.Countable { i : ι | 0 < μ (As i) } := by
@@ -671,58 +701,93 @@ theorem countable_meas_pos_of_disjoint_of_meas_iUnion_ne_top₀ {ι : Type*} [Me
 
 /-- If the union of disjoint measurable sets has finite measure, then there are only
 countably many members of the union whose measure is positive. -/
-theorem countable_meas_pos_of_disjoint_of_meas_iUnion_ne_top {ι : Type*} [MeasurableSpace α]
+theorem countable_meas_pos_of_disjoint_of_meas_iUnion_ne_top {ι : Type*} {_ : MeasurableSpace α}
     (μ : Measure α) {As : ι → Set α} (As_mble : ∀ i : ι, MeasurableSet (As i))
     (As_disj : Pairwise (Disjoint on As)) (Union_As_finite : μ (⋃ i, As i) ≠ ∞) :
     Set.Countable { i : ι | 0 < μ (As i) } :=
   countable_meas_pos_of_disjoint_of_meas_iUnion_ne_top₀ μ (fun i ↦ (As_mble i).nullMeasurableSet)
     ((fun _ _ h ↦ Disjoint.aedisjoint (As_disj h))) Union_As_finite
 #align measure_theory.measure.countable_meas_pos_of_disjoint_of_meas_Union_ne_top MeasureTheory.Measure.countable_meas_pos_of_disjoint_of_meas_iUnion_ne_top
 
-/-- In a σ-finite space, among disjoint null-measurable sets, only countably many can have positive
+/-- In an s-finite space, among disjoint null-measurable sets, only countably many can have positive
 measure. -/
-theorem countable_meas_pos_of_disjoint_iUnion₀ {ι : Type*} [MeasurableSpace α] {μ : Measure α}
-    [SigmaFinite μ] {As : ι → Set α} (As_mble : ∀ i : ι, NullMeasurableSet (As i) μ)
+theorem countable_meas_pos_of_disjoint_iUnion₀ {ι : Type*} { _ : MeasurableSpace α} {μ : Measure α}
+    [SFinite μ] {As : ι → Set α} (As_mble : ∀ i : ι, NullMeasurableSet (As i) μ)
     (As_disj : Pairwise (AEDisjoint μ on As)) :
     Set.Countable { i : ι | 0 < μ (As i) } := by
-  have obs : { i : ι | 0 < μ (As i) } ⊆ ⋃ n, { i : ι | 0 < μ (As i ∩ spanningSets μ n) } := by
-    intro i i_in_nonzeroes
+  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 *
-    simp [(forall_measure_inter_spanningSets_eq_zero _).mp con] at i_in_nonzeroes
+    rw [sum_apply₀] at hi
+    · simp_rw [con] at hi
+      simp at hi
+    · exact As_mble i
   apply Countable.mono obs
-  refine' countable_iUnion fun n => countable_meas_pos_of_disjoint_of_meas_iUnion_ne_top₀ μ _ _ _
-  · exact fun i ↦ NullMeasurableSet.inter (As_mble i)
-      (measurable_spanningSets μ n).nullMeasurableSet
-  · exact fun i j i_ne_j ↦ (As_disj i_ne_j).mono
-      (inter_subset_left (As i) (spanningSets μ n)) (inter_subset_left (As j) (spanningSets μ n))
-  · refine' (lt_of_le_of_lt (measure_mono _) (measure_spanningSets_lt_top μ n)).ne
-    exact iUnion_subset fun i => inter_subset_right _ _
-
-/-- In a σ-finite space, among disjoint measurable sets, only countably many can have positive
+  refine countable_iUnion fun n ↦ ?_
+  apply countable_meas_pos_of_disjoint_of_meas_iUnion_ne_top₀
+  · exact fun i ↦ (As_mble i).mono (le_sum _ _)
+  · exact fun i j hij ↦ AEDisjoint.of_le (As_disj hij) (le_sum _ _)
+  · exact measure_ne_top _ (⋃ i, As i)
+
+/-- In an s-finite space, among disjoint measurable sets, only countably many can have positive
 measure. -/
-theorem countable_meas_pos_of_disjoint_iUnion {ι : Type*} [MeasurableSpace α] {μ : Measure α}
-    [SigmaFinite μ] {As : ι → Set α} (As_mble : ∀ i : ι, MeasurableSet (As i))
+theorem countable_meas_pos_of_disjoint_iUnion {ι : Type*} {_ : MeasurableSpace α} {μ : Measure α}
+    [SFinite μ] {As : ι → Set α} (As_mble : ∀ i : ι, MeasurableSet (As i))
     (As_disj : Pairwise (Disjoint on As)) : Set.Countable { i : ι | 0 < μ (As i) } :=
   countable_meas_pos_of_disjoint_iUnion₀ (fun i ↦ (As_mble i).nullMeasurableSet)
     ((fun _ _ h ↦ Disjoint.aedisjoint (As_disj h)))
 #align measure_theory.measure.countable_meas_pos_of_disjoint_Union MeasureTheory.Measure.countable_meas_pos_of_disjoint_iUnion
 
-theorem countable_meas_level_set_pos₀ {α β : Type*} [MeasurableSpace α] {μ : Measure α}
-    [SigmaFinite μ] [MeasurableSpace β] [MeasurableSingletonClass β] {g : α → β}
+theorem countable_meas_level_set_pos₀ {α β : Type*} {_ : MeasurableSpace α} {μ : Measure α}
+    [SFinite μ] [MeasurableSpace β] [MeasurableSingletonClass β] {g : α → β}
     (g_mble : NullMeasurable g μ) : Set.Countable { t : β | 0 < μ { a : α | g a = t } } := by
   have level_sets_disjoint : Pairwise (Disjoint on fun t : β => { a : α | g a = t }) :=
     fun s t hst => Disjoint.preimage g (disjoint_singleton.mpr hst)
   exact Measure.countable_meas_pos_of_disjoint_iUnion₀
     (fun b => g_mble (‹MeasurableSingletonClass β›.measurableSet_singleton b))
     ((fun _ _ h ↦ Disjoint.aedisjoint (level_sets_disjoint h)))
 
-theorem countable_meas_level_set_pos {α β : Type*} [MeasurableSpace α] {μ : Measure α}
-    [SigmaFinite μ] [MeasurableSpace β] [MeasurableSingletonClass β] {g : α → β}
+theorem countable_meas_level_set_pos {α β : Type*} {_ : MeasurableSpace α} {μ : Measure α}
+    [SFinite μ] [MeasurableSpace β] [MeasurableSingletonClass β] {g : α → β}
     (g_mble : Measurable g) : Set.Countable { t : β | 0 < μ { a : α | g a = t } } :=
   countable_meas_level_set_pos₀ g_mble.nullMeasurable
 #align measure_theory.measure.countable_meas_level_set_pos MeasureTheory.Measure.countable_meas_level_set_pos
 
+/-- If a measure `μ` is the sum of a countable family `mₙ`, and a set `t` has finite measure for
+each `mₙ`, then its measurable superset `toMeasurable μ t` (which has the same measure as `t`)
+satisfies, for any measurable set `s`, the equality `μ (toMeasurable μ t ∩ s) = μ (t ∩ s)`. -/
+theorem measure_toMeasurable_inter_of_sum {s : Set α} (hs : MeasurableSet s) {t : Set α}
+    {m : ℕ → Measure α} (hv : ∀ n, m n t ≠ ∞) (hμ : μ = sum m) :
+    μ (toMeasurable μ t ∩ s) = μ (t ∩ s) := by
+  -- we show that there is a measurable superset of `t` satisfying the conclusion for any
+  -- measurable set `s`. It is built for each measure `mₙ` using `toMeasurable`
+  -- (which is well behaved for finite measure sets thanks to `measure_toMeasurable_inter`), and
+  -- then taking the intersection over `n`.
+  have A : ∃ t', t' ⊇ t ∧ MeasurableSet t' ∧ ∀ u, MeasurableSet u → μ (t' ∩ u) = μ (t ∩ u) := by
+    let w n := toMeasurable (m n) t
+    have T : t ⊆ ⋂ n, w n := subset_iInter (fun i ↦ subset_toMeasurable (m i) t)
+    have M : MeasurableSet (⋂ n, w n) :=
+      MeasurableSet.iInter (fun i ↦ measurableSet_toMeasurable (m i) t)
+    refine ⟨⋂ n, w n, T, M, fun u hu ↦ ?_⟩
+    refine le_antisymm ?_ (measure_mono (inter_subset_inter_left _ T))
+    rw [hμ, sum_apply _ (M.inter hu)]
+    apply le_trans _ (le_sum_apply _ _)
+    apply ENNReal.tsum_le_tsum (fun i ↦ ?_)
+    calc
+    m i ((⋂ n, w n) ∩ u) ≤ m i (w i ∩ u) :=
+      measure_mono (inter_subset_inter_left _ (iInter_subset _ _))
+    _ = m i (t ∩ u) := measure_toMeasurable_inter hu (hv i)
+  -- thanks to the definition of `toMeasurable`, the previous property will also be shared
+  -- by `toMeasurable μ t`, which is enough to conclude the proof.
+  rw [toMeasurable]
+  split_ifs with ht
+  · apply measure_congr
+    exact ae_eq_set_inter ht.choose_spec.2.2 (ae_eq_refl _)
+  · exact A.choose_spec.2.2 s hs
+
 /-- If a set `t` is covered by a countable family of finite measure sets, then its measurable
 superset `toMeasurable μ t` (which has the same measure as `t`) satisfies,
 for any measurable set `s`, the equality `μ (toMeasurable μ t ∩ s) = μ (t ∩ s)`. -/
@@ -798,27 +863,20 @@ theorem restrict_toMeasurable_of_cover {s : Set α} {v : ℕ → Set α} (hv : s
 
 /-- The measurable superset `toMeasurable μ t` of `t` (which has the same measure as `t`)
 satisfies, for any measurable set `s`, the equality `μ (toMeasurable μ t ∩ s) = μ (t ∩ s)`.
-This only holds when `μ` is σ-finite. For a version without this assumption (but requiring
-that `t` has finite measure), see `measure_toMeasurable_inter`. -/
-theorem measure_toMeasurable_inter_of_sigmaFinite [SigmaFinite μ] {s : Set α} (hs : MeasurableSet s)
-    (t : Set α) : μ (toMeasurable μ t ∩ s) = μ (t ∩ s) := by
-  have : t ⊆ ⋃ n, spanningSets μ n := by
-    rw [iUnion_spanningSets]
-    exact subset_univ _
-  refine measure_toMeasurable_inter_of_cover hs this fun n => ne_of_lt ?_
-  calc
-    μ (t ∩ spanningSets μ n) ≤ μ (spanningSets μ n) := measure_mono (inter_subset_right _ _)
-    _ < ∞ := measure_spanningSets_lt_top μ n
-
-#align measure_theory.measure.measure_to_measurable_inter_of_sigma_finite MeasureTheory.Measure.measure_toMeasurable_inter_of_sigmaFinite
+This only holds when `μ` is s-finite -- for example for σ-finite measures. For a version without
+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
+#align measure_theory.measure.measure_to_measurable_inter_of_sigma_finite MeasureTheory.Measure.measure_toMeasurable_inter_of_sFinite
 
 @[simp]
-theorem restrict_toMeasurable_of_sigmaFinite [SigmaFinite μ] (s : Set α) :
+theorem restrict_toMeasurable_of_sFinite [SFinite μ] (s : Set α) :
     μ.restrict (toMeasurable μ s) = μ.restrict s :=
   ext fun t ht => by
-    rw [restrict_apply ht, inter_comm t, measure_toMeasurable_inter_of_sigmaFinite ht,
+    rw [restrict_apply ht, inter_comm t, measure_toMeasurable_inter_of_sFinite ht,
       restrict_apply ht, inter_comm t]
-#align measure_theory.measure.restrict_to_measurable_of_sigma_finite MeasureTheory.Measure.restrict_toMeasurable_of_sigmaFinite
+#align measure_theory.measure.restrict_to_measurable_of_sigma_finite MeasureTheory.Measure.restrict_toMeasurable_of_sFinite
 
 namespace FiniteSpanningSetsIn
 

Mathlib/MeasureTheory/Measure/WithDensity.lean

@@ -52,7 +52,7 @@ theorem withDensity_apply_le (f : α → ℝ≥0∞) (s : Set α) :
   _ = μ.withDensity f s := measure_toMeasurable s
 
 
-/-! In the next theorem, the sigma-finiteness assumption is necessary. Here is a counterexample
+/-! In the next theorem, the s-finiteness assumption is necessary. Here is a counterexample
 without this assumption. Let `α` be an uncountable space, let `x₀` be some fixed point, and consider
 the σ-algebra made of those sets which are countable and do not contain `x₀`, and of their
 complements. This is the σ-algebra generated by the sets `{x}` for `x ≠ x₀`. Define a measure equal
@@ -65,14 +65,14 @@ to `+∞` on nonempty sets. Let `s = {x₀}` and `f` the indicator of `sᶜ`. Th
 One checks that `μ.withDensity f = μ`, while `μ.restrict s` gives zero mass to sets not
 containing `x₀`, and infinite mass to those that contain it. -/
 
-theorem withDensity_apply' [SigmaFinite μ] (f : α → ℝ≥0∞) (s : Set α) :
+theorem withDensity_apply' [SFinite μ] (f : α → ℝ≥0∞) (s : Set α) :
     μ.withDensity f s = ∫⁻ a in s, f a ∂μ := by
   apply le_antisymm ?_ (withDensity_apply_le f s)
   let t := toMeasurable μ s
   calc
   μ.withDensity f s ≤ μ.withDensity f t := measure_mono (subset_toMeasurable μ s)
   _ = ∫⁻ a in t, f a ∂μ := withDensity_apply f (measurableSet_toMeasurable μ s)
-  _ = ∫⁻ a in s, f a ∂μ := by congr 1; exact restrict_toMeasurable_of_sigmaFinite s
+  _ = ∫⁻ a in s, f a ∂μ := by congr 1; exact restrict_toMeasurable_of_sFinite s
 
 @[simp]
 lemma withDensity_zero_left (f : α → ℝ≥0∞) : (0 : Measure α).withDensity f = 0 := by