TangentBundle.tangentMap_tangentBundle_pure
theorem TangentBundle.tangentMap_tangentBundle_pure :
∀ {𝕜 : 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] [Is : SmoothManifoldWithCorners I M]
(p : TangentBundle I M),
tangentMap I I.tangent (Bundle.zeroSection E (TangentSpace I)) p =
{ proj := { proj := p.proj, snd := 0 }, snd := (p.snd, 0) }
This theorem is about the derivative of the zero section of the tangent bundle. More precisely, it states that for a smooth manifold with corners `M`, under certain conditions, the derivative of the zero section of the tangent bundle at a point `p`, represented as a pair `⟨x, v⟩`, is mapped to a pair `⟨⟨x, 0⟩, ⟨v, 0⟩⟩`. Although the statement is currently framed in coordinates, the result is coordinate-dependent only to the extent that the coordinates determine a splitting of the tangent bundle. Also, there is a canonical splitting at each point of the zero section, arising from the coordinates on the tangent bundle in our definitions. So this statement is not as arbitrary as it may first appear. Note: it would be beneficial to define splittings of vector bundles and state this result in an invariant manner in future work.
More concisely: The derivative of the zero section of a smooth manifold with corners's tangent bundle maps points `⟨x, v⟩` to `⟨⟨x, 0⟩, ⟨v, 0⟩⟩`.
|
ContMDiff.continuous_tangentMap
theorem ContMDiff.continuous_tangentMap :
∀ {𝕜 : 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] [Is : SmoothManifoldWithCorners I 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'] [I's : SmoothManifoldWithCorners I' M'] {f : M → M'} {n : ℕ∞},
ContMDiff I I' n f → 1 ≤ n → Continuous (tangentMap I I' f)
The theorem `ContMDiff.continuous_tangentMap` states that if a function `f` is continuously differentiable up to order `n` (`C^n`), with `n` being greater than or equal to 1, in a smooth manifold context, then the tangent map of this function is continuous. The manifold context is represented by types `M` and `M'`, the model with corners `I` and `I'`, along with the normed fields and spaces, and topological spaces they are subjected to.
More concisely: If `f` is a continuously differentiable function of class `C^n` (`n ≥ 1`) on smooth manifolds `M` and `M'`, then the tangent map of `f` is a continuous linear map.
|
ContMDiffAt.mfderiv_const
theorem ContMDiffAt.mfderiv_const :
∀ {𝕜 : 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] [Is : SmoothManifoldWithCorners I 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'] [I's : SmoothManifoldWithCorners I' M'] {m n : ℕ∞} {x₀ : M} {f : M → M'},
ContMDiffAt I I' n f x₀ →
m + 1 ≤ n →
ContMDiffAt I (modelWithCornersSelf 𝕜 (E →L[𝕜] E')) m (inTangentCoordinates I I' id f (mfderiv I I' f) x₀)
x₀
This theorem states that for a given function `f` mapping from a smooth manifold `M` to another smooth manifold `M'`, if `f` is continuously differentiable up to order `n` at a point `x₀`, and `n` is at least `m + 1`, then the derivative of `f` at `x₀`, denoted as `D_yf(y)`, is also continuously differentiable up to order `m`. The derivative here is taken as a continuous linear map. A coordinate change from `x₀` to `x` is inserted to make the derivative sensible. This is a specific case of the `ContMDiffAt.mfderiv` theorem where `f` does not contain any parameters and the function `g` is the identity function. The underlying field is a nontrivially normed field `𝕜`, `E` and `E'` are normed vector spaces over `𝕜`, and the manifolds `M` and `M'` are equipped with topological structures and charts making them into smooth manifolds with corners.
More concisely: If a continuously differentiable up to order n function f from a smooth manifold M to another smooth manifold M' is of class C^(m+1) at a point x0, then the derivative D_xfr(x0) of f at x0 is a continuously differentiable up to order m linear map.
|
ContMDiffOn.continuousOn_tangentMapWithin_aux
theorem ContMDiffOn.continuousOn_tangentMapWithin_aux :
∀ {𝕜 : 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}
{E' : Type u_5} [inst_4 : NormedAddCommGroup E'] [inst_5 : NormedSpace 𝕜 E'] {H' : Type u_6}
[inst_6 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {n : ℕ∞} {f : H → H'} {s : Set H},
ContMDiffOn I I' n f s →
1 ≤ n → UniqueMDiffOn I s → ContinuousOn (tangentMapWithin I I' f s) (Bundle.TotalSpace.proj ⁻¹' s)
The theorem `ContMDiffOn.continuousOn_tangentMapWithin_aux` asserts that if a function `f` from a topological space `H` to another topological space `H'` is `C^n` continuous (meaning that it has continuous derivatives up to order `n`) on a set `s` within `H`, where `1 ≤ n` and `s` has unique derivatives, then the bundled derivative of `f` is continuous on the preimage of `s` under the canonical projection from the total space to the base space. This theorem is a preparatory step towards a more general statement, and it assumes that `H` and `H'` are model spaces within a model with corners, a specific mathematical structure used in the analysis of manifolds.
More concisely: If a `C^n` function `f` with unique derivatives on a set `s` in a model space `H` with corners has a continuous bundled derivative, then the bundled derivative is continuous on the preimage of `s` under the canonical projection from the total space to the base space.
|
ContMDiffOn.continuousOn_tangentMapWithin
theorem ContMDiffOn.continuousOn_tangentMapWithin :
∀ {𝕜 : 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] [Is : SmoothManifoldWithCorners I 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'] [I's : SmoothManifoldWithCorners I' M'] {f : M → M'} {s : Set M} {n : ℕ∞},
ContMDiffOn I I' n f s →
1 ≤ n → UniqueMDiffOn I s → ContinuousOn (tangentMapWithin I I' f s) (Bundle.TotalSpace.proj ⁻¹' s)
The theorem `ContMDiffOn.continuousOn_tangentMapWithin` states that if a function `f` mapping from a manifold `M` to another manifold `M'` is continuously differentiable up to order `n` (`ContMDiffOn`) on a set `s` within manifold `M`, and this set `s` has unique derivatives (`UniqueMDiffOn`), then the bundled derivative of `f` on `s` (captured by the `tangentMapWithin` function) is continuous (`ContinuousOn`) on `s`, when projected from the total space to the base space (`Bundle.TotalSpace.proj`). This is under certain conditions: firstly, the order of differentiability `n` is at least `1`. Additionally, the manifolds `M` and `M'` are equipped with certain structures, including being associated with topological spaces and smooth structures (`SmoothManifoldWithCorners`), and the spaces on which the manifolds are modeled are normed spaces (`NormedSpace`) over a nontrivially normed field.
More concisely: If a continuously differentiable up to order `n` (`ContMDiffOn`) function `f : M → M'` between manifolds `M` and `M'`, with unique derivatives on a set `s ⊆ M`, has a continuous bundled derivative on `s` when projected to the base space (`Bundle.TotalSpace.proj (tangentMapWithin f s)`), then `n ≥ 1`, `M` and `M'` are SmoothManifoldWithCorners over NormedSpaces, and `s` is open in `M`.
|
ContMDiffOn.contMDiffOn_tangentMapWithin_aux
theorem ContMDiffOn.contMDiffOn_tangentMapWithin_aux :
∀ {𝕜 : 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}
{E' : Type u_5} [inst_4 : NormedAddCommGroup E'] [inst_5 : NormedSpace 𝕜 E'] {H' : Type u_6}
[inst_6 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {m n : ℕ∞} {f : H → H'} {s : Set H},
ContMDiffOn I I' n f s →
m + 1 ≤ n →
UniqueMDiffOn I s →
ContMDiffOn I.tangent I'.tangent m (tangentMapWithin I I' f s) (Bundle.TotalSpace.proj ⁻¹' s)
The theorem `ContMDiffOn.contMDiffOn_tangentMapWithin_aux` states that if a function `f` is `C^n` differentiable on a set `s`, where all points have unique derivatives (conditions given by `ContMDiffOn I I' n f s` and `UniqueMDiffOn I s`), then the bundled derivative of this function (expressed by `tangentMapWithin I I' f s`) is `C^m` differentiable whenever `m+1` is less than or equal to `n`. Note that `m` and `n` are of type `ℕ∞`, indicating they are natural numbers or infinity. This theorem is proved in the context where the source (`H`) and target space (`H'`) are model spaces in models with corners and it is an auxiliary step for the general fact which is proved in `ContMDiffOn.contMDiffOn_tangentMapWithin`. The theorem further specifies that the domain of the bundled derivative is the inverse image of `s` under the projection from the total space to the base space, denoted by `(Bundle.TotalSpace.proj ⁻¹' s)`.
More concisely: If a function `f` is `C^n` differentiable on a set `s` with unique derivatives, then the bundled derivative `tangentMapWithin s (Bundle.TotalSpace.proj) f` is `C^m` differentiable whenever `m+1` is less than or equal to `n`.
|
ContMDiff.contMDiff_tangentMap
theorem ContMDiff.contMDiff_tangentMap :
∀ {𝕜 : 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] [Is : SmoothManifoldWithCorners I 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'] [I's : SmoothManifoldWithCorners I' M'] {f : M → M'} {m n : ℕ∞},
ContMDiff I I' n f → m + 1 ≤ n → ContMDiff I.tangent I'.tangent m (tangentMap I I' f)
The theorem `ContMDiff.contMDiff_tangentMap` states that, given a function `f` between two smooth manifolds `M` and `M'`, if `f` is differentiable to class `C^n`, then the tangent map of `f` (which associates to each point of the manifold its image under `f` and to each tangent vector its derivative under `d(f)`) is differentiable to class `C^m` as long as `m + 1 ≤ n`. Here, `C^n` refers to the class of functions which have continuous derivatives up to order `n`, and `m` and `n` could be finite natural numbers or infinity.
More concisely: If `f` is a `C^n` differentiable function between smooth manifolds `M` and `M'`, then its tangent map is `C^m` differentiable with `m + 1 <= n`.
|