Theorems · Theorem · real analysis

Frullani.integral_Ioi_eq

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E} {a b : ℝ} {L R : E}
  [CompleteSpace E],
  MeasureTheory.LocallyIntegrableOn f (Set.Ioi 0) MeasureTheory.volume →
    0 < a →
      0 < b →
        Filter.Tendsto f (nhdsWithin 0 (Set.Ioi 0)) (nhds L) →
          Filter.Tendsto f Filter.atTop (nhds R) →
            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).

Defined in

Mathlib.Analysis.SpecialFunctions.FrullaniIntegral

Cited by

0 results in Mathlib

Foundations

Depth 276 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedSpaceCompleteSpace