ContDiff.locallyLipschitz
theorem ContDiff.locallyLipschitz :
∀ {𝕂 : Type u_1} [inst : RCLike 𝕂] {E' : Type u_2} [inst_1 : NormedAddCommGroup E'] [inst_2 : NormedSpace 𝕂 E']
{F' : Type u_3} [inst_3 : NormedAddCommGroup F'] [inst_4 : NormedSpace 𝕂 F'] {f : E' → F'},
ContDiff 𝕂 1 f → LocallyLipschitz f
The theorem `ContDiff.locallyLipschitz` states that if a function `f` (from a normed additive commutative group `E'` to another normed additive commutative group `F'`, both over a scalar field `𝕂`), is continuously differentiable (`C^1`), then it is locally Lipschitz continuous. In other words, for every point in the domain of the function, there exists a neighborhood around that point on which the function satisfies the Lipschitz condition (there is a constant `K` such that the distance between the function values at any two points in the neighborhood does not exceed `K` times the distance between the points themselves).
More concisely: If a continuously differentiable function between two normed additive commutative groups over a scalar field satisfies the Lipschitz condition on every point in its domain, then it is locally Lipschitz continuous.
|
ContDiff.hasStrictDerivAt
theorem ContDiff.hasStrictDerivAt :
∀ {n : ℕ∞} {𝕂 : Type u_1} [inst : RCLike 𝕂] {F' : Type u_3} [inst_1 : NormedAddCommGroup F']
[inst_2 : NormedSpace 𝕂 F'] {f : 𝕂 → F'} {x : 𝕂}, ContDiff 𝕂 n f → 1 ≤ n → HasStrictDerivAt f (deriv f x) x
The theorem `ContDiff.hasStrictDerivAt` states that if a function `f` is continuously differentiable of order `n` where `1 ≤ n`, then the derivative of `f` is also a strict derivative. In other words, for a function `f` from a type `𝕂` to a type `F'` that is `C^n` smooth at a point `x`, and for `n` at least 1, the derivative of `f` at the point `x` satisfies the condition of strict differentiability.
More concisely: If `f` is continuously differentiable of order `n` (`1 ≤ n`) at a point `x`, then the derivative `f'` of `f` at `x` is a strict derivative.
|
ContDiffAt.hasStrictFDerivAt'
theorem ContDiffAt.hasStrictFDerivAt' :
∀ {n : ℕ∞} {𝕂 : Type u_1} [inst : RCLike 𝕂] {E' : Type u_2} [inst_1 : NormedAddCommGroup E']
[inst_2 : NormedSpace 𝕂 E'] {F' : Type u_3} [inst_3 : NormedAddCommGroup F'] [inst_4 : NormedSpace 𝕂 F']
{f : E' → F'} {f' : E' →L[𝕂] F'} {x : E'},
ContDiffAt 𝕂 n f x → HasFDerivAt f f' x → 1 ≤ n → HasStrictFDerivAt f f' x
This theorem states that if a function `f` is continuously differentiable `n` times (with `n` being 1 or more) around a point `x`, and its derivative at that point is given as `f'`, then `f'` is also a strict derivative of `f` at `x`. In other words, if the function `f` is smooth enough (i.e., it has at least one continuous derivative) at a point, and we know its derivative at that point, then that derivative is indeed the "strict" derivative, meaning it not only approximates the change in `f` around `x` but also satisfies a stronger condition related to the rate of change.
More concisely: If a function `f` is continuously differentiable of order `n` at a point `x`, then the `n`th derivative `f^{(n)}` of `f` at `x` is the strict derivative of `f` at `x`.
|
ContDiff.hasStrictFDerivAt
theorem ContDiff.hasStrictFDerivAt :
∀ {n : ℕ∞} {𝕂 : Type u_1} [inst : RCLike 𝕂] {E' : Type u_2} [inst_1 : NormedAddCommGroup E']
[inst_2 : NormedSpace 𝕂 E'] {F' : Type u_3} [inst_3 : NormedAddCommGroup F'] [inst_4 : NormedSpace 𝕂 F']
{f : E' → F'} {x : E'}, ContDiff 𝕂 n f → 1 ≤ n → HasStrictFDerivAt f (fderiv 𝕂 f x) x
The theorem `ContDiff.hasStrictFDerivAt` states that if a function `f` is `C^n` - that is, the function is continuously differentiable up to the `n`th derivative - with `n` being 1 or more, then the function `f` has a strict Frechet derivative at any point `x` in its domain, and this strict derivative is exactly the Frechet derivative given by the function `fderiv 𝕂 f x`. Here, `𝕂` is a field that has structure similar to real or complex numbers (it's a topological field that has a norm inducing the topology), `E'` and `F'` are normed vector spaces over `𝕂`, and `f` is a function from `E'` to `F'`.
More concisely: If a continuously differentiable function `f : E' → F'` of class `C^n` has `n ≥ 1`, then it possesses a strict Frechet derivative at every point `x ∈ E'`, which coincides with the Frechet derivative `fderiv 𝕂 f x`.
|
ContDiffWithinAt.exists_lipschitzOnWith
theorem ContDiffWithinAt.exists_lipschitzOnWith :
∀ {E : Type u_4} {F : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
[inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {f : E → F} {s : Set E} {x : E},
ContDiffWithinAt ℝ 1 f s x → Convex ℝ s → ∃ K, ∃ t ∈ nhdsWithin x s, LipschitzOnWith K f t
This theorem states that if a function `f` is once continuously differentiable (`C^1`) within a convex set `s` at a point `x`, then `f` is Lipschitz continuous on a neighborhood of `x` within `s`. More specifically, for any function `f` from a normed add commutative group `E` to another normed add commutative group `F`, both equipped with a normed space structure over the real numbers ℝ, a set `s` of `E`, and a point `x` in `E`, if `f` is `C^1` within `s` at `x` and `s` is a convex set, then there exists a Lipschitz constant `K` and a neighborhood `t` of `x` within `s` such that `f` is Lipschitz with the constant `K` on `t`. In other words, the distance between the images of any two points in `t` under `f` is less than or equal to `K` times the distance between the two points.
More concisely: If a continuously differentiable function `f` on a convex set `s` is once differentiable at a point `x` in `s`, then there exists a Lipschitz constant `K` and a neighborhood `t` of `x` in `s` such that |`f(y) - f(z)|\leq K |y-z| for all `y,z` in `t`.
|
ContDiffAt.hasStrictDerivAt'
theorem ContDiffAt.hasStrictDerivAt' :
∀ {n : ℕ∞} {𝕂 : Type u_1} [inst : RCLike 𝕂] {F' : Type u_3} [inst_1 : NormedAddCommGroup F']
[inst_2 : NormedSpace 𝕂 F'] {f : 𝕂 → F'} {f' : F'} {x : 𝕂},
ContDiffAt 𝕂 n f x → HasDerivAt f f' x → 1 ≤ n → HasStrictDerivAt f f' x
The theorem `ContDiffAt.hasStrictDerivAt'` states that if a function `f`, mapping from type `𝕂` to `F'`, is `C^n` (meaning it's n-times continuously differentiable) around a point `x`, and its derivative at that point is denoted `f'`, then `f'` is also a strict derivative at that point. This holds true when `n` is 1 or more. In mathematical terms, if a function is continuously differentiable to at least the first degree at a point, its derivative at that point also satisfies the condition for strict differentiability.
More concisely: If a function `f : 𝕂 → F'` is `C^n` around a point `x` with derivative `f'`, then `f'` is a strict derivative of `f` at `x`.
|
HasFTaylorSeriesUpToOn.exists_lipschitzOnWith_of_nnnorm_lt
theorem HasFTaylorSeriesUpToOn.exists_lipschitzOnWith_of_nnnorm_lt :
∀ {E : Type u_4} {F : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
[inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {f : E → F} {p : E → FormalMultilinearSeries ℝ E F}
{s : Set E} {x : E},
HasFTaylorSeriesUpToOn 1 f p (insert x s) →
Convex ℝ s → ∀ (K : NNReal), ‖p x 1‖₊ < K → ∃ t ∈ nhdsWithin x s, LipschitzOnWith K f t
The theorem states that if a function `f` from a normed additive commutative group `E` to another `F` has a formal Taylor series `p` up to order `1` on a set that is the union of a single point `x` and a convex set `s`, and if the nonnegative norm of `p x 1` is less than a nonnegative real number `K`, then there exists a set `t` in the neighborhood of `x` within `s` where the function `f` is `K`-Lipschitz continuous.
In more simplified terms, if a function `f` has a first-order Taylor series that fits it well in a neighborhood of a point `x` within a convex set, and the size of the first derivative is controlled, then `f` behaves nearly linearly around `x` with a controlled slope.
More concisely: Given a normed additive commutative group `E`, a convex set `s` in `E`, a point `x` in `s`, a function `f : E -> E'` from `E` to another normed space `E'`, and a real number `K`, if `f` has a norm-convergent first-order Taylor series `p` on `x ∪ s` with `||p x 1|| < K`, then there exists a neighborhood `t` of `x` within `s` such that `||f(y) - f(x) - p(y)|| <= K * ||y - x||` for all `y` in `t`.
|
ContDiffAt.exists_lipschitzOnWith_of_nnnorm_lt
theorem ContDiffAt.exists_lipschitzOnWith_of_nnnorm_lt :
∀ {𝕂 : Type u_1} [inst : RCLike 𝕂] {E' : Type u_2} [inst_1 : NormedAddCommGroup E'] [inst_2 : NormedSpace 𝕂 E']
{F' : Type u_3} [inst_3 : NormedAddCommGroup F'] [inst_4 : NormedSpace 𝕂 F'] {f : E' → F'} {x : E'},
ContDiffAt 𝕂 1 f x → ∀ (K : NNReal), ‖fderiv 𝕂 f x‖₊ < K → ∃ t ∈ nhds x, LipschitzOnWith K f t
This theorem states that if a function `f` is `C^1` (once continuously differentiable) at a point `x` and there exists a nonnegative real number `K` that is greater than the norm of the derivative of `f` at `x`, then `f` is `K`-Lipschitz continuous within a neighborhood of `x`. In other words, there exists a set around `x`, within which the distance between the function values of any two points does not exceed `K` times the distance between these two points themselves.
More concisely: If a `C^1` function `f` has a derivative with norm `K` at a point `x`, then `f` is `K`-Lipschitz continuous in a neighborhood of `x`.
|
HasFTaylorSeriesUpToOn.exists_lipschitzOnWith
theorem HasFTaylorSeriesUpToOn.exists_lipschitzOnWith :
∀ {E : Type u_4} {F : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
[inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {f : E → F} {p : E → FormalMultilinearSeries ℝ E F}
{s : Set E} {x : E},
HasFTaylorSeriesUpToOn 1 f p (insert x s) → Convex ℝ s → ∃ K, ∃ t ∈ nhdsWithin x s, LipschitzOnWith K f t
The theorem `HasFTaylorSeriesUpToOn.exists_lipschitzOnWith` states the following: if a function `f` from a normed additively commutative group `E` to another such group `F` has a formal Taylor series `p` up to order `1` on the set `{x} ∪ s`, where `s` is a convex set in the reals, then `f` is Lipschitz continuous within a neighborhood of `x` in `s`. In other words, there exists a non-negative real number `K` and a set `t` which is a neighborhood of `x` within `s`, such that for every pair of points in `t`, the distance between their images under `f` is at most `K` times the distance between the points themselves.
More concisely: If a function `f` from a normed additively commutative group `E` to another such group `F` has a formal Taylor series up to order 1 on the convex set `s` in the reals, then there exists a neighborhood `t` of `x` in `s` and a constant `K` such that for all `x₁, x₂ in t`, `||f(x₁) - f(x₂)|| ≤ K ||x₁ - x₂||`.
|
ContDiffAt.exists_lipschitzOnWith
theorem ContDiffAt.exists_lipschitzOnWith :
∀ {𝕂 : Type u_1} [inst : RCLike 𝕂] {E' : Type u_2} [inst_1 : NormedAddCommGroup E'] [inst_2 : NormedSpace 𝕂 E']
{F' : Type u_3} [inst_3 : NormedAddCommGroup F'] [inst_4 : NormedSpace 𝕂 F'] {f : E' → F'} {x : E'},
ContDiffAt 𝕂 1 f x → ∃ K, ∃ t ∈ nhds x, LipschitzOnWith K f t
The theorem states that if a function `f` is once continuously differentiable at a point `x` (denoted as `C^1` at `x`), then there exists a non-negative real number `K` and a neighborhood of `x` such that `f` is Lipschitz continuous with constant `K` on this neighborhood. Here, a function is Lipschitz continuous on a set if the distance (in the target space) between the images of any two points in the set is at most `K` times the distance (in the domain space) between the two points. A neighborhood of `x` is a set that contains an open set around `x`.
More concisely: If a function `f` is once continuously differentiable at a point `x`, then there exists a Lipschitz constant `K` such that |`f(y) - f(z)|\leq K |y - z| for all `y` and `z` in some neighborhood of `x`.
|
ContDiffAt.hasStrictDerivAt
theorem ContDiffAt.hasStrictDerivAt :
∀ {n : ℕ∞} {𝕂 : Type u_1} [inst : RCLike 𝕂] {F' : Type u_3} [inst_1 : NormedAddCommGroup F']
[inst_2 : NormedSpace 𝕂 F'] {f : 𝕂 → F'} {x : 𝕂}, ContDiffAt 𝕂 n f x → 1 ≤ n → HasStrictDerivAt f (deriv f x) x
The theorem `ContDiffAt.hasStrictDerivAt` states that for any function `f` defined over a type `𝕂` (which behaves like a real constant) with values in a normed additive commutative group `F'`, if the function `f` is continuously differentiable of any order `n` such that `1 ≤ n` at a point `x`, then the derivative of `f` at this point is also a strict derivative. In other words, if we can differentiate `f` continuously `n` times around a point `x` with `n` greater than or equal to 1, the derivative of `f` at `x` satisfies the condition of strict differentiability.
More concisely: If a continuously differentiable function `f` of order `n ≥ 1` at a point `x` has derivatives of all orders at `x`, then the derivative of `f` at `x` is a strict derivative.
|
ContDiffAt.hasStrictFDerivAt
theorem ContDiffAt.hasStrictFDerivAt :
∀ {n : ℕ∞} {𝕂 : Type u_1} [inst : RCLike 𝕂] {E' : Type u_2} [inst_1 : NormedAddCommGroup E']
[inst_2 : NormedSpace 𝕂 E'] {F' : Type u_3} [inst_3 : NormedAddCommGroup F'] [inst_4 : NormedSpace 𝕂 F']
{f : E' → F'} {x : E'}, ContDiffAt 𝕂 n f x → 1 ≤ n → HasStrictFDerivAt f (fderiv 𝕂 f x) x
The theorem `ContDiffAt.hasStrictFDerivAt` states that if a function `f` is `n` times continuously differentiable at a point `x` in a normed space over a real-like field `𝕂`, with `n` being any countably infinite natural number and `1 ≤ n`, then the derivative of `f` at this point `x` is also a strict derivative. Here, a strict derivative refers to the fact that the derivative of `f` at `x`, given by `fderiv 𝕂 f x`, is a linear approximation of `f` near `x` that is not just accurate but also has optimal error bounds. This theorem is a key result in differential calculus in the context of real or complex normed vector spaces.
More concisely: If a function `f` is `n` times continuously differentiable at a point `x` in a normed space over a real- or complex-number field, then its derivative at `x` is a strict derivative.
|
ContDiff.lipschitzWith_of_hasCompactSupport
theorem ContDiff.lipschitzWith_of_hasCompactSupport :
∀ {𝕂 : Type u_1} [inst : RCLike 𝕂] {E' : Type u_2} [inst_1 : NormedAddCommGroup E'] [inst_2 : NormedSpace 𝕂 E']
{F' : Type u_3} [inst_3 : NormedAddCommGroup F'] [inst_4 : NormedSpace 𝕂 F'] {f : E' → F'} {n : ℕ∞},
HasCompactSupport f → ContDiff 𝕂 n f → 1 ≤ n → ∃ C, LipschitzWith C f
The theorem `ContDiff.lipschitzWith_of_hasCompactSupport` states that for any function `f` from a normed additive commutative group `E'` to another one `F'`, both over a field `𝕂` that behaves like real numbers, if `f` has compact support and is continuously differentiable (`C^1` or `ContDiff` for short) at least once (`1 ≤ n`), then there exists a nonnegative real number `C` such that `f` is Lipschitz continuous with constant `C`. In other words, for all points `x, y` in the domain of `f`, the distance between `f(x)` and `f(y)` is less than or equal to `C` times the distance between `x` and `y`.
More concisely: If `f` is a continuously differentiable function from a normed additive commutative group to another with compact support, then `f` is Lipschitz continuous.
|