Theorems · Theorem · real analysis

ContDiffPointwiseHolderAt.zero_order_iff

∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] {α : ↑unitInterval} {f : E → F} {a : E},
  ContDiffPointwiseHolderAt 0 α f a ↔ ContDiffAt ℝ 0 f a ∧ (fun x => f x - f a) =O[nhds a] fun x => ‖x - a‖ ^ ↑α

A function is $C^{0+(α)}$ at a point if and only if it is $C^0$ at the point (i.e., it is continuous on a neighborhood of the point) and $f(x) - f(a) = O(‖x - a‖ ^ α)$.

Defined in

Mathlib.Analysis.Calculus.ContDiffHolder.Pointwise

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpace