Theorems · Theorem · real analysis

Frullani.tendsto_integral_inv_smul_of_tendsto_uniform

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E} {a b : ℝ} [CompleteSpace E],
  MeasureTheory.LocallyIntegrableOn f (Set.Ioi 0) MeasureTheory.volume →
    0 < a →
      0 < b →
        ∀ {F : Filter ℝ},
          (∀ᶠ (t : ℝ) in F, 0 < t) →
            ∀ {V : E},
              (∀ δ > 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))

Defined in

Mathlib.Analysis.SpecialFunctions.FrullaniIntegral

Cited by

2 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceCompleteSpace