UniqueDiffWithinAt.uniqueMDiffWithinAt
theorem UniqueDiffWithinAt.uniqueMDiffWithinAt :
β {π : Type u_1} [inst : NontriviallyNormedField π] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {s : Set E} {x : E},
UniqueDiffWithinAt π s x β UniqueMDiffWithinAt (modelWithCornersSelf π E) s x
This theorem, known as an alias of the reverse direction of `uniqueMDiffWithinAt_iff_uniqueDiffWithinAt`, establishes a connection between the concepts of "unique differentiability" and "unique manifold differentiability". Specifically, it states that if a point `x` within a set `s` (which is a subset of a normed vector space `E` over a nontrivially normed field `π`) has the property of unique differentiability (`UniqueDiffWithinAt π s x`), then it also has the property of unique manifold differentiability (`UniqueMDiffWithinAt (modelWithCornersSelf π E) s x`). The unique manifold differentiability is expressed in the context of the "model with corners" constructed using the same vector space `E` as both the model and the target of the model.
More concisely: If a point in a subset of a normed vector space has unique differentiability, then it also has unique manifold differentiability in the context of the model with corners constructed using the same vector space.
|
HasMFDerivAt.hasFDerivAt
theorem HasMFDerivAt.hasFDerivAt :
β {π : Type u_1} [inst : NontriviallyNormedField π] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace π E']
{f : E β E'} {x : E}
{f' : TangentSpace (modelWithCornersSelf π E) x βL[π] TangentSpace (modelWithCornersSelf π E') (f x)},
HasMFDerivAt (modelWithCornersSelf π E) (modelWithCornersSelf π E') f x f' β HasFDerivAt f f' x
This theorem states that if a function `f` from a type `E` to a type `E'` has a manifold derivative at a point `x` in the sense of `HasMFDerivAt`, then it also has a Frechet derivative at that point in the sense of `HasFDerivAt`. Here, `π` represents a non-trivial normed field, `E` and `E'` are normed additive commutative groups over `π`, and `f'` is the derivative of `f` at `x`. The function `modelWithCornersSelf` constructs a model with corners, which is a space with additional structure that allows us to do calculus on manifolds. The "manifold derivative" is a generalization of the standard derivative concept to manifolds.
More concisely: If a function `f` from a normed additive commutative group `E` to another `E'`, over a non-trivial normed field, has a manifold derivative at a point `x` (in the sense of `HasMFDerivAt`), then it also has a Frechet derivative at `x` (in the sense of `HasFDerivAt`). In other words, `HasMFDerivAt f x` implies `HasFDerivAt f x`.
|
mdifferentiableAt_iff_differentiableAt
theorem mdifferentiableAt_iff_differentiableAt :
β {π : Type u_1} [inst : NontriviallyNormedField π] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace π E']
{f : E β E'} {x : E},
MDifferentiableAt (modelWithCornersSelf π E) (modelWithCornersSelf π E') f x β DifferentiableAt π f x
This theorem states that for maps between vector spaces, the property of being differentiable at a point according to the definition of `MDifferentiableAt` (using the concept of model with corners) is equivalent to being differentiable at that point as per the classic definition `DifferentiableAt`. In other words, a function from one vector space to another is differentiable at a certain point according to the manifold definition if and only if it is differentiable at that point in the traditional sense. Here, vector spaces are considered as manifolds with corners.
More concisely: For functions between vector spaces considered as manifolds with corners, the notions of differentiability at a point using `MDifferentiableAt` and `DifferentiableAt` definitions are equivalent.
|
Differentiable.mdifferentiable
theorem Differentiable.mdifferentiable :
β {π : Type u_1} [inst : NontriviallyNormedField π] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace π E']
{f : E β E'}, Differentiable π f β MDifferentiable (modelWithCornersSelf π E) (modelWithCornersSelf π E') f
This theorem, referred to as `Differentiable.mdifferentiable`, asserts that for maps between vector spaces, the properties of being `MDifferentiable` and `Differentiable` coincide. More specifically, it states that for any non-trivially normed field `π`, and any normed additive commutative groups `E` and `E'` which are also normed spaces over `π`, if a function `f` mapping `E` to `E'` is `Differentiable` over `π`, then `f` is also `MDifferentiable` with respect to the model with corners on `E` and `E'`.
More concisely: If a function between two normed vector spaces is differentiable, then it is also MDifferentiable with respect to the given norms.
|
MDifferentiableAt.differentiableAt
theorem MDifferentiableAt.differentiableAt :
β {π : Type u_1} [inst : NontriviallyNormedField π] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace π E']
{f : E β E'} {x : E},
MDifferentiableAt (modelWithCornersSelf π E) (modelWithCornersSelf π E') f x β DifferentiableAt π f x
This theorem, known as an alias of the forward direction of `mdifferentiableAt_iff_differentiableAt`, states that for maps between vector spaces, the properties `MDifferentiableAt` and `DifferentiableAt` coincide. In more specific terms, if a function `f` mapping from a vector space `E` to a vector space `E'` is manifold differentiable (`MDifferentiableAt`) at a point `x` in `E` under the model with corners being the vector spaces themselves, then `f` is also differentiable (`DifferentiableAt`) at the point `x`.
More concisely: If a function between vector spaces is manifold differentiable at a point, then it is differentiable at that point.
|
UniqueMDiffOn.uniqueDiffOn
theorem UniqueMDiffOn.uniqueDiffOn :
β {π : Type u_1} [inst : NontriviallyNormedField π] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {s : Set E}, UniqueMDiffOn (modelWithCornersSelf π E) s β UniqueDiffOn π s
The theorem `UniqueMDiffOn.uniqueDiffOn` states that for any nontrivially normed field `π`, any normed additive commutative group `E` which is also a normed space over `π`, and any set `s` of elements from `E`, if `s` is a Unique Differentiability Domain (i.e., every point in `s` has a unique differential structure) in the context of the model with corners mapping `E` to `E` over `π` (a mathematical structure used to define differential properties on manifolds), then `s` is also a Unique Differentiability Domain in the context of the field `π` alone. In other words, the uniqueness of differential structure on `s` in the more complex setting implies the uniqueness in the simpler setting.
More concisely: Given a nontrivially normed field `π`, a normed additive commutative group `E` over `π` that is a Unique Differentiability Domain as a normed space with respect to corners mapping, then `E` is a Unique Differentiability Domain as a normed space over `π`.
|
mdifferentiableWithinAt_iff_differentiableWithinAt
theorem mdifferentiableWithinAt_iff_differentiableWithinAt :
β {π : Type u_1} [inst : NontriviallyNormedField π] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace π E']
{f : E β E'} {s : Set E} {x : E},
MDifferentiableWithinAt (modelWithCornersSelf π E) (modelWithCornersSelf π E') f s x β
DifferentiableWithinAt π f s x
This theorem states that for maps between vector spaces, the properties of being differentiable, as defined by the Lean 4 functions `MDifferentiableWithinAt` and `DifferentiableWithinAt`, are equivalent. More specifically, a function `f` mapping from one vector space `E` to another vector space `E'` in the field `π` is differentiable at a point `x` within a set `s` in the sense of `MDifferentiableWithinAt` if and only if `f` is differentiable at `x` within `s` in the sense of `DifferentiableWithinAt`.
More concisely: The notions of differentiability with `MDifferentiableWithinAt` and `DifferentiableWithinAt` for a function between vector spaces are equivalent.
|
DifferentiableOn.mdifferentiableOn
theorem DifferentiableOn.mdifferentiableOn :
β {π : Type u_1} [inst : NontriviallyNormedField π] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace π E']
{f : E β E'} {s : Set E},
DifferentiableOn π f s β MDifferentiableOn (modelWithCornersSelf π E) (modelWithCornersSelf π E') f s
This theorem states that for a given map `f` between vector spaces `E` and `E'` over a non-trivially normed field `π`, if `f` is differentiable on a set `s` of `E`, then `f` is also differentiable in the manifold sense (`MDifferentiableOn`) on the set `s`. This statement is in the context of the model with corners associated with `E` and `E'`, which in this case are the vector spaces themselves. In other words, the concepts of differentiability and manifold differentiability coincide for maps between vector spaces.
More concisely: If `f` is a differentiable map between vector spaces `E` and `E'` over a non-trivially normed field `π`, then `f` is also manifold differentiable (`MDifferentiableOn`) on `E`.
|
mfderiv_eq_fderiv
theorem mfderiv_eq_fderiv :
β {π : Type u_1} [inst : NontriviallyNormedField π] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace π E']
{f : E β E'} {x : E}, mfderiv (modelWithCornersSelf π E) (modelWithCornersSelf π E') f x = fderiv π f x
This theorem states that for maps between vector spaces, the derivative in the manifold sense (`mfderiv`) is equivalent to the derivative in the usual sense (`fderiv`). More precisely, for any nontrivially normed field `π` and any two normed vector spaces `E` and `E'` over `π`, if `f` is a map from `E` to `E'` and `x` is a point in `E`, then the manifold derivative of `f` at `x` with respect to the model with corners associated to `π`, `E`, and `E'` is equal to the FrΓ©chet derivative of `f` at `x`.
More concisely: For any nontrivially normed field π and normed vector spaces E and E' over π, the manifold derivative (mfderiv) of a map f from E to E' at a point x is equal to the FrΓ©chet derivative (fderiv) of f at x.
|
HasFDerivWithinAt.hasMFDerivWithinAt
theorem HasFDerivWithinAt.hasMFDerivWithinAt :
β {π : Type u_1} [inst : NontriviallyNormedField π] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace π E']
{f : E β E'} {s : Set E} {x : E}
{f' : TangentSpace (modelWithCornersSelf π E) x βL[π] TangentSpace (modelWithCornersSelf π E') (f x)},
HasFDerivWithinAt f f' s x β HasMFDerivWithinAt (modelWithCornersSelf π E) (modelWithCornersSelf π E') f s x f'
This theorem states that, given a non-trivially normed field `π` and two normed vector spaces `E` and `E'` over `π`, if a function `f` from `E` to `E'` has a FrΓ©chet derivative `f'` at a point `x` within a set `s` of `E` (expressed as `HasFDerivWithinAt f f' s x`), then it also has a manifold derivative at the same point within the same set in the manifold context of these vector spaces being their own model with corners (expressed as `HasMFDerivWithinAt (modelWithCornersSelf π E) (modelWithCornersSelf π E') f s x f'`). Essentially, this theorem connects the concepts of FrΓ©chet and manifold derivatives, affirming that the existence of one implies the existence of the other under the given conditions.
More concisely: Given a non-trivially normed field `π` and normed spaces `E` and `E'` over `π`, if a function `f` from `E` to `E'` has a FrΓ©chet derivative at a point `x` within a set `s`, then it also has a manifold derivative at `x` within `s` in the context of `E` and `E'` being their own model with corners.
|
MDifferentiable.differentiable
theorem MDifferentiable.differentiable :
β {π : Type u_1} [inst : NontriviallyNormedField π] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace π E']
{f : E β E'}, MDifferentiable (modelWithCornersSelf π E) (modelWithCornersSelf π E') f β Differentiable π f
This theorem states that for any function `f` mapping between two vector spaces `E` and `E'` over a nontrivially normed field `π`, if `f` is `MDifferentiable` (meaning it is differentiable in the manifold sense, relative to the model with corners constructed from the vector spaces themselves), then `f` is also `Differentiable` (meaning it is differentiable at every point in the usual sense). In other words, for maps between vector spaces, the manifold differentiability and pointwise differentiability concepts coincide.
More concisely: If `f` is a `MDifferentiable` function between two vector spaces over a nontrivially normed field, then `f` is also `Differentiable`. (In other words, manifold differentiability implies pointwise differentiability for functions between vector spaces.)
|
HasFDerivAt.hasMFDerivAt
theorem HasFDerivAt.hasMFDerivAt :
β {π : Type u_1} [inst : NontriviallyNormedField π] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace π E']
{f : E β E'} {x : E}
{f' : TangentSpace (modelWithCornersSelf π E) x βL[π] TangentSpace (modelWithCornersSelf π E') (f x)},
HasFDerivAt f f' x β HasMFDerivAt (modelWithCornersSelf π E) (modelWithCornersSelf π E') f x f'
This theorem, an alias of the reverse direction of `hasMFDerivAt_iff_hasFDerivAt`, states that if a function `f` from `E` to `E'` has continuous linear map `f'` as its derivative at `x` in the context of a nontrivially normed field `π`, then `f` also has `f'` as its derivative in the manifold context at `x`, where `E` and `E'` are normed vector spaces over `π`, and `f'` is a linear map from the tangent space of `E` at `x` to the tangent space of `E'` at `f(x)`. This is also known as the manifold derivative at `x`, under the model with corners (which is a mathematical framework for defining manifolds with boundary) given by `modelWithCornersSelf π E` and `modelWithCornersSelf π E'`. The result is significant as it links the concept of derivatives in the settings of real analysis and differential geometry.
More concisely: If a function `f: E β E'` between normed vector spaces `E` and `E'` over a nontrivially normed field `π` has a continuous linear derivative `f'` at a point `x β E`, then `f` has derivative `f'` in the manifold context at `x`.
|
UniqueDiffOn.uniqueMDiffOn
theorem UniqueDiffOn.uniqueMDiffOn :
β {π : Type u_1} [inst : NontriviallyNormedField π] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {s : Set E}, UniqueDiffOn π s β UniqueMDiffOn (modelWithCornersSelf π E) s
This theorem, also known as the alias of the reverse direction of `uniqueMDiffOn_iff_uniqueDiffOn`, states that for any type `π` that forms a non-trivially normed field, and any type `E` that forms a normed additive commutative group and a normed space over `π`, if a set `s` of elements of type `E` possesses the property of `UniqueDiffOn π`, then it also possesses the property of `UniqueMDiffOn` when considered in the context of the model with corners `modelWithCornersSelf π E`.
In mathematical terms, this theorem links the concepts of unique differentiability on a set in the context of a given field with the more general concept of unique differentiability in a model with corners, a structure often used in differential geometry. In essence, if a set has unique differentiability properties with respect to a particular field, it retains those properties when viewed within a specific geometric framework (the model with corners).
More concisely: If a set of elements in a normed space over a non-trivially normed field possesses unique differentiability, then it also has unique mean value differentiability in the model with corners.
|
mdifferentiableOn_iff_differentiableOn
theorem mdifferentiableOn_iff_differentiableOn :
β {π : Type u_1} [inst : NontriviallyNormedField π] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace π E']
{f : E β E'} {s : Set E},
MDifferentiableOn (modelWithCornersSelf π E) (modelWithCornersSelf π E') f s β DifferentiableOn π f s
This theorem states that for maps between vector spaces, the condition of being MDifferentiableOn and the condition of being DifferentiableOn are equivalent. In other words, given a non-trivially normed field `π`, normed add commutative groups `E` and `E'`, normed spaces over `π` for `E` and `E'`, a function `f` from `E` to `E'`, and a set `s` of `E`, if the function `f` is MDifferentiableOn the model with corners `π` for `E` and `E'` and set `s`, then `f` is also DifferentiableOn `π`, `f` and `s`. The converse is also true. This means that in the context of vector spaces, both DifferentiableOn and MDifferentiableOn conditions can be used interchangeably.
More concisely: In the context of vector spaces over a non-trivially normed field, MDifferentiableOn and DifferentiableOn conditions are equivalent.
|
MDifferentiableOn.differentiableOn
theorem MDifferentiableOn.differentiableOn :
β {π : Type u_1} [inst : NontriviallyNormedField π] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace π E']
{f : E β E'} {s : Set E},
MDifferentiableOn (modelWithCornersSelf π E) (modelWithCornersSelf π E') f s β DifferentiableOn π f s
The theorem `MDifferentiableOn.differentiableOn` states that for functions mapping between vector spaces, the properties of being `MDifferentiableOn` and `DifferentiableOn` coincide. In more detail, given a nontrivial normed field `π`, vector spaces `E` and `E'` over `π`, a function `f` from `E` to `E'`, and a set `s` of elements in `E`, the theorem establishes that if `f` is `MDifferentiableOn` (i.e., differentiable in the manifold sense) on `s` with respect to the model with corners constructed from `π`, `E`, and `E'`, then `f` is also `DifferentiableOn` (i.e., differentiable in the traditional sense) on `s`.
More concisely: If a function between normed vector spaces is manifestly differentiable on a set using the manifold definition, then it is differentiable on that set using the traditional definition.
|
DifferentiableAt.mdifferentiableAt
theorem DifferentiableAt.mdifferentiableAt :
β {π : Type u_1} [inst : NontriviallyNormedField π] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace π E']
{f : E β E'} {x : E},
DifferentiableAt π f x β MDifferentiableAt (modelWithCornersSelf π E) (modelWithCornersSelf π E') f x
The theorem `DifferentiableAt.mdifferentiableAt` states that for maps between vector spaces, if a function `f` is differentiable at a point `x` under the field `π` (the field can be considered as a set which contains elements and these elements follow certain mathematical laws like addition, multiplication, etc.), then `f` is also `MDifferentiable` at point `x`. Here, `MDifferentiable` refers to differentiability in the manifold sense with respect to the model with corners, which in this case are the vector spaces themselves. This is essentially stating that the concepts of differentiability in the context of vector spaces and manifolds coincide.
More concisely: If a function between vector spaces is differentiable at a point, then it is MDifferentiable at that point.
|
mdifferentiable_iff_differentiable
theorem mdifferentiable_iff_differentiable :
β {π : Type u_1} [inst : NontriviallyNormedField π] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace π E']
{f : E β E'}, MDifferentiable (modelWithCornersSelf π E) (modelWithCornersSelf π E') f β Differentiable π f
This theorem states that for maps between vector spaces, the properties of being `MDifferentiable` and `Differentiable` are equivalent. To be more specific, in the context of a nontrivially normed field `π` and two normed vector spaces `E` and `E'` over `π`, a function `f` from `E` to `E'` is `MDifferentiable` with respect to the model-with-corners structure given by `modelWithCornersSelf π E` and `modelWithCornersSelf π E'` if and only if it is `Differentiable` over `π`.
More concisely: In the context of normed fields and vector spaces, a function is MDifferentiable if and only if it is Differentiable.
|
mfderivWithin_eq_fderivWithin
theorem mfderivWithin_eq_fderivWithin :
β {π : Type u_1} [inst : NontriviallyNormedField π] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace π E']
{f : E β E'} {s : Set E} {x : E},
mfderivWithin (modelWithCornersSelf π E) (modelWithCornersSelf π E') f s x = fderivWithin π f s x
This theorem states that for all maps between vector spaces, the Frechet derivative `fderivWithin` at a point within a set `s` coincides with the material derivative `mfderivWithin` at the same point within the same set `s`. This is true for any nontrivially normed field `π`, any normed additive commutative group `E` and `E'`, and any function `f` from `E` to `E'`. This result holds whether or not the space `E` or `E'` is equipped with a normed field structure.
More concisely: For any nontrivially normed field π, normed additive commutative groups E and E', and function f : E -> E' between them, the Frechet derivative fderivWithin of f at a point within set s in E is equal to the material derivative mfderivWithin of f at the same point within set s.
|
HasMFDerivWithinAt.hasFDerivWithinAt
theorem HasMFDerivWithinAt.hasFDerivWithinAt :
β {π : Type u_1} [inst : NontriviallyNormedField π] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace π E']
{f : E β E'} {s : Set E} {x : E}
{f' : TangentSpace (modelWithCornersSelf π E) x βL[π] TangentSpace (modelWithCornersSelf π E') (f x)},
HasMFDerivWithinAt (modelWithCornersSelf π E) (modelWithCornersSelf π E') f s x f' β HasFDerivWithinAt f f' s x
This theorem, which is an alias for the forward direction of `hasMFDerivWithinAt_iff_hasFDerivWithinAt`, states that if a function `f` from a normed space `E` to another normed space `E'` over a non-trivially normed field `π` has the manifold derivative `f'` at a point `x` within a set `s` in the context of the `modelWithCornersSelf` model, then `f` also has the FrΓ©chet derivative `f'` at the same point `x` within the same set `s`. Hence, this theorem provides a connection between the manifold and FrΓ©chet derivatives in a specific mathematical context.
More concisely: If a function `f` from a normed space `E` to another normed space `E'` over a non-trivially normed field `π` has the manifold derivative `f'` at a point `x` within a set `s`, then `f` also has the FrΓ©chet derivative `f'` at `x` within `s`.
|
MDifferentiableWithinAt.differentiableWithinAt
theorem MDifferentiableWithinAt.differentiableWithinAt :
β {π : Type u_1} [inst : NontriviallyNormedField π] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace π E']
{f : E β E'} {s : Set E} {x : E},
MDifferentiableWithinAt (modelWithCornersSelf π E) (modelWithCornersSelf π E') f s x β
DifferentiableWithinAt π f s x
The theorem `MDifferentiableWithinAt.differentiableWithinAt` establishes that for any function `f` mapping between two vector spaces `E` and `E'` over a nontrivially normed field `π`, if `f` is differentiable within a set `s` at a point `x` in the sense of the manifold-with-boundary definition (`MDifferentiableWithinAt`), then `f` is also differentiable at `x` within `s` in the sense of the standard calculus definition (`DifferentiableWithinAt`). This theorem is essentially an alias for the forward direction of `mdifferentiableWithinAt_iff_differentiableWithinAt`, stating the equivalence of two differentiable definitions in the context of maps between vector spaces.
More concisely: If a function between vector spaces is differentiable within a set in the manifold-with-boundary sense, then it is also differentiable within that set in the standard calculus sense.
|
Mathlib.Geometry.Manifold.MFDeriv.FDeriv._auxLemma.1
theorem Mathlib.Geometry.Manifold.MFDeriv.FDeriv._auxLemma.1 :
β {π : Type u_1} [inst : NontriviallyNormedField π] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {s : Set E} {x : E},
UniqueMDiffWithinAt (modelWithCornersSelf π E) s x = UniqueDiffWithinAt π s x
This theorem states that for any given type `π` which forms a nontrivially normed field, and any type `E` which is a normed additive commutative group and also a normed space over `π`, the property of having a unique differential within a set `s` at a point `x` is equivalent in the context of the natural model with corners in `E` and the context of `π`. In simpler terms, it means that the uniqueness of differentiation within a certain set at a point remains the same whether you view it in its own space or in the larger ambient space.
More concisely: For any nontrivially normed field `π` and a normed additive commutative group `E` over `π` with the same norm as a normed space, the uniqueness of differentiation at a point `x` in `E` holds if and only if it does in `E`'s subspace structure in `π`.
|
DifferentiableWithinAt.mdifferentiableWithinAt
theorem DifferentiableWithinAt.mdifferentiableWithinAt :
β {π : Type u_1} [inst : NontriviallyNormedField π] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace π E']
{f : E β E'} {s : Set E} {x : E},
DifferentiableWithinAt π f s x β
MDifferentiableWithinAt (modelWithCornersSelf π E) (modelWithCornersSelf π E') f s x
This theorem, known as `DifferentiableWithinAt.mdifferentiableWithinAt`, states that for a certain map `f` between vector spaces `E` and `E'` over a nontrivially normed field `π`, if `f` is differentiable at a point `x` within a set `s` (expressed as `DifferentiableWithinAt π f s x`), then `f` is also "smoothly" differentiable at that same point within the same set (expressed as `MDifferentiableWithinAt (modelWithCornersSelf π E) (modelWithCornersSelf π E') f s x`). In other words, in the context of maps between vector spaces, standard differentiability and smooth differentiability coincide.
More concisely: If a map between vector spaces is differentiable with the given conditions at a point within a set, then it is smoothly differentiable at that same point within the same set.
|
UniqueMDiffWithinAt.uniqueDiffWithinAt
theorem UniqueMDiffWithinAt.uniqueDiffWithinAt :
β {π : Type u_1} [inst : NontriviallyNormedField π] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {s : Set E} {x : E},
UniqueMDiffWithinAt (modelWithCornersSelf π E) s x β UniqueDiffWithinAt π s x
The theorem `UniqueMDiffWithinAt.uniqueDiffWithinAt` states that under certain conditions, if a point `x` in a set `s` of a vector space `E` over a nontrivially normed field `π` has the property of being uniquely differentiable (in the sense of having a unique differential at `x` within the set `s`), when the vector space is considered as a model with corners, then `x` also has the property of being uniquely differentiable within `s` in the usual sense. The conditions include that the field `π` is nontrivially normed, and the vector space `E` is a normed additive commutative group and a normed space over `π`. This theorem is an alias for the forward direction of another theorem `uniqueMDiffWithinAt_iff_uniqueDiffWithinAt`.
More concisely: Given a nontrivially normed field `π` and a normed additive commutative group `E` over `π`, if a point `x` in `E` has a unique differential at `x` within `E` when considered as a model with corners, then `x` has a unique differential at `x` in the usual sense.
|