# 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 `ℂ`).

source
theorem HasFTaylorSeriesUpToOn.hasStrictFDerivAt {𝕂 : Type u_1} [RCLike 𝕂] {E' : Type u_2} [NormedAddCommGroup E'] [NormedSpace 𝕂 E'] {F' : Type u_3} [NormedAddCommGroup F'] [NormedSpace 𝕂 F'] {n : WithTop ℕ∞} {s : Set E'} {f : E' → F'} {x : E'} {p : E' → FormalMultilinearSeries 𝕂 E' F'} (hf : HasFTaylorSeriesUpToOn n f p s) (hn : 1 ≤ n) (hs : s ∈ nhds x) :
HasStrictFDerivAt f ((continuousMultilinearCurryFin1 𝕂 E' 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`.

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

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.

source
theorem ContDiffAt.hasStrictDerivAt' {n : WithTop ℕ∞} {𝕂 : Type u_1} [RCLike 𝕂] {F' : Type u_3} [NormedAddCommGroup F'] [NormedSpace 𝕂 F'] {f : 𝕂 → F'} {f' : F'} {x : 𝕂} (hf : ContDiffAt 𝕂 n f x) (hf' : HasDerivAt f f' x) (hn : 1 ≤ n) :
HasStrictDerivAt f f' x

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.

source
theorem ContDiffAt.hasStrictFDerivAt {n : WithTop ℕ∞} {𝕂 : Type u_1} [RCLike 𝕂] {E' : Type u_2} [NormedAddCommGroup E'] [NormedSpace 𝕂 E'] {F' : Type u_3} [NormedAddCommGroup F'] [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.

source
theorem ContDiffAt.hasStrictDerivAt {n : WithTop ℕ∞} {𝕂 : Type u_1} [RCLike 𝕂] {F' : Type u_3} [NormedAddCommGroup F'] [NormedSpace 𝕂 F'] {f : 𝕂 → F'} {x : 𝕂} (hf : ContDiffAt 𝕂 n f x) (hn : 1 ≤ n) :
HasStrictDerivAt f (deriv 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.

source
theorem ContDiff.hasStrictFDerivAt {n : WithTop ℕ∞} {𝕂 : Type u_1} [RCLike 𝕂] {E' : Type u_2} [NormedAddCommGroup E'] [NormedSpace 𝕂 E'] {F' : Type u_3} [NormedAddCommGroup F'] [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.

source
theorem ContDiff.hasStrictDerivAt {n : WithTop ℕ∞} {𝕂 : Type u_1} [RCLike 𝕂] {F' : Type u_3} [NormedAddCommGroup F'] [NormedSpace 𝕂 F'] {f : 𝕂 → F'} {x : 𝕂} (hf : ContDiff 𝕂 n f) (hn : 1 ≤ n) :
HasStrictDerivAt f (deriv f x) x

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

source
theorem HasFTaylorSeriesUpToOn.exists_lipschitzOnWith_of_nnnorm_lt {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {f : E → F} {p : E → FormalMultilinearSeries ℝ E F} {s : Set E} {x : E} (hf : HasFTaylorSeriesUpToOn 1 f p (insert x s)) (hs : Convex ℝ s) (K : NNReal) (hK : ‖p x 1‖₊ < K) :
∃ t ∈ nhdsWithin x s, LipschitzOnWith K f 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`.

source
theorem HasFTaylorSeriesUpToOn.exists_lipschitzOnWith {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {f : E → F} {p : E → FormalMultilinearSeries ℝ E F} {s : Set E} {x : E} (hf : HasFTaylorSeriesUpToOn 1 f p (insert x s)) (hs : Convex ℝ s) :
∃ (K : NNReal), ∃ t ∈ nhdsWithin x s, LipschitzOnWith K f 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`.

source
theorem ContDiffWithinAt.exists_lipschitzOnWith {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {f : E → F} {s : Set E} {x : E} (hf : ContDiffWithinAt ℝ 1 f s x) (hs : Convex ℝ s) :
∃ (K : NNReal), ∃ t ∈ nhdsWithin x s, LipschitzOnWith K f t

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

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

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

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

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

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

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

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

A `C^1` function with compact support is Lipschitz.