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 {𝕂 : 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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.