feat(Analysis/FunctionalSpaces): the one-dimensional Poincaré inequality

Mathlib.lean

@@ -2014,6 +2014,7 @@ public import Mathlib.Analysis.Fourier.Notation
 public import Mathlib.Analysis.Fourier.PoissonSummation
 public import Mathlib.Analysis.Fourier.RiemannLebesgueLemma
 public import Mathlib.Analysis.Fourier.ZMod
+public import Mathlib.Analysis.FunctionalSpaces.PoincareInequality
 public import Mathlib.Analysis.FunctionalSpaces.SobolevInequality
 public import Mathlib.Analysis.Hofer
 public import Mathlib.Analysis.InnerProductSpace.Adjoint

Mathlib/Analysis/FunctionalSpaces/PoincareInequality.lean

@@ -0,0 +1,188 @@
+/-
+Copyright (c) 2026 Alejandro Soto Franco. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Alejandro Soto Franco
+-/
+module
+
+public import Mathlib.MeasureTheory.Integral.MeanInequalities
+public import Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff
+public import Mathlib.Analysis.SpecialFunctions.Integrals.Basic
+
+/-!
+# The one-dimensional Poincaré inequality
+
+For a function `f : ℝ → E` valued in a normed space that is continuous on a
+compact interval `[a, b]`, continuously differentiable on the open interval
+`(a, b)`, and vanishes at the left endpoint, the `Lᵖ` norm of `f` is controlled
+by the `Lᵖ` norm of its derivative, for any `1 ≤ p`:
+`∫⁻ x in Icc a b, ‖f x‖ₑ ^ p ≤`
+`ENNReal.ofReal ((b - a) ^ p / p) * ∫⁻ x in Icc a b, ‖deriv f x‖ₑ ^ p`.
+
+The statement is phrased with lower Lebesgue integrals, so that no integrability
+hypothesis on the derivative is needed: if the right-hand side integral is
+infinite the inequality is automatic, and otherwise the derivative is `Lᵖ` and
+the analytic argument goes through.
+
+## Proof outline
+
+* `enorm_sub_le_lintegral_deriv_of_contDiffOn_Ioo` is the pointwise estimate
+  coming from the fundamental theorem of calculus: `‖f x - f a‖ₑ ≤ ∫⁻ t in
+  Ioc a x, ‖deriv f t‖ₑ`. It holds with no integrability hypothesis and only
+  requires `f` to be `C¹` on the open interval.
+* `ENNReal.rpow_lintegral_le_measure_rpow_mul_lintegral_rpow` is the power-mean
+  inequality against the constant function `1`, in the form
+  `(∫⁻ t in s, g t) ^ p ≤ μ s ^ (p - 1) * ∫⁻ t in s, g t ^ p`. It is obtained
+  from the Hölder inequality `ENNReal.lintegral_mul_le_Lp_mul_Lq` with conjugate
+  exponents `p` and `p / (p - 1)`.
+* Combining the two gives the pointwise bound `‖f x‖ₑ ^ p ≤ ENNReal.ofReal
+  ((x - a) ^ (p - 1)) * M` with `M = ∫⁻ x in Icc a b, ‖deriv f x‖ₑ ^ p`.
+  Integrating over `[a, b]` and using `∫ x in a..b, (x - a) ^ (p - 1)
+  = (b - a) ^ p / p` yields the constant.
+
+## Main results
+
+* `MeasureTheory.poincare_1d`: the one-dimensional `Lᵖ` Poincaré inequality.
+* `MeasureTheory.poincare_1d_uIcc`: the same inequality over the unordered
+  interval `[[a, b]]`, requiring only `f a = 0`.
+-/
+
+public section
+
+open scoped ENNReal NNReal
+
+open MeasureTheory Set
+
+/-- **The one-dimensional `Lᵖ` Poincaré inequality.** For `1 ≤ p` and `f : ℝ → E`
+continuous on `[a, b]`, continuously differentiable on `(a, b)`, and vanishing at
+the left endpoint, the `Lᵖ` norm of `f` is controlled by the `Lᵖ` norm of its
+derivative:
+`∫⁻ x in Icc a b, ‖f x‖ₑ ^ p ≤`
+`ENNReal.ofReal ((b - a) ^ p / p) * ∫⁻ x in Icc a b, ‖deriv f x‖ₑ ^ p`.
+
+No integrability hypothesis on the derivative is required: the bound is phrased
+with lower Lebesgue integrals, so it is automatic when the right-hand side is
+infinite. -/
+theorem MeasureTheory.poincare_1d {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
+    {a b p : ℝ} (hab : a ≤ b) (hp : 1 ≤ p) {f : ℝ → E}
+    (hcont : ContinuousOn f (Icc a b)) (hdiff : ContDiffOn ℝ 1 f (Ioo a b))
+    (ha : f a = 0) :
+    ∫⁻ x in Icc a b, ‖f x‖ₑ ^ p
+      ≤ ENNReal.ofReal ((b - a) ^ p / p) * ∫⁻ x in Icc a b, ‖deriv f x‖ₑ ^ p := by
+  have hp0 : 0 < p := one_pos.trans_le hp
+  set M : ℝ≥0∞ := ∫⁻ x in Icc a b, ‖deriv f x‖ₑ ^ p
+  have hderiv_cont : ContinuousOn (deriv f) (Ioo a b) :=
+    (hdiff.continuousOn_derivWithin isOpen_Ioo.uniqueDiffOn le_rfl).congr
+      fun x hx => (derivWithin_of_isOpen isOpen_Ioo hx).symm
+  -- Pointwise bound: the FTC estimate followed by the power-mean inequality on `Ioc a x`.
+  have pointwise : ∀ x ∈ Icc a b, ‖f x‖ₑ ^ p ≤ ENNReal.ofReal ((x - a) ^ (p - 1)) * M := by
+    intro x ⟨hax, hxb⟩
+    have hmeas : AEMeasurable (fun t => ‖deriv f t‖ₑ) (volume.restrict (Ioc a x)) := by
+      rw [← Measure.restrict_congr_set (Ioo_ae_eq_Ioc (μ := volume))]
+      exact ((hderiv_cont.mono (Ioo_subset_Ioo_right hxb)).aestronglyMeasurable
+        measurableSet_Ioo).enorm
+    calc ‖f x‖ₑ ^ p
+        = ‖f x - f a‖ₑ ^ p := by rw [ha, sub_zero]
+      _ ≤ (∫⁻ t in Ioc a x, ‖deriv f t‖ₑ) ^ p :=
+          ENNReal.rpow_le_rpow (enorm_sub_le_lintegral_deriv_of_contDiffOn_Ioo
+            (hcont.mono (Icc_subset_Icc_right hxb)) (hdiff.mono (Ioo_subset_Ioo_right hxb)) hax)
+            hp0.le
+      _ ≤ volume (Ioc a x) ^ (p - 1) * ∫⁻ t in Ioc a x, ‖deriv f t‖ₑ ^ p :=
+          ENNReal.rpow_lintegral_le_measure_rpow_mul_lintegral_rpow hp hmeas
+      _ = ENNReal.ofReal ((x - a) ^ (p - 1)) * ∫⁻ t in Ioc a x, ‖deriv f t‖ₑ ^ p := by
+          rw [Real.volume_Ioc, ← ENNReal.ofReal_rpow_of_nonneg (by linarith) (by linarith)]
+      _ ≤ ENNReal.ofReal ((x - a) ^ (p - 1)) * M := by
+          gcongr
+          exact lintegral_mono_set ((Ioc_subset_Ioc_right hxb).trans Ioc_subset_Icc_self)
+  -- The remaining integral evaluates to `(b - a) ^ p / p`.
+  have hxa : ∫⁻ x in Icc a b, ENNReal.ofReal ((x - a) ^ (p - 1))
+      = ENNReal.ofReal ((b - a) ^ p / p) := by
+    have hcontxa : ContinuousOn (fun x : ℝ => (x - a) ^ (p - 1)) (Icc a b) :=
+      (show ContinuousOn (fun x : ℝ => x - a) (Icc a b) by fun_prop).rpow_const
+        fun x _ => Or.inr (by linarith)
+    have hnn : 0 ≤ᵐ[volume.restrict (Icc a b)] fun x : ℝ => (x - a) ^ (p - 1) := by
+      rw [Filter.EventuallyLE, ae_restrict_iff' measurableSet_Icc]
+      exact .of_forall fun x hx => Real.rpow_nonneg (by linarith [hx.1]) _
+    rw [← ofReal_integral_eq_lintegral_ofReal (hcontxa.integrableOn_compact isCompact_Icc) hnn]
+    congr 1
+    rw [integral_Icc_eq_integral_Ioc, ← intervalIntegral.integral_of_le hab,
+      intervalIntegral.integral_comp_sub_right (fun y => y ^ (p - 1)) a]
+    simp only [sub_self]
+    rw [integral_rpow (Or.inl (by linarith)), show p - 1 + 1 = p by ring,
+      Real.zero_rpow hp0.ne', sub_zero]
+  -- Integrate the pointwise estimate and pull out the constant `M`.
+  have hmeasf : Measurable fun x : ℝ => ENNReal.ofReal ((x - a) ^ (p - 1)) := by fun_prop
+  calc ∫⁻ x in Icc a b, ‖f x‖ₑ ^ p
+      ≤ ∫⁻ x in Icc a b, ENNReal.ofReal ((x - a) ^ (p - 1)) * M :=
+        setLIntegral_mono_ae (hmeasf.mul measurable_const).aemeasurable (.of_forall pointwise)
+    _ = (∫⁻ x in Icc a b, ENNReal.ofReal ((x - a) ^ (p - 1))) * M := lintegral_mul_const M hmeasf
+    _ = ENNReal.ofReal ((b - a) ^ p / p) * M := by rw [hxa]
+
+/-- **The one-dimensional `Lᵖ` Poincaré inequality on an unordered interval.** For
+`1 ≤ p` and `f : ℝ → E` continuous on `[[a, b]]`, continuously differentiable on
+the interior `(a ⊓ b, a ⊔ b)`, and vanishing at `a`, the `Lᵖ` norm of `f` is
+controlled by the `Lᵖ` norm of its derivative, with constant
+`edist a b ^ p / ENNReal.ofReal p`. -/
+theorem MeasureTheory.poincare_1d_uIcc {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
+    {a b p : ℝ} (hp : 1 ≤ p) {f : ℝ → E}
+    (hcont : ContinuousOn f (uIcc a b)) (hdiff : ContDiffOn ℝ 1 f (Ioo (a ⊓ b) (a ⊔ b)))
+    (ha : f a = 0) :
+    ∫⁻ x in uIcc a b, ‖f x‖ₑ ^ p
+      ≤ edist a b ^ p / ENNReal.ofReal p * ∫⁻ x in uIcc a b, ‖deriv f x‖ₑ ^ p := by
+  have hp0 : 0 < p := one_pos.trans_le hp
+  rcases le_total a b with hab | hba
+  · rw [uIcc_of_le hab] at hcont ⊢
+    rw [inf_eq_left.2 hab, sup_eq_right.2 hab] at hdiff
+    have hedist : edist a b ^ p / ENNReal.ofReal p = ENNReal.ofReal ((b - a) ^ p / p) := by
+      rw [ENNReal.ofReal_div_of_pos hp0,
+        ← ENNReal.ofReal_rpow_of_nonneg (sub_nonneg.2 hab) hp0.le,
+        show edist a b = ENNReal.ofReal (b - a) by
+          rw [edist_dist, Real.dist_eq, abs_sub_comm, abs_of_nonneg (sub_nonneg.2 hab)]]
+    rw [hedist]
+    exact poincare_1d hab hp hcont hdiff ha
+  · -- Reflect through `x ↦ (a + b) - x`, which fixes `[b, a]` and sends the right
+    -- endpoint `a` to the left endpoint `b`, reducing to `poincare_1d`.
+    rw [uIcc_of_ge hba] at hcont ⊢
+    rw [inf_eq_right.2 hba, sup_eq_left.2 hba] at hdiff
+    set R : ℝ → ℝ := fun x => (a + b) - x with hR
+    set g : ℝ → E := fun x => f (R x) with hg
+    have hRmem : ∀ {x : ℝ}, R x ∈ Icc b a ↔ x ∈ Icc b a := by
+      intro x; simp only [hR, mem_Icc]; constructor <;> intro ⟨h₁, h₂⟩ <;> constructor <;> linarith
+    have hRmapsIoo : MapsTo R (Ioo b a) (Ioo b a) := by
+      intro x hx; simp only [hR, mem_Ioo] at hx ⊢; exact ⟨by linarith [hx.2], by linarith [hx.1]⟩
+    have hRcont : Continuous R := by fun_prop
+    -- `g` inherits the Poincaré hypotheses on `[b, a]`, with `g b = f a = 0`.
+    have hgcont : ContinuousOn g (Icc b a) :=
+      hcont.comp hRcont.continuousOn fun x hx => hRmem.2 hx
+    have hgdiff : ContDiffOn ℝ 1 g (Ioo b a) :=
+      hdiff.comp ((contDiff_const.sub contDiff_id).contDiffOn) hRmapsIoo
+    have hgb : g b = 0 := by simp only [hg, hR, add_sub_cancel_right, ha]
+    -- `R` is a measure-preserving measurable embedding fixing `[b, a]` setwise.
+    have hRmp : MeasurePreserving R volume volume := by
+      have hneg : MeasurePreserving (fun x : ℝ => -1 * x) volume volume :=
+        ⟨by fun_prop, by rw [Real.map_volume_mul_left (by norm_num)]; norm_num⟩
+      have hadd : MeasurePreserving (fun x : ℝ => (a + b) + x) volume volume :=
+        measurePreserving_add_left volume (a + b)
+      simpa only [hR, Function.comp_def, neg_one_mul, ← sub_eq_add_neg] using hadd.comp hneg
+    have hRemb : MeasurableEmbedding R := (Homeomorph.subLeft (a + b)).measurableEmbedding
+    have hRpre : R ⁻¹' Icc b a = Icc b a := by ext x; exact hRmem
+    have hRderiv : ∀ x, deriv g x = -deriv f (R x) := fun x => deriv_comp_const_sub f (a + b) x
+    have hedist : edist a b ^ p / ENNReal.ofReal p = ENNReal.ofReal ((a - b) ^ p / p) := by
+      rw [ENNReal.ofReal_div_of_pos hp0,
+        ← ENNReal.ofReal_rpow_of_nonneg (sub_nonneg.2 hba) hp0.le,
+        show edist a b = ENNReal.ofReal (a - b) by
+          rw [edist_dist, Real.dist_eq, abs_of_nonneg (sub_nonneg.2 hba)]]
+    -- Reflect both integrals back to `f` via the measure-preserving change of variables.
+    have hlhs : ∫⁻ x in Icc b a, ‖g x‖ₑ ^ p = ∫⁻ x in Icc b a, ‖f x‖ₑ ^ p := by
+      have := hRmp.setLIntegral_comp_preimage_emb hRemb (fun x => ‖f x‖ₑ ^ p) (Icc b a)
+      rwa [hRpre] at this
+    have hrhs : ∫⁻ x in Icc b a, ‖deriv g x‖ₑ ^ p = ∫⁻ x in Icc b a, ‖deriv f x‖ₑ ^ p := by
+      have hcomp : ∫⁻ x in Icc b a, ‖deriv f (R x)‖ₑ ^ p = ∫⁻ x in Icc b a, ‖deriv f x‖ₑ ^ p := by
+        have := hRmp.setLIntegral_comp_preimage_emb hRemb
+          (fun x => ‖deriv f x‖ₑ ^ p) (Icc b a)
+        rwa [hRpre] at this
+      rw [← hcomp]
+      refine lintegral_congr fun x => ?_
+      rw [hRderiv, enorm_neg]
+    rw [hedist, ← hlhs, ← hrhs]
+    exact poincare_1d hba hp hgcont hgdiff hgb

Mathlib/MeasureTheory/Integral/IntervalIntegral/ContDiff.lean

@@ -84,27 +84,64 @@ end intervalIntegral
 
 open intervalIntegral
 
+/-- Auxiliary form of `enorm_sub_le_lintegral_deriv_of_contDiffOn_Ioo` for a complete codomain,
+where the second fundamental theorem of calculus is available. -/
+private theorem enorm_sub_le_lintegral_deriv_aux [CompleteSpace E]
+    (hcont : ContinuousOn f (Icc a b)) (hdiff : ContDiffOn ℝ 1 f (Ioo a b)) (hab : a ≤ b) :
+    ‖f b - f a‖ₑ ≤ ∫⁻ t in Ioc a b, ‖deriv f t‖ₑ := by
+  have hderiv_cont : ContinuousOn (deriv f) (Ioo a b) :=
+    (hdiff.continuousOn_derivWithin isOpen_Ioo.uniqueDiffOn le_rfl).congr
+      fun t ht => (derivWithin_of_isOpen isOpen_Ioo ht).symm
+  by_cases hint : IntegrableOn (deriv f) (Ioc a b) volume
+  · -- The fundamental theorem of calculus writes `f b - f a` as an integral.
+    have hftc : f b - f a = ∫ t in a..b, deriv f t :=
+      (intervalIntegral.integral_eq_sub_of_hasDerivAt_of_le hab hcont
+        (fun t ht => ((hdiff.differentiableOn one_ne_zero).differentiableAt
+          (isOpen_Ioo.mem_nhds ht)).hasDerivAt)
+        ((intervalIntegrable_iff_integrableOn_Ioc_of_le hab).mpr hint)).symm
+    rw [hftc, intervalIntegral.integral_of_le hab]
+    exact enorm_integral_le_lintegral_enorm _
+  · -- Otherwise `deriv f` has infinite enorm integral, so the right-hand side is `⊤`.
+    rw [show ∫⁻ t in Ioc a b, ‖deriv f t‖ₑ = ⊤ by
+      by_contra h
+      refine hint ⟨?_, hasFiniteIntegral_iff_enorm.mpr (lt_top_iff_ne_top.2 h)⟩
+      rw [← Measure.restrict_congr_set (Ioo_ae_eq_Ioc (μ := volume))]
+      exact hderiv_cont.aestronglyMeasurable measurableSet_Ioo]
+    exact le_top
+
+open UniformSpace in
+/-- **The second fundamental theorem of calculus, as an extended-norm bound.** If `f : ℝ → E` is
+continuous on `[a, b]` and continuously differentiable on the open interval `(a, b)`, then the
+extended norm of `f b - f a` is bounded by the lower Lebesgue integral of the extended norm of its
+derivative. No integrability hypothesis is required: when the derivative is not integrable the
+right-hand side is `⊤`. Unlike `enorm_sub_le_lintegral_deriv_of_contDiffOn_Icc`, differentiability
+at the endpoints is not assumed. -/
+theorem enorm_sub_le_lintegral_deriv_of_contDiffOn_Ioo
+    (hcont : ContinuousOn f (Icc a b)) (hdiff : ContDiffOn ℝ 1 f (Ioo a b)) (hab : a ≤ b) :
+    ‖f b - f a‖ₑ ≤ ∫⁻ t in Ioc a b, ‖deriv f t‖ₑ := by
+  -- Compose with the isometric inclusion `ι : E →ₗᵢ Completion E`, apply the complete-space lemma,
+  -- then transfer back: `ι` preserves norms and derivatives.
+  set ι : E →ₗᵢ[ℝ] Completion E := Completion.toComplₗᵢ
+  have key := enorm_sub_le_lintegral_deriv_aux (ι.continuous.comp_continuousOn hcont)
+    (hdiff.continuousLinearMap_comp ι.toContinuousLinearMap) hab
+  simp only [Function.comp_def, ← map_sub, ι.enorm_map] at key
+  refine key.trans (le_of_eq (lintegral_congr_ae ?_))
+  have hae : ∀ᵐ t ∂volume.restrict (Ioc a b), t ∈ Ioo a b := by
+    rw [← Measure.restrict_congr_set (Ioo_ae_eq_Ioc (μ := volume))]
+    exact ae_restrict_mem measurableSet_Ioo
+  filter_upwards [hae] with t ht
+  have hfx : DifferentiableAt ℝ f t :=
+    (hdiff.differentiableOn one_ne_zero).differentiableAt (isOpen_Ioo.mem_nhds ht)
+  have hg : HasDerivAt (fun y => ι (f y)) (ι (deriv f t)) t :=
+    ι.toContinuousLinearMap.hasFDerivAt.comp_hasDerivAt t hfx.hasDerivAt
+  rw [hg.deriv, ι.enorm_map]
+
 theorem enorm_sub_le_lintegral_deriv_of_contDiffOn_Icc (h : ContDiffOn ℝ 1 f (Icc a b))
     (hab : a ≤ b) :
     ‖f b - f a‖ₑ ≤ ∫⁻ x in Icc a b, ‖deriv f x‖ₑ := by
-  /- We want to write `f b - f a = ∫ x in Icc a b, deriv f x` and use the inequality between
-  norm of integral and integral of norm. There is a small difficulty that this formula is not
-  true when `E` is not complete, so we need to go first to the completion, and argue there. -/
-  let g := UniformSpace.Completion.toComplₗᵢ (𝕜 := ℝ) (E := E)
-  have : ‖(g ∘ f) b - (g ∘ f) a‖ₑ = ‖f b - f a‖ₑ := by
-    rw [← edist_eq_enorm_sub, Function.comp_def, g.isometry.edist_eq, edist_eq_enorm_sub]
-  rw [← this, ← integral_deriv_of_contDiffOn_Icc (g.contDiff.comp_contDiffOn h) hab,
-    integral_of_le hab, restrict_Ioc_eq_restrict_Icc]
-  apply (enorm_integral_le_lintegral_enorm _).trans
-  apply lintegral_mono_ae
-  rw [← restrict_Ioo_eq_restrict_Icc]
-  filter_upwards [self_mem_ae_restrict measurableSet_Ioo] with x hx
-  rw [fderiv_comp_deriv]; rotate_left
-  · exact (g.contDiff.differentiable one_ne_zero).differentiableAt
-  · exact (h x ⟨hx.1.le, hx.2.le⟩).contDiffAt (Icc_mem_nhds hx.1 hx.2)
-      |>.differentiableAt one_ne_zero
-  have : fderiv ℝ g (f x) = g.toContinuousLinearMap := g.toContinuousLinearMap.fderiv
-  simp [this]
+  rw [← restrict_Ioc_eq_restrict_Icc]
+  exact enorm_sub_le_lintegral_deriv_of_contDiffOn_Ioo h.continuousOn
+    (h.mono Ioo_subset_Icc_self) hab
 
 theorem enorm_sub_le_lintegral_derivWithin_Icc_of_contDiffOn_Icc (h : ContDiffOn ℝ 1 f (Icc a b))
     (hab : a ≤ b) :

Mathlib/MeasureTheory/Integral/MeanInequalities.lean

@@ -165,6 +165,34 @@ theorem lintegral_mul_le_Lp_mul_Lq (μ : Measure α) {p q : ℝ} (hpq : p.Holder
   -- non-⊤ non-zero case
   exact ENNReal.lintegral_mul_le_Lp_mul_Lq_of_ne_zero_of_ne_top hpq hf hf_top hg_top hf_zero hg_zero
 
+/-- **Power-mean inequality against the constant function `1`.** For `1 ≤ p`, the
+`p`-th power of `∫⁻ t in s, g t` is at most `μ s ^ (p - 1)` times
+`∫⁻ t in s, g t ^ p`. The case `p = 2` is Cauchy–Schwarz. It follows from
+Hölder's inequality with conjugate exponents `p` and `p / (p - 1)`. -/
+theorem rpow_lintegral_le_measure_rpow_mul_lintegral_rpow {s : Set α} {g : α → ℝ≥0∞}
+    {p : ℝ} (hp : 1 ≤ p) (hg : AEMeasurable g (μ.restrict s)) :
+    (∫⁻ t in s, g t ∂μ) ^ p ≤ μ s ^ (p - 1) * ∫⁻ t in s, g t ^ p ∂μ := by
+  rcases hp.lt_or_eq with hp1 | hp1
+  · -- `1 < p`: Hölder against `1` with conjugate exponent `q = p / (p - 1)`.
+    set q := p.conjExponent with hq
+    have hpq : p.HolderConjugate q := .conjExponent hp1
+    have hp0 : 0 < p := hpq.pos
+    have hH := ENNReal.lintegral_mul_le_Lp_mul_Lq (μ.restrict s) hpq hg
+      (g := fun _ => (1 : ℝ≥0∞)) aemeasurable_const
+    simp only [Pi.mul_apply, mul_one, ENNReal.one_rpow, setLIntegral_const, one_mul] at hH
+    calc (∫⁻ t in s, g t ∂μ) ^ p
+        ≤ ((∫⁻ t in s, g t ^ p ∂μ) ^ (1 / p) * μ s ^ (1 / q)) ^ p :=
+          ENNReal.rpow_le_rpow hH hp0.le
+      _ = (∫⁻ t in s, g t ^ p ∂μ) ^ (1 / p * p) * μ s ^ (1 / q * p) := by
+          rw [ENNReal.mul_rpow_of_nonneg _ _ hp0.le, ← ENNReal.rpow_mul, ← ENNReal.rpow_mul]
+      _ = μ s ^ (p - 1) * ∫⁻ t in s, g t ^ p ∂μ := by
+          rw [one_div_mul_cancel hp0.ne', ENNReal.rpow_one,
+            show 1 / q * p = p - 1 by rw [one_div, inv_mul_eq_div, hpq.div_conj_eq_sub_one],
+            mul_comm]
+  · -- `p = 1`: both sides equal `∫⁻ t in s, g t`.
+    subst hp1
+    simp
+
 /-- A different formulation of Hölder's inequality for two functions, with two exponents that sum to
 1, instead of reciprocals of -/
 theorem lintegral_mul_norm_pow_le {α} [MeasurableSpace α] {μ : Measure α}