HasStrictFDerivAt.to_localInverse
theorem HasStrictFDerivAt.to_localInverse :
β {π : 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]
[inst_5 : CompleteSpace E] {f : E β F} {f' : E βL[π] F} {a : E} (hf : HasStrictFDerivAt f (βf') a),
HasStrictFDerivAt (HasStrictFDerivAt.localInverse f f' a hf) (βf'.symm) (f a)
The theorem `HasStrictFDerivAt.to_localInverse` states that if a function `f` has an invertible derivative `f'` at a point `a`, in the sense of strict differentiability `(hf)`, then the inverse function (denoted as `hf.localInverse f`), computed using the derivative `f'`, has its own derivative `f'.symm` (the inverse of `f'`) at the point `f a`. This theorem is defined in the context of a certain type `π` which has a nontrivial normed field structure, and two other types `E` and `F` which have normed additive commutative group and normed space structures over `π`. `E` is also required to be a complete space.
More concisely: If a strict differentiable function `f : E β F` with invertible derivative `f'` at `a β E` has an invertible strict derivative, then the inverse function `hf.localInverse f` has the inverse derivative `f'.symm` at `f a`.
|
HasStrictFDerivAt.approximates_deriv_on_nhds
theorem HasStrictFDerivAt.approximates_deriv_on_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} {a : E},
HasStrictFDerivAt f f' a β β {c : NNReal}, Subsingleton E β¨ 0 < c β β s β nhds a, ApproximatesLinearOn f f' s c
This theorem states that for a given function `f` from a normed additive commutative group `E` to another normed additive commutative group `F`, if `f` has a strict derivative `f'` at a point `a` and there is a nonnegative real number `c` such that `c` is greater than `0` or `E` is a subsingleton, then there exists a neighborhood `s` of `a` such that `f` approximates its derivative `f'` on this neighborhood with a constant `c`. This means that `f` behaves nearly linearly around `a` with a linear approximation given by `f'` and deviation measured by `c`. This theorem is foundational in the analysis of functions in normed spaces, underpinning the rigorous formalization of concepts such as continuity and differentiability.
More concisely: Given a continuous, norm-preserving function `f` from a normed additive commutative group `E` to another such group `F`, with strict derivative `f'` at `a β E`, there exists a neighborhood `s` of `a` such that `||f(x) - f(a) - f'(a) * (x - a)|| β€ c * ||x - a||` for all `x β s`, where `c` is a positive constant.
|
open_map_of_strict_fderiv_equiv
theorem open_map_of_strict_fderiv_equiv :
β {π : 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]
[inst_5 : CompleteSpace E] {f : E β F} {f' : E β E βL[π] F},
(β (x : E), HasStrictFDerivAt f (β(f' x)) x) β IsOpenMap f
The theorem `open_map_of_strict_fderiv_equiv` states that if a function has an invertible strict derivative at all points, then the function is an open map. Here, an open map is defined as a function whose image of any open set remains open. In more formal terms, given a function `f` from a complete normed space `E` to another normed space `F`, both over a nontrivial normed field `π`, and a function `f'` that assigns to each point in `E` an invertible bounded linear map from `E` to `F`, if `f` has an invertible strict derivative `f'` at every point in `E`, then `f` is an open map.
More concisely: If a function `f : E β F` between complete normed spaces, with invertible and bounded strict derivatives `f'` at all points in `E`, then `f` is an open map.
|
HasStrictFDerivAt.approximates_deriv_on_open_nhds
theorem HasStrictFDerivAt.approximates_deriv_on_open_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} {a : E},
HasStrictFDerivAt f (βf') a β β s, a β s β§ IsOpen s β§ ApproximatesLinearOn f (βf') s (ββf'.symmβββ»ΒΉ / 2)
This theorem states that for a function `f: E β F` having a strict Frechet derivative `f'` at a point `a` in a normed space over a nontrivially normed field, there exists a set `s` such that `a` is in `s`, `s` is open in the topological space, and `f` approximates linearly on `s` with error term bounded by half the inverse of the norm of the continuous linear inverse of `f'`. This essentially means that around every point where the function `f` has a derivative, we can find an open set where the function behaves nearly linearly, with a precise bound given on the error.
More concisely: Given a function `f: E β F` with a strict Frechet derivative `f'` at a point `a` in a normed space over a nontrivially normed field, there exists an open set `s` containing `a` such that `f` approximates `f(x) β f(a) + f'(a)(x - a)` for all `x β s`, with an error bound `||(x - a) - f'(a)β»ΒΉ(f(x) - f(a) - f'(a)(x - a))|| β€ ||f'(a)β»ΒΉ||/2`.
|
HasStrictFDerivAt.mem_toPartialHomeomorph_source
theorem HasStrictFDerivAt.mem_toPartialHomeomorph_source :
β {π : 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]
[inst_5 : CompleteSpace E] {f : E β F} {f' : E βL[π] F} {a : E} (hf : HasStrictFDerivAt f (βf') a),
a β (HasStrictFDerivAt.toPartialHomeomorph f hf).source
The theorem `HasStrictFDerivAt.mem_toPartialHomeomorph_source` states that for a function `f` from a normed add commutative group `E` to another normed add commutative group `F`, both over a nontrivially normed field `π`, if this function has a strict Frechet derivative at a point `a` in `E`, then `a` belongs to the source of the partial homeomorphism associated with the strict Frechet derivative.
More concisely: If `f : E β F` is a function between normed add commutative groups over a nontrivially normed field with a strict Frechet derivative at `a β E`, then `a` is in the domain of the partial homeomorphism defined by the strict Frechet derivative.
|
HasStrictFDerivAt.to_local_left_inverse
theorem HasStrictFDerivAt.to_local_left_inverse :
β {π : 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]
[inst_5 : CompleteSpace E] {f : E β F} {f' : E βL[π] F} {a : E},
HasStrictFDerivAt f (βf') a β
β {g : F β E}, (βαΆ (x : E) in nhds a, g (f x) = x) β HasStrictFDerivAt g (βf'.symm) (f a)
This theorem states that if we have a function `f : E β F`, with an invertible derivative `f'` at the point `a` in the sense of strict differentiability, and another function `g` that undoes the effect of `f` in the neighborhood of `a` - i.e., `g (f x) = x` - then `g` has a derivative at the point `f a` that is the inverse of `f'`. The theorem assumes that the domain `E` is a complete space. A variant of this theorem is also available that doesn't require `E` to be complete, but instead requires `f (g y) = y` and the continuity of `g` at `f a`.
More concisely: If `f : E β F` is a strict differentiable function with invertible derivative `f'` at `a β E` and there exists a function `g : F β E` such that `g (f x) = x` in a neighborhood of `f a`, then `g` has a derivative at `f a` and `(g ')(f a) = (f ')β»ΒΉ`.
|
HasStrictFDerivAt.image_mem_toPartialHomeomorph_target
theorem HasStrictFDerivAt.image_mem_toPartialHomeomorph_target :
β {π : 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]
[inst_5 : CompleteSpace E] {f : E β F} {f' : E βL[π] F} {a : E} (hf : HasStrictFDerivAt f (βf') a),
f a β (HasStrictFDerivAt.toPartialHomeomorph f hf).target
This theorem states that for any non-trivial normed field `π`, normed additive commutative groups `E` and `F` equipped with a normed space structure over `π`, where `E` is complete, if a function `f : E β F` has a strict FrΓ©chet derivative at a point `a` in `E`, represented by the linear map `f' : E βL[π] F`, then the image of `a` under `f` is within the target set of the partial homeomorphism induced by the strict derivative of `f` at `a`.
More concisely: If `f : E β F` is a strict differentiable function from a complete normed additive commutative group `E` to a normed space `F` over a non-trivial normed field `π`, with strict derivative `f' : E βL[π] F` at a point `a` in `E`, then `f(a)` lies in the image of the partial homeomorphism induced by `f'` at `a`.
|
HasStrictFDerivAt.map_nhds_eq_of_equiv
theorem HasStrictFDerivAt.map_nhds_eq_of_equiv :
β {π : 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]
[inst_5 : CompleteSpace E] {f : E β F} {f' : E βL[π] F} {a : E},
HasStrictFDerivAt f (βf') a β Filter.map f (nhds a) = nhds (f a)
This theorem states that for a given strict Frechet derivative at a point `a` in a complete normed additive commutative group `E` over a nontrivially normed field `π`, mapped to another normed additive commutative group `F` under a continuous linear equivalence `f'`, if the function `f` has a strict Frechet derivative `f'` at `a`, then the forward map of the neighborhood filter at `a` under `f` is equal to the neighborhood filter at `f(a)`. In simpler terms, this theorem provides a condition under which the derivative of a function at a point determines the local behavior of the function around that point in the sense of filters.
More concisely: If `f : E β F` is a continuous linear map between complete normed additive commutative groups with `f'` its strict Frechet derivative at `a β E`, then the forward neighborhood filter of `a` under `f` equals the neighborhood filter of `f(a)`.
|