Frullani's integral

This file proves Frullani's integral: if f : ℝ → E 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 Ioi 0, x⁻¹ • (f (a * x) - f (b * x)) = log (b / a) • (L - R) (Frullani.integral_Ioi_eq), provided the integrand is integrable on (0, ∞).

We also prove a limit form Frullani.tendsto_intervalIntegral, which does not require global integrability of the integrand.

theorem Frullani.intervalIntegrable_inv_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} {a b : ℝ} (hf : MeasureTheory.LocallyIntegrableOn f (Set.Ioi 0) MeasureTheory.volume) (ha : 0 < a) (hb : 0 < b) : IntervalIntegrable (fun (x : ℝ) => x⁻¹ • f x) MeasureTheory.volume a b

theorem Frullani.intervalIntegrable_inv_smul_comp_mul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} {a b c : ℝ} (hf : MeasureTheory.LocallyIntegrableOn f (Set.Ioi 0) MeasureTheory.volume) (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) : IntervalIntegrable (fun (x : ℝ) => x⁻¹ • f (c * x)) MeasureTheory.volume a b

theorem Frullani.integral_comp_mul_inv_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} {c ε r : ℝ} (hc : c ≠ 0) : ∫ (x : ℝ) in ε..r, x⁻¹ • f (c * x) = ∫ (x : ℝ) in c * ε..c * r, x⁻¹ • f x

theorem Frullani.norm_integral_inv_smul_sub_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} {a b : ℝ} [CompleteSpace E] (hf : MeasureTheory.LocallyIntegrableOn f (Set.Ioi 0) MeasureTheory.volume) (ha : 0 < a) (hb : 0 < b) {V : E} {δ : ℝ} (hδ : 0 ≤ δ) (h : ∀ x ∈ Set.uIoc a b, ‖f x - V‖ ≤ δ) : ‖(∫ (x : ℝ) in a..b, x⁻¹ • f x) - Real.log (b / a) • V‖ ≤ δ * |Real.log (b / a)|

theorem Frullani.tendsto_integral_inv_smul_of_tendsto_uniform {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} {a b : ℝ} [CompleteSpace E] (hf : MeasureTheory.LocallyIntegrableOn f (Set.Ioi 0) MeasureTheory.volume) (ha : 0 < a) (hb : 0 < b) {F : Filter ℝ} (hpos : ∀ᶠ (t : ℝ) in F, 0 < t) {V : E} (huni : ∀ δ > 0, ∀ᶠ (t : ℝ) in F, ∀ x ∈ Set.uIoc (a * t) (b * t), ‖f x - V‖ ≤ δ) : Filter.Tendsto (fun (t : ℝ) => ∫ (x : ℝ) in a * t..b * t, x⁻¹ • f x) F (nhds (Real.log (b / a) • V))

theorem Frullani.tendsto_integral_inv_smul_nhdsWithin {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} {a b : ℝ} {L : E} [CompleteSpace E] (hf : MeasureTheory.LocallyIntegrableOn f (Set.Ioi 0) MeasureTheory.volume) (ha : 0 < a) (hb : 0 < b) (hL : Filter.Tendsto f (nhdsWithin 0 (Set.Ioi 0)) (nhds L)) : Filter.Tendsto (fun (ε : ℝ) => ∫ (x : ℝ) in a * ε..b * ε, x⁻¹ • f x) (nhdsWithin 0 (Set.Ioi 0)) (nhds (Real.log (b / a) • L))

theorem Frullani.tendsto_integral_inv_smul_atTop {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} {a b : ℝ} {R : E} [CompleteSpace E] (hf : MeasureTheory.LocallyIntegrableOn f (Set.Ioi 0) MeasureTheory.volume) (ha : 0 < a) (hb : 0 < b) (hR : Filter.Tendsto f Filter.atTop (nhds R)) : Filter.Tendsto (fun (r : ℝ) => ∫ (x : ℝ) in a * r..b * r, x⁻¹ • f x) Filter.atTop (nhds (Real.log (b / a) • R))

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 → +∞.

theorem Frullani.tendsto_intervalIntegral {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} {a b : ℝ} {L R : E} [CompleteSpace E] (hf : MeasureTheory.LocallyIntegrableOn f (Set.Ioi 0) MeasureTheory.volume) (ha : 0 < a) (hb : 0 < b) (hL : Filter.Tendsto f (nhdsWithin 0 (Set.Ioi 0)) (nhds L)) (hR : Filter.Tendsto f Filter.atTop (nhds R)) : Filter.Tendsto (fun (p : ℝ × ℝ) => ∫ (x : ℝ) in p.1..p.2, x⁻¹ • (f (a * x) - f (b * x))) (nhdsWithin 0 (Set.Ioi 0) ×ˢ Filter.atTop) (nhds (Real.log (b / a) • (L - R)))

Frullani's integral, limit form, for functions valued in a complete normed space. 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 Frullani.integral_Ioi_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} {a b : ℝ} {L R : E} [CompleteSpace E] (hf : MeasureTheory.LocallyIntegrableOn f (Set.Ioi 0) MeasureTheory.volume) (ha : 0 < a) (hb : 0 < b) (hL : Filter.Tendsto f (nhdsWithin 0 (Set.Ioi 0)) (nhds L)) (hR : Filter.Tendsto f Filter.atTop (nhds R)) (hint : MeasureTheory.IntegrableOn (fun (x : ℝ) => x⁻¹ • (f (a * x) - f (b * x))) (Set.Ioi 0) MeasureTheory.volume) : ∫ (x : ℝ) in Set.Ioi 0, x⁻¹ • (f (a * x) - f (b * x)) = Real.log (b / a) • (L - R)

Frullani's integral for functions valued in a complete normed space. 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).