feat(measure_theory/integral/layercake): Add versions of layercake fo…

…rmula with strict inequality. (#17920)

This PR adds versions of layercake formula with measures of sets strictly above a given level, i.e., of the form `{x | f x > t}`. This is useful particularly when `f` is continuous and one wants the set in question to be open (rather than closed).



Co-authored-by: Kalle-swift <kalle.kytola@aalto.fi>
Co-authored-by: kkytola <39528102+kkytola@users.noreply.github.com>

src/measure_theory/integral/layercake.lean

@@ -30,12 +30,22 @@ We also give the two most common applications of the layer cake formula
  * a representation of the integral of the p:th power of a nonnegative function f:
    ∫ f(ω)^p ∂μ(ω) = p * ∫ t^(p-1) * μ {ω | f(ω) ≥ t} dt .
 
+Variants of the formulas with measures of sets of the form {ω | f(ω) > t} instead of {ω | f(ω) ≥ t}
+are also included.
+
 ## Main results
 
- * `lintegral_comp_eq_lintegral_meas_le_mul`: The general layer cake formula with Lebesgue
-   integrals.
- * `lintegral_eq_lintegral_meas_le`: The most common special case of the layer cake formula, which
-   states that for a nonnegative function f we have ∫ f(ω) ∂μ(ω) = ∫ μ {ω | f(ω) ≥ t} dt .
+ * `lintegral_comp_eq_lintegral_meas_le_mul` and `lintegral_comp_eq_lintegral_meas_lt_mul`:
+   The general layer cake formulas with Lebesgue integrals, written in terms of measures of
+   sets of the forms {ω | t ≤ f(ω)} and {ω | t < f(ω)}, respectively.
+ * `lintegral_eq_lintegral_meas_le` and `lintegral_eq_lintegral_meas_lt`:
+   The most common special cases of the layer cake formulas, stating that for a nonnegative
+   function f we have ∫ f(ω) ∂μ(ω) = ∫ μ {ω | f(ω) ≥ t} dt and
+   ∫ f(ω) ∂μ(ω) = ∫ μ {ω | f(ω) > t} dt, respectively.
+ * `lintegral_rpow_eq_lintegral_meas_le_mul` and `lintegral_rpow_eq_lintegral_meas_lt_mul`:
+   Other common special cases of the layer cake formulas, stating that for a nonnegative function f
+   and p > 0, we have ∫ f(ω)^p ∂μ(ω) = p * ∫ μ {ω | f(ω) ≥ t} * t^(p-1) dt and
+   ∫ f(ω)^p ∂μ(ω) = p * ∫ μ {ω | f(ω) > t} * t^(p-1) dt, respectively.
 
 ## Tags
 
@@ -46,18 +56,20 @@ noncomputable theory
 open_locale ennreal measure_theory
 open set measure_theory filter
 
-/-! ### Layercake theorem -/
+/-! ### Layercake formula -/
 section layercake
 
 namespace measure_theory
 
 variables {α : Type*} [measurable_space α] {f : α → ℝ} {g : ℝ → ℝ} {s : set α}
 
-/-- An auxiliary version of the layer cake theorem (Cavalieri's principle, tail probability
+/-- An auxiliary version of the layer cake formula (Cavalieri's principle, tail probability
 formula), with a measurability assumption that would also essentially follow from the
 integrability assumptions.
 
-See `measure_theory.layercake` for the main formulation of the layer cake theorem. -/
+See `measure_theory.lintegral_comp_eq_lintegral_meas_le_mul` and
+`measure_theory.lintegral_comp_eq_lintegral_meas_lt_mul` for the main formulations of the layer
+cake formula. -/
 lemma lintegral_comp_eq_lintegral_meas_le_mul_of_measurable (μ : measure α) [sigma_finite μ]
   (f_nn : 0 ≤ f) (f_mble : measurable f)
   (g_intble : ∀ t > 0, interval_integrable g volume 0 t)
@@ -132,15 +144,18 @@ begin
   exact (ennreal.measurable_of_real.comp (g_mble.comp measurable_snd)).ae_measurable.indicator mble,
 end
 
-/-- The layer cake theorem / Cavalieri's principle / tail probability formula:
+/-- The layer cake formula / Cavalieri's principle / tail probability formula:
 
 Let `f` be a non-negative measurable function on a sigma-finite measure space. Let `G` be an
 increasing absolutely continuous function on the positive real line, vanishing at the origin,
 with derivative `G' = g`. Then the integral of the composition `G ∘ f` can be written as
 the integral over the positive real line of the "tail measures" `μ {ω | f(ω) ≥ t}` of `f`
 weighted by `g`.
 
-Roughly speaking, the statement is: `∫⁻ (G ∘ f) ∂μ = ∫⁻ t in 0 .. ∞, g(t) * μ {ω | f(ω) ≥ t}`. -/
+Roughly speaking, the statement is: `∫⁻ (G ∘ f) ∂μ = ∫⁻ t in 0 .. ∞, g(t) * μ {ω | f(ω) ≥ t}`.
+
+See `lintegral_comp_eq_lintegral_meas_lt_mul` for a version with sets of the form `{ω | f(ω) > t}`
+instead. -/
 theorem lintegral_comp_eq_lintegral_meas_le_mul (μ : measure α) [sigma_finite μ]
   (f_nn : 0 ≤ f) (f_mble : measurable f)
   (g_intble : ∀ t > 0, interval_integrable g volume 0 t)
@@ -177,7 +192,10 @@ end
 /-- The standard case of the layer cake formula / Cavalieri's principle / tail probability formula:
 
 For a nonnegative function `f` on a sigma-finite measure space, the Lebesgue integral of `f` can
-be written (roughly speaking) as: `∫⁻ f ∂μ = ∫⁻ t in 0 .. ∞, μ {ω | f(ω) ≥ t}`. -/
+be written (roughly speaking) as: `∫⁻ f ∂μ = ∫⁻ t in 0 .. ∞, μ {ω | f(ω) ≥ t}`.
+
+See `lintegral_eq_lintegral_meas_lt` for a version with sets of the form `{ω | f(ω) > t}`
+instead. -/
 theorem lintegral_eq_lintegral_meas_le (μ : measure α) [sigma_finite μ]
   (f_nn : 0 ≤ f) (f_mble : measurable f) :
   ∫⁻ ω, ennreal.of_real (f ω) ∂μ = ∫⁻ t in Ioi 0, (μ {a : α | t ≤ f a}) :=
@@ -196,7 +214,10 @@ end
 /-- An application of the layer cake formula / Cavalieri's principle / tail probability formula:
 
 For a nonnegative function `f` on a sigma-finite measure space, the Lebesgue integral of `f` can
-be written (roughly speaking) as: `∫⁻ f^p ∂μ = p * ∫⁻ t in 0 .. ∞, t^(p-1) * μ {ω | f(ω) ≥ t}`. -/
+be written (roughly speaking) as: `∫⁻ f^p ∂μ = p * ∫⁻ t in 0 .. ∞, t^(p-1) * μ {ω | f(ω) ≥ t}`.
+
+See `lintegral_rpow_eq_lintegral_meas_lt_mul` for a version with sets of the form `{ω | f(ω) > t}`
+instead. -/
 theorem lintegral_rpow_eq_lintegral_meas_le_mul (μ : measure α) [sigma_finite μ]
   (f_nn : 0 ≤ f) (f_mble : measurable f) {p : ℝ} (p_pos: 0 < p) :
   ∫⁻ ω, ennreal.of_real ((f ω)^p) ∂μ
@@ -226,3 +247,114 @@ end
 end measure_theory
 
 end layercake
+
+section layercake_lt
+
+open measure_theory
+
+variables {α : Type*} [measurable_space α] (μ : measure α)
+variables {β : Type*} [measurable_space β] [measurable_singleton_class β]
+
+namespace measure
+
+lemma meas_le_ne_meas_lt_subset_meas_pos {R : Type*} [linear_order R]
+  [measurable_space R] [measurable_singleton_class R] {g : α → R} (g_mble : measurable g) {t : R}
+  (ht : μ {a : α | t ≤ g a} ≠ μ {a : α | t < g a}) :
+  0 < μ {a : α | g a = t} :=
+begin
+  have uni : {a : α | t ≤ g a } = {a : α | t < g a} ∪ {a : α | t = g a},
+  { ext a,
+    simp only [mem_set_of_eq, mem_union],
+    apply le_iff_lt_or_eq, },
+  rw (show {a : α | t = g a} = {a : α | g a = t}, by simp_rw [eq_comm]) at uni,
+  have disj : {a : α | t < g a} ∩ {a : α | g a = t} = ∅,
+  { ext a,
+    simp only [mem_inter_iff, mem_set_of_eq, mem_empty_iff_false, iff_false, not_and],
+    exact ne_of_gt, },
+  have μ_add : μ {a : α | t ≤ g a} = μ {a : α | t < g a} + μ {a : α | g a = t},
+    by rw [uni, measure_union (disjoint_iff_inter_eq_empty.mpr disj)
+                              (g_mble (finite.measurable_set (finite_singleton t)))],
+  by_contra con,
+  rw [not_lt, nonpos_iff_eq_zero] at con,
+  rw [con, add_zero] at μ_add,
+  exact ht μ_add,
+end
+
+lemma countable_meas_le_ne_meas_lt [sigma_finite μ] {R : Type*} [linear_order R]
+  [measurable_space R] [measurable_singleton_class R] {g : α → R} (g_mble : measurable g) :
+  {t : R | μ {a : α | t ≤ g a } ≠ μ {a : α | t < g a}}.countable :=
+countable.mono (show _, from λ t ht, meas_le_ne_meas_lt_subset_meas_pos μ g_mble ht)
+               (measure.countable_meas_level_set_pos g_mble)
+
+lemma meas_le_ae_eq_meas_lt [sigma_finite μ] {R : Type*} [linear_order R] [measurable_space R]
+  [measurable_singleton_class R] (ν : measure R) [has_no_atoms ν]
+  {g : α → R} (g_mble : measurable g) :
+  (λ t, μ {a : α | t ≤ g a}) =ᵐ[ν] (λ t, μ {a : α | t < g a}) :=
+set.countable.measure_zero (measure.countable_meas_le_ne_meas_lt μ g_mble) _
+
+end measure
+
+variables {f : α → ℝ} {g : ℝ → ℝ} {s : set α}
+
+/-- The layer cake formula / Cavalieri's principle / tail probability formula:
+
+Let `f` be a non-negative measurable function on a sigma-finite measure space. Let `G` be an
+increasing absolutely continuous function on the positive real line, vanishing at the origin,
+with derivative `G' = g`. Then the integral of the composition `G ∘ f` can be written as
+the integral over the positive real line of the "tail measures" `μ {ω | f(ω) > t}` of `f`
+weighted by `g`.
+
+Roughly speaking, the statement is: `∫⁻ (G ∘ f) ∂μ = ∫⁻ t in 0 .. ∞, g(t) * μ {ω | f(ω) > t}`.
+
+See `lintegral_comp_eq_lintegral_meas_le_mul` for a version with sets of the form `{ω | f(ω) ≥ t}`
+instead. -/
+theorem lintegral_comp_eq_lintegral_meas_lt_mul (μ : measure α) [sigma_finite μ]
+  (f_nn : 0 ≤ f) (f_mble : measurable f)
+  (g_intble : ∀ t > 0, interval_integrable g volume 0 t)
+  (g_nn : ∀ᵐ t ∂(volume.restrict (Ioi 0)), 0 ≤ g t) :
+  ∫⁻ ω, ennreal.of_real (∫ t in 0 .. f ω, g t) ∂μ
+    = ∫⁻ t in Ioi 0, μ {a : α | t < f a} * ennreal.of_real (g t) :=
+begin
+  rw lintegral_comp_eq_lintegral_meas_le_mul μ f_nn f_mble g_intble g_nn,
+  apply lintegral_congr_ae,
+  filter_upwards [measure.meas_le_ae_eq_meas_lt μ (volume.restrict (Ioi 0)) f_mble] with t ht,
+  rw ht,
+end
+
+/-- The standard case of the layer cake formula / Cavalieri's principle / tail probability formula:
+
+For a nonnegative function `f` on a sigma-finite measure space, the Lebesgue integral of `f` can
+be written (roughly speaking) as: `∫⁻ f ∂μ = ∫⁻ t in 0 .. ∞, μ {ω | f(ω) > t}`.
+
+See `lintegral_eq_lintegral_meas_le` for a version with sets of the form `{ω | f(ω) ≥ t}`
+instead. -/
+theorem lintegral_eq_lintegral_meas_lt (μ : measure α) [sigma_finite μ]
+  (f_nn : 0 ≤ f) (f_mble : measurable f) :
+  ∫⁻ ω, ennreal.of_real (f ω) ∂μ = ∫⁻ t in Ioi 0, (μ {a : α | t < f a}) :=
+begin
+  rw lintegral_eq_lintegral_meas_le μ f_nn f_mble,
+  apply lintegral_congr_ae,
+  filter_upwards [measure.meas_le_ae_eq_meas_lt μ (volume.restrict (Ioi 0)) f_mble] with t ht,
+  rw ht,
+end
+
+/-- An application of the layer cake formula / Cavalieri's principle / tail probability formula:
+
+For a nonnegative function `f` on a sigma-finite measure space, the Lebesgue integral of `f` can
+be written (roughly speaking) as: `∫⁻ f^p ∂μ = p * ∫⁻ t in 0 .. ∞, t^(p-1) * μ {ω | f(ω) > t}`.
+
+See `lintegral_rpow_eq_lintegral_meas_le_mul` for a version with sets of the form `{ω | f(ω) ≥ t}`
+instead. -/
+theorem lintegral_rpow_eq_lintegral_meas_lt_mul (μ : measure α) [sigma_finite μ]
+  (f_nn : 0 ≤ f) (f_mble : measurable f) {p : ℝ} (p_pos: 0 < p) :
+  ∫⁻ ω, ennreal.of_real ((f ω)^p) ∂μ
+    = (ennreal.of_real p) * ∫⁻ t in Ioi 0, (μ {a : α | t < f a}) * ennreal.of_real (t^(p-1)) :=
+begin
+  rw lintegral_rpow_eq_lintegral_meas_le_mul μ f_nn f_mble p_pos,
+  apply congr_arg (λ z, (ennreal.of_real p * z)),
+  apply lintegral_congr_ae,
+  filter_upwards [measure.meas_le_ae_eq_meas_lt μ (volume.restrict (Ioi 0)) f_mble] with t ht,
+  rw ht,
+end
+
+end layercake_lt

src/measure_theory/measure/measure_space.lean

@@ -3134,6 +3134,17 @@ begin
     exact Union_subset (λ i, inter_subset_right _ _), },
 end
 
+lemma countable_meas_level_set_pos {α β : Type*}
+  [measurable_space α] {μ : measure α} [sigma_finite μ]
+  [measurable_space β] [measurable_singleton_class β] {g : α → β} (g_mble : measurable g) :
+  set.countable {t : β | 0 < μ {a : α | g a = t}} :=
+begin
+  have level_sets_disjoint : pairwise (disjoint on (λ (t : β), {a : α | g a = t})),
+    from λ s t hst, disjoint.preimage g (disjoint_singleton.mpr hst),
+  exact measure.countable_meas_pos_of_disjoint_Union
+    (λ b, g_mble (‹measurable_singleton_class β›.measurable_set_singleton b)) level_sets_disjoint,
+end
+
 /-- The measurable superset `to_measurable μ t` of `t` (which has the same measure as `t`)
 satisfies, for any measurable set `s`, the equality `μ (to_measurable μ t ∩ s) = μ (t ∩ s)`.
 This only holds when `μ` is σ-finite. For a version without this assumption (but requiring