Theorems · Theorem · real analysis

ContDiffPointwiseHolderAt.of_contDiffOn_holderOnWith

∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] {k : ℕ} {α : ↑unitInterval} {f : E → F} {a : E} {s : Set E} {C : NNReal},
  ContDiffOn ℝ (↑k) f s →
    s ∈ nhds a → HolderOnWith C ⟨↑α, ⋯⟩ (iteratedFDeriv ℝ k f) s → ContDiffPointwiseHolderAt k α f a

If a function is $C^{k+α}$ on a neighborhood of a point a, i.e., it is $C^k$ on this neighborhood and $D^k f$ is Hölder continuous on it, then the function is $C^{k+(α)}$ at a.

Defined in

Mathlib.Analysis.Calculus.ContDiffHolder.Pointwise

Cited by

0 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpace