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} [IsROrC 𝕂] {E' : Type u_2} [NormedAddCommGroup E'] [NormedSpace 𝕂 E'] {F' : Type u_3} [NormedAddCommGroup F'] [NormedSpace 𝕂 F'] {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) :

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} [IsROrC 𝕂] {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) :

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} [IsROrC 𝕂] {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) :

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} [IsROrC 𝕂] {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 : ℕ∞} {𝕂 : Type u_1} [IsROrC 𝕂] {F' : Type u_3} [NormedAddCommGroup F'] [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} [IsROrC 𝕂] {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 : ℕ∞} {𝕂 : Type u_1} [IsROrC 𝕂] {F' : Type u_3} [NormedAddCommGroup F'] [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} [NormedAddCommGroup E] [NormedSpace E] [NormedAddCommGroup F] [NormedSpace F] {f : EF} {p : EFormalMultilinearSeries 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 : EF} {p : EFormalMultilinearSeries 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 : EF} {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} [IsROrC 𝕂] {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} [IsROrC 𝕂] {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} [IsROrC 𝕂] {E' : Type u_2} [NormedAddCommGroup E'] [NormedSpace 𝕂 E'] {F' : Type u_3} [NormedAddCommGroup F'] [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} [IsROrC 𝕂] {E' : Type u_2} [NormedAddCommGroup E'] [NormedSpace 𝕂 E'] {F' : Type u_3} [NormedAddCommGroup F'] [NormedSpace 𝕂 F'] {f : E'F'} {n : ℕ∞} (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.