HasDerivWithinAt.Ioi_of_Ici
theorem HasDerivWithinAt.Ioi_of_Ici :
β {π : Type u} [inst : NontriviallyNormedField π] {F : Type v} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace π F] {f : π β F} {f' : F} {x : π} [inst_3 : PartialOrder π],
HasDerivWithinAt f f' (Set.Ici x) x β HasDerivWithinAt f f' (Set.Ioi x) x
This theorem states that if a function `f` has a derivative `f'` at a point `x` within a left-closed, right-infinite interval `Set.Ici x` (that is, the set of all values greater than or equal to `x`), then `f` also has the same derivative `f'` at `x` within a left-open, right-infinite interval `Set.Ioi x` (that is, the set of all values strictly greater than `x`). Here, both `f` and `f'` are functions from a nontrivially normed field `π` to a normed additive commutative group `F`, and `π` is also a partial order.
More concisely: If a function `f` with derivative `f'` at a point `x` in a nontrivially normed field `π` has the property that `f'` exists in the left-closed, right-infinite interval `Set.Ici x` of `π`, then `f'` also exists and is equal to `f'` in the left-open, right-infinite interval `Set.Ioi x`.
|
hasDerivWithinAt_iff_hasFDerivWithinAt
theorem hasDerivWithinAt_iff_hasFDerivWithinAt :
β {π : Type u} [inst : NontriviallyNormedField π] {F : Type v} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace π F] {f : π β F} {x : π} {s : Set π} {f' : F},
HasDerivWithinAt f f' s x β HasFDerivWithinAt f (ContinuousLinearMap.smulRight 1 f') s x
This theorem states that for any nontrivially normed field `π`, normed add commutative group `F`, normed space over `π` and `F`, function `f` from `π` to `F`, point `x` in `π`, subset `s` of `π`, and a derivative `f'` of type `F`, the function `f` has the derivative `f'` at the point `x` within the subset `s` if and only if `f` has the FrΓ©chet derivative `ContinuousLinearMap.smulRight 1 f'` at `x` within `s`. In other words, the concept of having a derivative within a set in the traditional sense is equivalent to having a FrΓ©chet derivative in the same context.
More concisely: For any nontrivially normed field `π`, normed add commutative group `F`, normed space over `π` and `F`, and function `f` from `π` to `F`, the derivative `f'` of `f` at a point `x` in a subset `s` of `π` is equal to the FrΓ©chet derivative of `f` at `x` within `s` if and only if `f` has the derivative `f'` at `x` within `s`.
|
deriv_zero_of_not_differentiableAt
theorem deriv_zero_of_not_differentiableAt :
β {π : Type u} [inst : NontriviallyNormedField π] {F : Type v} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace π F] {f : π β F} {x : π}, Β¬DifferentiableAt π f x β deriv f x = 0
The theorem `deriv_zero_of_not_differentiableAt` states that for any point `x` in the domain of a function `f` from the field `π` to a normed additively commutative group `F`, if `f` is not differentiable at `x`, then the derivative of `f` at `x` is zero. In other words, for all `f : π β F` and `x : π`, if `f` does not admit a derivative at `x`, then the value of the derivative function `deriv f` at `x` equals zero.
More concisely: If a function `f` from a field to a normed additively commutative group is not differentiable at a point `x`, then its derivative at `x` is zero.
|
HasDerivAt.continuousOn
theorem HasDerivAt.continuousOn :
β {π : Type u} [inst : NontriviallyNormedField π] {F : Type v} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace π F] {s : Set π} {f f' : π β F}, (β x β s, HasDerivAt f (f' x) x) β ContinuousOn f s
This theorem states that for any type π which is a nontrivially normed field, and any type F which is a normed additive commutative group and a normed space over π, if a function f from π to F has a derivative at every point x in a set s, then the function f is continuous on the set s. In mathematical terms, if β x β s, f has derivative f'(x) at x, then f is continuous on s.
More concisely: If a function between a nontrivially normed field and a normed additive commutative group, which is also a normed space over the field, has a derivative at every point in a set, then the function is continuous on that set.
|
HasDerivWithinAt.mono_of_mem
theorem HasDerivWithinAt.mono_of_mem :
β {π : Type u} [inst : NontriviallyNormedField π] {F : Type v} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace π F] {f : π β F} {f' : F} {x : π} {s t : Set π},
HasDerivWithinAt f f' t x β t β nhdsWithin x s β HasDerivWithinAt f f' s x
The theorem `HasDerivWithinAt.mono_of_mem` states that if a function `f` has a derivative `f'` at a point `x` within a subset `t` of the domain, and the subset `t` is contained in the intersection of `s` and a neighborhood of `x`, then `f` also has the derivative `f'` at the point `x` within the subset `s`. Here `π` is a field with a norm that is not trivial, `F` is a normed additively commutative group, and `F` is a normed space over `π`.
More concisely: If a function `f` has a derivative `f'` at `x` in subset `t` of the normed space `F` over field `β` with a non-trivial norm, and `t` is contained in the intersection of `s` and a neighborhood of `x`, then `f` has derivative `f'` at `x` in subset `s`.
|
deriv_eqOn
theorem deriv_eqOn :
β {π : Type u} [inst : NontriviallyNormedField π] {F : Type v} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace π F] {f : π β F} {s : Set π} {f' : π β F},
IsOpen s β (β x β s, HasDerivWithinAt f (f' x) s x) β Set.EqOn (deriv f) f' s
The theorem `deriv_eqOn` states that for any nontrivially normed field `π`, normed additively commutative group `F`, and normed space over `π` with `F`, given a function `f` from `π` to `F`, a set `s` of `π`, and another function `f'` from `π` to `F`, if the set `s` is open in the topological space on `π` and for every element `x` in `s`, the function `f` has a derivative within `s` at the point `x` equal to `f'(x)`, then the derivative of the function `f` is equal to the function `f'` on the set `s`. This means that on the open set `s`, the derivative of `f` at any point `x` in `s` is the same as the function value of `f'` at `x`.
More concisely: If a function between a nontrivially normed field and a normed additively commutative group has derivatives equal to a given function on an open set where the domain is a nontrivially normed field, then the functions are equal on that open set.
|
hasStrictDerivAt_const
theorem hasStrictDerivAt_const :
β {π : Type u} [inst : NontriviallyNormedField π] {F : Type v} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace π F] (x : π) (c : F), HasStrictDerivAt (fun x => c) 0 x
The theorem `hasStrictDerivAt_const` states that for any non-trivially normed field `π`, normed addition-commutative group `F`, and normed space over `π` and `F`, and for any element `x` from `π` and `c` from `F`, the function that maps every element to a constant `c` has a strict derivative at the point `x`, and the value of this derivative is `0`. This is equivalent to saying that the rate of change of a constant function is zero, which aligns with the intuitive understanding in calculus.
More concisely: For any non-trivially normed field π, normed add-commutative group F, and normed space over π and F, the constant function from F to π with value c at every x has a strict derivative equal to the zero function.
|
HasDerivWithinAt.congr
theorem HasDerivWithinAt.congr :
β {π : Type u} [inst : NontriviallyNormedField π] {F : Type v} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace π F] {f fβ : π β F} {f' : F} {x : π} {s : Set π},
HasDerivWithinAt f f' s x β (β x β s, fβ x = f x) β fβ x = f x β HasDerivWithinAt fβ f' s x
The theorem `HasDerivWithinAt.congr` states that for any types `π` (with `NontriviallyNormedField π`) and `F` (with `NormedAddCommGroup F` and `NormedSpace π F`), given two functions `f` and `fβ` from `π` to `F`, a derivative `f'` of type `F`, a point `x` of type `π`, and a set `s` of points of type `π`, if the function `f` has the derivative `f'` at the point `x` within the set `s`, and for all `x` in `s`, `fβ x` equals `f x`, and `fβ x` equals `f x`, then the function `fβ` also has the derivative `f'` at the point `x` within the set `s`. In other words, if two functions agree on a subset and have the same point value at a given point, then having a derivative at that point for one implies the same for the other.
More concisely: If two real-valued functions agree on a set and have the same value at a point, and one of them has a derivative at that point within the set, then the other function also has the derivative of the same value at that point within the set.
|
HasDerivAt.hasDerivWithinAt
theorem HasDerivAt.hasDerivWithinAt :
β {π : Type u} [inst : NontriviallyNormedField π] {F : Type v} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace π F] {f : π β F} {f' : F} {x : π} {s : Set π},
HasDerivAt f f' x β HasDerivWithinAt f f' s x
This theorem asserts that for any non-trivial normed field π, normed additive commutative group F, and normed vector space over π and F, if a function f: π β F has a derivative f' at a point x in π, then f also has the derivative f' at the point x within any subset s of π. The derivative at a point x is defined as `f x' = f x + (x' - x) β’ f' + o(x' - x)` where `x'` converges to `x`. The derivative within a subset s at a point x is the same, but `x'` converges to `x` within the subset s.
More concisely: If a function f from a normed field to a normed vector space over the field, has a derivative at a point x in the field, then the derivative exists at x in any subset of the field containing x.
|
HasStrictDerivAt.hasStrictFDerivAt
theorem HasStrictDerivAt.hasStrictFDerivAt :
β {π : Type u} [inst : NontriviallyNormedField π] {F : Type v} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace π F] {f : π β F} {f' : F} {x : π},
HasStrictDerivAt f f' x β HasStrictFDerivAt f (ContinuousLinearMap.smulRight 1 f') x
The theorem `HasStrictDerivAt.hasStrictFDerivAt` states that for any type `π` that is a nontrivial normed field, any type `F` that forms a normed additive commutative group and a normed space over `π`, and for any function `f` from `π` to `F`, if `f` has a strict derivative `f'` at a point `x` in the sense of strict differentiability, then `f` also has a Frechet derivative at the same point `x`. This Frechet derivative is represented by the continuous linear map obtained by right-multiplication by `f'`. Strict differentiability in this context means that `f y - f z = (y - z) β’ f' + o(y - z)` as `y, z β x`.
More concisely: If `π` is a nontrivial normed field, `F` is a normed additive commutative group and normed space over `π`, and `f: π β F` is strictly differentiable at `x β π`, then `f` has a Frechet derivative `f'` at `x`, represented by the continuous linear map obtained by right-multiplication by `f'`.
|
derivWithin_zero_of_not_differentiableWithinAt
theorem derivWithin_zero_of_not_differentiableWithinAt :
β {π : Type u} [inst : NontriviallyNormedField π] {F : Type v} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace π F] {f : π β F} {x : π} {s : Set π},
Β¬DifferentiableWithinAt π f s x β derivWithin f s x = 0
The theorem `derivWithin_zero_of_not_differentiableWithinAt` asserts that for any type `π` which is a nontrivially normed field, any type `F` which is a normed add commutative group over this field, any function `f` from `π` to `F`, any point `x` in `π`, and any set `s` of points in `π`, if the function `f` is not differentiable at the point `x` within the set `s`, then the derivative of `f` at the point `x` within the set `s` is zero. In mathematical terms, this would be equivalent to stating that if a function does not have a derivative at a particular point within a set, then the derivative of the function at that point, considered within the set, is zero.
More concisely: If a function is not differentiable at a point within a set in a normed add commutative group over a nontrivially normed field, then its derivative at that point within the set is zero.
|
HasFDerivAtFilter.hasDerivAtFilter
theorem HasFDerivAtFilter.hasDerivAtFilter :
β {π : Type u} [inst : NontriviallyNormedField π] {F : Type v} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace π F] {f : π β F} {x : π} {L : Filter π} {f' : π βL[π] F},
HasFDerivAtFilter f f' x L β HasDerivAtFilter f (f' 1) x L
This theorem states that for any nontrivially normed field `π` and any normed add commutative group `F` that is also a normed space over `π`, if a function `f` from `π` to `F` has a Frechet derivative `f'` at a point `x` as `x` approaches along a filter `L`, then `f` also has the standard derivative at the point `x` along the filter `L`, where the standard derivative is given by the application of the Frechet derivative `f'` at `1`. This bridges the concept of the Frechet derivative and the standard derivative in the given settings.
More concisely: If a function from a nontrivially normed field to a normed add commutative group, which is also a normed space over that field, has a Frechet derivative at a point along a filter, then that function has the standard derivative equal to the application of the Frechet derivative at 1 along that filter.
|
HasDerivWithinAt.congr_of_eventuallyEq_of_mem
theorem HasDerivWithinAt.congr_of_eventuallyEq_of_mem :
β {π : Type u} [inst : NontriviallyNormedField π] {F : Type v} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace π F] {f fβ : π β F} {f' : F} {x : π} {s : Set π},
HasDerivWithinAt f f' s x β (nhdsWithin x s).EventuallyEq fβ f β x β s β HasDerivWithinAt fβ f' s x
This theorem states that if a function `f` has a derivative `f'` at a point `x` within a subset `s` of type `π`, and if another function `fβ` is eventually equal to `f` (i.e., `fβ` equals `f` near `x` within `s`), then `fβ` also has the derivative `f'` at the point `x` within the subset `s`, provided that `x` belongs to `s`. Here, `π` is a field endowed with a norm (not necessarily complete), and `F` is a normed additive commutative group over `π` that forms a normed space.
More concisely: If `f` has a derivative `f'` at `x` in the subset `s` of the normed space `F` over the field `π` with a norm, and `fβ` is equal to `f` near `x` in `s`, then `fβ` has the derivative `f'` at `x` in `s`.
|
UniqueDiffWithinAt.eq_deriv
theorem UniqueDiffWithinAt.eq_deriv :
β {π : Type u} [inst : NontriviallyNormedField π] {F : Type v} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace π F] {f : π β F} {f' fβ' : F} {x : π} (s : Set π),
UniqueDiffWithinAt π s x β HasDerivWithinAt f f' s x β HasDerivWithinAt f fβ' s x β f' = fβ'
This theorem, `UniqueDiffWithinAt.eq_deriv`, states that if a function `f` has a derivative within a subset `s` of a nontrivial normed field at a point `x`, and also has another derivative within the same subset at the same point, then these two derivatives must be equal, provided the set `s` has the unique differentiability property at `x`. More precisely, for any nontrivially normed field `π`, normed additive commutative group `F`, function `f` from `π` to `F`, derivatives `f'` and `fβ'` of `F`, and point `x` in `π`, if `s` is a set in `π` such that `UniqueDiffWithinAt π s x` holds and both `HasDerivWithinAt f f' s x` and `HasDerivWithinAt f fβ' s x` hold, then `f'` must be equal to `fβ'`.
More concisely: If a function has two derivatives within a set in a nontrivially normed field at a point where the set has the unique differentiability property, then those derivatives are equal.
|
hasDerivWithinAt_diff_singleton
theorem hasDerivWithinAt_diff_singleton :
β {π : Type u} [inst : NontriviallyNormedField π] {F : Type v} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace π F] {f : π β F} {f' : F} {x : π} {s : Set π},
HasDerivWithinAt f f' (s \ {x}) x β HasDerivWithinAt f f' s x
The theorem `hasDerivWithinAt_diff_singleton` states that for any nontrivially normed field `π`, any normed additive commutative group `F`, any normed space over `π` and `F`, any function `f` from `π` to `F`, any value `f'` in `F`, any point `x` in `π`, and any set `s` in `π`, the derivative of `f` at `x` within the set `s` excluding `x` is the same as the derivative of `f` at `x` within the set `s`. In mathematical terms, it says that $f'(x)$ exists within $s \setminus \{x\}$ if and only if $f'(x)$ exists within $s$.
More concisely: The derivative of a function from a nontrivially normed field to a normed space exists at a point in a set if and only if it exists in the set excluding that point.
|
hasDerivAtFilter_id
theorem hasDerivAtFilter_id :
β {π : Type u} [inst : NontriviallyNormedField π] (x : π) (L : Filter π), HasDerivAtFilter id 1 x L
The theorem `hasDerivAtFilter_id` states that for any type `π` which forms a non-trivially normed field, any element `x` of type `π`, and any filter `L` on `π`, the identity function `id` has derivative 1 at the point `x` as `x` converges along the filter `L`. In mathematical terms, it means that $ \lim_{x' \to x} \frac{id(x') - id(x)}{x' - x} = 1 $ for all x' in the neighbourhood of x defined by the filter `L`.
More concisely: For any non-trivially normed field `π`, element `x` in `π`, and filter `L` on `π`, the identity function `id` has derivative 1 at `x` as `x` converges along `L`. Equivalently, $ \lim\_{x' \to x} \frac{id(x') - id(x)}{x' - x} = 1 $ for all `x'` in the neighborhood of `x` defined by `L`.
|
derivWithin_congr
theorem derivWithin_congr :
β {π : Type u} [inst : NontriviallyNormedField π] {F : Type v} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace π F] {f fβ : π β F} {x : π} {s : Set π},
Set.EqOn fβ f s β fβ x = f x β derivWithin fβ s x = derivWithin f s x
This theorem, named `derivWithin_congr`, states that for any field `π` that is not trivially normed, any normed additive commutative group `F` over `π`, any functions `f` and `fβ` from `π` to `F`, any point `x` in `π`, and any set `s` of elements of `π`, if `fβ` and `f` are equal on the set `s` and at the point `x`, then the derivative of `fβ` at the point `x` within the set `s` is equal to the derivative of `f` at the point `x` within the set `s`.
In simple terms, if two functions are equal over a certain set and at a specific point, their derivatives are also equal at that point when considered within the same set.
More concisely: If functions `f` and `fβ` are equal on a set `s` containing a point `x` and `f'(x)` and `fβ'(x)` exist within `s`, then `f'(x) = fβ'(x)`.
|
HasDerivAt.continuousAt
theorem HasDerivAt.continuousAt :
β {π : Type u} [inst : NontriviallyNormedField π] {F : Type v} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace π F] {f : π β F} {f' : F} {x : π}, HasDerivAt f f' x β ContinuousAt f x
This theorem states that if a function `f` has a derivative `f'` at a point `x` in a nontrivially normed field `π` mapped into a normed additive commutative group `F` (where `F` is a normed space over `π`), then the function `f` is continuous at the point `x`. In mathematical terms, it means if `f` is differentiable at a point, then it is also continuous at that point. This is a fundamental concept in calculus and real analysis.
More concisely: If a function `f : β β β` is differentiable at a point `x`, then it is continuous at `x`.
|
hasDerivWithinAt_id
theorem hasDerivWithinAt_id :
β {π : Type u} [inst : NontriviallyNormedField π] (x : π) (s : Set π), HasDerivWithinAt id 1 s x
The theorem `hasDerivWithinAt_id` states that for any nontrivially normed field `π`, any element `x` of `π`, and any set `s` of elements of `π`, the identity function `id` has a derivative of `1` at the point `x` within the subset `s`. In mathematical terms, this means that the limit of the difference quotient as `x'` approaches `x` within `s` is `1` for the identity function, which is consistent with the standard calculus result that the derivative of the identity function is `1`.
More concisely: For any nontrivially normed field `π`, the identity function `id` has a derivative equal to `1` at every point `x` in `π`.
|
HasDerivAt.differentiableAt
theorem HasDerivAt.differentiableAt :
β {π : Type u} [inst : NontriviallyNormedField π] {F : Type v} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace π F] {f : π β F} {f' : F} {x : π}, HasDerivAt f f' x β DifferentiableAt π f x
This theorem states that for every function `f` from a field `π` to a normed add commutative group `F`, if the derivative of `f` at a point `x` in `π` exists and is equal to `f'`, then `f` is differentiable at `x`. In mathematical terms, if `f(x') = f(x) + (x' - x) β’ f' + o(x' - x)` when `x'` converges to `x`, then there exists a derivative for `f` at `x`. This derivative may not be unique.
More concisely: If a function `f` from a field to a normed add commutative group has an exponentially convergent derivative at a point, then `f` is differentiable at that point. (Note: Lean's statement assumes the derivative is unique, but this is not always the case in general.)
|
norm_deriv_le_of_lip'
theorem norm_deriv_le_of_lip' :
β {π : Type u} [inst : NontriviallyNormedField π] {F : Type v} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace π F] {f : π β F} {xβ : π} {C : β},
0 β€ C β (βαΆ (x : π) in nhds xβ, βf x - f xββ β€ C * βx - xββ) β βderiv f xββ β€ C
This theorem, named `norm_deriv_le_of_lip'`, is a converse to the mean value inequality in the context of a Lipschitz continuous function `f`. It states that if `f` is `C`-Lipschitz on a neighborhood of a point `xβ`, then the norm of its derivative at `xβ` is bounded by `C`. The Lipschitz condition is expressed here as `βf x - f xββ β€ C * βx - xββ` for all `x` in a neighborhood of `xβ`. Here, `π` is a nontrivially normed field, `F` is a normed add commutative group over `π`, and `xβ` and `C` are elements of `π` and β respectively, with `C` being nonnegative. The neighborhood is defined in the context of a topological space.
More concisely: If a Lipschitz continuous function `f` with constant `C` is defined on a neighborhood of `xβ` in a topological space with values in a normed add commutative group over a nontrivially normed field, then the norm of its derivative at `xβ` is bounded by `C`.
|
hasDerivAtFilter_const
theorem hasDerivAtFilter_const :
β {π : Type u} [inst : NontriviallyNormedField π] {F : Type v} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace π F] (x : π) (L : Filter π) (c : F), HasDerivAtFilter (fun x => c) 0 x L
The theorem `hasDerivAtFilter_const` asserts that for all types `π` with a nontrivial normed field structure, all types `F` with a normed additive commutative group structure, and any value `x` of type `π`, any filter `L` on `π`, and any value `c` of type `F`, the function which sends all inputs to `c` has a derivative of `0` at point `x` along the filter `L`. In other words, a constant function has a zero derivative everywhere, in the sense of Frechet derivatives.
More concisely: For any normed field `π` and normed additive commutative group `F`, a constant function from `π` to `F` has a Frechet derivative of 0 at every point in `π`.
|
HasDerivAt.le_of_lip'
theorem HasDerivAt.le_of_lip' :
β {π : Type u} [inst : NontriviallyNormedField π] {F : Type v} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace π F] {f : π β F} {f' : F} {xβ : π},
HasDerivAt f f' xβ β β {C : β}, 0 β€ C β (βαΆ (x : π) in nhds xβ, βf x - f xββ β€ C * βx - xββ) β βf'β β€ C
This theorem states that if a function `f` is differentiable at a point `xβ` and `C`-Lipschitz on a neighborhood of `xβ`, then the norm of its derivative at `xβ` is bounded by `C`. Here, being `C`-Lipschitz is defined as the condition 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 a neighborhood of `xβ`. Therefore, the theorem provides a converse to the mean value inequality under these conditions.
More concisely: If a differentiable function `f` at `xβ` is `C`-Lipschitz on a neighborhood of `xβ`, then the norm of its derivative at `xβ` is bounded by `C`.
|
hasFDerivAtFilter_iff_hasDerivAtFilter
theorem hasFDerivAtFilter_iff_hasDerivAtFilter :
β {π : Type u} [inst : NontriviallyNormedField π] {F : Type v} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace π F] {f : π β F} {x : π} {L : Filter π} {f' : π βL[π] F},
HasFDerivAtFilter f f' x L β HasDerivAtFilter f (f' 1) x L
The theorem `hasFDerivAtFilter_iff_hasDerivAtFilter` states that, given a nontrivial normed field `π`, a normed add commutative group `F`, and a normed space `F` over `π`, for any function `f` from `π` to `F`, any point `x` in `π`, any filter `L` on `π`, and any continuous linear map `f'` from `π` to `F`, the property `f` having the FrΓ©chet derivative `f'` at the point `x` as `x` goes along the filter `L` is equivalent to `f` having the derivative `(f' 1)` at the point `x` as `x` goes along the filter `L` (where `1` is the multiplicative identity in `π`).
In mathematical terms, it says that `f` has FrΓ©chet derivative `f'` at `x` along `L` if and only if `f` has the derivative `(f' 1)` at `x` along `L`.
More concisely: Given a nontrivial normed field π, a normed add commutative group F, and a normed space F over π, for any function f from π to F, point x in π, filter L on π, and continuous linear map f': π β F, the FrΓ©chet derivative f' has the same value as the derivative (f' 1) at x along L.
|
HasDerivWithinAt.Iic_of_Iio
theorem HasDerivWithinAt.Iic_of_Iio :
β {π : Type u} [inst : NontriviallyNormedField π] {F : Type v} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace π F] {f : π β F} {f' : F} {x : π} [inst_3 : PartialOrder π],
HasDerivWithinAt f f' (Set.Iio x) x β HasDerivWithinAt f f' (Set.Iic x) x
The theorem `HasDerivWithinAt.Iic_of_Iio` states that for any function `f` mapping from a non-trivially normed field `π` to a normed additive commutative group `F`, if `f` has a derivative `f'` at a point `x` within a left-infinite right-open interval `(Set.Iio x)` - meaning all points less than `x`, then `f` also has the same derivative `f'` at the same point `x` within a left-infinite right-closed interval `(Set.Iic x)` - meaning all points less than or equal to `x`.
More concisely: If a function `f` from a non-trivially normed field to a normed additive commutative group has a derivative at `x` within the left-infinite right-open interval `(Set.Iio x)`, then `f` has the same derivative at `x` within the larger left-infinite right-closed interval `(Set.Iic x)`.
|
HasDerivWithinAt.Ici_of_Ioi
theorem HasDerivWithinAt.Ici_of_Ioi :
β {π : Type u} [inst : NontriviallyNormedField π] {F : Type v} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace π F] {f : π β F} {f' : F} {x : π} [inst_3 : PartialOrder π],
HasDerivWithinAt f f' (Set.Ioi x) x β HasDerivWithinAt f f' (Set.Ici x) x
This theorem, `HasDerivWithinAt.Ici_of_Ioi`, states that for any non-trivial normed field `π`, normed additive commutative group `F`, a function `f` from `π` to `F`, its derivative `f'`, and a point `x` in `π`, if `f` has a derivative `f'` at the point `x` within the open interval greater than `x` (`Set.Ioi x`), then `f` also has the derivative `f'` at the point `x` within the closed interval greater than or equal to `x` (`Set.Ici x`).
In simpler terms, if a function has a certain derivative at a point within all values greater than the point, then the function has the same derivative at the point within all values greater than or equal to the point. This theorem essentially allows us to extend the interval of the derivative from open to closed without changing the derivative itself.
More concisely: If a function has a derivative at a point in an open interval, then it also has the same derivative at that point in the closed interval containing the open interval.
|
HasDerivAtFilter.tendsto_nhds
theorem HasDerivAtFilter.tendsto_nhds :
β {π : Type u} [inst : NontriviallyNormedField π] {F : Type v} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace π F] {f : π β F} {f' : F} {x : π} {L : Filter π},
L β€ nhds x β HasDerivAtFilter f f' x L β Filter.Tendsto f L (nhds (f x))
This theorem states that for a given function `f` from a non-trivially normed field to a normed additive commutative group, if `f` has a derivative `f'` at point `x` along the filter `L`, and `L` is less than or equal to the neighborhood filter of `x`, then the function `f` tends towards the filter of the neighborhood of `f(x)` as `x` tends towards `L`. Here, the filter is a mathematical construct that describes the limiting behavior of functions. The neighborhood of a point in a topological space is a set that includes an open set containing that point. A function has a derivative at a point if it can be approximated by a linear function at this point.
More concisely: If `f` is a function from a non-trivially normed field to a normed additive commutative group, has a derivative `f'` at point `x` along filter `L` with `L` being a neighborhood filter of `x`, then `f(x)` tends to the filter of neighborhoods of `f(x)` as `x` tends to `L` through `f'`.
|
deriv_const
theorem deriv_const :
β {π : Type u} [inst : NontriviallyNormedField π] {F : Type v} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace π F] (x : π) (c : F), deriv (fun x => c) x = 0
This theorem, `deriv_const`, states that for any nontrivially normed field `π` and normed additive commutative group `F` (which is also a normed space over `π`), the derivative at any point `x` in `π` of a constant function (a function that maps every input to the same constant value `c` in `F`) is zero. This corresponds to the standard calculus result that the derivative of a constant function is always zero.
More concisely: The derivative of a constant function is zero in the setting of a normed field and normed additive commutative group.
|
hasDerivAt_id
theorem hasDerivAt_id : β {π : Type u} [inst : NontriviallyNormedField π] (x : π), HasDerivAt id 1 x
This theorem states that the derivative of the identity function, `id`, is always `1` for any point `x` in a nontrivial normed field `π`. Here, the identity function `id` is a function that returns its input unchanged. In mathematical terms, if `π` is a field equipped with a norm (a function defining a notion of distance), where there exists at least one non-zero element, then the derivative of the identity function at any point `x` in `π` is `1`. This result is a fundamental property in calculus.
More concisely: The derivative of the identity function in a nontrivial normed field is equal to 1 for all points in the field.
|
hasDerivWithinAt_univ
theorem hasDerivWithinAt_univ :
β {π : Type u} [inst : NontriviallyNormedField π] {F : Type v} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace π F] {f : π β F} {f' : F} {x : π}, HasDerivWithinAt f f' Set.univ x β HasDerivAt f f' x
The theorem `hasDerivWithinAt_univ` states that for any function `f` from a non-trivially normed field `π` to a normed additive commutative group `F` over `π`, the derivative of `f` at a point `x` within the universal set (which contains all elements of `π`) is equivalent to saying the function `f` has a derivative at the point `x` without any restriction to a subset of `π`. In simpler terms, the derivative within the whole set is just the derivative at a point. In mathematical notation, it translates to the equivalence of these two statements: $f'(x) \text{ within } \mathbb{R} = f'(x)$.
More concisely: The theorem `hasDerivWithinAt_univ` asserts that the derivative of a function from a non-trivially normed field to a normed additive commutative group at a point equals the derivative of the function without restriction to a subset, within the universal set.
|
norm_deriv_le_of_lipschitzOn
theorem norm_deriv_le_of_lipschitzOn :
β {π : Type u} [inst : NontriviallyNormedField π] {F : Type v} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace π F] {f : π β F} {xβ : π} {s : Set π},
s β nhds xβ β β {C : NNReal}, LipschitzOnWith C f s β βderiv f xββ β€ βC
The theorem `norm_deriv_le_of_lipschitzOn` states that if a function `f` is `C`-Lipschitz continuous on a neighborhood of a point `xβ`, then the norm of its derivative at `xβ` is bounded by `C`. Here, `C` is a non-negative real number, and a function is said to be `C`-Lipschitz continuous on a set `s` if for all `x, y` in `s`, the distance between `f(x)` and `f(y)` is less than or equal to `C` times the distance between `x` and `y`. A neighborhood of a point is a set that contains an open set around the point. The derivative of `f` at a point is the rate at which `f` changes at that point, if it exists. If the derivative does not exist, it is considered to be zero.
More concisely: If a function `f` is `C`-Lipschitz continuous at a point `xβ`, then the norm of its derivative at `xβ` is bounded by `C`.
|
differentiableAt_of_deriv_ne_zero
theorem differentiableAt_of_deriv_ne_zero :
β {π : Type u} [inst : NontriviallyNormedField π] {F : Type v} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace π F] {f : π β F} {x : π}, deriv f x β 0 β DifferentiableAt π f x
This theorem states that for any function `f` of a type `π` with a nontrivial normed field structure mapping to a type `F` with a normed additive commutative group structure and a normed space structure over `π`, and for any point `x` of `π`, if the derivative of `f` at the point `x` is not zero, then `f` is differentiable at the point `x`. In mathematical terms, if $\text{deriv } f(x) \neq 0$, then `f` is differentiable at `x` in the field `π`.
More concisely: If a function `f` from a normed field `π` to a normed space `F` over `π` has a non-zero derivative at a point `x` in `π`, then `f` is differentiable at `x`.
|
HasDerivAt.unique
theorem HasDerivAt.unique :
β {π : Type u} [inst : NontriviallyNormedField π] {F : Type v} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace π F] {f : π β F} {fβ' fβ' : F} {x : π},
HasDerivAt f fβ' x β HasDerivAt f fβ' x β fβ' = fβ'
The theorem `HasDerivAt.unique` states that if a function `f` has derivatives `fβ'` and `fβ'` at a particular point `x` in a non-trivially normed field `π` with normed additive commutative group structure `F` and normed space structure over `π`, then `fβ'` and `fβ'` must be equal. This essentially asserts the uniqueness of the derivative at a given point. If there are two derivatives at the same point, they cannot be different; they have to be the same.
More concisely: If a function `f` has two derivatives `fβ²0` and `fβ²1` at a point `x` in a normed field `β` with corresponding normed additive commutative group structure and normed space structure, then `fβ²0 = fβ²1`.
|
HasDerivAt.deriv
theorem HasDerivAt.deriv :
β {π : Type u} [inst : NontriviallyNormedField π] {F : Type v} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace π F] {f : π β F} {f' : F} {x : π}, HasDerivAt f f' x β deriv f x = f'
The theorem `HasDerivAt.deriv` states that for any nontrivially normed field `π`, additively commutative normed group `F` and a function `f` mapping from `π` to `F`, if `f` has a derivative `f'` at a point `x` in `π` (denoted as `HasDerivAt f f' x`), then the derivative of `f` at this point `x` (denoted as `deriv f x`) is equal to `f'`. The derivative here is considered in the sense of Frechet derivatives.
More concisely: For any nontrivially normed field π, additively commutative normed group F, and differentiable function f from π to F at x in π, the Frechet derivative f' of f at x equals the derivative deriv f of f at x.
|
HasStrictFDerivAt.hasStrictDerivAt
theorem HasStrictFDerivAt.hasStrictDerivAt :
β {π : Type u} [inst : NontriviallyNormedField π] {F : Type v} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace π F] {f : π β F} {x : π} {f' : π βL[π] F},
HasStrictFDerivAt f f' x β HasStrictDerivAt f (f' 1) x
This theorem states that for any nontrivially normed field `π` and normed additively commutative group `F` that also forms a normed space over `π`, if a function `f` from `π` to `F` has a strict Frechet derivative `f'` at a point `x` in `π`, then `f` also has a strict derivative at `x` in the sense of strict differentiability. Specifically, the derivative at `x` is given by the value of the Frechet derivative `f'` at 1. This means that the change in `f` as we move away from `x` can be approximated by the value `f'(1)` times the change in the input, up to an error term that goes to zero faster than the change in the input.
More concisely: If a function from a nontrivially normed field to a normed additively commutative group, which is also a normed space, has a strict Frechet derivative at a point, then its strict derivative at that point equals the value of its Frechet derivative at 1.
|
HasDerivWithinAt.congr_of_eventuallyEq
theorem HasDerivWithinAt.congr_of_eventuallyEq :
β {π : Type u} [inst : NontriviallyNormedField π] {F : Type v} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace π F] {f fβ : π β F} {f' : F} {x : π} {s : Set π},
HasDerivWithinAt f f' s x β (nhdsWithin x s).EventuallyEq fβ f β fβ x = f x β HasDerivWithinAt fβ f' s x
The theorem `HasDerivWithinAt.congr_of_eventuallyEq` states that for a given type `π` with a nontrivial normed field, a type `F` with a normed additive commutative group and normed space over `π`, two functions `f` and `fβ` from `π` to `F`, a derivative function `f'` of type `F`, a point `x` of type `π`, and a set `s` of type `π`, if `f` has a derivative `f'` at the point `x` within the subset `s`, and `fβ` eventually equals `f` (i.e., `fβ` equals `f` in a neighborhood of `x` within `s`), and `fβ` at `x` equals `f` at `x`, then `fβ` also has the derivative `f'` at the point `x` within the set `s`.
In other words, if two functions coincide in a neighborhood of a point where the first function has a derivative, and they also have the same value at that point, then the second function has the same derivative at that point within the same neighborhood.
More concisely: If `f` has a derivative `f'` at `x` within `s` in the normed space `F` over the nontrivial normed field `π`, and `fβ` eventually equals `f` in `s` and `fβ(x) = f(x)`, then `fβ` has the derivative `f'` at `x` within `s`.
|
hasDerivWithinAt_const
theorem hasDerivWithinAt_const :
β {π : Type u} [inst : NontriviallyNormedField π] {F : Type v} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace π F] (x : π) (s : Set π) (c : F), HasDerivWithinAt (fun x => c) 0 s x
The theorem `hasDerivWithinAt_const` states that, for any non-trivially normed field `π`, normed additive commutative group `F`, any point `x` in `π`, any subset `s` of `π`, and any constant `c` in `F`, the function `f` defined as `f(x) = c` for all `x` has a derivative of `0` at the point `x` within the subset `s`. In other words, it states that the derivative of a constant function is always `0`, regardless of the point and the subset within which we are considering.
More concisely: For any non-trivially normed field π, normed additive commutative group F, constant c in F, and subset s of π, the constant function f(x) = c has derivative 0 at x in s.
|
derivWithin_of_isOpen
theorem derivWithin_of_isOpen :
β {π : Type u} [inst : NontriviallyNormedField π] {F : Type v} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace π F] {f : π β F} {x : π} {s : Set π}, IsOpen s β x β s β derivWithin f s x = deriv f x
The theorem `derivWithin_of_isOpen` states that for any nontrivially normed field `π`, any normed additive commutative group `F`, and any function `f` from `π` to `F`, if `s` is an open set in `π` and `x` is an element of `s`, then the derivative of `f` at the point `x` within the set `s` equals the derivative of `f` at the point `x`. This implies that if `x` is in the interior of `s`, the derivative of `f` at `x` does not change whether we consider it within `s` or in the whole space `π`.
More concisely: If `π` is a nontrivially normed field, `F` is a normed additive commutative group, `f` is a function from `π` to `F`, `s` is an open set in `π`, and `x` is an element of `s`, then the derivative of `f` at `x` within `s` equals the derivative of `f` at `x`.
|
HasDerivWithinAt.Ioi_of_Ioo
theorem HasDerivWithinAt.Ioi_of_Ioo :
β {π : Type u} [inst : NontriviallyNormedField π] {F : Type v} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace π F] {f : π β F} {f' : F} [inst_3 : LinearOrder π] [inst_4 : OrderClosedTopology π]
{x y : π}, x < y β HasDerivWithinAt f f' (Set.Ioo x y) x β HasDerivWithinAt f f' (Set.Ioi x) x
This theorem, `HasDerivWithinAt.Ioi_of_Ioo`, states that for any function `f` from a non-trivially normed field `π` to a normed additive commutative group `F` where `π` is a normed space, given `f'` as the derivative of `f`, and given `x` and `y` as elements of `π` where `x` is less than `y`, if `f` has a derivative `f'` at `x` within the left-open right-open interval `(x, y)`, then `f` also has the derivative `f'` at `x` within the left-open right-infinite interval `(x, β)`. Essentially, this theorem asserts that the existence of a derivative within an open interval implies the existence of the derivative in the corresponding half-open infinite interval.
More concisely: If a function `f` from a normed field to a normed additive commutative group has a derivative at an element `x` in an open interval `(x, y)`, then `f` has the same derivative at `x` in the left-open right-infinite interval `(x, β)`.
|
hasFDerivAt_iff_hasDerivAt
theorem hasFDerivAt_iff_hasDerivAt :
β {π : Type u} [inst : NontriviallyNormedField π] {F : Type v} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace π F] {f : π β F} {x : π} {f' : π βL[π] F}, HasFDerivAt f f' x β HasDerivAt f (f' 1) x
The theorem `hasFDerivAt_iff_hasDerivAt` establishes an equivalence between the properties `HasFDerivAt f f' x` and `HasDerivAt f (f' 1) x` for a given function `f` from a nontrivially normed field `π` to a normed additive commutative group `F`. That is, it provides a way to express the derivative of a function at a point in the domain, in terms of two different derivative concepts: `HasFDerivAt` and `HasDerivAt`. Specifically, it states that a function `f` has a continuous linear map `f'` as its derivative at point `x` (`HasFDerivAt f f' x`) if and only if the function `f` has `f' 1` as its derivative at the point `x` (`HasDerivAt f (f' 1) x`).
More concisely: A function between a nontrivially normed field and a normed additive commutative group has a continuous linear derivative at a point if and only if it has that derivative's value as its derivative at that point.
|
HasDerivWithinAt.Ioo_of_Ioi
theorem HasDerivWithinAt.Ioo_of_Ioi :
β {π : Type u} [inst : NontriviallyNormedField π] {F : Type v} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace π F] {f : π β F} {f' : F} [inst_3 : LinearOrder π] [inst_4 : OrderClosedTopology π]
{x y : π}, x < y β HasDerivWithinAt f f' (Set.Ioi x) x β HasDerivWithinAt f f' (Set.Ioo x y) x
This theorem, named `HasDerivWithinAt.Ioo_of_Ioi`, states that for any function `f` from a non-trivially normed field `π` to a normed additive commutative group `F`, and for any `f'` in `F`, given a linear order on `π` and an order-closed topology on `π`, if `x` is strictly less than `y` in `π`, and `f` has a derivative `f'` at the point `x` within the set of all points in `π` that are strictly greater than `x` (notation `Set.Ioi x`), then `f` also has the derivative `f'` at the point `x` within the open interval `(x, y)` (notation `Set.Ioo x y`). In other words, if the derivative of `f` exists on a half-open, right-infinite interval, it also exists on any open interval contained within that half-open interval.
More concisely: If a function from a non-trivially normed field to a normed additive commutative group has a derivative at a point within the open right half-line and the order topology, then it has that derivative at that point in any open interval contained within the right half-line.
|
HasStrictDerivAt.hasDerivAt
theorem HasStrictDerivAt.hasDerivAt :
β {π : Type u} [inst : NontriviallyNormedField π] {F : Type v} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace π F] {f : π β F} {f' : F} {x : π}, HasStrictDerivAt f f' x β HasDerivAt f f' x
This theorem states that for any nontrivially normed field π, normed add commutative group F, and π-valued function f, if f has a strict derivative of f' at the point x (meaning that `f y - f z = (y - z) β’ f' + o(y - z)` as `y, z β x`), then f also has a derivative of f' at the point x (meaning that `f x' = f x + (x' - x) β’ f' + o(x' - x)` where `x'` converges to `x`). In other words, the condition of having a strict derivative at a point implies the condition of having a derivative at that point.
More concisely: If a nontrivially normed field functions from a normed additive group to the field with a strict derivative at a point, then the function has a derivative at that point.
|
HasDerivWithinAt.congr_set
theorem HasDerivWithinAt.congr_set :
β {π : Type u} [inst : NontriviallyNormedField π] {F : Type v} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace π F] {f : π β F} {f' : F} {x : π} {s t : Set π},
(nhds x).EventuallyEq s t β HasDerivWithinAt f f' s x β HasDerivWithinAt f f' t x
This theorem, referred to as an alias of the forward direction of `hasDerivWithinAt_congr_set`, states that for any type `π` with a nontrivially normed field, type `F` with a normed additive commutative group and a normed space over `π`, a function `f` mapping from `π` to `F`, a derivative `f'` of type `F`, and points `x` of type `π`, if two sets `s` and `t` of type `π` are eventually equal at the neighborhood of `x` and if `f` has the derivative `f'` at `x` within the subset `s`, then `f` also has the derivative `f'` at `x` within the subset `t`. In mathematical terms, the theorem establishes the equivalence of derivative within two subsets under the condition of their eventual equality at a neighborhood.
More concisely: If `π` is a nontrivially normed field, `F` is a normed additive commutative group and a normed space over `π`, `f: π β F` has derivative `f'` at `x β π`, sets `s` and `t` are eventually equal at a neighborhood of `x`, then `f` has derivative `f'` at `x` within both `s` and `t`.
|
HasDerivWithinAt.hasFDerivWithinAt
theorem HasDerivWithinAt.hasFDerivWithinAt :
β {π : Type u} [inst : NontriviallyNormedField π] {F : Type v} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace π F] {f : π β F} {x : π} {s : Set π} {f' : F},
HasDerivWithinAt f f' s x β HasFDerivWithinAt f (ContinuousLinearMap.smulRight 1 f') s x
This theorem states that for any non-trivially normed field `π`, and any normed additive commutative group `F` over `π`, if a function `f` from `π` to `F` has a derivative `f'` at a point `x` within a subset `s` of `π`, then `f` has a FrΓ©chet derivative at `x` within `s` which is represented by the continuous linear map obtained by right multiplication of `f'` by `1`. In mathematical terms, this means that if `f` satisfies the property `f(x') = f(x) + (x' - x) β’ f' + o(x' - x)`, as `x'` converges to `x` inside `s`, then it possesses a FrΓ©chet derivative at `x` within `s`.
More concisely: If a function `f` from a non-trivially normed field `π` to a normed additive commutative group `F` over `π` has a derivative `f'` at a point `x` within a subset `s` of `π`, then `f` has a FrΓ©chet derivative at `x` within `s` equal to the continuous linear map obtained by right multiplication of `f'` by `1`.
|
HasDerivAt.hasFDerivAt
theorem HasDerivAt.hasFDerivAt :
β {π : Type u} [inst : NontriviallyNormedField π] {F : Type v} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace π F] {f : π β F} {x : π} {f' : F},
HasDerivAt f f' x β HasFDerivAt f (ContinuousLinearMap.smulRight 1 f') x
The theorem `HasDerivAt.hasFDerivAt` states that, given a nontrivially normed field `π`, a normed additive commutative group `F`, and a normed space `π F`, for any function `f : π β F`, point `x` in `π`, and derivative `f'` in `F`, if `f` has the derivative `f'` at the point `x` (expressed as `HasDerivAt f f' x`), then `f` also has the continuous linear map `f'` as a derivative at `x` (expressed as `HasFDerivAt f (ContinuousLinearMap.smulRight 1 f') x`). The continuous linear map in this case is represented by the scalar multiplication of `f'` by `1`.
More concisely: Given a nontrivially normed field π, a normed additive commutative group F, and a normed space πβF over π, if a function f : π β F has the derivative f' at x in π and f' is continuous, then f has the continuous linear derivative f' at x.
|
HasDerivAt.le_of_lipschitzOn
theorem HasDerivAt.le_of_lipschitzOn :
β {π : Type u} [inst : NontriviallyNormedField π] {F : Type v} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace π F] {f : π β F} {f' : F} {xβ : π},
HasDerivAt f f' xβ β β {s : Set π}, s β nhds xβ β β {C : NNReal}, LipschitzOnWith C f s β βf'β β€ βC
This theorem, named `HasDerivAt.le_of_lipschitzOn`, states that: if a function `f` is differentiable at a point `xβ` and it is `C`-Lipschitz continuous on a neighborhood of `xβ`, then the norm of the derivative of `f` at `xβ` is bounded by `C`.
Here, `C`-Lipschitz continuous on a neighborhood means that for all pairs of points in the neighborhood, the distance between `f` applied to those points is less than or equal to `C` times the distance between the points themselves. The derivative being bounded by `C` refers to the property that the length (or norm) of the function's derivative at `xβ` is less than or equal to `C`.
More concisely: If a differentiable function `f` at point `xβ` is `C-`Lipschitz continuous on a neighborhood of `xβ`, then the norm of its derivative at `xβ` is bounded by `C`.
|
Filter.EventuallyEq.deriv_eq
theorem Filter.EventuallyEq.deriv_eq :
β {π : Type u} [inst : NontriviallyNormedField π] {F : Type v} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace π F] {f fβ : π β F} {x : π}, (nhds x).EventuallyEq fβ f β deriv fβ x = deriv f x
This theorem states that for any nontrivially normed field `π` and any normed additive commutative group `F` that also forms a normed space over `π`, if two functions `f` and `fβ` from `π` to `F` are eventually equal at a point `x` in the neighborhood filter of `x`, then their derivatives at `x` are equal. In other words, if `fβ` and `f` differ only within an infinitesimally small neighborhood around `x`, their derivatives at `x` are identical.
More concisely: If `f` and `fβ` are normed `π`-valued functions on a normed additive commutative group `F` that agree in some neighborhood of a point `x`, then their derivatives at `x` are equal.
|
HasDerivWithinAt.Iio_of_Iic
theorem HasDerivWithinAt.Iio_of_Iic :
β {π : Type u} [inst : NontriviallyNormedField π] {F : Type v} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace π F] {f : π β F} {f' : F} {x : π} [inst_3 : PartialOrder π],
HasDerivWithinAt f f' (Set.Iic x) x β HasDerivWithinAt f f' (Set.Iio x) x
The theorem `HasDerivWithinAt.Iio_of_Iic` states that if a function `f` from a nontrivially normed field to a normed add commutative group has a derivative `f'` at the point `x` within the left-infinite right-closed interval up to `x` (`Set.Iic x`), then `f` also has the derivative `f'` at `x` within the left-infinite right-open interval up to `x` (`Set.Iio x`). In other words, if a function is differentiable on an interval including its endpoint, it is also differentiable on the interval excluding the endpoint.
More concisely: If a function has a derivative within the left-infinite right-closed interval up to a point in a normed add commutative group, then it also has that derivative within the left-infinite right-open interval up to that point. (In other words, differentiability at a point implies differentiability on the left-hand side of that point.)
|
hasDerivAt_id'
theorem hasDerivAt_id' : β {π : Type u} [inst : NontriviallyNormedField π] (x : π), HasDerivAt (fun x => x) 1 x := by
sorry
The theorem `hasDerivAt_id'` states that for any value `x` in the non-trivially normed field `π`, the function `f(x) = x` has a derivative of `1` at `x`. In other words, the change in the function `f(x) = x` with respect to `x` is constant and equal to `1` for all `x` in the field `π`.
More concisely: The function `f(x) = x` is differentiable with derivative `1` over the non-trivially normed field `π`.
|
deriv_const'
theorem deriv_const' :
β {π : Type u} [inst : NontriviallyNormedField π] {F : Type v} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace π F] (c : F), (deriv fun x => c) = fun x => 0
This theorem states that the derivative of a constant function is zero, regardless of the point at which it is evaluated. More formally, for any non-trivial normed field `π`, normed additive commutative group `F`, and a normed space over `π` and `F`, if `c` is a constant in `F`, then the derivative at any point `x` of the function `f` defined by `f(x) = c` is zero. This is consistent with the standard calculus result that the derivative of a constant function is always zero.
More concisely: For any constant function `f(x) = c` in a normed vector space, the derivative `df/dx` is the zero function.
|
hasStrictDerivAt_id
theorem hasStrictDerivAt_id : β {π : Type u} [inst : NontriviallyNormedField π] (x : π), HasStrictDerivAt id 1 x := by
sorry
This theorem states that the identity function has a strict derivative of 1 at any point `x` in the domain of a nontrivially normed field. In mathematical terms, the derivative of the identity function is always 1, which is expressed in the theorem as `HasStrictDerivAt id 1 x`. Thus, in the limit as `y` and `z` approach `x`, the difference between the values of the identity function at `y` and `z` is equal to the difference between `y` and `z`, plus a term that tends to zero faster than `y - z`.
More concisely: The identity function over a nontrivially normed field has a strict derivative equal to 1 at every point.
|
HasFDerivAt.hasDerivAt
theorem HasFDerivAt.hasDerivAt :
β {π : Type u} [inst : NontriviallyNormedField π] {F : Type v} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace π F] {f : π β F} {x : π} {f' : π βL[π] F}, HasFDerivAt f f' x β HasDerivAt f (f' 1) x
The theorem `HasFDerivAt.hasDerivAt` states that for any field `π` which is a non-trivially normed field, and for any normed add commutative group `F` over the field `π`, if a function `f` from `π` to `F` has the continuous linear map `f'` as its Frechet derivative at a point `x` in π, then `f` also has `f' 1` as its derivative at the same point `x`. In other words, if `f` satisfies the condition `f x' = f x + f' (x' - x) + o(x' - x)` as `x'` approaches `x`, then it also satisfies `f x' = f x + (x' - x) β’ f' 1 + o(x' - x)` as `x'` approaches `x`.
More concisely: If `f : ββ β F` is a differentiable function from a non-trivially normed field `ββ` to a normed additive group `F`, and `f' : ββ β L(ββ, F)` is its Frechet derivative, then `f' 1` is its derivative at any point `x β ββ`, i.e., `df x = dx β’ f' 1 + r(x)` with `β₯r(x)β₯ β€ Ξ΅β
β₯x' - xβ₯ for any Ξ΅ > 0 and `x' β x`.
|
norm_deriv_le_of_lipschitz
theorem norm_deriv_le_of_lipschitz :
β {π : Type u} [inst : NontriviallyNormedField π] {F : Type v} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace π F] {f : π β F} {xβ : π} {C : NNReal}, LipschitzWith C f β βderiv f xββ β€ βC
This theorem, named `norm_deriv_le_of_lipschitz`, states that if a function `f` is `C`-Lipschitz (i.e., it satisfies a Lipschitz continuity condition with a nonnegative real constant `C`), then the norm of its derivative at a specific point `xβ` is bounded by `C`. In other words, for a function that does not change too rapidly (its rate of change between any two points is bounded by `C`), the magnitude of its instantaneous rate of change (derivative) at a specific point can't exceed `C`. This theorem is the converse to the mean value inequality. This theorem is defined over a nontrivially normed field `π` and a normed additive commutative group `F`, both of which constitute a normed space.
More concisely: If a function `f` is `C-Lipschitz` on a normed space `(F, ||Β·||)`, then `||f'(xβ)|| β€ C` for all `xβ β F`.
|
HasDerivWithinAt.differentiableWithinAt
theorem HasDerivWithinAt.differentiableWithinAt :
β {π : Type u} [inst : NontriviallyNormedField π] {F : Type v} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace π F] {f : π β F} {f' : F} {x : π} {s : Set π},
HasDerivWithinAt f f' s x β DifferentiableWithinAt π f s x
The theorem `HasDerivWithinAt.differentiableWithinAt` states that for any type `π` that has a non-trivial normed field, type `F` that has a normed add commutative group and a normed space over `π`, a function `f` from `π` to `F`, a derivative `f'` of type `F`, a point `x` of type `π`, and a set `s` of type `Set π`; if the function `f` has the derivative `f'` at the point `x` within the subset `s`, then the function `f` is differentiable at the point `x` within the set `s`. In other words, if a function has a derivative within a certain set at a certain point, then it is differentiable within that set at that point.
More concisely: If a function has a derivative within a set at a point, then it is differentiable within that set at that point.
|
DifferentiableAt.hasDerivAt
theorem DifferentiableAt.hasDerivAt :
β {π : Type u} [inst : NontriviallyNormedField π] {F : Type v} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace π F] {f : π β F} {x : π}, DifferentiableAt π f x β HasDerivAt f (deriv f x) x
This theorem states that for any function `f` from a non-trivially normed field `π` to a normed additive commutative group `F` (which is a normed space over `π`), at any point `x` in `π`, if `f` is differentiable at `x`, then `f` has a derivative at `x` and that derivative is given by the function `deriv f x`. This means the derivative of `f` at the point `x` exists and satisfies the property of being the rate of change of `f` at `x`. In mathematical terms, if `f` is differentiable at `x`, then the function `f` at `x` approximates to `f x + (x' - x) β’ deriv f x + o(x' - x)` as `x'` converges to `x`, where `deriv f x` is the derivative of `f` at `x`.
More concisely: If `f` is a differentiable function from a non-trivially normed field to a normed additive commutative group, then the derivative `deriv f x` exists at any point `x` in the field, and `f(x) β f(x + h) + h β’ deriv f x` as `h` approaches 0.
|
derivWithin_univ
theorem derivWithin_univ :
β {π : Type u} [inst : NontriviallyNormedField π] {F : Type v} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace π F] {f : π β F}, derivWithin f Set.univ = deriv f
This theorem, `derivWithin_univ`, states that for any function `f` from a nontrivially normed field `π` to a normed group `F`, the derivative of `f` at any point `x` within the universal set (which contains all elements of `π`) is equal to the derivative of `f` at `x`. In mathematical terms, for any function `f : π β F`, the derivative of `f` within the entire domain `π` (represented by `Set.univ` or the universal set) at any point is the same as the general derivative of `f` at that point.
More concisely: For any function `f` from a nontrivially normed field to a normed group, the derivative of `f` at any point within the universal set equals the general derivative of `f` at that point.
|
DifferentiableWithinAt.hasDerivWithinAt
theorem DifferentiableWithinAt.hasDerivWithinAt :
β {π : Type u} [inst : NontriviallyNormedField π] {F : Type v} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace π F] {f : π β F} {x : π} {s : Set π},
DifferentiableWithinAt π f s x β HasDerivWithinAt f (derivWithin f s x) s x
The theorem `DifferentiableWithinAt.hasDerivWithinAt` states that for any type `π` that forms a non-trivial normed field, any type `F` that forms a normed addition commutative group and a normed space over `π`, any function `f` mapping from `π` to `F`, any point `x` of type `π`, and any set `s` made up of elements of type `π`, if the function `f` is differentiable at the point `x` within the set `s`, then `f` has the derivative `derivWithin f s x` at the point `x` within the subset `s`. In mathematical terms, it means if there exists a derivative of `f` at `x` within `s`, then the function `f` follows the differential relationship `f x' = f x + (x' - x) β’ derivWithin f s x + o(x' - x)` where `x'` converges to `x` within `s`.
More concisely: If a function between a normed field and a normed additive commutative group is differentiable at a point within a set, then it has the derivative at that point within the set.
|
HasDerivAt.le_of_lipschitz
theorem HasDerivAt.le_of_lipschitz :
β {π : Type u} [inst : NontriviallyNormedField π] {F : Type v} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace π F] {f : π β F} {f' : F} {xβ : π},
HasDerivAt f f' xβ β β {C : NNReal}, LipschitzWith C f β βf'β β€ βC
This theorem states that if a function `f` is differentiable at a point `xβ` and is Lipschitz continuous with constant `C`, then the norm of its derivative at `xβ` is bounded by `C`. In other words, the derivative of `f` at `xβ` cannot be larger than `C`. This is the converse to the mean value inequality. In mathematical terms, if `f'` is the derivative of `f` at `xβ`, then `βf'β β€ C`.
More concisely: If a differentiable function `f` at `xβ` is Lipschitz continuous with constant `C`, then the norm of its derivative `βf'β β€ C` at `xβ`.
|
HasDerivAt.congr_of_eventuallyEq
theorem HasDerivAt.congr_of_eventuallyEq :
β {π : Type u} [inst : NontriviallyNormedField π] {F : Type v} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace π F] {f fβ : π β F} {f' : F} {x : π},
HasDerivAt f f' x β (nhds x).EventuallyEq fβ f β HasDerivAt fβ f' x
This theorem, `HasDerivAt.congr_of_eventuallyEq`, states that for any nontrivially normed field `π`, normed additive commutative group `F`, and normed space over `π` and `F`, if a function `f` has a derivative `f'` at a point `x`, and another function `fβ` equals `f` in a neighborhood of `x` (more precisely, `fβ` equals `f` eventually at `x`), then `fβ` also has the derivative `f'` at the point `x`. In other words, the existence of the derivative at a point is stable under small perturbations of the function in a neighborhood of that point.
More concisely: If `f` has a derivative `f'` at `x` and `fβ` equals `f` eventually at `x`, then `fβ` also has derivative `f'` at `x` in a nontrivially normed field.
|
HasDerivWithinAt.derivWithin
theorem HasDerivWithinAt.derivWithin :
β {π : Type u} [inst : NontriviallyNormedField π] {F : Type v} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace π F] {f : π β F} {f' : F} {x : π} {s : Set π},
HasDerivWithinAt f f' s x β UniqueDiffWithinAt π s x β derivWithin f s x = f'
The theorem states that for a function `f` from a nontrivially normed field to a normed additive commutative group, if `f` has a derivative `f'` at a point `x` within a set `s` and `s` is uniquely differentiable at `x`, then the derivative of `f` at the point `x` within the set `s` is equal to `f'`. In mathematical terms, given a function $f: π β F$, a point $x β π$, and a subset $s β π$, if $f$ has a derivative $f'$ at $x$ within $s$ and the differentiability of $s$ at $x$ is unique, then the derivative of $f$ at $x$ within $s$ is $f'$.
More concisely: If a function between a nontrivially normed field and a normed additive commutative group has a unique derivative at a point in a subset, then the derivative equals the function's value at that point within the subset.
|
hasDerivAt_iff_hasFDerivAt
theorem hasDerivAt_iff_hasFDerivAt :
β {π : Type u} [inst : NontriviallyNormedField π] {F : Type v} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace π F] {f : π β F} {x : π} {f' : F},
HasDerivAt f f' x β HasFDerivAt f (ContinuousLinearMap.smulRight 1 f') x
This theorem states that, for any non-trivially normed field `π`, any normed additive commutative group `F` over `π`, any function `f` from `π` to `F`, any point `x` in `π`, and any element `f'` in `F`, the property that `f` has the derivative `f'` at the point `x` (expressed as `HasDerivAt f f' x`) is equivalent to the property that `f` has the continuous linear map `f'` scaled by 1 as its derivative at `x` (expressed as `HasFDerivAt f (ContinuousLinearMap.smulRight 1 f') x`). In other words, a function has a derivative at a point if and only if it has a continuous linear map, which is the derivative scaled by 1, at that same point.
More concisely: Given a non-trivially normed field `π`, any normed additive commutative group `F` over `π`, and a function `f` from `π` to `F`, the derivative `HasDerivAt f x` of `f` at point `x` in `π` is equivalent to `f` having the continuous linear map `f' = ContinuousLinearMap.smulRight 1 f'` as its derivative at `x`.
|
hasFDerivWithinAt_iff_hasDerivWithinAt
theorem hasFDerivWithinAt_iff_hasDerivWithinAt :
β {π : Type u} [inst : NontriviallyNormedField π] {F : Type v} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace π F] {f : π β F} {x : π} {s : Set π} {f' : π βL[π] F},
HasFDerivWithinAt f f' s x β HasDerivWithinAt f (f' 1) s x
This theorem establishes an equivalence between `HasFDerivWithinAt f f' s x` and `HasDerivWithinAt f (f' 1) s x` for any subset `s` of a nontrivially normed field `π`, any function `f : π β F` from `π` to a normed additive commutative group `F`, any point `x` in `π`, and any continuous linear map `f' : π βL[π] F`. This means that the condition of `f` having a FrΓ©chet derivative `f'` within the subset `s` at the point `x` is precisely equivalent to `f` having a derivative of `f' 1` at the point `x` within `s` under the given conditions.
More concisely: The theorem asserts that for any nontrivially normed field π, function f from π to a normed additive commutative group F, point x in π, and continuous linear map f' from π to the vector space of linear maps L[π] F, the condition of `HasFDerivWithinAt f f' s x` holds if and only if `HasDerivWithinAt f (f' 1) s x` holds.
|
norm_deriv_eq_norm_fderiv
theorem norm_deriv_eq_norm_fderiv :
β {π : Type u} [inst : NontriviallyNormedField π] {F : Type v} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace π F] {f : π β F} {x : π}, βderiv f xβ = βfderiv π f xβ
The theorem `norm_deriv_eq_norm_fderiv` asserts that for any type `π` with a non-trivially normed field structure, any type `F` with a normed additive commutative group structure and a normed space over `π`, any function `f` from `π` to `F`, and any point `x` of type `π`, the norm of the derivative of `f` at `x` is equal to the norm of `fderiv π f x`. In other words, it states that the norms of the derivative of `f` at `x` and `fderiv π f x` are equivalent.
More concisely: For any normed field `π`, normed additive commutative group `F`, normed space `F` over `π`, function `f` from `π` to `F`, and point `x` in `π`, the norm of `f'(x)` is equal to the norm of `fderiv π f x`.
|