hasFDerivAt_const
theorem hasFDerivAt_const :
β {π : Type u_1} [inst : NontriviallyNormedField π] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] (c : F)
(x : E), HasFDerivAt (fun x => c) 0 x
The theorem `hasFDerivAt_const` states that for any non-trivially normed field `π`, normed additive commutative group `E` and `F`, and any normed spaces over `π` for `E` and `F`, the derivative at any point `x` in `E` of a constant function (a function that always returns the same value `c` in `F`) is zero. This is consistent with the idea in calculus that the derivative of a constant function is always zero because a constant function does not change, so its rate of change is zero.
More concisely: For any non-trivially normed field `π`, normed additive commutative groups `E` and `F`, and constant function `f : E β F`, the derivative `(hasFDerivAt f x)` at any point `x` in `E` equals the zero map `0 : F β F`.
|
norm_fderiv_le_of_lip'
theorem norm_fderiv_le_of_lip' :
β (π : Type u_1) [inst : NontriviallyNormedField π] {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} {C : β}, 0 β€ C β (βαΆ (x : E) in nhds xβ, βf x - f xββ β€ C * βx - xββ) β βfderiv π f xββ β€ C
This theorem, named `norm_fderiv_le_of_lip'`, is a converse to the mean value inequality. In particular, it states that if a function `f` is `C`-Lipschitz on a neighborhood of a point `xβ`, then the norm of its derivative at `xβ` is bounded by `C`. Here, being `C`-Lipschitz means that the norm of the difference `f(x) - f(xβ)` is less than or equal to `C` times the norm of `x - xβ` for all `x` in the neighborhood of `xβ`. This version of the theorem only assumes the Lipschitz condition in a neighborhood of `xβ`.
More concisely: If a function `f` is `C-Lipschitz` around `xβ`, then the norm of its derivative at `xβ` is bounded by `C`.
|
hasFDerivWithinAt_inter
theorem hasFDerivWithinAt_inter :
β {π : Type u_1} [inst : NontriviallyNormedField π] {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} {s t : Set E},
t β nhds x β (HasFDerivWithinAt f f' (s β© t) x β HasFDerivWithinAt f f' s x)
This theorem states that for any nontrivially normed field `π`, normed additive commutative group `E`, and normed space `π E`, along with another normed additive commutative group `F` and normed space `π F`, and for a given function `f` mapping `E` to `F` along with its derivative `f'` at point `x` in `E`, and sets `s` and `t` of `E`, if `t` is a neighborhood of `x` (i.e., `t` belongs to the neighborhood filter of `x`), then the function `f` has a derivative within the intersection of `s` and `t` at `x` if and only if `f` has a derivative within `s` at `x`. In mathematical terms, we can say that the existence of the Frechet derivative of a function at a point within a set is invariant under intersection with a neighborhood of the point.
More concisely: For any nontrivially normed field `π`, normed additive commutative groups `E` and `F`, normed spaces `π E` and `π F`, function `f : E β F` with derivative `f'` at `x β E`, and sets `s` and `t` that are neighborhoods of `x` in `E`, if `t` is a subset of `s`, then `f` has a derivative at `x` within `s` if and only if it has a derivative at `x` within the intersection of `s` and `t`.
|
DifferentiableAt.hasFDerivAt
theorem DifferentiableAt.hasFDerivAt :
β {π : Type u_1} [inst : NontriviallyNormedField π] {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}, DifferentiableAt π f x β HasFDerivAt f (fderiv π f x) x
The theorem `DifferentiableAt.hasFDerivAt` states that for any given function `f` from `E` to `F`, if `f` is differentiable at a point `x` in `E`, then `f` has a derivative at `x` and this derivative is given by `fderiv π f x`. Here, `π` is a nontrivial normed field, `E` and `F` are normed additive commutative groups equipped with a normed space structure over `π`, and `fderiv π f x` is the derivative of `f` at `x` (or zero if `f` is not differentiable at `x`).
More concisely: If `f` is differentiable at `x` in the normed additive commutative groups `E` and `F` over a nontrivial normed field `π`, then `fderiv π f x` exists and is the derivative of `f` at `x`.
|
HasFDerivAt.le_of_lipschitzOn
theorem HasFDerivAt.le_of_lipschitzOn :
β {π : Type u_1} [inst : NontriviallyNormedField π] {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},
HasFDerivAt f f' xβ β β {s : Set E}, s β nhds xβ β β {C : NNReal}, LipschitzOnWith C f s β βf'β β€ βC
This theorem, named `HasFDerivAt.le_of_lipschitzOn`, states that if a function `f` is differentiable at a point `xβ` and is `C`-Lipschitz on a neighborhood of `xβ`, then the norm of its derivative at `xβ` is bounded by `C`. In other words, if `f` changes at a rate no faster than `C` around `xβ` (as indicated by the Lipschitz condition), then the derivative of `f` at `xβ` is also no larger than `C`. This theorem provides a converse to the mean value inequality in the specified context.
More concisely: If a differentiable function at a point is Lipschitz continuous on a neighborhood of that point, then the norm of its derivative at that point is bounded by the Lipschitz constant.
|
hasFDerivWithinAt_univ
theorem hasFDerivWithinAt_univ :
β {π : Type u_1} [inst : NontriviallyNormedField π] {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}, HasFDerivWithinAt f f' Set.univ x β HasFDerivAt f f' x
This theorem states that, for any nontrivially normed field π, normed additive commutative groups E and F, and a normed space π over E and F, if we consider a function `f` from E to F and a continuous linear map `f'` from E to π to F, and a point `x` in E. The function `f` has `f'` as its derivative at `x` within the universal set if and only if `f` has `f'` as its derivative at `x`. In other words, the condition of the function `f` having `f'` as its derivative at a point `x` is the same whether we consider it within the whole space or any specific subset of the space.
More concisely: For any nontrivially normed field π, normed additive commutative groups E and F, and a normed space π over E and F, the derivative of a continuous linear map `f'` from E to π being equal to the derivative of the function `f` from E to F at a point `x` holds both in the whole space and in the subset of π.
|
HasFDerivAt.le_of_lipschitz
theorem HasFDerivAt.le_of_lipschitz :
β {π : Type u_1} [inst : NontriviallyNormedField π] {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}, HasFDerivAt f f' xβ β β {C : NNReal}, LipschitzWith C f β βf'β β€ βC
This theorem states that, given a function `f` that is differentiable at a point `xβ` and is `C`-Lipschitz continuous, then the norm of its derivative at `xβ` is bounded by `C`. The term `C`-Lipschitz continuity refers to the property of a function where the distance between the output values is at most `C` times the distance between the input values (`C` is a nonnegative real number). In other words, the theorem is saying that if a function behaves well (in the sense that it is Lipschitz continuous), then its derivative at a certain point also behaves well (in the sense that it has a bounded norm).
More concisely: If a differentiable function `f` at point `xβ` is `C`-Lipschitz continuous, then the norm of its derivative `f'` at `xβ` is bounded by `C`.
|
HasFDerivWithinAt.insert'
theorem HasFDerivWithinAt.insert' :
β {π : Type u_1} [inst : NontriviallyNormedField π] {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} {s : Set E} {y : E},
HasFDerivWithinAt f f' s x β HasFDerivWithinAt f f' (insert y s) x
This theorem, referred to as an alias of the reverse direction of `hasFDerivWithinAt_insert`, asserts that for any nontrivially normed field `π`, normed additively commutative group `E` and `F`, and `E` being a normed space over `π` as well as `F`, given a function `f` mapping `E` to `F`, a bounded linear map `f'` from `E` to `F`, a point `x` in `E`, a set `s` of `E`, and another point `y` in `E`, if `f` has derivative `f'` within the set `s` at point `x`, then `f` also has derivative `f'` within the set formed by inserting `y` into `s` at point `x`. Thus, the presence or absence of any additional point in the set does not affect the derivative of the function at a particular point within the set.
More concisely: Given a nontrivially normed field `π`, normed additively commutative groups `E` and `F`, a function `f : E β F` from a normed space `E` over `π` to `F`, a bounded linear map `f' : E β F`, a point `x β E`, a set `s β E`, and another point `y β E`, if `f` has derivative `f'` within `s` at `x`, then `f` also has derivative `f'` within `s βͺ {y}` at `x`.
|
HasFDerivWithinAt.continuousWithinAt
theorem HasFDerivWithinAt.continuousWithinAt :
β {π : Type u_1} [inst : NontriviallyNormedField π] {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} {s : Set E}, HasFDerivWithinAt f f' s x β ContinuousWithinAt f s x
This theorem states that for any non-trivially normed field `π` and normed additive commutative groups `E` and `F` that are also normed spaces over `π`, if a function `f` from `E` to `F` has a Frechet derivative `f'` within a subset `s` of `E` at a point `x` in `E` (denoted by `HasFDerivWithinAt f f' s x`), then `f` is continuous at `x` within `s`. This means that as points in `s` get arbitrarily close to `x`, the function values `f` of these points get arbitrarily close to `f(x)`.
More concisely: If a function `f` between two normed spaces `E` and `F` over a non-trivially normed field `π` has a Frechet derivative `f'` within a subset `s` of `E` at a point `x` in `E`, then `f` is continuous at `x` within `s`. In other words, for all `Ξ΅ > 0`, there exists `Ξ΄ > 0` such that for all `y` in `s` with `βy - xβ < Ξ΄`, we have `βf(y) - f(x) - f'(x)(y - x)β < Ξ΅`.
|
HasFDerivWithinAt.hasFDerivAt_of_univ
theorem HasFDerivWithinAt.hasFDerivAt_of_univ :
β {π : Type u_1} [inst : NontriviallyNormedField π] {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}, HasFDerivWithinAt f f' Set.univ x β HasFDerivAt f f' x
This theorem, known as an alias of the forward direction of `hasFDerivWithinAt_univ`, states that for any nontrivially normed field `π`, normed add commutative groups `E` and `F`, which are also normed vector spaces over `π`, a function `f` from `E` to `F`, a continuous linear map `f'`, and an element `x` in `E`, if the function `f` has `f'` as its derivative within the universal set at `x`, then the function `f` also has `f'` as its derivative at `x`. In mathematical terms, it suggests that if the derivative of `f` exists at every point in its domain, then the derivative of `f` exists at a particular point `x` in its domain.
More concisely: If a function between two normed vector spaces over a nontrivially normed field has a continuous linear derivative everywhere, then it has a derivative at any given point.
|
DifferentiableAt.differentiableWithinAt
theorem DifferentiableAt.differentiableWithinAt :
β {π : Type u_1} [inst : NontriviallyNormedField π] {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} {s : Set E}, DifferentiableAt π f x β DifferentiableWithinAt π f s x
The theorem `DifferentiableAt.differentiableWithinAt` states that for any nontrivially normed field `π`, normed add commutative group `E`, and normed add commutative group `F`, with a normed space structure over `π` for `E` and `F`, if a function `f` mapping from `E` to `F` is differentiable at a point `x` in `E`, then `f` is also differentiable at the same point `x` within any set `s` of `E`. In mathematical terms, this theorem asserts that if a function is differentiable at a point, then it remains differentiable at that point when restricted to any subset of its domain.
More concisely: If a function is differentiable at a point in a normed add commutative group, then it is differentiable at that point in any subset of its domain in the same normed add commutative groups.
|
DifferentiableAt.continuousAt
theorem DifferentiableAt.continuousAt :
β {π : Type u_1} [inst : NontriviallyNormedField π] {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}, DifferentiableAt π f x β ContinuousAt f x
This theorem states that for any function `f` mapping from a normed vector space `E` to another normed vector space `F` (both over a nontrivially normed field `π`), if the function `f` is differentiable at a point `x` in `E`, then `f` is also continuous at that point `x`. This echoes the fundamental concept in calculus that differentiability implies continuity.
More concisely: If `f` is a differentiable function from a normed vector space `E` to another normed vector space `F` over a nontrivially normed field `π`, then `f` is continuous at every point `x` in `E`.
|
HasFDerivAtFilter.congr_of_eventuallyEq
theorem HasFDerivAtFilter.congr_of_eventuallyEq :
β {π : Type u_1} [inst : NontriviallyNormedField π] {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 fβ : E β F} {f' : E βL[π] F} {x : E} {L : Filter E},
HasFDerivAtFilter f f' x L β L.EventuallyEq fβ f β fβ x = f x β HasFDerivAtFilter fβ f' x L
This theorem states that for any nontrivially normed field `π`, normed add commutative groups `E` and `F` with `E` and `F` being normed spaces over `π`, two functions `f` and `fβ` from `E` to `F`, a continuous linear map `f'` from `E` to `F`, a point `x` in `E`, and a filter `L` on `E`, if `f` has a derivative at `x` with respect to filter `L`, and if `fβ` is eventually equal to `f` at filter `L` and `fβ` at `x` is equal to `f` at `x`, then `fβ` also has a derivative at `x` with respect to filter `L`. This theorem is essentially about the continuity of the derivative under certain conditions.
More concisely: If `f` and `fβ` are functions from a normed space `E` to another normed space `F` over a nontrivially normed field, `f` is continuously linear and has a derivative at `x` in `E` with respect to filter `L`, and `fβ` is eventually equal to `f` at filter `L` and `fβ(x) = f(x)`, then `fβ` has a derivative at `x` with respect to filter `L`.
|
Differentiable.continuous
theorem Differentiable.continuous :
β {π : Type u_1} [inst : NontriviallyNormedField π] {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},
Differentiable π f β Continuous f
The theorem `Differentiable.continuous` states that for any nontrivial normed field `π`, if a function `f` mapping from a normed vector space `E` over `π` to another normed vector space `F` over `π` is differentiable at every point in `E`, then `f` is also continuous. In other words, if a function is differentiable everywhere, it is also continuous everywhere. This result holds in the context of real or complex numbers (or, more generally, in any nontrivial normed field) and with possibly infinite-dimensional vector spaces.
More concisely: If a function between two normed vector spaces over a nontrivial normed field is differentiable at every point, then it is continuous.
|
Differentiable.differentiableOn
theorem Differentiable.differentiableOn :
β {π : Type u_1} [inst : NontriviallyNormedField π] {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}
{s : Set E}, Differentiable π f β DifferentiableOn π f s
The theorem `Differentiable.differentiableOn` states that for any nontrivially normed field `π`, normed addative commutative group `E`, normed space `π E`, normed addative commutative group `F`, normed space `π F`, a function `f` from `E` to `F`, and a set `s` of `E`, if the function `f` is differentiable at any point, then the function `f` is also differentiable within the set `s` at any point of `s`. In other words, global differentiability implies local differentiability.
More concisely: If a function between normed spaces is differentiable at any point, then it is differentiable at every point in its domain.
|
HasFDerivWithinAt.congr_mono
theorem HasFDerivWithinAt.congr_mono :
β {π : Type u_1} [inst : NontriviallyNormedField π] {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 fβ : E β F} {f' : E βL[π] F} {x : E} {s t : Set E},
HasFDerivWithinAt f f' s x β Set.EqOn fβ f t β fβ x = f x β t β s β HasFDerivWithinAt fβ f' t x
The theorem `HasFDerivWithinAt.congr_mono` states that for any types `π`, `E`, and `F` where `π` is a nontrivially normed field, `E` is a normed addition commutative group and a normed space over `π`, and `F` is a normed addition commutative group and a normed space over `π`, given two functions `f` and `fβ` from `E` to `F`, a continuous linear map `f'` from `E` to `F`, a point `x` in `E`, and two sets `s` and `t` of `E`, if `f` has a derivative within `s` at `x` equal to `f'`, function `fβ` equals function `f` on set `t`, `fβ` at `x` is equal to `f` at `x`, and set `t` is a subset of set `s`, then `fβ` also has a derivative within `t` at `x` equal to `f'`.
More concisely: If `f` has a derivative within `s` at `x` equal to `f'`, `fβ` equals `f` on `t`, `fβ(x) = f(x)`, and `t` is a subset of `s`, then `fβ` has a derivative within `t` at `x` equal to `f'`.
|
HasFDerivAt.lim
theorem HasFDerivAt.lim :
β {π : Type u_1} [inst : NontriviallyNormedField π] {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},
HasFDerivAt f f' x β
β (v : E) {Ξ± : Type u_6} {c : Ξ± β π} {l : Filter Ξ±},
Filter.Tendsto (fun n => βc nβ) l Filter.atTop β
Filter.Tendsto (fun n => c n β’ (f (x + (c n)β»ΒΉ β’ v) - f x)) l (nhds (f' v))
This theorem states that if a function `f` has a derivative `f'` at a point `x` in a normed field over a normed vector space, then for any vector `v` and any scalar-valued function `c` that tends to infinity, the limit of the sequence `c n β’ (f (x + (c n)β»ΒΉ β’ v) - f x)` as `n` tends to infinity, exists and equals `f' v`. This essentially asserts that the directional derivative of `f` at `x` along `v` agrees with the action of the derivative `f'` on `v`.
More concisely: If a function `f` has a derivative `f'` at a point `x` in a normed field over a normed vector space, then the limit as `nββ` of `(f (x + (1/c n) * v) - f x) / (1/c n)` exists and equals `f' v`, where `c` tends to infinity and `v` is a vector. This asserts the directional derivative of `f` at `x` along `v` equals the action of `f'` on `v`.
|
HasFDerivWithinAt.of_insert
theorem HasFDerivWithinAt.of_insert :
β {π : Type u_1} [inst : NontriviallyNormedField π] {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} {s : Set E} {y : E},
HasFDerivWithinAt f f' (insert y s) x β HasFDerivWithinAt f f' s x
This theorem, **Alias of the forward direction of `hasFDerivWithinAt_insert`**, states that for any non-trivially normed field `π`, any normed additive commutative groups `E` and `F` equipped with a normed space structure over `π`, a function `f` from `E` to `F`, a continuous linear map `f'`, an element `x` of `E`, a set `s` of `E`, and an element `y` of `E`, if `f` has a derivative `f'` within the set resulting from the insertion of `y` into `s` at point `x`, then `f` also has a derivative `f'` within the set `s` at point `x`.
In simpler terms, if a function has a derivative at a point within a certain set after an element is added, it also has a derivative at that point within the original set.
More concisely: If a function has a derivative within a set after an element is added, then it also has a derivative within the original set at the same point.
|
hasFDerivAtFilter_iff_isLittleO
theorem hasFDerivAtFilter_iff_isLittleO :
β {π : Type u_1} [inst : NontriviallyNormedField π] {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) (L : Filter E),
HasFDerivAtFilter f f' x L β (fun x' => f x' - f x - f' (x' - x)) =o[L] fun x' => x' - x
This theorem holds for a function `f` from a normed additive commutative group `E` to another normed additive commutative group `F`, both over a nontrivially normed field `π`. It states that the function `f` has a derivative `f'` at a point `x` with respect to a filter `L` if and only if the difference between `f(x')` and `f(x)` and the linear approximation `f'(x' - x)` is little-o of `x' - x` at the filter `L`. In other words, the error of linear approximation is infinitesimal compared to `x' - x` as `x'` approaches `x` according to the filter `L`.
More concisely: A function `f` from normed additive commutative groups `E` and `F` over a nontrivially normed field has a derivative `f'` at `x` with respect to filter `L` if and only if the difference `f(x') - f(x) - f'(x' - x)` is o(`x' - x`) as `x'` approaches `x` according to the filter `L`.
|
hasFDerivAt_id
theorem hasFDerivAt_id :
β {π : Type u_1} [inst : NontriviallyNormedField π] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] (x : E), HasFDerivAt id (ContinuousLinearMap.id π E) x
The theorem `hasFDerivAt_id` states that for any type `π` that is a nontrivially normed field and any type `E` that is a normed space over `π`, the identity function has its derivative at any point `x` in `E`, which is the identity map itself as a continuous linear map. In mathematical terms, it says that the derivative of the identity function at any point is still the identity function.
More concisely: For any nontrivially normed field `π` and normed space `E` over `π`, the identity function on `E` is its own derivative as a continuous linear map.
|
HasFDerivAt.unique
theorem HasFDerivAt.unique :
β {π : Type u_1} [inst : NontriviallyNormedField π] {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β' fβ' : E βL[π] F} {x : E}, HasFDerivAt f fβ' x β HasFDerivAt f fβ' x β fβ' = fβ'
The theorem `HasFDerivAt.unique` states that for any non-trivially normed field `π`, normed additive commutative groups `E` and `F`, a function `f` from `E` to `F`, continuous linear maps `fβ'` and `fβ'` from `E` to `F` over `π`, and an element `x` of `E`, if `f` has `fβ'` as its derivative at `x` and `f` also has `fβ'` as its derivative at `x`, then `fβ'` and `fβ'` must be equal. In other words, the derivative of a function at a point, if it exists, is unique.
More concisely: Given a non-trivially normed field `π`, normed additive commutative groups `E` and `F`, a continuous linear function `f` from `E` to `F`, and elements `x` in `E` and `fβ'`, `fβ'` in the space of continuous linear maps from `E` to `F` over `π`, if `fβ'` and `fβ'` are the derivatives of `f` at `x`, then `fβ' = fβ'`.
|
DifferentiableWithinAt.mono
theorem DifferentiableWithinAt.mono :
β {π : Type u_1} [inst : NontriviallyNormedField π] {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} {s t : Set E}, DifferentiableWithinAt π f t x β s β t β DifferentiableWithinAt π f s x
This theorem states that if a function `f` of type `E β F`, where `π` is a non-trivially normed field, `E` is a normed additive commutative group over `π`, and `F` is a normed additive commutative group over `π`, is differentiable at a point `x` within a set `t`, then `f` is also differentiable at `x` within any subset `s` of `t`. This theorem is usually used to restrict the domain of differentiability to a smaller set.
More concisely: If a function `f` from a normed additive commutative group `E` to a normed additive commutative group `F` over a non-trivially normed field is differentiable at a point `x` in a set `t`, then it is differentiable at `x` in any subset `s` of `t`.
|
hasFDerivWithinAt_congr_set'
theorem hasFDerivWithinAt_congr_set' :
β {π : Type u_1} [inst : NontriviallyNormedField π] {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} {s t : Set E} (y : E),
(nhdsWithin x {y}αΆ).EventuallyEq s t β (HasFDerivWithinAt f f' s x β HasFDerivWithinAt f f' t x)
This theorem, named `hasFDerivWithinAt_congr_set'`, states that for any non-trivially normed field `π`, normed additive commutative groups `E` and `F`, and normed spaces over `π` of `E` and `F`, given two functions `f` and `f'` that are mappings from `E` to `F` and `E` to `F` respectively, a point `x` in `E` and two sets `s` and `t` of `E`, and another point `y` in `E`, if the set `s` is almost everywhere equal to the set `t` within the neighborhood of `x` that excludes `y`, then the statement "the function `f` has a derivative `f'` at the point `x` within the set `s`" is equivalent to the statement "the function `f` has a derivative `f'` at the point `x` within the set `t`". In other words, the existence and nature of the derivative of the function `f` at the point `x` does not depend on the sets that are almost everywhere equal within the neighborhood of `x` excluding `y`.
More concisely: If two sets around a point exclude a third point and are almost everywhere equal, then a function has a derivative of the same value in both sets.
|
HasFDerivWithinAt.of_nhdsWithin_eq_bot
theorem HasFDerivWithinAt.of_nhdsWithin_eq_bot :
β {π : Type u_1} [inst : NontriviallyNormedField π] {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} {s : Set E}, nhdsWithin x (s \ {x}) = β₯ β HasFDerivWithinAt f f' s x
This theorem states that if `x` is an isolated point in the set `s`, then any function `f` from a normed additive commutative group `E` to another normed additive commutative group `F` (both groups being normed spaces over a non-trivially normed field `π`) has any derivative at the point `x` within the set `s`. This is because the statement is vacuous, resulting from the definition of the isolated point where the neighborhood within the set `s` at `x`, excluding `x` itself, is the bottom element of the filter lattice, commonly interpreted as an "empty" set or situation.
More concisely: If a point `x` is an isolated point in a set `s` of a normed additive commutative group `E`, then any function `f` from `E` to another normed additive commutative group `F` has a derivative at `x` within `s`. (However, this statement is vacuous since an isolated point has no neighborhood within `s` excluding the point itself.)
|
DifferentiableWithinAt.continuousWithinAt
theorem DifferentiableWithinAt.continuousWithinAt :
β {π : Type u_1} [inst : NontriviallyNormedField π] {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} {s : Set E}, DifferentiableWithinAt π f s x β ContinuousWithinAt f s x
This theorem states that for any non-trivial normed field `π` and normed spaces `E` and `F`, if a function `f` from `E` to `F` is differentiable at a point `x` within a set `s`, then `f` is also continuous at `x` within `s`. In other words, differentiability within a set at a specific point implies continuity at that point within the set.
More concisely: If a differentiable function between normed spaces is differentiable at a point within a set, then it is continuous at that point within the set.
|
differentiable_const
theorem differentiable_const :
β {π : Type u_1} [inst : NontriviallyNormedField π] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] (c : F),
Differentiable π fun x => c
The theorem `differentiable_const` states that for any nontrivially normed field `π`, normed additive commutative group `E` over `π`, normed additive commutative group `F` over `π`, and any constant `c` of type `F`, the function that maps every element of `E` to `c` is differentiable at any point in `E`. In other words, constant functions are differentiable everywhere in the domain.
More concisely: For any nontrivially normed field `π`, normed additive commutative groups `E` and `F` over `π`, and constant `c` in `F`, the function `x β¦ c` from `E` to `F` is differentiable at every point in `E`.
|
Filter.EventuallyEq.fderivWithin_eq
theorem Filter.EventuallyEq.fderivWithin_eq :
β {π : Type u_1} [inst : NontriviallyNormedField π] {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 fβ : E β F} {x : E} {s : Set E},
(nhdsWithin x s).EventuallyEq fβ f β fβ x = f x β fderivWithin π fβ s x = fderivWithin π f s x
This theorem states that for a nontrivially normed field `π`, a normed additive commutative group `E` that is also a normed space over `π`, another normed additive commutative group `F` that is also a normed space over `π`, for any two functions `f` and `fβ` from `E` to `F`, any point `x` in `E`, and any set `s` of `E`, if `fβ` and `f` are eventually equal in the neighborhood within `s` of `x` and if `fβ` and `f` are equal at `x`, then the derivative of `fβ` within `s` at `x` is equal to the derivative of `f` within `s` at `x`. In other words, under these conditions, the local derivative of two functions that are eventually equal and equal at a given point is also equal at that point.
More concisely: If `f` and `fβ` are two functions from a normed space `E` over a nontrivially normed field `π` to another normed space `F` over `π`, are equal at a point `x` in `E`, and are eventually equal in every neighborhood of `x` within a set `s` of `E`, then their derivatives at `x` are equal.
|
norm_fderiv_le_of_lipschitzOn
theorem norm_fderiv_le_of_lipschitzOn :
β (π : Type u_1) [inst : NontriviallyNormedField π] {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} {s : Set E}, s β nhds xβ β β {C : NNReal}, LipschitzOnWith C f s β βfderiv π f xββ β€ βC
This theorem states that if a function `f` is `C`-Lipschitz continuous on a neighborhood of a point `xβ` (meaning that the distance between the function values at any two points in the neighborhood does not exceed `C` times the distance between the points themselves), then the norm of the derivative of `f` at `xβ` is bounded by `C`. The derivative is calculated using `fderiv`, which returns the derivative if it exists and `0` otherwise. This theorem is a converse to the mean value inequality in the context of Lipschitz continuity.
More concisely: If a function `f` is `C`-Lipschitz continuous near a point `xβ`, then the norm of its derivative at `xβ` is bounded by `C`.
|
fderivWithin_of_isOpen
theorem fderivWithin_of_isOpen :
β {π : Type u_1} [inst : NontriviallyNormedField π] {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} {s : Set E}, IsOpen s β x β s β fderivWithin π f s x = fderiv π f x
The theorem `fderivWithin_of_isOpen` asserts that for any non-trivially normed field `π`, and any normed additive commutative group `E` and `F` over `π`, given a function `f` from `E` to `F`, element `x` in `E`, and a set `s` of elements of `E`, if the set `s` is open in the ambient topological space and `x` is an element of `s`, then the derivative of the function `f` within the set `s` at the point `x` is equivalent to the derivative of the function `f` at the point `x`.
More concisely: If `f` is a function from a normed additive commutative group `E` over a non-trivially normed field `π` to another such group `F`, `x` is an element of an open set `s` in `E`, and `f` is differentiable at `x`, then the derivative of `f` within `s` at `x` equals the derivative of `f` at `x`.
|
DifferentiableOn.mono
theorem DifferentiableOn.mono :
β {π : Type u_1} [inst : NontriviallyNormedField π] {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}
{s t : Set E}, DifferentiableOn π f t β s β t β DifferentiableOn π f s
The theorem `DifferentiableOn.mono` states that for any non-trivially normed field `π`, normed additive commutative group `E`, and normed additive commutative group `F`, if a function `f` from `E` to `F` is differentiable on a set `t` and `s` is a subset of `t`, then `f` is also differentiable on `s`. This means that the differentiability of a function within a set is preserved even if we restrict our attention to a smaller subset.
More concisely: If a function is differentiable on a set and that set is a subset of another, then the function is differentiable on the smaller set (in the context of non-trivially normed fields and normed additive commutative groups).
|
hasFDerivWithinAt_diff_singleton
theorem hasFDerivWithinAt_diff_singleton :
β {π : Type u_1} [inst : NontriviallyNormedField π] {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} {s : Set E} (y : E), HasFDerivWithinAt f f' (s \ {y}) x β HasFDerivWithinAt f f' s x
The theorem `hasFDerivWithinAt_diff_singleton` states that for any types `π` (which is a nontrivially normed field), `E` (a normed add-commutative group and normed space over `π`), and `F` (another normed add-commutative group and normed space over `π`), along with a function `f` from `E` to `F` and its derivative function `f'`, a point `x` in `E`, a set `s` of elements of type `E` and another point `y` in `E`, the function `f` has a Frechet derivative `f'` at point `x` within the set `s` excluding `{y}` if and only if `f` has a Frechet derivative `f'` at point `x` within the entire set `s`. In other words, the presence or absence of an individual point `y` in the set `s` does not affect whether `f` has a Frechet derivative at `x` within `s`.
More concisely: The presence or absence of a single point in a set does not affect the existence of a Frechet derivative of a function at a given point within that set. (Assuming the function, its derivative, the types involved are normed add-commutative groups and normed spaces over a nontrivially normed field.)
|
HasFDerivAtFilter.tendsto_nhds
theorem HasFDerivAtFilter.tendsto_nhds :
β {π : Type u_1} [inst : NontriviallyNormedField π] {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} {L : Filter E},
L β€ nhds x β HasFDerivAtFilter f f' x L β Filter.Tendsto f L (nhds (f x))
The theorem `HasFDerivAtFilter.tendsto_nhds` states that for any non-trivially normed field `π`, normed additive commutative groups `E` and `F`, and normed spaces over `E` and `F`. Given a function `f : E β F`, its Frechet derivative `f' : E βL[π] F` at a point `x : E` and a filter `L` on `E` that is less than or equal to the neighborhood filter at `x`, if `f` has its Frechet derivative `f'` at `x` with respect to filter `L`, then the function `f` tends to the neighborhood of `f(x)` along the filter `L`. In other words, the values of `f` get arbitrarily close to `f(x)` for all points in a set that becomes arbitrarily close to `x` (as defined by the filter `L`).
More concisely: Given a non-trivially normed field `π`, normed additive commutative groups `E` and `F`, a function `f : E β F`, its Frechet derivative `f' : E βL[π] F` at a point `x : E`, and a filter `L` on `E` with `L β€` neighborhood filter at `x`, if `f` has its Frechet derivative `f'` at `x` with respect to filter `L`, then `f` tends to `f(x)` along the filter `L`, i.e., for all `Ξ΅ > 0`, there exists a neighborhood `N` of `x` in `E` such that `x' β N β© L` implies `|f(x') - f(x)| < Ξ΅`.
|
HasFDerivAt.continuousAt
theorem HasFDerivAt.continuousAt :
β {π : Type u_1} [inst : NontriviallyNormedField π] {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}, HasFDerivAt f f' x β ContinuousAt f x
The theorem `HasFDerivAt.continuousAt` states that for any function `f` from a normed vector space `E` over a nontrivially normed field `π` to another normed vector space `F` over the same field `π`, if `f` has a derivative `f'` at a point `x in E`, then `f` is continuous at `x`. In other words, if `f` satisfies the condition that `f x'` approaches `f x + f' (x' - x) + o (x' - x)` as `x'` tends to `x`, then `f x` tends to `f xβ` when `x` tends to `xβ`, which is the definition of continuity at a point.
More concisely: If a function `f` from a normed vector space to another normed vector space has a derivative at a point, then it is continuous at that point.
|
HasFDerivWithinAt.mono_of_mem
theorem HasFDerivWithinAt.mono_of_mem :
β {π : Type u_1} [inst : NontriviallyNormedField π] {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} {s t : Set E},
HasFDerivWithinAt f f' t x β t β nhdsWithin x s β HasFDerivWithinAt f f' s x
This theorem, `HasFDerivWithinAt.mono_of_mem`, states that for any non-trivially normed field `π`, normed additively commutative groups `E` and `F` where `E` and `F` are both normed spaces over `π`, a function `f` from `E` to `F`, its derivative `f'` at a point `x` in `E`, and two sets of elements in `E`, `s` and `t`. If `f` has derivative `f'` within the set `t` at the point `x` and `t` is in the neighborhood within the set `s` of point `x` (meaning that `t` intersected with a neighborhood of `x` is a subset of `s`), then `f` also has the derivative `f'` within the set `s` at the point `x`. In other words, if `f` has a derivative at a point within a certain set, and this set is in the neighborhood of the point within a larger set, then `f` also has a derivative at that point within the larger set.
More concisely: If `f` has a derivative within set `t` at point `x` in normed spaces `E` and `F` over field `π`, and `t` is in the neighborhood of `x` within set `s`, then `f` has a derivative within set `s` at point `x`.
|
Differentiable.differentiableAt
theorem Differentiable.differentiableAt :
β {π : Type u_1} [inst : NontriviallyNormedField π] {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}, Differentiable π f β DifferentiableAt π f x
The theorem `Differentiable.differentiableAt` states that for any non-trivially normed field `π`, any normed additive commutative group `E` and `F`, any normed space over `π` for `E` and `F`, any function `f` from `E` to `F`, and any point `x` in `E`, if the function is differentiable everywhere (`Differentiable π f`), then it is also differentiable at the specific point `x` (`DifferentiableAt π f x`). In mathematical terms, this means that if a function `f` is differentiable over its entire domain, then it admits a derivative at any particular point in its domain.
More concisely: If a function is differentiable at every point in its domain over a non-trivially normed field, then it is differentiable at any specific point in its domain.
|
UniqueDiffWithinAt.eq
theorem UniqueDiffWithinAt.eq :
β {π : Type u_1} [inst : NontriviallyNormedField π] {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' fβ' : E βL[π] F} {x : E} {s : Set E},
UniqueDiffWithinAt π s x β HasFDerivWithinAt f f' s x β HasFDerivWithinAt f fβ' s x β f' = fβ'
This theorem, named `UniqueDiffWithinAt.eq`, asserts the uniqueness of derivatives within a given set. In more detail, given a nontrivial normed field `π`, and normed additive commutative groups `E` and `F` over `π`, along with the corresponding normed spaces. If a function `f` from `E` to `F` has two derivatives, `f'` and `fβ'`, at a point `x` within a set `s` such that `s` is uniquely differentiable at `x`, then `f'` and `fβ'` must be equal. This affirms the uniqueness of the derivative within the set at the point `x`.
More concisely: Given a nontrivial normed field `π`, normed additive commutative groups `E` and `F` over `π`, and a function `f : E β F` that is twice differentiable at `x β E` within a uniquely differentiable set `s β E`, then `f' (x) = fβ' (x)`.
|
differentiableOn_univ
theorem differentiableOn_univ :
β {π : Type u_1} [inst : NontriviallyNormedField π] {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},
DifferentiableOn π f Set.univ β Differentiable π f
The theorem `differentiableOn_univ` states that for any nontrivially normed field `π`, any normed add commutative group `E` and `F` in the normed space over `π`, and any function `f` mapping from `E` to `F`, the function `f` is differentiable on the universal set (i.e., the set of all points in `E`) if and only if the function `f` is differentiable at any point in `E`. Essentially, it connects the concepts of being differentiable over the entire space (`Differentiable π f`) and being differentiable at every point within a specific set (`DifferentiableOn π f Set.univ`), where the set is the set of all points (universal set).
More concisely: A function between two normed spaces is differentiable on the universal set if and only if it is differentiable at every point.
|
HasFDerivAt.fderiv
theorem HasFDerivAt.fderiv :
β {π : Type u_1} [inst : NontriviallyNormedField π] {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}, HasFDerivAt f f' x β fderiv π f x = f'
The theorem `HasFDerivAt.fderiv` states that for any nontrivially normed field `π`, normed additive commutative groups `E` and `F`, and normed vector spaces over `π` for `E` and `F`, given a function `f : E β F`, a continuous linear map `f' : E βL[π] F` and an element `x : E`, if `f` has `f'` as a derivative at `x` (in the sense that `f x'` approaches `f x + f' (x' - x)` as `x'` tends to `x`), then the FrΓ©chet derivative of `f` at `x` also equals `f'`. This means that if a function `f` has a derivative at a point, then it matches the FrΓ©chet derivative at that point.
More concisely: If a function `f : E -> F` between normed vector spaces over a nontrivially normed field, with continuous linear derivative `f'`, satisfies `f x' - f x -> 0` as `x' -> x`, then `f'` is the FrΓ©chet derivative of `f` at `x`.
|
DifferentiableOn.differentiableAt
theorem DifferentiableOn.differentiableAt :
β {π : Type u_1} [inst : NontriviallyNormedField π] {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} {s : Set E}, DifferentiableOn π f s β s β nhds x β DifferentiableAt π f x
This theorem states that for any non-trivially normed field 'π', normed additive commutative group 'E', 'F', a function 'f' from 'E' to 'F', a point 'x' in 'E', and a set 's' of 'E', if the function 'f' is differentiable on the set 's' and the set 's' is a neighborhood of the point 'x', then the function 'f' is differentiable at the point 'x'. In simpler terms, if a function is differentiable everywhere in a neighborhood around a point, then it is differentiable at that point.
More concisely: If a function is differentiable on a neighborhood of a point in a normed additive commutative group, then it is differentiable at that point.
|
HasFDerivWithinAt.mono
theorem HasFDerivWithinAt.mono :
β {π : Type u_1} [inst : NontriviallyNormedField π] {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} {s t : Set E}, HasFDerivWithinAt f f' t x β s β t β HasFDerivWithinAt f f' s x
This theorem, named `HasFDerivWithinAt.mono`, states that for any nontrivially normed field `π`, normed additive commutative groups `E` and `F`, and normed spaces over `π` of `E` and `F`, if a function `f` from `E` to `F` has a FrΓ©chet derivative `f'` at a point `x` within a set `t`, then `f` also has a FrΓ©chet derivative `f'` at the point `x` within any subset `s` of `t`. In mathematical terms, if $f$ has a FrΓ©chet derivative $f'$ at $x$ within a set $t$, then it also has this derivative at $x$ within any subset $s$ of $t$.
More concisely: If a function between normed spaces has a FrΓ©chet derivative at a point within a set, then it also has that derivative at the point within any smaller set.
|
differentiable_id
theorem differentiable_id :
β {π : Type u_1} [inst : NontriviallyNormedField π] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E], Differentiable π id
The theorem `differentiable_id` states that the identity function is differentiable at any point, for all non-trivially normed fields `π` and all normed additive commutative groups `E` which form a normed space over `π`. In other words, no matter what point you choose from `E`, you can calculate the derivative of the identity function at that point. This aligns with the intuitive understanding of the identity function's derivative, which is constantly equal to 1.
More concisely: The identity function is differentiable on any normed additive commutative group over any non-trivially normed field.
|
hasStrictFDerivAt_id
theorem hasStrictFDerivAt_id :
β {π : Type u_1} [inst : NontriviallyNormedField π] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] (x : E), HasStrictFDerivAt id (ContinuousLinearMap.id π E) x
This theorem states that, for any nontrivially normed field `π` and normed additive commutative group `E` that is a normed space over `π`, the identity function has a strict FrΓ©chet derivative at any point `x` in `E`. The derivative is given by the identity map itself as a continuous linear map. In other words, the rate of change of the identity function at any point is constant and equal to the identity map.
More concisely: The identity function on a normed space over a nontrivially normed field has the identity map as its strict FrΓ©chet derivative at every point.
|
fderivWithin_univ
theorem fderivWithin_univ :
β {π : Type u_1} [inst : NontriviallyNormedField π] {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},
fderivWithin π f Set.univ = fderiv π f
This theorem, `fderivWithin_univ`, states that for any type `π` with a non-trivial normed field structure, type `E` with a normed group and a normed space over `π` structure, and type `F` with the same structure as `E`, for any function `f` from `E` to `F`, the derivative of `f` within the universal set is identical to the derivative of `f`. This essentially establishes that taking the derivative of a function anywhere in the universal set is the same as taking the derivative without any set restriction.
More concisely: For any normed field `π`, normed groups and normed spaces `E` and `F` over `π`, and a function `f` from `E` to `F`, the derivative of `f` within the universal set equals the derivative of `f` without any set restriction.
|
HasFDerivAtFilter.isBigO_sub
theorem HasFDerivAtFilter.isBigO_sub :
β {π : Type u_1} [inst : NontriviallyNormedField π] {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} {L : Filter E},
HasFDerivAtFilter f f' x L β (fun x' => f x' - f x) =O[L] fun x' => x' - x
This theorem states that, given a nontrivially normed field `π`, a normed additive commutative group `E` as the domain and `F` as the codomain, a function `f : E β F`, its FrΓ©chet derivative `f' : E βL[π] F` at a point `x : E`, and a filter `L` on `E`, if the function `f` has a FrΓ©chet derivative `f'` at the point `x` with respect to the filter `L`, then the function `x' β¦ f(x') - f(x)` is a big O of the function `x' β¦ x' - x` with respect to the filter `L`. In simpler terms, the difference between the function values of `f` at points `x'` and `x` grows at most as fast as the difference between `x'` and `x` itself, in the limit as `x'` approaches `x` according to the filter `L`.
More concisely: Given a nontrivially normed field `π`, a normed additive commutative group `E`, a function `f : E β F` with FrΓ©chet derivative `f'` at a point `x β E`, and a filter `L` on `E`, if `f` is FrΓ©chet differentiable at `x` with respect to `L`, then the difference `f(x') - f(x)` is O(||x' - x||) as `x'` approaches `x` according to filter `L`.
|
HasFDerivAt.le_of_lip'
theorem HasFDerivAt.le_of_lip' :
β {π : Type u_1} [inst : NontriviallyNormedField π] {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},
HasFDerivAt f f' xβ β β {C : β}, 0 β€ C β (βαΆ (x : E) in nhds xβ, βf x - f xββ β€ C * βx - xββ) β βf'β β€ C
This theorem, named `HasFDerivAt.le_of_lip'`, states the converse to the mean value inequality. Specifically, given a function `f` that is differentiable at a point `xβ` and is `C`-Lipschitz within a neighborhood of `xβ`, the theorem asserts that the norm of the derivative of `f` at `xβ` is no greater than `C`. This version of the theorem only requires the condition that the norm of `f(x) - f(xβ)` is no more than `C` times the norm of `x - xβ` within a neighborhood of `xβ`. In mathematical notation, if `βf(x) - f(xβ)β β€ C * βx - xββ` holds within a neighborhood of `xβ`, then `βf'β β€ C`, where `f'` is the derivative of `f` at `xβ`.
More concisely: If a differentiable function `f` at `xβ` is `C`-Lipschitz in a neighborhood of `xβ`, then the norm of its derivative at `xβ` is bounded by `C`.
|
hasFDerivWithinAt_of_nmem_closure
theorem hasFDerivWithinAt_of_nmem_closure :
β {π : Type u_1} [inst : NontriviallyNormedField π] {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} {s : Set E}, x β closure s β HasFDerivWithinAt f f' s x
This theorem states that for any non-trivially normed field `π`, normed additive commutative group `E` and `F`, normed space `π E` and `π F`, a function `f` from `E` to `F`, its derivative `f'`, a point `x` in `E`, and a set `s` of `E`; if `x` is not an element of the closure of set `s`, then `f` has any derivative at the point `x` within the set `s`. The theorem asserts this because the statement would be empty under the condition that `x` is not in the closure of `s`.
More concisely: For any non-trivially normed field `π`, normed additive commutative groups `E` and `F`, normed spaces `π E` and `π F`, and a continuous function `f` from `E` to `F`, if `x` is not in the closure of the domain `s` of `f'`, then `f` has a derivative `f'(x)` within `s`.
|
HasStrictFDerivAt.exists_lipschitzOnWith
theorem HasStrictFDerivAt.exists_lipschitzOnWith :
β {π : Type u_1} [inst : NontriviallyNormedField π] {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}, HasStrictFDerivAt f f' x β β K, β s β nhds x, LipschitzOnWith K f s
This theorem states that if a function `f` is strictly differentiable at a point `x` with derivative `f'`, then `f` is Lipschitz continuous in a neighborhood of `x`. Here, the term Lipschitz continuous refers to the property that the distance between the images of any two points in the neighborhood under `f` is at most `K` times the distance between the two points themselves, for some non-negative real number `K`. The theorem further specifies that `K` and the neighborhood, which is a set around `x` in the domain of `f`, can be found in the neighborhood filter of `x`. This is captured by the existence of `K` and `s` such that `s` is in the neighborhood of `x` and `f` is Lipschitz on `s` with Lipschitz constant `K`.
More concisely: If a function `f` is strictly differentiable at a point `x`, then there exists a neighborhood `s` of `x` and a constant `K` such that |`f(y) - f(z)`| β€ `K` |`y - z`| for all `y` and `z` in `s`.
|
hasFDerivWithinAt_congr_set
theorem hasFDerivWithinAt_congr_set :
β {π : Type u_1} [inst : NontriviallyNormedField π] {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} {s t : Set E},
(nhds x).EventuallyEq s t β (HasFDerivWithinAt f f' s x β HasFDerivWithinAt f f' t x)
This theorem states that for any non-trivially normed field `π`, normed additive commutative groups `E` and `F`, and normed spaces over `π` corresponding to `E` and `F`, given a function `f` from `E` to `F`, its Frechet derivative `f'`, a point `x` in `E`, and two sets `s` and `t` in `E`, if `s` and `t` are eventually equal in the neighborhood of `x` (i.e., they are equal when restricted to some open set around `x`), then `f` has a Frechet derivative within `s` at `x` if and only if `f` has a Frechet derivative within `t` at `x`. In other words, the existence of the Frechet derivative of a function at a point within a set is invariant under changes to the set that only affect points outside a neighborhood of the point.
More concisely: Given a non-trivially normed field `π`, normed spaces `E` and `F` over `π`, a function `f` from `E` to `F`, and points `x` in `E` with sets `s` and `t` in `E` equivalent in a neighborhood of `x`, if `f` has a Frechet derivative at `x` in both `s` and `t`, then the Frechet derivatives are equal.
|
HasStrictFDerivAt.hasFDerivAt
theorem HasStrictFDerivAt.hasFDerivAt :
β {π : Type u_1} [inst : NontriviallyNormedField π] {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}, HasStrictFDerivAt f f' x β HasFDerivAt f f' x
The theorem `HasStrictFDerivAt.hasFDerivAt` states that for any field `π` with a non-trivial norm structure, and for any normed additive commutative groups `E` and `F` that also have a normed space structure over `π`, if a function `f : E β F` has a strict FrΓ©chet derivative `f' : E βL[π] F` at a point `x : E` (that is, the change in `f` at `x` is exactly described by `f'`), then `f` also has (the possibly weaker notion of) a FrΓ©chet derivative `f'` at `x` (that is, the change in `f` at `x` can be approximated by `f'` plus a term that vanishes faster than the difference `x' - x` as `x'` tends to `x`).
More concisely: If a function `f : E β F` between normed additive commutative groups endowed with a normed space structure over a field `π` with a non-trivial norm structure has a strict FrΓ©chet derivative `f' : E βL[π] F` at a point `x : E`, then `f` has a FrΓ©chet derivative `f'` at `x`.
|
HasFDerivAt.differentiableAt
theorem HasFDerivAt.differentiableAt :
β {π : Type u_1} [inst : NontriviallyNormedField π] {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}, HasFDerivAt f f' x β DifferentiableAt π f x
The theorem `HasFDerivAt.differentiableAt` states that for any non-trivially normed field `π`, if a function `f` from a normed additive commutative group `E` to another such group `F` (both of which are normed over `π`) has a continuous linear map `f'` as its derivative at a point `x` in `E`, then the function `f` is differentiable at the point `x`. In other words, if `f` satisfies the condition `f x' = f x + f' (x' - x) + o (x' - x)` as `x'` tends to `x`, then `f` is differentiable at `x`.
More concisely: If a function between two normed additive commutative groups over a non-trivially normed field has a continuous linear derivative at a point, then the function is differentiable at that point.
|
DifferentiableWithinAt.differentiableAt
theorem DifferentiableWithinAt.differentiableAt :
β {π : Type u_1} [inst : NontriviallyNormedField π] {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} {s : Set E}, DifferentiableWithinAt π f s x β s β nhds x β DifferentiableAt π f x
The theorem `DifferentiableWithinAt.differentiableAt` states that for any nontrivially normed field `π`, normed additive commutative groups `E` and `F` also being normed spaces over `π`, a function `f` from `E` to `F`, a point `x` in `E`, and a set `s` of elements from `E`, if `f` is differentiable at the point `x` within the set `s` (`DifferentiableWithinAt π f s x`), and if the set `s` is a neighborhood of the point `x` (`s β nhds x`), then the function `f` is differentiable at the point `x` (`DifferentiableAt π f x`). In other words, if a function is differentiable at a point within a local neighborhood, and the neighborhood is "close" to the point, then the function is also differentiable at the point itself.
More concisely: If a function is differentiable within a neighborhood of a point in a normed space, then the function is differentiable at that point.
|
Mathlib.Analysis.Calculus.FDeriv.Basic._auxLemma.18
theorem Mathlib.Analysis.Calculus.FDeriv.Basic._auxLemma.18 :
β {π : Type u_1} [inst : NontriviallyNormedField π] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] {x : E}
(c : F), DifferentiableAt π (fun x => c) x = True
This theorem states that for any non-trivially normed field `π`, normed add commutative group `E`, normed space of `E` over `π`, normed add commutative group `F`, normed space of `F` over `π`, and any element `x` of `E`, and any element `c` of `F`, the function that maps every element `x` of `E` to `c` of `F` is always differentiable at `x`. In other words, constant functions are always differentiable, regardless of the point at which their derivative is evaluated.
More concisely: For any non-trivially normed fields `π`, and normed spaces `E` over `π` and `F`, the constant function from `E` to `F` is differentiable.
|
fderivWithin_zero_of_not_differentiableWithinAt
theorem fderivWithin_zero_of_not_differentiableWithinAt :
β {π : Type u_1} [inst : NontriviallyNormedField π] {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} {s : Set E}, Β¬DifferentiableWithinAt π f s x β fderivWithin π f s x = 0
This theorem states that if a function `f` is not differentiable at a point `x` within a set `s`, then the derivative of `f` within `s` at `x` is zero. Here, `π` is a normed field, `E` and `F` are normed spaces over `π`, and `f` is a function from `E` to `F`. Essentially, if we can't find a derivative for `f` at a certain point within a specific set, we assign the derivative at that point to be zero for convenience and mathematical consistency.
More concisely: If a function `f` : `E` β `F` is not differentiable at a point `x` in a set `s` in the normed fields `π` and `E`, then the derivative of `f` at `x` within `s` is the zero map from `E` to `F`.
|
hasStrictFDerivAt_const
theorem hasStrictFDerivAt_const :
β {π : Type u_1} [inst : NontriviallyNormedField π] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] (c : F)
(x : E), HasStrictFDerivAt (fun x => c) 0 x
This theorem states that for any non-trivially normed field π, normed additive commutative groups E and F, and normed spaces π of E and F, a constant function (represented by a constant c of type F) has a strict Frechet derivative of 0 at any point x in E. In simple terms, it's saying that the rate of change (or derivative) of a constant function is always 0, which aligns with our intuitive understanding of derivatives in calculus.
More concisely: For any normed field π, normed additive commutative groups E, and normed spaces π[E] and π[F], the constant function from E to F has a strict Frechet derivative equal to 0 at every point in E.
|
norm_fderiv_le_of_lipschitz
theorem norm_fderiv_le_of_lipschitz :
β (π : Type u_1) [inst : NontriviallyNormedField π] {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} {C : NNReal}, LipschitzWith C f β βfderiv π f xββ β€ βC
This theorem states the converse to the mean value inequality in the context of Lipschitz continuity and derivatives. Specifically, it says that if a function `f` from a normed space `E` to another normed space `F` over a non-trivially normed field `π` is `C`-Lipschitz continuous, meaning that the distance between its image points is at most `C` times the distance between the corresponding domain points, then the norm of its derivative at a particular point `xβ` in `E` is bounded by `C`. The version of the derivative used here is `fderiv`, which gives a derivative if it exists, otherwise it gives `0`.
More concisely: If a Lipschitz continuous function `f` from a normed space `E` to another normed space `F` over a non-trivially normed field `π` has a derivative `f'` at `xβ` in `E`, then `βf'(xβ)β β€ C`, where `C` is the Lipschitz constant of `f`.
|
HasFDerivWithinAt.differentiableWithinAt
theorem HasFDerivWithinAt.differentiableWithinAt :
β {π : Type u_1} [inst : NontriviallyNormedField π] {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} {s : Set E}, HasFDerivWithinAt f f' s x β DifferentiableWithinAt π f s x
The theorem `HasFDerivWithinAt.differentiableWithinAt` states that for any non-trivially normed field `π` and normed additive commutative groups `E` and `F` that are also normed spaces over `π`, if a function `f` from `E` to `F` has a Frechet derivative `f'` at a point `x` within a set `s` of `E` (denoted by `HasFDerivWithinAt f f' s x`), then `f` is differentiable at the point `x` within the set `s` (denoted by `DifferentiableWithinAt π f s x`). This theorem is a fundamental result in differential calculus that connects the existence of a derivative to the property of differentiability.
More concisely: If a function between normed spaces has a Frechet derivative at a point within a set, then the function is differentiable at that point within the set.
|
DifferentiableOn.continuousOn
theorem DifferentiableOn.continuousOn :
β {π : Type u_1} [inst : NontriviallyNormedField π] {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}
{s : Set E}, DifferentiableOn π f s β ContinuousOn f s
The theorem `DifferentiableOn.continuousOn` states that, given a nontrivially normed field `π`, a normed addition commutative group `E` and `F` (which are also normed spaces over `π`), a function `f` from `E` to `F`, and a set `s` of elements of `E`, if the function `f` is differentiable at any point within the set `s`, then `f` is also continuous at every point within `s`. In other words, differentiability of a function on a set implies its continuity on the same set.
More concisely: If a function between two normed spaces is differentiable at any point in a set, then it is continuous at every point in that set.
|
differentiableAt_id
theorem differentiableAt_id :
β {π : Type u_1} [inst : NontriviallyNormedField π] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {x : E}, DifferentiableAt π id x
The theorem `differentiableAt_id` states that for all types `π` and `E`, where `π` is a nontrivial normed field and `E` is a normed vector space over `π`, the identity function `id` is differentiable at every point `x` in `E`. This means that at any given point, the identity function has a derivative.
More concisely: For every normed field `π` and normed vector space `E` over `π`, the identity function on `E` is differentiable at every point in `E`.
|
hasFDerivAtFilter_const
theorem hasFDerivAtFilter_const :
β {π : Type u_1} [inst : NontriviallyNormedField π] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] (c : F)
(x : E) (L : Filter E), HasFDerivAtFilter (fun x => c) 0 x L
This theorem states that for any nontrivial normed field `π`, normed add-commutative group `E`, normed space over `π` and `E`, normed add-commutative group `F`, normed space over `π` and `F`, a constant `c` from `F`, a point `x` from `E`, and a filter `L` on `E`, the function that maps any input to `c` has a derivative of zero at point `x` with respect to the filter `L`. In more mathematically precise terms, the constant function `f(x) = c` has a Frechet derivative of 0 at any point `x` in its domain, under any given filter on the domain.
More concisely: For any nontrivial normed field `π`, normed add-commutative groups `E` and `F`, normed space `E` over `π` and `F`, constant `c` in `F`, point `x` in `E`, and filter `L` on `E`, the constant function `f(x) = c` has a Frechet derivative of 0 at `x` with respect to `L`.
|
HasStrictFDerivAt.exists_lipschitzOnWith_of_nnnorm_lt
theorem HasStrictFDerivAt.exists_lipschitzOnWith_of_nnnorm_lt :
β {π : Type u_1} [inst : NontriviallyNormedField π] {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},
HasStrictFDerivAt f f' x β β (K : NNReal), βf'ββ < K β β s β nhds x, LipschitzOnWith K f s
The theorem states that if a function `f` is strictly differentiable at a point `x` with derivative `f'`, and there exists a nonnegative real number `K` such that `K` is greater than the norm of `f'`, then `f` is `K`-Lipschitz continuous in a neighborhood of `x`. Here, Lipschitz continuity means that the distance between the outputs of `f` for any two points in the neighborhood is at most `K` times the distance between the points themselves. A neighborhood of `x` is a set that contains an open set around `x`.
More concisely: If a function `f` is strictly differentiable at `x` with Lipschitz constant `K` for its derivative, then `f` is `K`-Lipschitz continuous in a neighborhood of `x`.
|
HasFDerivWithinAt.unique_on
theorem HasFDerivWithinAt.unique_on :
β {π : Type u_1} [inst : NontriviallyNormedField π] {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' fβ' : E βL[π] F} {x : E} {s : Set E},
HasFDerivWithinAt f f' s x β HasFDerivWithinAt f fβ' s x β Set.EqOn (βf') (βfβ') (tangentConeAt π s x)
This theorem states that if `f'` and `fβ'` are two derivatives of a function `f` within a set `s` at a point `x`, then `f'` and `fβ'` are equal on the tangent cone to `s` at `x`. Here, `π` is a nontrivially normed field, `E` and `F` are normed additive commutative groups over which `π` is a normed space, and `f : E β F` is our function. The derivatives `f'` and `fβ'` are continuous linear maps from `E` to `F`. The tangent cone is a set of all possible tangent directions to `s` at `x`. The theorem essentially tells us about the uniqueness of the derivative within the tangent cone.
More concisely: If `f : E β F` is a function with continuous linear derivatives `f'` and `fβ'` at a point `x` in the normed additive commutative group `E` over the nontrivially normed field `π`, then `f'` and `fβ'` are equal on the tangent cone to the domain of `f` at `x`.
|
hasFDerivAtFilter_iff_tendsto
theorem hasFDerivAtFilter_iff_tendsto :
β {π : Type u_1} [inst : NontriviallyNormedField π] {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} {L : Filter E},
HasFDerivAtFilter f f' x L β Filter.Tendsto (fun x' => βx' - xββ»ΒΉ * βf x' - f x - f' (x' - x)β) L (nhds 0)
The theorem `hasFDerivAtFilter_iff_tendsto` states that for any nontrivially normed field `π`, normed additive commutative groups `E` and `F`, and a function `f` mapping `E` to `F`, a derivative `f'` of `f` at a point `x` in the domain `E` exists with respect to a filter `L` if and only if the function, which maps `x'` to the norm of the difference between `x'` and `x` divided by the norm of the difference between `f` at `x'` and `f` at `x` minus `f'` applied to the difference between `x'` and `x`, tends to the neighborhood of zero under the filter `L`. Here, the term "neighborhood of zero" is defined in the context of topological spaces, and `HasFDerivAtFilter` represents the existence of a derivative at a point with respect to a filter.
More concisely: A function between two normed additive commutative groups has a derivative at a point with respect to a filter if and only if the function value of the difference quotient, evaluated at points close to that point according to the filter, tends to zero.
|
hasFDerivAtFilter_id
theorem hasFDerivAtFilter_id :
β {π : Type u_1} [inst : NontriviallyNormedField π] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] (x : E) (L : Filter E), HasFDerivAtFilter id (ContinuousLinearMap.id π E) x L
The theorem `hasFDerivAtFilter_id` asserts that for any nontrivially normed field `π`, normed add commutative group `E`, a vector `x` in `E`, and a filter `L` on `E`, the identity function has its FrΓ©chet derivative at `x` with respect to the filter `L` and the derivative is given by the continuous linear map `ContinuousLinearMap.id π E`. This means that the rate of change of the identity function at `x` in the `L`-direction is precisely the identity map on the space `E`.
More concisely: For any nontrivially normed field π, normed add commutative group E, vector x in E, and filter L on E, the identity function on E has its Frechet derivative at x with respect to the filter L equal to the identity map ContinuousLinearMap.id π E.
|
differentiableWithinAt_univ
theorem differentiableWithinAt_univ :
β {π : Type u_1} [inst : NontriviallyNormedField π] {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}, DifferentiableWithinAt π f Set.univ x β DifferentiableAt π f x
The theorem `differentiableWithinAt_univ` states that for any nontrivially normed field `π`, any normed additive commutative groups `E` and `F` which are also normed spaces over `π`, any function `f` from `E` to `F`, and any point `x` in `E`, the function `f` is differentiable at the point `x` within the universal set (which includes all elements of `E`) if and only if `f` is differentiable at the point `x`. Basically, being differentiable everywhere is equivalent to being differentiable at a particular point.
More concisely: For any nontrivially normed field `π`, and normed additive commutative groups `E` and `F` over `π` as normed spaces, a function `f` from `E` to `F` is differentiable at every point `x` in `E` if and only if it is differentiable at `x`.
|
Filter.EventuallyEq.hasFDerivAtFilter_iff
theorem Filter.EventuallyEq.hasFDerivAtFilter_iff :
β {π : Type u_1} [inst : NontriviallyNormedField π] {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β fβ : E β F} {fβ' fβ' : E βL[π] F} {x : E} {L : Filter E},
L.EventuallyEq fβ fβ β
fβ x = fβ x β (β (x : E), fβ' x = fβ' x) β (HasFDerivAtFilter fβ fβ' x L β HasFDerivAtFilter fβ fβ' x L)
This theorem states that for a given non-trivially normed field 'π', normed add commutative group 'E', normed space 'E' over 'π', normed add commutative group 'F', normed space 'F' over 'π', functions 'fβ' and 'fβ' from 'E' to 'F', linear maps 'fβ'' and 'fβ'' from 'E' to 'F', element 'x' of 'E', and filter 'L' on 'E', if 'fβ' and 'fβ' are eventually equal with respect to the filter 'L', 'fβ' at 'x' is equal to 'fβ' at 'x', and 'fβ'' is identical to 'fβ'' at all points, then the fact that 'fβ' is Frechet differentiable at 'x' with respect to the filter 'L' using 'fβ'' as the derivative is equivalent to 'fβ' being Frechet differentiable at 'x' with respect to the filter 'L' using 'fβ'' as the derivative. This theorem establishes a kind of continuity of differentiation under changes of the underlying function that preserve the function's value at a point and its derivative.
More concisely: If functions $f\_0$ and $f\_1$ from a normed space $E$ to another normed space $F$ over a non-trivially normed field, with linear derivatives $f\_0''$ and $f\_1''$, are eventually equal with respect to a filter $L$ and have the same value and derivative at a point $x$ in $E$, then $f\_0$ is Frechet differentiable at $x$ with respect to $L$ using $f\_0''$ if and only if $f\_1$ is Frechet differentiable at $x$ with respect to $L$ using $f\_1''$.
|
differentiableAt_const
theorem differentiableAt_const :
β {π : Type u_1} [inst : NontriviallyNormedField π] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] {x : E}
(c : F), DifferentiableAt π (fun x => c) x
The theorem `differentiableAt_const` states that for every non-trivially normed field `π`, normed additive commutative group `E` and `F` which are also normed spaces over `π`, and any point `x` in `E` and a constant `c` in `F`, the constant function that assigns `c` to each `x` is differentiable at `x`. In mathematical terms, this means that constant functions are always differentiable.
More concisely: For any non-trivially normed field `π`, normed additive commutative groups `E` and `F` over `π`, and constant `c` in `F`, the constant function `fc : E β F` defined by `fc x := c` is differentiable at every point `x` in `E`.
|
DifferentiableAt.fderivWithin
theorem DifferentiableAt.fderivWithin :
β {π : Type u_1} [inst : NontriviallyNormedField π] {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} {s : Set E}, DifferentiableAt π f x β UniqueDiffWithinAt π s x β fderivWithin π f s x = fderiv π f x
The theorem `DifferentiableAt.fderivWithin` states that for any nontrivially normed field `π`, any normed vector spaces `E` and `F` over `π`, any function `f` from `E` to `F`, any point `x` in `E`, and any set `s` of elements in `E`, if the function `f` is differentiable at point `x` and the tangent space to `s` at `x` is unique (`UniqueDiffWithinAt π s x`), then the derivative of `f` at `x` within `s` (`fderivWithin π f s x`) equals the derivative of `f` at `x` (`fderiv π f x`). In mathematical terms, this theorem states that if a function's derivative exists at a point and the tangent space at that point is unique, then the derivative within a subset is the same as the derivative over the entire space.
More concisely: If a function is differentiable at a point x in a normed vector space, and the tangent space to any set s at x is unique, then the derivative of the function within s at x equals the derivative of the function at x.
|
DifferentiableOn.hasFDerivAt
theorem DifferentiableOn.hasFDerivAt :
β {π : Type u_1} [inst : NontriviallyNormedField π] {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} {s : Set E}, DifferentiableOn π f s β s β nhds x β HasFDerivAt f (fderiv π f x) x
The theorem `DifferentiableOn.hasFDerivAt` states that for any scalar field `π` with a non-trivially normed field structure, and any normed additive commutative groups `E` and `F` with normed space structures over `π`, if a function `f` from `E` to `F` is differentiable on a set `s` and the set `s` is a neighborhood of a point `x` in `E`, then `f` has the continuous linear map `fderiv π f x` as its derivative at `x`. In other words, if the function is differentiable at every point in some neighborhood of `x`, then the derivative of `f` at `x` exists and is given by `fderiv π f x`.
More concisely: If a differentiable function between normed spaces is defined on a neighborhood of a point, then it has a continuous linear derivative at that point.
|
HasStrictFDerivAt.congr_of_eventuallyEq
theorem HasStrictFDerivAt.congr_of_eventuallyEq :
β {π : Type u_1} [inst : NontriviallyNormedField π] {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 fβ : E β F} {f' : E βL[π] F} {x : E},
HasStrictFDerivAt f f' x β (nhds x).EventuallyEq f fβ β HasStrictFDerivAt fβ f' x
This theorem states that if a function `f` has a strict Frechet derivative `f'` at a point `x` in a nontrivial normed field, then if `f` equals another function `fβ` in a neighborhood of `x`, `fβ` also has a strict Frechet derivative `f'` at `x`. Here, both `f` and `fβ` are functions from a normed additive commutative group `E` to another such group `F`, and the topology on `E` and `F` is defined by a norm. This neighborhood is defined in the context of a topological space, and the Frechet derivative is a linear map from `E` to `F`.
More concisely: If `f` and `fβ` are functions from a normed additive commutative group `E` to another such group `F`, with `f` having a strict Frechet derivative `f'` at `x` in `E`, and `f` equals `fβ` in a neighborhood of `x`, then `fβ` also has a strict Frechet derivative `f'` at `x`.
|
HasFDerivAtFilter.mono
theorem HasFDerivAtFilter.mono :
β {π : Type u_1} [inst : NontriviallyNormedField π] {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} {Lβ Lβ : Filter E},
HasFDerivAtFilter f f' x Lβ β Lβ β€ Lβ β HasFDerivAtFilter f f' x Lβ
This theorem, `HasFDerivAtFilter.mono`, is stating a property about the derivative of a function `f` at a point `x` with respect to filters `Lβ` and `Lβ`. Specifically, it says that if a function `f` has a derivative `f'` at a point `x` with respect to a filter `Lβ`, and `Lβ` is a subset of (or equal to) `Lβ`, then `f` also has a derivative `f'` at `x` with respect to `Lβ`. Here, `π`, `E`, and `F` are types representing normed fields and normed vector spaces respectively, and `βL[π]` represents bounded linear maps from E to F over the field `π`.
More concisely: If a function `f` has a derivative `f'` at point `x` with respect to filter `Lβ`, and `Lβ` is a subset of `Lβ`, then `f` has a derivative `f'` at `x` with respect to filter `Lβ`.
|
fderiv_zero_of_not_differentiableAt
theorem fderiv_zero_of_not_differentiableAt :
β {π : Type u_1} [inst : NontriviallyNormedField π] {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}, Β¬DifferentiableAt π f x β fderiv π f x = 0
This theorem states that for any non-trivially normed field `π`, a normed add commutative group `E`, a normed space over `π` and `E`, a normed add commutative group `F`, and a normed space over `π` and `F`, if a function `f` from `E` to `F` is not differentiable at a point `x` in `E`, then the Frechet derivative (`fderiv`) of the function `f` at point `x` is zero.
More concisely: If a function between two normed spaces is not differentiable at a point, then its Frechet derivative at that point is the zero mapping.
|
differentiableWithinAt_id
theorem differentiableWithinAt_id :
β {π : Type u_1} [inst : NontriviallyNormedField π] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {x : E} {s : Set E}, DifferentiableWithinAt π id s x
The theorem `differentiableWithinAt_id` states that, for every type `π` that forms a nontrivially normed field, and any type `E` that has the structure of a normed additive commutative group and is a normed space over `π`, the identity function `id` is differentiable at any point `x` within any set `s` of `E`. In mathematical terms, this means that the identity function is differentiable everywhere, i.e., its derivative exists at every point in its domain.
More concisely: For every nontrivially normed field `π` and normed additive commutative group `E` that is a normed space over `π`, the identity function `id` is differentiable at every point `x` in `E`.
|
DifferentiableOn.congr
theorem DifferentiableOn.congr :
β {π : Type u_1} [inst : NontriviallyNormedField π] {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 fβ : E β F} {s : Set E}, DifferentiableOn π f s β (β x β s, fβ x = f x) β DifferentiableOn π fβ s
The theorem `DifferentiableOn.congr` states that for any nontrivially normed field `π`, and any normed additive commutative groups `E` and `F` with `E` and `F` being vector spaces over `π`, if a function `f` is differentiable on a set `s` of elements from `E` to `F`, and there is another function `fβ` which equals `f` for all points `x` in the set `s`, then `fβ` is also differentiable on the set `s`. This theorem essentially shows that the differentiability of a function on a set is not affected if we replace the function with another function that agrees with it on that set.
More concisely: If `f` is differentiable on a set `s` in the vector spaces `E` and `F` over a nontrivially normed field `π`, and `fβ` equals `f` on `s`, then `fβ` is differentiable on `s`.
|
DifferentiableWithinAt.hasFDerivWithinAt
theorem DifferentiableWithinAt.hasFDerivWithinAt :
β {π : Type u_1} [inst : NontriviallyNormedField π] {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} {s : Set E}, DifferentiableWithinAt π f s x β HasFDerivWithinAt f (fderivWithin π f s x) s x
This theorem states that for a given non-trivially normed field 'π', normed addition-commutative groups 'E' and 'F', and a normed space over 'π' for 'E' and 'F', if a function 'f' from 'E' to 'F' is differentiable at a point 'x' within a set 's', then the derivative of 'f' at 'x' within 's' exists, and is equal to the value given by the function 'fderivWithin' at 'x'. In more mathematical terms, if `f` is differentiable at `x` within `s` (which is represented by `DifferentiableWithinAt π f s x`), then `f` has a derivative at `x` within `s` (which is represented by `HasFDerivWithinAt f (fderivWithin π f s x) s x`).
More concisely: If a function between two normed spaces over a non-trivially normed field is differentiable at a point within a set, then it has a derivative with the same value as the derivative function evaluated at that point within that set.
|
HasFDerivAt.hasFDerivWithinAt
theorem HasFDerivAt.hasFDerivWithinAt :
β {π : Type u_1} [inst : NontriviallyNormedField π] {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} {s : Set E}, HasFDerivAt f f' x β HasFDerivWithinAt f f' s x
The theorem `HasFDerivAt.hasFDerivWithinAt` states that if a function `f` of type `E β F` has a continuous linear map `f'` as its derivative at a certain point `x`, then `f` also has `f'` as its derivative within any set `s` of elements of type `E` at the same point `x`. This applies in the context where `π` is a nontrivially normed field, `E` is a normed additive commutative group over `π`, and `F` is also a normed additive commutative group over `π`. The derivatives are defined in the sense of FrΓ©chet derivatives. This theorem is essentially asserting that if a derivative exists at a point, it remains the same regardless of the context or 'set' you consider around that point.
More concisely: If a FrΓ©chet derivative exists for a function between normed additive commutative groups over a nontrivially normed field at a point, then it is the derivative within any neighborhood of that point.
|
HasFDerivWithinAt.fderivWithin
theorem HasFDerivWithinAt.fderivWithin :
β {π : Type u_1} [inst : NontriviallyNormedField π] {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} {s : Set E},
HasFDerivWithinAt f f' s x β UniqueDiffWithinAt π s x β fderivWithin π f s x = f'
This theorem, named `HasFDerivWithinAt.fderivWithin`, states that for every nontrivially normed field `π`, normed additive commutative groups `E` and `F` (where `E` and `F` are also normed spaces over `π`), a function `f` from `E` to `F`, a continuous linear map `f'` from `E` to `F`, a point `x` in `E`, and a set `s` of elements from `E`; if the function `f` has a derivative `f'` within the set `s` at the point `x`, and the set `s` has unique tangent vectors at `x` (indicated by `UniqueDiffWithinAt π s x`), then the Frechet derivative of `f` within the set `s` at `x` (given by `fderivWithin π f s x`) equals `f'`. This theorem provides a connection between having a derivative at a point within a set and the Frechet derivative at that point within the set.
More concisely: If a function between normed spaces has a unique derivative within a set at a point and the set has the property of unique tangent vectors at that point, then the Frechet derivative of the function within the set at that point equals the derivative at that point.
|
HasFDerivWithinAt.lim
theorem HasFDerivWithinAt.lim :
β {π : Type u_1} [inst : NontriviallyNormedField π] {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} {s : Set E},
HasFDerivWithinAt f f' s x β
β {Ξ± : Type u_6} (l : Filter Ξ±) {c : Ξ± β π} {d : Ξ± β E} {v : E},
(βαΆ (n : Ξ±) in l, x + d n β s) β
Filter.Tendsto (fun n => βc nβ) l Filter.atTop β
Filter.Tendsto (fun n => c n β’ d n) l (nhds v) β
Filter.Tendsto (fun n => c n β’ (f (x + d n) - f x)) l (nhds (f' v))
This theorem, `HasFDerivWithinAt.lim`, asserts that for a function `f` that has a derivative `f'` at a point `x` within a set `s`, if a sequence of rescaled versions of `f` around `x` is such that the scaling factors `c n` tend to infinity and `c n * d n` converges to a vector `v`, then the sequence of `c n * (f (x + d n) - f x)` will converge to `f' v`. More specifically, given a filter `l`, if for almost every `n` in `l`, `x + d n` belongs to `s`, and `c n` tends to infinity along `l`, and `c n * d n` tends to `v` along `l`, then `c n * (f (x + d n) - f x)` will tend to `f' v` along `l`. This is a generalization of the standard fact that a function's derivative at a point is equal to the limit of the difference quotients of the function at that point.
More concisely: Given a function `f` with derivative `f'` at a point `x` within a set `s`, if for a sequence `{d n}` and scalars `{c n}` converging to a vector `v` with `c n tending to infinity`, `x + d n` is in `s` for almost all `n`, then `c n * (f (x + d n) - f x)` converges to `f' v`.
|