Theorems · Inductive type · real analysis

ContDiffPointwiseHolderAt

{E : Type u_1} →
  {F : Type u_2} →
    [inst : NormedAddCommGroup E] →
      [NormedSpace ℝ E] → [inst : NormedAddCommGroup F] → [NormedSpace ℝ F] → ℕ → ↑unitInterval → (E → F) → E → Prop

A map f is said to be $C^{k+(α)}$ at a, where k is a natural number and 0 ≤ α ≤ 1, if it is $C^k$ at this point and $D^kf(x)-D^kf(a) = O(‖x - a‖ ^ α)$ as x → a. When naming lemmas about this predicate, k is called "order", and α is called "exponent".

Defined in

Mathlib.Analysis.Calculus.ContDiffHolder.Pointwise

Cited by

30 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpace