# Documentation

Mathlib.Analysis.Calculus.ContDiff.IsROrC

# Higher differentiability over ℝ or ℂ#

### Results over ℝ or ℂ#

The results in this section rely on the Mean Value Theorem, and therefore hold only over ℝ (and its extension fields such as ℂ).

theorem HasFTaylorSeriesUpToOn.hasStrictFDerivAt {n : ℕ∞} {𝕂 : Type u_1} [] {E' : Type u_2} [] [NormedSpace 𝕂 E'] {F' : Type u_3} [] [NormedSpace 𝕂 F'] {s : Set E'} {f : E'F'} {x : E'} {p : E'} (hf : ) (hn : 1 n) (hs : s nhds x) :
HasStrictFDerivAt f (() (p x 1)) x

If a function has a Taylor series at order at least 1, then at points in the interior of the domain of definition, the term of order 1 of this series is a strict derivative of f.

theorem ContDiffAt.hasStrictFDerivAt' {n : ℕ∞} {𝕂 : Type u_1} [] {E' : Type u_2} [] [NormedSpace 𝕂 E'] {F' : Type u_3} [] [NormedSpace 𝕂 F'] {f : E'F'} {f' : E' →L[𝕂] F'} {x : E'} (hf : ContDiffAt 𝕂 n f x) (hf' : HasFDerivAt f f' x) (hn : 1 n) :

If a function is C^n with 1 ≤ n around a point, and its derivative at that point is given to us as f', then f' is also a strict derivative.

theorem ContDiffAt.hasStrictDerivAt' {n : ℕ∞} {𝕂 : Type u_1} [] {F' : Type u_3} [] [NormedSpace 𝕂 F'] {f : 𝕂F'} {f' : F'} {x : 𝕂} (hf : ContDiffAt 𝕂 n f x) (hf' : HasDerivAt f f' x) (hn : 1 n) :

If a function is C^n with 1 ≤ n around a point, and its derivative at that point is given to us as f', then f' is also a strict derivative.

theorem ContDiffAt.hasStrictFDerivAt {n : ℕ∞} {𝕂 : Type u_1} [] {E' : Type u_2} [] [NormedSpace 𝕂 E'] {F' : Type u_3} [] [NormedSpace 𝕂 F'] {f : E'F'} {x : E'} (hf : ContDiffAt 𝕂 n f x) (hn : 1 n) :
HasStrictFDerivAt f (fderiv 𝕂 f x) x

If a function is C^n with 1 ≤ n around a point, then the derivative of f at this point is also a strict derivative.

theorem ContDiffAt.hasStrictDerivAt {n : ℕ∞} {𝕂 : Type u_1} [] {F' : Type u_3} [] [NormedSpace 𝕂 F'] {f : 𝕂F'} {x : 𝕂} (hf : ContDiffAt 𝕂 n f x) (hn : 1 n) :

If a function is C^n with 1 ≤ n around a point, then the derivative of f at this point is also a strict derivative.

theorem ContDiff.hasStrictFDerivAt {n : ℕ∞} {𝕂 : Type u_1} [] {E' : Type u_2} [] [NormedSpace 𝕂 E'] {F' : Type u_3} [] [NormedSpace 𝕂 F'] {f : E'F'} {x : E'} (hf : ContDiff 𝕂 n f) (hn : 1 n) :
HasStrictFDerivAt f (fderiv 𝕂 f x) x

If a function is C^n with 1 ≤ n, then the derivative of f is also a strict derivative.

theorem ContDiff.hasStrictDerivAt {n : ℕ∞} {𝕂 : Type u_1} [] {F' : Type u_3} [] [NormedSpace 𝕂 F'] {f : 𝕂F'} {x : 𝕂} (hf : ContDiff 𝕂 n f) (hn : 1 n) :

If a function is C^n with 1 ≤ n, then the derivative of f is also a strict derivative.

theorem HasFTaylorSeriesUpToOn.exists_lipschitzOnWith_of_nnnorm_lt {E : Type u_4} {F : Type u_5} [] [] {f : EF} {p : E} {s : Set E} {x : E} (hf : HasFTaylorSeriesUpToOn 1 f p (insert x s)) (hs : ) (K : NNReal) (hK : p x 1‖₊ < K) :
∃ t ∈ ,

If f has a formal Taylor series p up to order 1 on {x} ∪ s, where s is a convex set, and ‖p x 1‖₊ < K, then f is K-Lipschitz in a neighborhood of x within s.

theorem HasFTaylorSeriesUpToOn.exists_lipschitzOnWith {E : Type u_4} {F : Type u_5} [] [] {f : EF} {p : E} {s : Set E} {x : E} (hf : HasFTaylorSeriesUpToOn 1 f p (insert x s)) (hs : ) :
∃ (K : NNReal), ∃ t ∈ ,

If f has a formal Taylor series p up to order 1 on {x} ∪ s, where s is a convex set, then f is Lipschitz in a neighborhood of x within s.

theorem ContDiffWithinAt.exists_lipschitzOnWith {E : Type u_4} {F : Type u_5} [] [] {f : EF} {s : Set E} {x : E} (hf : ) (hs : ) :
∃ (K : NNReal), ∃ t ∈ ,

If f is C^1 within a convex set s at x, then it is Lipschitz on a neighborhood of x within s.

theorem ContDiffAt.exists_lipschitzOnWith_of_nnnorm_lt {𝕂 : Type u_1} [] {E' : Type u_2} [] [NormedSpace 𝕂 E'] {F' : Type u_3} [] [NormedSpace 𝕂 F'] {f : E'F'} {x : E'} (hf : ContDiffAt 𝕂 1 f x) (K : NNReal) (hK : fderiv 𝕂 f x‖₊ < K) :
∃ t ∈ nhds x,

If f is C^1 at x and K > ‖fderiv 𝕂 f x‖, then f is K-Lipschitz in a neighborhood of x.

theorem ContDiffAt.exists_lipschitzOnWith {𝕂 : Type u_1} [] {E' : Type u_2} [] [NormedSpace 𝕂 E'] {F' : Type u_3} [] [NormedSpace 𝕂 F'] {f : E'F'} {x : E'} (hf : ContDiffAt 𝕂 1 f x) :
∃ (K : NNReal), ∃ t ∈ nhds x,

If f is C^1 at x, then f is Lipschitz in a neighborhood of x.

theorem ContDiff.locallyLipschitz {𝕂 : Type u_1} [] {E' : Type u_2} [] [NormedSpace 𝕂 E'] {F' : Type u_3} [] [NormedSpace 𝕂 F'] {f : E'F'} (hf : ContDiff 𝕂 1 f) :

If f is C^1, it is locally Lipschitz.

theorem ContDiff.lipschitzWith_of_hasCompactSupport {𝕂 : Type u_1} [] {E' : Type u_2} [] [NormedSpace 𝕂 E'] {F' : Type u_3} [] [NormedSpace 𝕂 F'] {f : E'F'} {n : ℕ∞} (hf : ) (h'f : ContDiff 𝕂 n f) (hn : 1 n) :
∃ (C : NNReal),

A C^1 function with compact support is Lipschitz.