Theorems · Theorem · real analysis

not_intervalIntegrable_of_tendsto_norm_atTop_of_deriv_isBigO_within_sdiff_singleton

∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  {f : ℝ → E} {g : ℝ → F} {a b c : ℝ},
  a ≠ b →
    c ∈ Set.uIcc a b →
      (∀ᶠ (x : ℝ) in nhdsWithin c (Set.uIcc a b \ {c}), DifferentiableAt ℝ f x) →
        Filter.Tendsto (fun x => ‖f x‖) (nhdsWithin c (Set.uIcc a b \ {c})) Filter.atTop →
          deriv f =O[nhdsWithin c (Set.uIcc a b \ {c})] g → ¬IntervalIntegrable g MeasureTheory.volume a b

If a ≠ b, c ∈ [a, b], f is differentiable in the neighborhood of c within [a, b] \ {c}, ‖f x‖ → ∞ as x → c within [a, b] \ {c}, and f' = O(g) along 𝓝[[a, b] \ {c}] c, where f' is the derivative of f, then g is not interval integrable on a..b.

Defined in

Mathlib.Analysis.SpecialFunctions.NonIntegrable

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceNormedAddCommGroup