feat: generalise more lemmas to enorms (#27456)

grunweg · grunweg · commit cd9fe442121c · 2025-07-26T12:55:37.000Z
The selection of lemmas may seem eclectic, but follows a clear path: these are necessary for generalising the last section of IntegrableOn.lean to enorms.
diff --git a/Mathlib/Analysis/BoxIntegral/Integrability.lean b/Mathlib/Analysis/BoxIntegral/Integrability.lean
@@ -336,7 +336,7 @@ theorem AEContinuous.hasBoxIntegral [CompleteSpace E] {f : (ι → ℝ) → E} (
       isFiniteMeasure_of_le (μ.restrict (Box.Icc I))
                             (μ.restrict_mono Box.coe_subset_Icc (le_refl μ))
     obtain ⟨C, hC⟩ := hb
-    refine hasFiniteIntegral_of_bounded (C := C) (Filter.eventually_iff_exists_mem.2 ?_)
+    refine .of_bounded (C := C) (Filter.eventually_iff_exists_mem.2 ?_)
     use I, self_mem_ae_restrict I.measurableSet_coe, fun y hy ↦ hC y (I.coe_subset_Icc hy)
 
 end MeasureTheory
diff --git a/Mathlib/MeasureTheory/Function/L1Space/HasFiniteIntegral.lean b/Mathlib/MeasureTheory/Function/L1Space/HasFiniteIntegral.lean
@@ -194,21 +194,27 @@ theorem HasFiniteIntegral.of_mem_Icc [IsFiniteMeasure μ] (a b : ℝ) {X : α 
   apply (hasFiniteIntegral_const (max ‖a‖ ‖b‖)).mono'
   filter_upwards [h.mono fun ω h ↦ h.1, h.mono fun ω h ↦ h.2] with ω using abs_le_max_abs_abs
 
-theorem hasFiniteIntegral_of_bounded_enorm [IsFiniteMeasure μ] {f : α → ε} {C : ℝ≥0}
-    (hC : ∀ᵐ a ∂μ, ‖f a‖ₑ ≤ C) : HasFiniteIntegral f μ :=
-  (hasFiniteIntegral_const_enorm (enorm_ne_top (x := C))).mono'_enorm hC
+theorem HasFiniteIntegral.of_bounded_enorm [IsFiniteMeasure μ] {f : α → ε} {C : ℝ≥0∞}
+    (hC' : ‖C‖ₑ ≠ ∞ := by finiteness) (hC : ∀ᵐ a ∂μ, ‖f a‖ₑ ≤ C) : HasFiniteIntegral f μ :=
+  (hasFiniteIntegral_const_enorm hC').mono'_enorm hC
 
-theorem hasFiniteIntegral_of_bounded [IsFiniteMeasure μ] {f : α → β} {C : ℝ}
+@[deprecated (since := "2025-07-26")]
+alias hasFiniteIntegral_of_bounded_enorm := HasFiniteIntegral.of_bounded_enorm
+
+theorem HasFiniteIntegral.of_bounded [IsFiniteMeasure μ] {f : α → β} {C : ℝ}
     (hC : ∀ᵐ a ∂μ, ‖f a‖ ≤ C) : HasFiniteIntegral f μ :=
   (hasFiniteIntegral_const C).mono' hC
 
+@[deprecated (since := "2025-07-26")]
+alias hasFiniteIntegral_of_bounded := HasFiniteIntegral.of_bounded
+
 -- TODO: generalise this to f with codomain ε
 -- requires generalising `norm_le_pi_norm` and friends to enorms
 @[simp]
 theorem HasFiniteIntegral.of_finite [Finite α] [IsFiniteMeasure μ] {f : α → β} :
     HasFiniteIntegral f μ :=
   let ⟨_⟩ := nonempty_fintype α
-  hasFiniteIntegral_of_bounded <| ae_of_all μ <| norm_le_pi_norm f
+  .of_bounded <| ae_of_all μ <| norm_le_pi_norm f
 
 theorem HasFiniteIntegral.mono_measure {f : α → ε} (h : HasFiniteIntegral f ν) (hμ : μ ≤ ν) :
     HasFiniteIntegral f μ :=
@@ -445,14 +451,27 @@ variable {𝕜 : Type*}
 
 @[fun_prop]
 theorem HasFiniteIntegral.smul [NormedAddCommGroup 𝕜] [SMulZeroClass 𝕜 β] [IsBoundedSMul 𝕜 β]
-    (c : 𝕜) {f : α → β} :
-    HasFiniteIntegral f μ → HasFiniteIntegral (c • f) μ := by
-  simp only [HasFiniteIntegral]; intro hfi
+    (c : 𝕜) {f : α → β} (hf : HasFiniteIntegral f μ) :
+    HasFiniteIntegral (c • f) μ := by
+  simp only [HasFiniteIntegral]
   calc
     ∫⁻ a : α, ‖c • f a‖ₑ ∂μ ≤ ∫⁻ a : α, ‖c‖ₑ * ‖f a‖ₑ ∂μ := lintegral_mono fun i ↦ enorm_smul_le
     _ < ∞ := by
       rw [lintegral_const_mul']
-      exacts [mul_lt_top coe_lt_top hfi, coe_ne_top]
+      exacts [mul_lt_top coe_lt_top hf, coe_ne_top]
+
+-- TODO: weaken the hypothesis to a version of `ENormSMulClass` with `≤`,
+-- once such a typeclass exists.
+-- This will let us unify with `HasFiniteIntegral.smul` above.
+@[fun_prop]
+theorem HasFiniteIntegral.smul_enorm [NormedAddGroup 𝕜] [SMul 𝕜 ε''] [ENormSMulClass 𝕜 ε'']
+    (c : 𝕜) {f : α → ε''} (hf : HasFiniteIntegral f μ) : HasFiniteIntegral (c • f) μ := by
+  simp only [HasFiniteIntegral]
+  calc
+    ∫⁻ a : α, ‖c • f a‖ₑ ∂μ = ∫⁻ a : α, ‖c‖ₑ * ‖f a‖ₑ ∂μ := lintegral_congr fun i ↦ enorm_smul _ _
+    _ < ∞ := by
+      rw [lintegral_const_mul']
+      exacts [mul_lt_top coe_lt_top hf, coe_ne_top]
 
 theorem hasFiniteIntegral_smul_iff [NormedRing 𝕜] [MulActionWithZero 𝕜 β] [IsBoundedSMul 𝕜 β]
     {c : 𝕜} (hc : IsUnit c) (f : α → β) :
diff --git a/Mathlib/MeasureTheory/Function/L1Space/Integrable.lean b/Mathlib/MeasureTheory/Function/L1Space/Integrable.lean
@@ -951,6 +951,7 @@ end PosPart
 section IsBoundedSMul
 
 variable {𝕜 : Type*}
+  {ε : Type*} [TopologicalSpace ε] [ENormedAddMonoid ε]
 
 @[fun_prop]
 theorem Integrable.smul [NormedAddCommGroup 𝕜] [SMulZeroClass 𝕜 β] [IsBoundedSMul 𝕜 β] (c : 𝕜)
@@ -962,6 +963,17 @@ theorem Integrable.fun_smul [NormedAddCommGroup 𝕜] [SMulZeroClass 𝕜 β] [I
     {f : α → β} (hf : Integrable f μ) : Integrable (fun x ↦ c • f x) μ :=
   hf.smul c
 
+@[fun_prop]
+theorem Integrable.smul_enorm
+    [NormedAddCommGroup 𝕜] [SMul 𝕜 ε] [ContinuousConstSMul 𝕜 ε] [ENormSMulClass 𝕜 ε] (c : 𝕜)
+    {f : α → ε} (hf : Integrable f μ) : Integrable (c • f) μ := by
+  constructor <;> fun_prop
+
+theorem Integrable.fun_smul_enorm
+    [NormedAddCommGroup 𝕜] [SMul 𝕜 ε] [ContinuousConstSMul 𝕜 ε] [ENormSMulClass 𝕜 ε] (c : 𝕜)
+    {f : α → ε} (hf : Integrable f μ) : Integrable (fun x ↦ c • f x) μ :=
+  hf.smul_enorm c
+
 theorem _root_.IsUnit.integrable_smul_iff [NormedRing 𝕜] [MulActionWithZero 𝕜 β]
     [IsBoundedSMul 𝕜 β] {c : 𝕜} (hc : IsUnit c) (f : α → β) :
     Integrable (c • f) μ ↔ Integrable f μ :=
diff --git a/Mathlib/MeasureTheory/Function/LocallyIntegrable.lean b/Mathlib/MeasureTheory/Function/LocallyIntegrable.lean
@@ -444,7 +444,7 @@ theorem ContinuousOn.integrableOn_compact'
   have : Fact (μ K < ∞) := ⟨hK.measure_lt_top⟩
   obtain ⟨C, hC⟩ : ∃ C, ∀ x ∈ f '' K, ‖x‖ ≤ C :=
     IsBounded.exists_norm_le (hK.image_of_continuousOn hf).isBounded
-  apply hasFiniteIntegral_of_bounded (C := C)
+  apply HasFiniteIntegral.of_bounded (C := C)
   filter_upwards [ae_restrict_mem h'K] with x hx using hC _ (mem_image_of_mem f hx)
 
 theorem ContinuousOn.integrableOn_compact [T2Space X]
diff --git a/Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean b/Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
@@ -1377,8 +1377,7 @@ In this section we show inequalities on the norm.
 
 section IsBoundedSMul
 
-variable {𝕜 : Type*} [NormedRing 𝕜] [MulActionWithZero 𝕜 E] [MulActionWithZero 𝕜 F]
-variable [IsBoundedSMul 𝕜 E] [IsBoundedSMul 𝕜 F] {c : 𝕜} {f : α → F}
+variable {𝕜 : Type*} [NormedRing 𝕜] [MulActionWithZero 𝕜 F] [IsBoundedSMul 𝕜 F] {c : 𝕜} {f : α → F}
 
 theorem eLpNorm'_const_smul_le (hq : 0 < q) : eLpNorm' (c • f) q μ ≤ ‖c‖ₑ * eLpNorm' f q μ :=
   eLpNorm'_le_nnreal_smul_eLpNorm'_of_ae_le_mul (Eventually.of_forall fun _ => nnnorm_smul_le ..) hq
@@ -1392,8 +1391,7 @@ theorem eLpNorm_const_smul_le : eLpNorm (c • f) p μ ≤ ‖c‖ₑ * eLpNorm
     (Eventually.of_forall fun _ => by simp [nnnorm_smul_le]) _
 
 theorem MemLp.const_smul (hf : MemLp f p μ) (c : 𝕜) : MemLp (c • f) p μ :=
-  ⟨AEStronglyMeasurable.const_smul hf.1 c,
-    eLpNorm_const_smul_le.trans_lt (ENNReal.mul_lt_top ENNReal.coe_lt_top hf.2)⟩
+  ⟨hf.1.const_smul c, eLpNorm_const_smul_le.trans_lt (ENNReal.mul_lt_top ENNReal.coe_lt_top hf.2)⟩
 
 @[deprecated (since := "2025-02-21")]
 alias Memℒp.const_smul := MemLp.const_smul
@@ -1406,6 +1404,33 @@ alias Memℒp.const_mul := MemLp.const_mul
 
 end IsBoundedSMul
 
+section ENormSMulClass
+
+variable {𝕜 : Type*} [NormedRing 𝕜]
+  {ε : Type*} [TopologicalSpace ε] [ENormedAddMonoid ε] [SMul 𝕜 ε] [ENormSMulClass 𝕜 ε]
+  {c : 𝕜} {f : α → ε}
+
+theorem eLpNorm'_const_smul_le' (hq : 0 < q) : eLpNorm' (c • f) q μ ≤ ‖c‖ₑ * eLpNorm' f q μ :=
+  eLpNorm'_le_nnreal_smul_eLpNorm'_of_ae_le_mul'
+    (Eventually.of_forall fun _ ↦ le_of_eq (enorm_smul ..)) hq
+
+theorem eLpNormEssSup_const_smul_le' : eLpNormEssSup (c • f) μ ≤ ‖c‖ₑ * eLpNormEssSup f μ :=
+  eLpNormEssSup_le_nnreal_smul_eLpNormEssSup_of_ae_le_mul'
+    (Eventually.of_forall fun _ => by simp [enorm_smul])
+
+theorem eLpNorm_const_smul_le' : eLpNorm (c • f) p μ ≤ ‖c‖ₑ * eLpNorm f p μ :=
+  eLpNorm_le_nnreal_smul_eLpNorm_of_ae_le_mul'
+    (Eventually.of_forall fun _ => le_of_eq (enorm_smul ..)) _
+
+theorem MemLp.const_smul' [ContinuousConstSMul 𝕜 ε] (hf : MemLp f p μ) (c : 𝕜) :
+    MemLp (c • f) p μ :=
+  ⟨hf.1.const_smul c, eLpNorm_const_smul_le'.trans_lt (ENNReal.mul_lt_top ENNReal.coe_lt_top hf.2)⟩
+
+theorem MemLp.const_mul' {f : α → 𝕜} (hf : MemLp f p μ) (c : 𝕜) : MemLp (fun x => c * f x) p μ :=
+  hf.const_smul c
+
+end ENormSMulClass
+
 /-!
 ### Bounded actions by normed division rings
 The inequalities in the previous section are now tight.
@@ -1415,8 +1440,7 @@ TODO: do these results hold for any `NormedRing` assuming `NormSMulClass`?
 
 section NormedSpace
 
-variable {𝕜 : Type*} [NormedDivisionRing 𝕜] [MulActionWithZero 𝕜 E] [Module 𝕜 F]
-variable [NormSMulClass 𝕜 E] [NormSMulClass 𝕜 F]
+variable {𝕜 : Type*} [NormedDivisionRing 𝕜] [Module 𝕜 F] [NormSMulClass 𝕜 F]
 
 theorem eLpNorm'_const_smul {f : α → F} (c : 𝕜) (hq_pos : 0 < q) :
     eLpNorm' (c • f) q μ = ‖c‖ₑ * eLpNorm' f q μ := by
diff --git a/Mathlib/MeasureTheory/Integral/IntegrableOn.lean b/Mathlib/MeasureTheory/Integral/IntegrableOn.lean
@@ -72,15 +72,24 @@ namespace MeasureTheory
 
 section NormedAddCommGroup
 
-theorem hasFiniteIntegral_restrict_of_bounded [NormedAddCommGroup E] {f : α → E} {s : Set α}
+theorem HasFiniteIntegral.restrict_of_bounded [NormedAddCommGroup E] {f : α → E} {s : Set α}
     {μ : Measure α} {C} (hs : μ s < ∞) (hf : ∀ᵐ x ∂μ.restrict s, ‖f x‖ ≤ C) :
     HasFiniteIntegral f (μ.restrict s) :=
   haveI : IsFiniteMeasure (μ.restrict s) := ⟨by rwa [Measure.restrict_apply_univ]⟩
-  hasFiniteIntegral_of_bounded hf
+  .of_bounded hf
+
+@[deprecated (since := "2025-07-26")]
+alias hasFiniteIntegral_restrict_of_bounded := HasFiniteIntegral.restrict_of_bounded
 
 variable [NormedAddCommGroup E] {f g : α → ε} {s t : Set α} {μ ν : Measure α}
   [TopologicalSpace ε] [ContinuousENorm ε]
 
+theorem HasFiniteIntegral.restrict_of_bounded_enorm {C : ℝ≥0∞} (hC : ‖C‖ₑ ≠ ∞ := by finiteness)
+    (hs : μ s ≠ ∞ := by finiteness) (hf : ∀ᵐ x ∂μ.restrict s, ‖f x‖ₑ ≤ C) :
+    HasFiniteIntegral f (μ.restrict s) :=
+  haveI : IsFiniteMeasure (μ.restrict s) := ⟨by rw [Measure.restrict_apply_univ]; exact hs.lt_top⟩
+  .of_bounded_enorm hC hf
+
 /-- A function is `IntegrableOn` a set `s` if it is almost everywhere strongly measurable on `s`
 and if the integral of its pointwise norm over `s` is less than infinity. -/
 def IntegrableOn (f : α → ε) (s : Set α) (μ : Measure α := by volume_tac) : Prop :=
@@ -533,7 +542,7 @@ theorem Measure.FiniteAtFilter.integrableAtFilter {f : α → E} {l : Filter α}
     hf.imp fun C hC => eventually_smallSets.2 ⟨_, hC, fun t => id⟩
   rcases (hfm.eventually.and (hμ.eventually.and hC)).exists_measurable_mem_of_smallSets with
     ⟨s, hsl, hsm, hfm, hμ, hC⟩
-  refine ⟨s, hsl, ⟨hfm, hasFiniteIntegral_restrict_of_bounded hμ (C := C) ?_⟩⟩
+  refine ⟨s, hsl, ⟨hfm, .restrict_of_bounded hμ (C := C) ?_⟩⟩
   rw [ae_restrict_eq hsm, eventually_inf_principal]
   exact Eventually.of_forall hC
 
@@ -557,7 +566,7 @@ alias _root_.Filter.Tendsto.integrableAtFilter :=
 lemma Measure.integrableOn_of_bounded {f : α → E} (s_finite : μ s ≠ ∞)
     (f_mble : AEStronglyMeasurable f μ) {M : ℝ} (f_bdd : ∀ᵐ a ∂(μ.restrict s), ‖f a‖ ≤ M) :
     IntegrableOn f s μ :=
-  ⟨f_mble.restrict, hasFiniteIntegral_restrict_of_bounded (C := M) s_finite.lt_top f_bdd⟩
+  ⟨f_mble.restrict, .restrict_of_bounded (C := M) s_finite.lt_top f_bdd⟩
 
 theorem integrable_add_of_disjoint {f g : α → E} (h : Disjoint (support f) (support g))
     (hf : StronglyMeasurable f) (hg : StronglyMeasurable g) :
diff --git a/Mathlib/MeasureTheory/Integral/Prod.lean b/Mathlib/MeasureTheory/Integral/Prod.lean
@@ -572,7 +572,7 @@ lemma integral_integral_swap_of_hasCompactSupport
     apply (integrableOn_iff_integrable_of_support_subset (subset_tsupport f.uncurry)).mp
     refine ⟨(h'f.stronglyMeasurable_of_prod hf).aestronglyMeasurable, ?_⟩
     obtain ⟨C, hC⟩ : ∃ C, ∀ p, ‖f.uncurry p‖ ≤ C := hf.bounded_above_of_compact_support h'f
-    exact hasFiniteIntegral_of_bounded (C := C) (Eventually.of_forall hC)
+    exact .of_bounded (C := C) (.of_forall hC)
   _ = ∫ y, (∫ x in U, f x y ∂μ) ∂ν := by
     apply setIntegral_eq_integral_of_forall_compl_eq_zero (fun y hy ↦ ?_)
     have : ∀ x, f x y = 0 := by
diff --git a/Mathlib/Probability/Martingale/Upcrossing.lean b/Mathlib/Probability/Martingale/Upcrossing.lean
@@ -750,7 +750,7 @@ theorem Adapted.integrable_upcrossingsBefore [IsFiniteMeasure μ] (hf : Adapted
     rw [Real.norm_eq_abs, Nat.abs_cast, Nat.cast_le]
     exact upcrossingsBefore_le _ _ hab
   ⟨Measurable.aestronglyMeasurable (measurable_from_top.comp (hf.measurable_upcrossingsBefore hab)),
-    hasFiniteIntegral_of_bounded this⟩
+    .of_bounded this⟩
 
 /-- The number of upcrossings of a realization of a stochastic process (`upcrossings` takes value
 in `ℝ≥0∞` and so is allowed to be `∞`). -/
