Theorems · Theorem · real analysis

Frullani.norm_integral_inv_smul_sub_le

∀ {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 →
        ∀ {V : E} {δ : ℝ},
          0 ≤ δ →
            (∀ x ∈ Set.uIoc a b, ‖f x - V‖ ≤ δ) →
              ‖(∫ (x : ℝ) in a..b, x⁻¹ • f x) - Real.log (b / a) • V‖ ≤ δ * |Real.log (b / a)|

Defined in

Mathlib.Analysis.SpecialFunctions.FrullaniIntegral

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceCompleteSpace