norm_lineDeriv_le_of_lipschitz
theorem norm_lineDeriv_le_of_lipschitz :
β (π : Type u_1) [inst : NontriviallyNormedField π] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace π F] {E : Type u_3} [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace π E] {v : E}
{f : E β F} {xβ : E} {C : NNReal}, LipschitzWith C f β βlineDeriv π f xβ vβ β€ βC * βvβ
The theorem `norm_lineDeriv_le_of_lipschitz` states that if a function `f` is `C`-Lipschitz continuous, then the norm of its line derivative at a point `xβ` in the direction `v` is bounded by `C` times the norm of `v`.
In other words, if `f` is Lipschitz continuous with constant `C` in a vector space over a non-trivially normed field `π`, then for all `xβ` and `v` in this vector space, the norm of the line derivative of `f` at `xβ` in the direction `v` is less than or equal to `C` times the norm of `v`. This is a version of the theorem that uses the concept of a line derivative.
More concisely: If `f` is `C-`Lipschitz continuous on a vector space over a non-trivially normed field, then the norm of its line derivative of `f` at any point in the direction of any vector is bounded by `C` times the norm of the vector.
|
LineDifferentiableWithinAt.hasLineDerivWithinAt
theorem LineDifferentiableWithinAt.hasLineDerivWithinAt :
β {π : Type u_1} [inst : NontriviallyNormedField π] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace π F] {E : Type u_3} [inst_3 : AddCommGroup E] [inst_4 : Module π E] {f : E β F} {s : Set E}
{x v : E}, LineDifferentiableWithinAt π f s x v β HasLineDerivWithinAt π f (lineDerivWithin π f s x v) s x v
This theorem, `LineDifferentiableWithinAt.hasLineDerivWithinAt`, states that for any non-trivially normed field `π`, a normed additive commutative group `F` that is also a normed space over `π`, an additive group `E` that is a module over `π`, a function `f` mapping from `E` to `F`, a set `s` of elements of `E`, and two elements `x` and `v` of `E`, if `f` is line differentiable at `x` with direction `v` within the set `s` (i.e., `LineDifferentiableWithinAt π f s x v`), then `f` also has a line derivative at `x` with direction `v` within `s`, and the derivative is given by `lineDerivWithin π f s x v` (i.e., `HasLineDerivWithinAt π f (lineDerivWithin π f s x v) s x v`). The theorem asserts the existence of a line derivative for a function that is line differentiable within a certain set.
More concisely: If a function `f` is line differentiable within a set `s` at point `x` in the direction `v` over a normed field `π`, then `f` has a line derivative at `x` in the direction `v` within `s`, which is equal to the line derivative of `f` within `s` at `x` and `v`.
|
HasLineDerivAt.le_of_lipschitz
theorem HasLineDerivAt.le_of_lipschitz :
β {π : Type u_1} [inst : NontriviallyNormedField π] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace π F] {E : Type u_3} [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace π E] {v : E}
{f : E β F} {f' : F} {xβ : E}, HasLineDerivAt π f f' xβ v β β {C : NNReal}, LipschitzWith C f β βf'β β€ βC * βvβ
The theorem `HasLineDerivAt.le_of_lipschitz` states that if a function `f` is line differentiable at a given point `xβ` and `C`-Lipschitz continuous, then the norm of its line derivative at `xβ` in the direction `v` is bounded by `C` times the norm of `v`. Here, `C` is a nonnegative real number, the Lipschitz constant, which captures how much `f` can change for a small change in its input. The norm `βf'β` of the derivative `f'` measures the "size" or "length" of the derivative vector. The theorem essentially links the Lipschitz continuity of `f` with a bound on the size of its derivative.
More concisely: If a function `f` is line differentiable at `xβ` with a `C`-Lipschitz continuous derivative, then `βf'(xβ)β β€ C * βvβ` for any direction vector `v`.
|
HasLineDerivAt.le_of_lip'
theorem HasLineDerivAt.le_of_lip' :
β {π : Type u_1} [inst : NontriviallyNormedField π] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace π F] {E : Type u_3} [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace π E] {v : E}
{f : E β F} {f' : F} {xβ : E},
HasLineDerivAt π f f' xβ v β
β {C : β}, 0 β€ C β (βαΆ (x : E) in nhds xβ, βf x - f xββ β€ C * βx - xββ) β βf'β β€ C * βvβ
This theorem, "HasLineDerivAt.le_of_lip'", is a converse to the mean value inequality. It states that if a function `f` is differentiable at a point `xβ` in the direction `v` and is `C`-Lipschitz on a neighborhood of `xβ`, then the norm of its line derivative at `xβ` in the direction `v` is bounded by `C` times the norm of `v`. Here, being `C`-Lipschitz on a neighborhood of `xβ` means that for every `x` in some neighborhood of `xβ`, the norm of `f(x) - f(xβ)` is less than or equal to `C` times the norm of `x - xβ`. The theorem only requires that the inequality `βf x - f xββ β€ C * βx - xββ` holds in a neighborhood of `xβ`.
More concisely: If a differentiable function at a point is C-Lipschitz in a neighborhood, then its line derivative's norm is bounded by C times the direction vector's norm.
|
norm_lineDeriv_le_of_lip'
theorem norm_lineDeriv_le_of_lip' :
β (π : Type u_1) [inst : NontriviallyNormedField π] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace π F] {E : Type u_3} [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace π E] {v : E}
{f : E β F} {xβ : E} {C : β},
0 β€ C β (βαΆ (x : E) in nhds xβ, βf x - f xββ β€ C * βx - xββ) β βlineDeriv π f xβ vβ β€ C * βvβ
The theorem `norm_lineDeriv_le_of_lip'` states that if a function `f` is `C`-Lipschitz on a neighborhood of a point `xβ`, then the norm of its line derivative at `xβ` in the direction `v` is bounded by `C` times the norm of `v`. More specifically, this is a converse to the mean value inequality which only assumes that the norm of the difference between `f(x)` and `f(xβ)` is less than or equal to `C` times the norm of the difference between `x` and `xβ` in a neighborhood of `x`. The Lipschitz condition is fulfilled if for all `x` in the neighborhood of `xβ`, the norm of `f(x) - f(xβ)` is less than or equal to `C` times the norm of `x - xβ`. The theorem is applicable in the context of a nontrivially normed field `π`, a normed additively commutative group `F`, and a normed space `E` over `π`.
More concisely: If a function `f` is `C-`Lipschitz around `xβ` in the normed space `E` over the field `π`, then the norm of `f'(`xβ`, v)` is bounded by `C * ||v||`, where `v` is a vector in `E` and `||.||` denotes the norm.
|
LineDifferentiableAt.hasLineDerivAt
theorem LineDifferentiableAt.hasLineDerivAt :
β {π : Type u_1} [inst : NontriviallyNormedField π] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace π F] {E : Type u_3} [inst_3 : AddCommGroup E] [inst_4 : Module π E] {f : E β F} {x v : E},
LineDifferentiableAt π f x v β HasLineDerivAt π f (lineDeriv π f x v) x v
The theorem `LineDifferentiableAt.hasLineDerivAt` states that for any function `f` mapping from a vector space `E` to another vector space `F`, if `f` is line-differentiable at a point `x` in the direction `v`, then `f` has a line derivative at that point `x` in the direction `v`. The line derivative is given by the function `lineDeriv π f x v` where `π` is a nontrivial normed field. Here, a function is line-differentiable at a point in a direction if it can be approximated by a linear function at that point in that direction as we approach the point along the line.
More concisely: If a function `f` from a vector space `E` to another vector space `F` is line-differentiable at point `x` in direction `v`, then there exists a linear function `l` such that the limit `βΞ΅>0. βΞ΄>0, βh. βhβ<Ξ΄ β βf(x+h) - (f(x) + l(h))β < Ξ΅βhβ holds.
|
HasLineDerivWithinAt.lineDifferentiableWithinAt
theorem HasLineDerivWithinAt.lineDifferentiableWithinAt :
β {π : Type u_1} [inst : NontriviallyNormedField π] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace π F] {E : Type u_3} [inst_3 : AddCommGroup E] [inst_4 : Module π E] {f : E β F} {f' : F}
{s : Set E} {x v : E}, HasLineDerivWithinAt π f f' s x v β LineDifferentiableWithinAt π f s x v
This theorem, `HasLineDerivWithinAt.lineDifferentiableWithinAt`, states that given a field `π` that is nontrivially normed, a normed add-commutative group `F`, a normed space over `π` and `F`, an add-commutative group `E`, a module over `π` and `E`, a function `f` mapping `E` to `F`, a derivative `f'` of `F`, a set `s` of `E`, and two elements `x` and `v` of `E`, if `f` has a line derivative within `s` at `x` along `v`, then `f` is line differentiable within `s` at `x` along `v`. This theorem establishes a connection between the existence of a line derivative and the line differentiability of a function at a certain point within a given set.
More concisely: If a function has a line derivative within a set at a point along a vector, then it is line differentiable within that set at that point along that vector.
|
HasLineDerivAt.lineDifferentiableAt
theorem HasLineDerivAt.lineDifferentiableAt :
β {π : Type u_1} [inst : NontriviallyNormedField π] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace π F] {E : Type u_3} [inst_3 : AddCommGroup E] [inst_4 : Module π E] {f : E β F} {f' : F}
{x v : E}, HasLineDerivAt π f f' x v β LineDifferentiableAt π f x v
This theorem states that for any nontrivially normed field π, normed additive commutative group F, and additive commutative group E which is a π module, a function `f` from E to F is "line differentiable" at a point `x` in the direction `v` if there exists a derivative `f'` such that the function `f` has a line derivative at `x` in the direction `v`. Here, "line differentiable" refers to the existence of a derivative `f'` such that the function `f (x + t v) = f x + t β’ f' + o (t)` as `t` tends to `0`.
More concisely: For any nontrivially normed field π, normed additive commutative group F, and additive commutative group E which is a π module, a function `f` from E to F is line differentiable at a point `x` in the direction `v` if there exists a derivative `f'` such that `f (x + tv) = f x + tβ’f' + o(t)` as `t` approaches 0.
|
HasLineDerivAt.le_of_lipschitzOn
theorem HasLineDerivAt.le_of_lipschitzOn :
β {π : Type u_1} [inst : NontriviallyNormedField π] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace π F] {E : Type u_3} [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace π E] {v : E}
{f : E β F} {f' : F} {xβ : E},
HasLineDerivAt π f f' xβ v β
β {s : Set E}, s β nhds xβ β β {C : NNReal}, LipschitzOnWith C f s β βf'β β€ βC * βvβ
The theorem `HasLineDerivAt.le_of_lipschitzOn` states that if a function `f` is line differentiable at a point `xβ` and it's Lipschitz continuous with a constant `C` on a neighborhood of `xβ`, then the norm of its line derivative at `xβ` in the direction `v` is bounded by `C` times the norm of `v`. This version only assumes that the norm of the difference `f x - f xβ` is less than or equal to `C` times the norm of the difference `x - xβ` in a neighborhood of `x`. The neighborhood is represented as a set `s` in the topological space structure of `E` and it belongs to the neighborhood filter at `xβ`. This theorem is relevant in the field of analysis and provides a converse to the mean value inequality.
More concisely: If a line differentiable function `f` at `xβ` is Lipschitz continuous with constant `C` in a neighborhood `s` of `xβ`, then the line derivative's norm at `xβ` is bounded by `C` times the norm of the direction vector.
|
norm_lineDeriv_le_of_lipschitzOn
theorem norm_lineDeriv_le_of_lipschitzOn :
β (π : Type u_1) [inst : NontriviallyNormedField π] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace π F] {E : Type u_3} [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace π E] {v : E}
{f : E β F} {xβ : E} {s : Set E},
s β nhds xβ β β {C : NNReal}, LipschitzOnWith C f s β βlineDeriv π f xβ vβ β€ βC * βvβ
The theorem `norm_lineDeriv_le_of_lipschitzOn` is a conversely stated form of the mean value inequality in the context of Lipschitz continuity. Specifically, it states that for a nontrivially normed field `π`, a normed additively commutative group `F` and `E`, and a normed space `F` and `E` over `π`, if a function `f` mapping from `E` to `F` is `C`-Lipschitz continuous on a set `s` that is a neighborhood of a point `xβ` in `E`, then the norm of the line derivative of `f` at `xβ` in the direction of a given vector `v` is bounded by `C` times the norm of `v`. Here `C` is a nonnegative real number, `s` is a neighborhood of `xβ`, and `LipschitzOnWith C f s` is the condition that `f` is `C`-Lipschitz on `s`.
More concisely: For a nontrivially normed field `π`, given a normed additively commutative group `F` and `E`, a normed space `F` and `E` over `π`, and a `C-`Lipschitz continuous function `f: E β F` on a neighborhood `s` of a point `xβ` in `E`, the norm of the line derivative of `f` at `xβ` in the direction of a vector `v` is bounded by `C * ||v||`.
|
HasLineDerivWithinAt.smul
theorem HasLineDerivWithinAt.smul :
β {π : Type u_1} [inst : NontriviallyNormedField π] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace π F] {E : Type u_3} [inst_3 : AddCommGroup E] [inst_4 : Module π E] {f : E β F} {s : Set E}
{x v : E} {f' : F},
HasLineDerivWithinAt π f f' s x v β β (c : π), HasLineDerivWithinAt π f (c β’ f') s x (c β’ v)
This theorem, named `HasLineDerivWithinAt.smul`, states that for any type `π` that forms a non-trivially normed field, type `F` that forms a normed add commutative group, type `E` that forms both an add commutative group and a `π`-module, a function `f` from `E` to `F`, a set `s` of elements of type `E`, elements `x` and `v` of type `E`, and an element `f'` of type `F`, if `f` has a linear derivative at `x` within the set `s` in the direction of `v` with respect to `f'`, then for any scalar `c` from `π`, `f` also has a linear derivative at `x` within the set `s` in the direction of `c β’ v` with respect to `c β’ f'`. In other words, the derivative of the function `f` at a point `x` within a set `s` scales linearly with both the derivative and the direction vector.
More concisely: If `f` has a linear derivative at `x` within set `s` in direction `v` with respect to `f'` in a normed field `π`, then it has a linear derivative at `x` within `s` in direction `cv` with respect to `cf'` for any scalar `c` from `π`.
|
HasLineDerivAt.tendsto_slope_zero
theorem HasLineDerivAt.tendsto_slope_zero :
β {π : Type u_1} [inst : NontriviallyNormedField π] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace π F] {E : Type u_3} [inst_3 : AddCommGroup E] [inst_4 : Module π E] {f : E β F} {f' : F}
{x v : E},
HasLineDerivAt π f f' x v β Filter.Tendsto (fun t => tβ»ΒΉ β’ (f (x + t β’ v) - f x)) (nhdsWithin 0 {0}αΆ) (nhds f')
The theorem `HasLineDerivAt.tendsto_slope_zero` is an alias for the forward direction of `hasLineDerivAt_iff_tendsto_slope_zero`. It states that for a given function `f` from a normed vector space `E` over a non-trivial normed field `π` to another normed add commutative group `F`, if the function `f` has a line derivative at a point `x` in the direction of a vector `v` and the derivative is `f'`, then the function mapping `t` to `tβ»ΒΉ β’ (f (x + t β’ v) - f x)` tends to `f'` as `t` tends to `0` within the set of all non-zero real numbers.
More concisely: If a function from a normed vector space to another normed add commutative group has a line derivative at a point with value `f'` in direction `v`, then the difference quotient `(f (x + tv) - f x) / t` tends to `f'` as `t` approaches `0`.
|