ContinuousLinearEquiv.hasFDerivWithinAt
theorem ContinuousLinearEquiv.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] {x : E}
{s : Set E} (iso : E βL[π] F), HasFDerivWithinAt (βiso) (βiso) s x
The theorem `ContinuousLinearEquiv.hasFDerivWithinAt` states that for any nontrivially normed field `π`, and any normed additive commutative groups `E` and `F` which are also normed spaces over `π`, for any element `x` of `E` and any set `s` of `E`, if `iso` is a continuous linear equivalence between `E` and `F`, then the function `iso` has a derivative within the set `s` at the point `x`, and that derivative is `iso` itself.
More concisely: For any nontrivially normed field `π`, given a continuous linear equivalence `iso` between normed additive commutative groups `E` and `F` over `π`, and for any `x` in `E` and set `s` in `E`, `iso` has a derivative equal to itself at `x` within `s`.
|
PartialHomeomorph.hasFDerivAt_symm
theorem PartialHomeomorph.hasFDerivAt_symm :
β {π : 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 : PartialHomeomorph E F) {f' : E βL[π] F} {a : F},
a β f.target β HasFDerivAt (βf) (βf') (βf.symm a) β HasFDerivAt (βf.symm) (βf'.symm) a
The theorem `PartialHomeomorph.hasFDerivAt_symm` states that for any non-trivially normed field `π`, normed add commutative groups `E` and `F` which are also normed spaces over `π`, if `f` is a partial homeomorphism defined on a neighbourhood of `f.symm a`, and `f` has an invertible derivative `f'` at `f.symm a`, then the derivative of the inverse function `f.symm` at `a` is the inverse of `f'`. This is a part of the inverse function theorem, assuming we already have an inverse function.
More concisely: If `f` is a partial homeomorphism with invertible derivative at `a` in the neighborhood of `f.symm a` in the normed spaces `E` and `F` over a non-trivially normed field `π`, then `(df.symm /. (f.symm a)) = (f'.inv)`.
|
ContinuousLinearEquiv.hasFDerivAt
theorem ContinuousLinearEquiv.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] {x : E}
(iso : E βL[π] F), HasFDerivAt (βiso) (βiso) x
This theorem states that for any nontrivially normed field π, normed add commutative groups E and F, and normed vector spaces over π, E and F, if we have a continuous linear equivalence `iso` from E to F, then the function defined by the application of this equivalence `βiso` has a derivative at any point `x` in E. This derivative is given by the representation `βiso` of the continuous linear equivalence. In other words, this theorem asserts that the continuous linear equivalences are differentiable and its derivative is itself at any point in the domain.
More concisely: For any nontrivially normed field π, any continuous linear equivalence between normed additive groups of normed vector spaces over π is differentiable, and its derivative is given by the representation of the equivalence.
|
HasStrictFDerivAt.of_local_left_inverse
theorem HasStrictFDerivAt.of_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] {f : E β F}
{f' : E βL[π] F} {g : F β E} {a : F},
ContinuousAt g a β
HasStrictFDerivAt f (βf') (g a) β (βαΆ (y : F) in nhds a, f (g y) = y) β HasStrictFDerivAt g (βf'.symm) a
This theorem states that if we have a function `f` from a normed vector space `E` to another normed vector space `F` and its local left inverse `g` (i.e., `f` composed with `g` equals the identity function around a point `a`), such that `g` is continuous at `a` and `f` has a strictly differentiable inverse `f'` at `g(a)`, then `g` has a derivative at `a`, which is the inverse of `f'`.
In other words, under these conditions, the derivative of the inverse function `g` exists and it's given by the inverse of the derivative of the function `f`. This is a part of the inverse function theorem, which essentially gives conditions under which an inverse function exists and is differentiable.
More concisely: If a function `f` from a normed vector space to another normed vector space has a local left inverse `g` that is continuous at `a`, and `f` has a strictly differentiable inverse `f'` at `g(a)`, then `g` has a derivative at `a` equal to the inverse of `f'`.
|
PartialHomeomorph.hasStrictFDerivAt_symm
theorem PartialHomeomorph.hasStrictFDerivAt_symm :
β {π : 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 : PartialHomeomorph E F) {f' : E βL[π] F} {a : F},
a β f.target β HasStrictFDerivAt (βf) (βf') (βf.symm a) β HasStrictFDerivAt (βf.symm) (βf'.symm) a
This theorem states that if `f` is a partial homeomorphism (a bijective function between an open subset of one topological space and an open subset of another) that is defined on a neighborhood of the inverse of `a` (`f.symm a`), and if `f` has an invertible derivative `f'` at `f.symm a` in the sense of strict differentiability, then the inverse of `f` (`f.symm`) has the derivative which is the inverse of `f'` (`f'.symm`) at `a`. This is a component of the inverse function theorem in the context of differentiable functions, and it assumes the existence of the inverse function.
More concisely: If `f` is a partial homeomorphism with strict differentiability at `x = f.symm a` such that `f'` is invertible, then `f.symm` has the derivative `(f'.symm)` at `a`.
|
ContinuousLinearEquiv.differentiableAt
theorem ContinuousLinearEquiv.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] {x : E}
(iso : E βL[π] F), DifferentiableAt π (βiso) x
The theorem `ContinuousLinearEquiv.differentiableAt` states that for any non-trivially normed field `π` and normed additive commutative groups `E` and `F` which are also normed spaces over `π`, and any point `x` in `E`, if there exists a continuous linear equivalence `iso` between `E` and `F`, then the function represented by this equivalence `(βiso)` is differentiable at point `x`. In other words, for a given continuous linear equivalence, the associated function has a derivative at every point in its domain.
More concisely: If `iso` is a continuous linear equivalence between normed spaces `E` and `F` over a non-trivially normed field `π`, then `(βiso)` is differentiable at every point `x` in `E`.
|
HasFDerivWithinAt.uniqueDiffWithinAt
theorem HasFDerivWithinAt.uniqueDiffWithinAt :
β {π : 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} {f' : E βL[π] F} {x : E},
HasFDerivWithinAt f f' s x β UniqueDiffWithinAt π s x β DenseRange βf' β UniqueDiffWithinAt π (f '' s) (f x)
The theorem `HasFDerivWithinAt.uniqueDiffWithinAt` states that given a non-trivially normed field `π`, and normed additive commutative groups `E` and `F` each equipped with a normed space structure over `π`, if you have a function `f` from `E` to `F`, a set `s` of elements in `E`, a continuous linear map `f'` from `E` to `F`, and a point `x` in `E`, then if `f` has a derivative within the set `s` at the point `x` that maps onto its target space (the range of `f'` is dense), and the set `s` has the unique differentiability property at `x`, then the image of the set `s` under the function `f` also has the unique differentiability property at the image point `f(x)`. In simpler terms, this theorem relates the unique differentiability of a set at a point to that of its image under a function with a dense derivative.
More concisely: Given a non-trivially normed field `π`, normed additive commutative groups `E` and `F` over `π`, a continuous linear map `f': E β F`, a function `f: E β F`, a set `s β E`, a point `x β E`, and if `f` has a dense derivative at `x` in `s` and `s` has the unique differentiability property at `x`, then the image of `s` under `f` also has the unique differentiability property at `f(x)`.
|
HasFDerivAt.of_local_left_inverse
theorem HasFDerivAt.of_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] {f : E β F}
{f' : E βL[π] F} {g : F β E} {a : F},
ContinuousAt g a β HasFDerivAt f (βf') (g a) β (βαΆ (y : F) in nhds a, f (g y) = y) β HasFDerivAt g (βf'.symm) a
The theorem `HasFDerivAt.of_local_left_inverse` states that if you have two functions `f` and `g`, where `f` is a function from a normed vector space `E` to another normed vector space `F` and `g` is a function from `F` to `E`, with a neighborhood around a point `a` in `F` such that `f (g y) = y` for all `y` in this neighborhood, and given that `g` is continuous at the point `a` and `f` has the derivative `f'` at point `g a`, which is a continuous linear map and is invertible, then `g` will have the derivative `f'β»ΒΉ` at point `a`. Here, `f'β»ΒΉ` represents the inverse of `f'`. This is a part of the inverse function theorem which assumes the existence of an inverse function.
More concisely: If `f: E β F` is a continuously differentiable function with invertible derivative `f'` at `a β F`, and `g: F β E` is a continuous function such that `g` maps a neighborhood of `a` to `{x β E | f(g(x)) = x}`, then `g` is differentiable at `a` and `g'(a) = (f'β»ΒΉ)(f'(a))`.
|
HasFDerivWithinAt.mapsTo_tangent_cone
theorem HasFDerivWithinAt.mapsTo_tangent_cone :
β {π : 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} {f' : E βL[π] F} {x : E},
HasFDerivWithinAt f f' s x β Set.MapsTo (βf') (tangentConeAt π s x) (tangentConeAt π (f '' s) (f x))
This theorem, `HasFDerivWithinAt.mapsTo_tangent_cone`, states that for a given function `f` from a normed vector space `E` to another normed vector space `F` over a nontrivially normed field `π`, if `f` has a derivative `f'` at a point `x` within a set `s` in `E`, then the image of the tangent cone at `x` in `s` under the linear map `f'` is contained within the tangent cone at the image of `x` under `f` in the image of `s` under `f`. In simpler terms, the differential of a function maps the tangent cone of a point within a set to the tangent cone of the image of the point within the image of the set.
More concisely: If a function between normed vector spaces has a derivative at a point within a set, then the image of the tangent cone at that point under the derivative is contained in the tangent cone of the image point under the function.
|