Theorems · Theorem · real analysis

not_intervalIntegrable_of_tendsto_norm_atTop_of_deriv_isBigO_punctured

∀ {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 : ℝ},
  (∀ᶠ (x : ℝ) in nhdsWithin c {c}ᶜ, DifferentiableAt ℝ f x) →
    Filter.Tendsto (fun x => ‖f x‖) (nhdsWithin c {c}ᶜ) Filter.atTop →
      deriv f =O[nhdsWithin c {c}ᶜ] g → a ≠ b → c ∈ Set.uIcc a b → ¬IntervalIntegrable g MeasureTheory.volume a b

If f is differentiable in a punctured neighborhood of c, ‖f x‖ → ∞ as x → c (more formally, along the filter 𝓝[≠] c), and f' = O(g) along 𝓝[≠] c, where f' is the derivative of f, then g is not interval integrable on any nontrivial interval a..b such that c ∈ [a, b].

Defined in

Mathlib.Analysis.SpecialFunctions.NonIntegrable

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceNormedAddCommGroup