refactor(Analysis/SpecialFunctions/ImproperIntegrals): generalize Frullani's integral to locally integrable functions

Address review: weaken `ContinuousOn` to `LocallyIntegrableOn`, drop unused helper lemmas, require only `c ≠ 0` in `integral_comp_mul_inv_smul`, and localize `[CompleteSpace E]`.

Author: Deep0Thinking

Mathlib/Analysis/SpecialFunctions/ImproperIntegrals.lean

@@ -19,6 +19,9 @@ half-infinite intervals in `ℝ`.
 These lemmas are stated in terms of either `Iic` or `Ioi` (neglecting `Iio` and `Ici`) to match
 mathlib's conventions for integrals over finite intervals (see `intervalIntegral`).
 
+The file also proves **Frullani's integral** (`Frullani.integral_Ioi_eq`), together with its limit
+form `Frullani.tendsto_intervalIntegral`.
+
 ## See also
 
 - `Mathlib/Analysis/SpecialFunctions/Integrals/Basic.lean`: specific integrals over finite intervals
@@ -292,28 +295,32 @@ namespace Frullani
 
 open Metric
 
-variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E}
+variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E}
          {a b c : ℝ} {L R : E}
 
-omit [CompleteSpace E] in
-lemma intervalIntegrable_inv_smul (hf : ContinuousOn f (Ioi 0)) {p q : ℝ} (hp : 0 < p)
+lemma intervalIntegrable_inv_smul (hf : LocallyIntegrableOn f (Ioi 0)) {p q : ℝ} (hp : 0 < p)
     (hq : 0 < q) : IntervalIntegrable (fun x ↦ x⁻¹ • f x) volume p q := by
-  apply ContinuousOn.intervalIntegrable
   have hsub : uIcc p q ⊆ Ioi 0 := by simp [uIcc, Icc_subset_Ioi_iff, hp, hq]
-  exact (continuousOn_inv₀.mono (fun x hx ↦ ne_of_gt (hsub hx))).smul (hf.mono hsub)
-
-omit [CompleteSpace E] in
-lemma intervalIntegrable_inv_smul_comp_mul (hf : ContinuousOn f (Ioi 0)) {p q : ℝ} (hp : 0 < p)
-    (hq : 0 < q) (hc : 0 < c) : IntervalIntegrable (fun x ↦ x⁻¹ • f (c * x)) volume p q := by
-  apply ContinuousOn.intervalIntegrable
+  have hf_int : IntervalIntegrable f volume p q :=
+    intervalIntegrable_iff.mpr
+      ((hf.integrableOn_compact_subset hsub isCompact_uIcc).mono_set uIoc_subset_uIcc)
+  exact hf_int.continuousOn_smul (continuousOn_inv₀.mono fun x hx ↦ ne_of_gt (hsub hx))
+
+lemma intervalIntegrable_inv_smul_comp_mul (hf : LocallyIntegrableOn f (Ioi 0)) {p q : ℝ}
+    (hp : 0 < p) (hq : 0 < q) (hc : 0 < c) :
+    IntervalIntegrable (fun x ↦ x⁻¹ • f (c * x)) volume p q := by
   have hsub : uIcc p q ⊆ Ioi 0 := by simp [uIcc, Icc_subset_Ioi_iff, hp, hq]
-  exact (continuousOn_inv₀.mono (fun x hx ↦ ne_of_gt (hsub hx))).smul
-    (hf.comp (continuousOn_const.mul continuousOn_id) fun x hx ↦ mul_pos hc (hsub hx))
-
-omit [CompleteSpace E] in
-lemma integral_comp_mul_inv_smul {ε r : ℝ} (hc : 0 < c) :
+  have hf_cint : IntervalIntegrable f volume (c * p) (c * q) :=
+    intervalIntegrable_iff.mpr
+      ((hf.integrableOn_compact_subset (by simp [uIcc, Icc_subset_Ioi_iff, mul_pos hc hp,
+        mul_pos hc hq]) isCompact_uIcc).mono_set uIoc_subset_uIcc)
+  have hf_comp : IntervalIntegrable (fun x ↦ f (c * x)) volume p q := by
+    have h := hf_cint.comp_mul_left (c := c)
+    rwa [mul_div_cancel_left₀ p hc.ne', mul_div_cancel_left₀ q hc.ne'] at h
+  exact hf_comp.continuousOn_smul (continuousOn_inv₀.mono fun x hx ↦ ne_of_gt (hsub hx))
+
+lemma integral_comp_mul_inv_smul {ε r : ℝ} (hc : c ≠ 0) :
     ∫ x in ε..r, x⁻¹ • f (c * x) = ∫ x in c * ε..c * r, x⁻¹ • f x := by
-  have hc' : c ≠ 0 := ne_of_gt hc
   let u : ℝ → E := fun x ↦ x⁻¹ • f x
   have key : (fun x ↦ x⁻¹ • f (c * x)) = fun x ↦ c • u (c * x) := by
     funext x
@@ -322,7 +329,9 @@ lemma integral_comp_mul_inv_smul {ε r : ℝ} (hc : 0 < c) :
     field_simp
   rw [key, intervalIntegral.integral_smul, smul_integral_comp_mul_left]
 
-lemma norm_integral_inv_smul_sub_le (hf : ContinuousOn f (Ioi 0)) {p q : ℝ} (hp : 0 < p)
+variable [CompleteSpace E]
+
+lemma norm_integral_inv_smul_sub_le (hf : LocallyIntegrableOn f (Ioi 0)) {p q : ℝ} (hp : 0 < p)
     (hq : 0 < q) {V : E} {δ : ℝ} (hδ : 0 ≤ δ) (h : ∀ x ∈ uIoc p q, ‖f x - V‖ ≤ δ) :
     ‖(∫ x in p..q, x⁻¹ • f x) - log (q / p) • V‖ ≤ δ * |log (q / p)| := by
   have hsub : uIcc p q ⊆ Ioi 0 := by simp [uIcc, Icc_subset_Ioi_iff, hp, hq]
@@ -334,7 +343,7 @@ lemma norm_integral_inv_smul_sub_le (hf : ContinuousOn f (Ioi 0)) {p q : ℝ} (h
   have hint_inv : IntervalIntegrable (fun x : ℝ ↦ x⁻¹ * δ) volume p q := by
     apply ContinuousOn.intervalIntegrable
     exact (continuousOn_inv₀.mono (fun x hx ↦ ne_of_gt (hsub hx))).mul continuousOn_const
-  calc
+  calc ‖(∫ x in p..q, x⁻¹ • f x) - log (q / p) • V‖
     _ = ‖∫ x in p..q, x⁻¹ • (f x - V)‖ := by
         congr 1
         have : log (q / p) • V = ∫ x in p..q, x⁻¹ • V := by
@@ -359,7 +368,7 @@ lemma norm_integral_inv_smul_sub_le (hf : ContinuousOn f (Ioi 0)) {p q : ℝ} (h
         rw [heq, intervalIntegral.integral_const_mul, integral_inv_of_pos hp hq]
         exact (abs_mul δ (log (q / p))).trans (by rw [abs_of_nonneg hδ])
 
-lemma tendsto_integral_inv_smul_of_tendsto_uniform (hf : ContinuousOn f (Ioi 0)) (ha : 0 < a)
+lemma tendsto_integral_inv_smul_of_tendsto_uniform (hf : LocallyIntegrableOn f (Ioi 0)) (ha : 0 < a)
     (hb : 0 < b) {F : Filter ℝ} (hpos : ∀ᶠ t in F, 0 < t) {V : E}
     (huni : ∀ δ > 0, ∀ᶠ t in F, ∀ x ∈ uIoc (a * t) (b * t), ‖f x - V‖ ≤ δ) :
     Tendsto (fun t ↦ ∫ x in (a * t)..(b * t), x⁻¹ • f x) F (𝓝 (log (b / a) • V)) := by
@@ -373,21 +382,21 @@ lemma tendsto_integral_inv_smul_of_tendsto_uniform (hf : ContinuousOn f (Ioi 0))
   have hbε : 0 < b * t := mul_pos hb ht_pos
   have hlog_eq : log (b * t / (a * t)) = log (b / a) := by
     rw [mul_div_mul_right b a (ne_of_gt ht_pos)]
-  calc
+  calc dist (∫ x in a * t..b * t, x⁻¹ • f x) (log (b / a) • V)
     _ = ‖(∫ x in a * t..b * t, x⁻¹ • f x) - log (b / a) • V‖ := dist_eq_norm _ _
     _ = ‖(∫ x in a * t..b * t, x⁻¹ • f x) - log (b * t / (a * t)) • V‖ := by rw [hlog_eq]
     _ ≤ δ' * |log (b * t / (a * t))| :=
         norm_integral_inv_smul_sub_le hf haε hbε hδ'.le hbound
     _ = δ' * C := by rw [hlog_eq]
     _ < δ := by
-        calc
+        calc δ' * C
           _ = δ * (C / (C + 1)) := by ring
           _ < δ * 1 :=
             mul_lt_mul_of_pos_left ((div_lt_one (by positivity)).2 (lt_add_one C)) hδ
           _ = δ := mul_one δ
 
-lemma tendsto_integral_inv_smul_nhdsWithin (hf : ContinuousOn f (Ioi 0)) (ha : 0 < a) (hb : 0 < b)
-    (hL : Tendsto f (𝓝[>] 0) (𝓝 L)) :
+lemma tendsto_integral_inv_smul_nhdsWithin (hf : LocallyIntegrableOn f (Ioi 0)) (ha : 0 < a)
+    (hb : 0 < b) (hL : Tendsto f (𝓝[>] 0) (𝓝 L)) :
     Tendsto (fun ε ↦ ∫ x in (a * ε)..(b * ε), x⁻¹ • f x) (𝓝[>] 0) (𝓝 (log (b / a) • L)) := by
   apply tendsto_integral_inv_smul_of_tendsto_uniform hf ha hb self_mem_nhdsWithin
   intro δ hδ
@@ -405,7 +414,7 @@ lemma tendsto_integral_inv_smul_nhdsWithin (hf : ContinuousOn f (Ioi 0)) (ha : 0
   have hx_pos : 0 < x := lt_of_lt_of_le (lt_min haε hbε) (uIoc_subset_uIcc hx).1
   have hx_lt_η : dist x 0 < η := by
     rw [Real.dist_eq, sub_zero, abs_of_pos hx_pos]
-    calc
+    calc x
       _ ≤ max (a * t) (b * t) := (uIoc_subset_uIcc hx).2
       _ = M * t := by rw [hM_def, max_mul_of_nonneg _ _ ht_pos.le]
       _ < M * (η / M) := mul_lt_mul_of_pos_left ht_bound hM
@@ -414,9 +423,9 @@ lemma tendsto_integral_inv_smul_nhdsWithin (hf : ContinuousOn f (Ioi 0)) (ha : 0
   rw [mem_setOf_eq, dist_eq_norm] at this
   exact le_of_lt this
 
-/-- If `f → R` as `x → +∞` and `f` is continuous on `(0, ∞)`, then the weighted integral
+/-- If `f → R` as `x → +∞` and `f` is locally integrable on `(0, ∞)`, then the weighted integral
 `∫ x in a*r..b*r, x⁻¹ • f x` converges to `log(b/a) • R` as `r → +∞`. -/
-lemma tendsto_integral_inv_smul_atTop (hf : ContinuousOn f (Ioi 0)) (ha : 0 < a) (hb : 0 < b)
+lemma tendsto_integral_inv_smul_atTop (hf : LocallyIntegrableOn f (Ioi 0)) (ha : 0 < a) (hb : 0 < b)
     (hR : Tendsto f atTop (𝓝 R)) :
     Tendsto (fun r ↦ ∫ x in (a * r)..(b * r), x⁻¹ • f x) atTop (𝓝 (log (b / a) • R)) := by
   apply tendsto_integral_inv_smul_of_tendsto_uniform hf ha hb
@@ -433,7 +442,7 @@ lemma tendsto_integral_inv_smul_atTop (hf : ContinuousOn f (Ioi 0)) (ha : 0 < a)
   have haε : 0 < a * t := mul_pos ha ht_pos
   have hbε : 0 < b * t := mul_pos hb ht_pos
   have hNx : N ≤ x :=
-    calc
+    calc N
       _ = min a b * (N / min a b) := by field_simp
       _ ≤ min a b * t :=
         mul_le_mul_of_nonneg_left ((le_max_right _ _).trans ht) hm.le
@@ -444,10 +453,10 @@ lemma tendsto_integral_inv_smul_atTop (hf : ContinuousOn f (Ioi 0)) (ha : 0 < a)
   exact le_of_lt hdist
 
 /-- **Frullani's integral**, limit form, for functions valued in a complete normed space.
-If `f` is continuous on `(0, ∞)` with `f x → L` as `x → 0⁺` and `f x → R` as `x → +∞`,
+If `f` is locally integrable on `(0, ∞)` with `f x → L` as `x → 0⁺` and `f x → R` as `x → +∞`,
 and `0 < a` and `0 < b`, then `∫ x in ε..r, x⁻¹ • (f (a * x) - f (b * x)) → log (b / a) • (L - R)`
 as `ε → 0⁺` and `r → +∞`. -/
-theorem tendsto_intervalIntegral (hf : ContinuousOn f (Ioi 0)) (ha : 0 < a) (hb : 0 < b)
+theorem tendsto_intervalIntegral (hf : LocallyIntegrableOn f (Ioi 0)) (ha : 0 < a) (hb : 0 < b)
     (hL : Tendsto f (𝓝[>] 0) (𝓝 L)) (hR : Tendsto f atTop (𝓝 R)) :
     Tendsto (fun p : ℝ × ℝ ↦ ∫ x in p.1..p.2, x⁻¹ • (f (a * x) - f (b * x)))
       ((𝓝[>] 0) ×ˢ atTop) (𝓝 (log (b / a) • (L - R))) := by
@@ -457,13 +466,13 @@ theorem tendsto_intervalIntegral (hf : ContinuousOn f (Ioi 0)) (ha : 0 < a) (hb
   have hsplit {ε r : ℝ} (hε : 0 < ε) (hr : 0 < r) :
       ∫ x in ε..r, x⁻¹ • (f (a * x) - f (b * x)) =
       (∫ x in (a * ε)..(b * ε), u x) - ∫ x in (a * r)..(b * r), u x := by
-    calc
+    calc ∫ x in ε..r, x⁻¹ • (f (a * x) - f (b * x))
       _ = (∫ x in ε..r, x⁻¹ • f (a * x)) - ∫ x in ε..r, x⁻¹ • f (b * x) := by
         simp_rw [smul_sub]
         exact integral_sub (intervalIntegrable_inv_smul_comp_mul hf hε hr ha)
           (intervalIntegrable_inv_smul_comp_mul hf hε hr hb)
       _ = (∫ y in a * ε..a * r, u y) - ∫ y in b * ε..b * r, u y := by
-        rw [integral_comp_mul_inv_smul ha, integral_comp_mul_inv_smul hb]
+        rw [integral_comp_mul_inv_smul ha.ne', integral_comp_mul_inv_smul hb.ne']
       _ = _ := integral_interval_sub_interval_comm
                  (hint (mul_pos ha hε) (mul_pos ha hr))
                  (hint (mul_pos hb hε) (mul_pos hb hr))
@@ -479,10 +488,10 @@ theorem tendsto_intervalIntegral (hf : ContinuousOn f (Ioi 0)) (ha : 0 < a) (hb
     ((tendsto_integral_inv_smul_atTop hf ha hb hR).comp tendsto_snd)
 
 /-- **Frullani's integral** for functions valued in a complete normed space.
-If `f` is continuous on `(0, ∞)` with `f x → L` as `x → 0⁺` and `f x → R` as `x → +∞`,
+If `f` is locally integrable on `(0, ∞)` with `f x → L` as `x → 0⁺` and `f x → R` as `x → +∞`,
 `0 < a` and `0 < b`, and `x ↦ x⁻¹ • (f (a * x) - f (b * x))` is integrable on `(0, ∞)`, then
 `∫ x in Ioi 0, x⁻¹ • (f (a * x) - f (b * x)) = log (b / a) • (L - R)`. -/
-theorem integral_Ioi_eq (hf : ContinuousOn f (Ioi 0)) (ha : 0 < a) (hb : 0 < b)
+theorem integral_Ioi_eq (hf : LocallyIntegrableOn f (Ioi 0)) (ha : 0 < a) (hb : 0 < b)
     (hL : Tendsto f (𝓝[>] 0) (𝓝 L)) (hR : Tendsto f atTop (𝓝 R))
     (hint : IntegrableOn (fun x ↦ x⁻¹ • (f (a * x) - f (b * x))) (Ioi 0)) :
     ∫ x in Ioi 0, x⁻¹ • (f (a * x) - f (b * x)) = log (b / a) • (L - R) := by

Mathlib/MeasureTheory/Integral/IntervalIntegral/MeanValue.lean

@@ -7,7 +7,6 @@ module
 
 public import Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
 public import Mathlib.MeasureTheory.Integral.MeanValue
-public import Mathlib.Analysis.SpecialFunctions.Integrals.Basic
 
 /-!
 # First mean value theorem for interval integrals
@@ -34,7 +33,7 @@ mean value theorem, interval integral
 
 public section
 
-open MeasureTheory Set intervalIntegral Real
+open MeasureTheory Set intervalIntegral
 
 open scoped Interval
 
@@ -82,24 +81,3 @@ theorem exists_eq_const_mul_intervalIntegral_of_nonneg
     rw [ae_restrict_iff' measurableSet_uIoc]
     exact ae_of_all μ hg0
   exact exists_eq_const_mul_intervalIntegral_of_ae_nonneg hf hg hg0_ae
-
-theorem exists_integral_div_eq_mul_log {p q : ℝ} {f : ℝ → ℝ} (hp : 0 < p) (hq : 0 < q)
-    (hf : ContinuousOn f (uIcc p q)) :
-    ∃ c ∈ uIcc p q, ∫ x in p..q, f x / x = f c * log (q / p) := by
-  let g : ℝ → ℝ := fun x ↦ 1 / x
-  have hfg (x : ℝ) : f x / x = f x * g x := by unfold g; field_simp
-  have h_integrand_eq : (∫ x in p..q, f x * g x) = (∫ x in p..q, f x / x) := by simp [hfg]
-  rw [← h_integrand_eq]
-  have hg' : IntervalIntegrable g volume p q := by
-    unfold g
-    simp only [one_div, intervalIntegrable_inv_iff]
-    right
-    exact notMem_uIcc_of_lt (by linarith) (by linarith)
-  have hg_nonneg : ∀ x ∈ uIoc p q, 0 ≤ g x := by
-    intro x hx
-    rw [one_div_nonneg]
-    rw [mem_uIoc] at hx
-    rcases hx with h | h
-    all_goals linarith
-  rw [← integral_one_div_of_pos hp hq]
-  exact exists_eq_const_mul_intervalIntegral_of_nonneg hf hg' hg_nonneg

Mathlib/Topology/Algebra/GroupWithZero.lean

@@ -209,16 +209,6 @@ nonrec theorem ContinuousWithinAt.div (hf : ContinuousWithinAt f s a)
 theorem ContinuousOn.div (hf : ContinuousOn f s) (hg : ContinuousOn g s) (h₀ : ∀ x ∈ s, g x ≠ 0) :
     ContinuousOn (f / g) s := fun x hx => (hf x hx).div (hg x hx) (h₀ x hx)
 
-theorem ContinuousOn.comp_mul_left_div {f g : G₀ → G₀} {s t : Set G₀} {c : G₀}
-    (hf : ContinuousOn f t) (hg : ContinuousOn g s) (hct : Set.MapsTo (fun x ↦ c * x) s t)
-    (hne : ∀ x ∈ s, g x ≠ 0) : ContinuousOn (fun x ↦ f (c * x) / g x) s :=
-  (hf.comp_mul_left hct).div hg hne
-
-theorem ContinuousOn.comp_mul_right_div {f g : G₀ → G₀} {s t : Set G₀} {c : G₀}
-    (hf : ContinuousOn f t) (hg : ContinuousOn g s) (hct : Set.MapsTo (fun x ↦ x * c) s t)
-    (hne : ∀ x ∈ s, g x ≠ 0) : ContinuousOn (fun x ↦ f (x * c) / g x) s :=
-  (hf.comp_mul_right hct).div hg hne
-
 /-- Continuity at a point of the result of dividing two functions continuous at that point, where
 the denominator is nonzero. -/
 nonrec theorem ContinuousAt.div (hf : ContinuousAt f a) (hg : ContinuousAt g a) (h₀ : g a ≠ 0) :

Mathlib/Topology/Algebra/Monoid.lean

@@ -109,16 +109,6 @@ alias continuous_mul_left := continuous_const_mul
 @[to_additive existing, deprecated (since := "2026-02-20")]
 alias continuous_mul_right := continuous_mul_const
 
-@[to_additive]
-theorem ContinuousOn.comp_mul_left {f : M → X} {s t : Set M} {c : M} (hf : ContinuousOn f t)
-    (hct : Set.MapsTo (fun x : M => c * x) s t) : ContinuousOn (fun x => f (c * x)) s :=
-  hf.comp (continuous_const_mul c).continuousOn hct
-
-@[to_additive]
-theorem ContinuousOn.comp_mul_right {f : M → X} {s t : Set M} {c : M} (hf : ContinuousOn f t)
-    (hct : Set.MapsTo (fun x : M => x * c) s t) : ContinuousOn (fun x => f (x * c)) s :=
-  hf.comp (continuous_mul_const c).continuousOn hct
-
 @[to_additive]
 theorem tendsto_mul {a b : M} : Tendsto (fun p : M × M => p.fst * p.snd) (𝓝 (a, b)) (𝓝 (a * b)) :=
   continuous_iff_continuousAt.mp ContinuousMul.continuous_mul (a, b)