MDifferentiableAt.mdifferentiableWithinAt
theorem MDifferentiableAt.mdifferentiableWithinAt :
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H}
{M : Type u_4} [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5}
[inst_6 : NormedAddCommGroup E'] [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M']
{f : M → M'} {x : M} {s : Set M}, MDifferentiableAt I I' f x → MDifferentiableWithinAt I I' f s x
This theorem, `MDifferentiableAt.mdifferentiableWithinAt`, states that within any non-trivially normed field and for any selection of normed additive commutative groups, normed spaces, topologies, charts, models with corners, and a function `f` from `M` to `M'`, if `f` is differentiable at a point `x` in `M` under the models with corners `I` and `I'`, then `f` is also differentiable within any set `s` in `M` at the same point `x` under the same models. In mathematical terms, it asserts local differentiability implies differentiability within a subset.
More concisely: If a function is differentiable at a point in a normed space under certain models with corners, then it is differentiable within any subset of the space at that point under the same models.
|
HasMFDerivWithinAt.mdifferentiableWithinAt
theorem HasMFDerivWithinAt.mdifferentiableWithinAt :
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H}
{M : Type u_4} [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5}
[inst_6 : NormedAddCommGroup E'] [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M']
{f : M → M'} {x : M} {s : Set M} [Is : SmoothManifoldWithCorners I M] [I's : SmoothManifoldWithCorners I' M']
{f' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)},
HasMFDerivWithinAt I I' f s x f' → MDifferentiableWithinAt I I' f s x
This theorem states that for any non-trivially normed field `𝕜`, normed additive commutative groups `E` and `E'`, normed spaces `𝕜 E` and `𝕜 E'`, topological spaces `H`, `M`, `H'`, and `M'`, models with corners `I`, `I'`, charted spaces `H M`, `H' M'`, function `f` from `M` to `M'`, point `x` in `M`, a set `s` of `M`, and smooth manifolds with corners `I M` and `I' M'`, if a function `f` has a manifold derivative within a set `s` at point `x` (as captured by `HasMFDerivWithinAt I I' f s x f'`), then the function `f` is manifold differentiable within the set `s` at the point `x` (as captured by `MDifferentiableWithinAt I I' f s x`). This theorem thus establishes a relationship between having a manifold derivative and being manifold differentiable at a given point within a set in the context of differential geometry.
More concisely: If a function between smooth manifolds with corners has a manifold derivative within a set at a point, then it is manifold differentiable within that set at the point.
|
mdifferentiableWithinAt_iff_of_mem_source
theorem mdifferentiableWithinAt_iff_of_mem_source :
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H}
{M : Type u_4} [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5}
[inst_6 : NormedAddCommGroup E'] [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M']
{f : M → M'} {x : M} {s : Set M} [Is : SmoothManifoldWithCorners I M] [I's : SmoothManifoldWithCorners I' M']
{x' : M} {y : M'},
x' ∈ (chartAt H x).source →
f x' ∈ (chartAt H' y).source →
(MDifferentiableWithinAt I I' f s x' ↔
ContinuousWithinAt f s x' ∧
DifferentiableWithinAt 𝕜 (↑(extChartAt I' y) ∘ f ∘ ↑(extChartAt I x).symm)
(↑(extChartAt I x).symm ⁻¹' s ∩ Set.range ↑I) (↑(extChartAt I x) x'))
This theorem states that for any non-trivially normed field 𝕜, normed additive commutative groups E and E', normed spaces 𝕜 E and 𝕜 E', topological spaces H, M, H', and M', model spaces with corners I (from E to H) and I' (from E' to H'), charted spaces M and M' on topological spaces H and H' respectively, a function f from M to M', a point x in M, a set s of M, smooth manifolds with corners I M and I' M', and points x' in M and y in M' such that x' is in the source of the chart at x, and f(x') is in the source of the chart at y: f is differentiable within the set s at the point x' if and only if f is continuous within s at x' and the composition of the extension of the chart at y with f and the inversion of the extension of the chart at x is differentiable within the preimage of s under the inversion of the extension of the chart at x intersected with the range of I at the extension of the chart at x applied to x'.
More concisely: For any non-trivially normed fields 𝕜, normed additive commutative groups E and E', topological spaces H and H', smooth manifolds with corners I, M, and I' M', and functions f from M to M' between their charted spaces, if x is a point in M, s is a set in M, and x' is in the source of the chart at x with image y in the source of the chart at y, then f is differentiable at x' within the set s if and only if f is continuous at x' within s and the composite of the inversions of the extensions of the charts at x and y, followed by f, is differentiable at the point in the preimage of x' under the inversion of the extension of the chart at x intersected with the range of I at the extension of the chart at x.
|
HasMFDerivAt.hasMFDerivWithinAt
theorem HasMFDerivAt.hasMFDerivWithinAt :
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H}
{M : Type u_4} [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5}
[inst_6 : NormedAddCommGroup E'] [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M']
{f : M → M'} {x : M} {s : Set M} [Is : SmoothManifoldWithCorners I M] [I's : SmoothManifoldWithCorners I' M']
{f' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)},
HasMFDerivAt I I' f x f' → HasMFDerivWithinAt I I' f s x f'
This theorem states that, given a non-trivially normed field `𝕜`, normed additive commutative groups `E` and `E'`, topological spaces `H`, `M`, `H'`, and `M'`, a model with corners `I` between `𝕜`, `E`, and `H`, a model with corners `I'` between `𝕜`, `E'`, and `H'`, charted spaces `M` and `M'` with `H` and `H'` respectively, a function `f` from `M` to `M'`, a point `x` in `M`, a set `s` of `M`, smooth manifolds `M` and `M'` with corners `I` and `I'` respectively, and a derivative `f'` of `f` at `x`, if `f` has a manifold derivative at `x`, then `f` also has a manifold derivative within the set `s` at `x`.
More concisely: Given a smooth function `f` between smooth manifolds `M` and `M'`, with `M` and `M'` having corners `I` and `I'`, respectively, and `f` having a manifold derivative at a point `x` in `M`, then `f` also has a manifold derivative within any set `s` in `M` containing `x`.
|
mfderiv_congr_point
theorem mfderiv_congr_point :
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H}
{M : Type u_4} [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5}
[inst_6 : NormedAddCommGroup E'] [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M']
{f : M → M'} {x : M} [Is : SmoothManifoldWithCorners I M] [I's : SmoothManifoldWithCorners I' M'] {x' : M},
x = x' → mfderiv I I' f x = mfderiv I I' f x'
The theorem `mfderiv_congr_point` states that for a given smooth function `f` from a manifold `M` to another manifold `M'`, and two points `x` and `x'` in `M`, if `x` and `x'` are the same point (i.e., `x = x'`), then the `mfderiv` (the derivative of `f` in the manifold sense) of `f` at `x` is equal to the `mfderiv` of `f` at `x'`. It essentially states that the derivative at a point is independent of the particular label we use for that point. This theorem holds in the context of differentiable manifolds modeled on normed vector spaces over a nontrivially normed field.
More concisely: For smooth functions between differentiable manifolds modeled on normed vector spaces, the derivative of a function at two identical points is equal.
|
UniqueMDiffWithinAt.eq
theorem UniqueMDiffWithinAt.eq :
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H}
{M : Type u_4} [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5}
[inst_6 : NormedAddCommGroup E'] [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M']
{f : M → M'} {x : M} {s : Set M} [Is : SmoothManifoldWithCorners I M] [I's : SmoothManifoldWithCorners I' M']
{f' f₁' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)},
UniqueMDiffWithinAt I s x → HasMFDerivWithinAt I I' f s x f' → HasMFDerivWithinAt I I' f s x f₁' → f' = f₁'
This theorem states that if there exists a unique maximal differentiable structure within a set `s` at a point `x` in a smooth manifold `M`, and if there are two possible derivatives `f'` and `f₁'` of a function `f` mapping this manifold to another smooth manifold `M'` within the set `s` at the point `x`, then these two derivatives must be equal. The hypothesis is that the function `f` has maximal Frechet Derivative (MFDeriv) within the set `s` at the point `x` for both possible derivatives `f'` and `f₁'`. The theorem is applicable for manifolds `M` and `M'` with any non-trivially normed field and under the model with corners `I` and `I'`. The manifolds are endowed with normed addition commutative group structures and normed spaces, and their topologies are generated by the model with corners.
More concisely: If two derivatives of a function between smooth manifolds exist and have maximal Frechet Derivatives within a set at a point, then they are equal.
|
HasMFDerivAt.mfderiv
theorem HasMFDerivAt.mfderiv :
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H}
{M : Type u_4} [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5}
[inst_6 : NormedAddCommGroup E'] [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M']
{f : M → M'} {x : M} [Is : SmoothManifoldWithCorners I M] [I's : SmoothManifoldWithCorners I' M']
{f' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)}, HasMFDerivAt I I' f x f' → mfderiv I I' f x = f'
This theorem states that for a function `f` mapping one smooth manifold `M` to another `M'`, under the conditions established by certain structures (such as `NontriviallyNormedField`, `NormedAddCommGroup`, `NormedSpace`, `TopologicalSpace`, `ModelWithCorners`, `ChartedSpace`, `SmoothManifoldWithCorners`), if `f` has a manifold derivative `f'` at a point `x` in `M` (expressed as `HasMFDerivAt`), then the manifold derivative of `f` at `x` (expressed as `mfderiv`) equals `f'`. In other words, if `f` has a certain manifold derivative at a point, that derivative is the manifold derivative at that point.
More concisely: Given a smooth manifold function `f : M → M'` between two smooth manifolds `M` and `M'`, if `f` has a manifold derivative `HasMFDerivAt f x` at a point `x ∈ M`, then the manifold derivative `mfderiv f x` of `f` at `x` equals `f'`.
|
MDifferentiableAt.hasMFDerivAt
theorem MDifferentiableAt.hasMFDerivAt :
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H}
{M : Type u_4} [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5}
[inst_6 : NormedAddCommGroup E'] [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M']
{f : M → M'} {x : M} [Is : SmoothManifoldWithCorners I M] [I's : SmoothManifoldWithCorners I' M'],
MDifferentiableAt I I' f x → HasMFDerivAt I I' f x (mfderiv I I' f x)
This theorem states that, given a nontrivially normed field `𝕜`, normed additive commutative groups `E` and `E'`, normed spaces over `𝕜` for `E` and `E'`, topological spaces `H`, `M`, `H'`, `M'`, models with corners `I` and `I'`, with `M` and `M'` being charted spaces with respect to `H` and `H'` respectively, a function `f` mapping `M` to `M'`, and a point `x` in `M`, if `f` is differentiable at `x` (in the sense of manifolds, denoted by `MDifferentiableAt I I' f x`), then `f` has a manifold derivative at `x` (denoted by `HasMFDerivAt I I' f x (mfderiv I I' f x)`). The manifolds `M` and `M'` are assumed to be smooth with corners with respect to the corresponding models with corners `I` and `I'`.
More concisely: Given a nontrivially normed field `𝕜`, normed additive commutative groups `E` and `E'`, topological spaces `H`, `M`, `H'`, `M'`, models with corners `I` and `I'`, smooth manifolds with corners `M` and `M'`, a differentiable function `f` from `M` to `M'` at point `x` in `M`, then `f` has a manifold derivative `mfderiv I I' f x` at `x`.
|
mfderiv_congr
theorem mfderiv_congr :
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H}
{M : Type u_4} [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5}
[inst_6 : NormedAddCommGroup E'] [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M']
{f : M → M'} {x : M} [Is : SmoothManifoldWithCorners I M] [I's : SmoothManifoldWithCorners I' M'] {f' : M → M'},
f = f' → mfderiv I I' f x = mfderiv I I' f' x
This theorem, `mfderiv_congr`, is a congruence lemma for `mfderiv`, a term in Lean 4 representing the derivative of a function between manifolds. The theorem states that for any two functions `f` and `f'` from a manifold `M` to another manifold `M'`, if `f` and `f'` are equal, then the derivatives of `f` and `f'` at a point `x` in `M` are also equal. The manifolds `M` and `M'` are smooth (i.e., infinitely differentiable), as specified by the `SmoothManifoldWithCorners` instances `Is` and `I's`. Further, the spaces `E` and `E'` are normed additively commutative groups over a nontrivially normed field `𝕜` and can be thought of as the tangent spaces at the points in `M` and `M'`.
More concisely: If `f` and `f'` are equal smooth functions from a smooth manifold `M` to another smooth manifold `M'`, then their derivatives at any point `x` in `M` are equal, where the derivatives are taken in the tangent spaces of `M` and `M'`.
|
HasMFDerivAt.mdifferentiableAt
theorem HasMFDerivAt.mdifferentiableAt :
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H}
{M : Type u_4} [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5}
[inst_6 : NormedAddCommGroup E'] [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M']
{f : M → M'} {x : M} [Is : SmoothManifoldWithCorners I M] [I's : SmoothManifoldWithCorners I' M']
{f' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)}, HasMFDerivAt I I' f x f' → MDifferentiableAt I I' f x
This theorem states that given a smooth manifold with corners `I` and `I'` over a non-trivially normed field `𝕜`, if there is a function `f` from manifold `M` to `M'` that has a manifold derivative `f'` at a point `x` in `M` (i.e., `HasMFDerivAt I I' f x f'`), then `f` is differentiable at `x` in the manifold sense (i.e., `MDifferentiableAt I I' f x`). In other words, having a manifold derivative implies manifold differentiability.
More concisely: A smooth manifold function `f` with manifold derivatives at a point `x` implies `f` is differentiable at `x` in the manifold sense.
|