Theorems · Theorem · real analysis

sub_isBigO_norm_rpow_add_one_of_fderiv

∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] {f : E → F} {a : E} {r : ℝ},
  0 ≤ r →
    (∀ᶠ (x : E) in nhds a, DifferentiableAt ℝ f x) →
      (fderiv ℝ f =O[nhds a] fun x => ‖x - a‖ ^ r) → (fun x => f x - f a) =O[nhds a] fun x => ‖x - a‖ ^ (r + 1)

Let f : E → F be a function differentiable in a neighborhood of a. If $Df(x) = O(‖x - a‖ ^ r)$ as x → a, where r ≥ 0, then $f(x) - f(a) = O(‖x - a‖ ^ {r + 1})$ as x → a.

Defined in

Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpace