contMDiff_iff_target
theorem contMDiff_iff_target :
∀ {𝕜 : 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] [inst_6 : SmoothManifoldWithCorners I M]
{E' : Type u_5} [inst_7 : NormedAddCommGroup E'] [inst_8 : NormedSpace 𝕜 E'] {H' : Type u_6}
[inst_9 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [inst_10 : TopologicalSpace M']
[inst_11 : ChartedSpace H' M'] [inst_12 : SmoothManifoldWithCorners I' M'] {f : M → M'} {n : ℕ∞},
ContMDiff I I' n f ↔
Continuous f ∧
∀ (y : M'),
ContMDiffOn I (modelWithCornersSelf 𝕜 E') n (↑(extChartAt I' y) ∘ f) (f ⁻¹' (extChartAt I' y).source)
The theorem `contMDiff_iff_target` states that for a function `f` from a smooth manifold `M` to another smooth manifold `M'`, both equipped with specific model with corners `I` and `I'` respectively, and for any `n` in ℕ∞, the function is continuously differentiable up to order `n` iff it is continuous and for all points `y` in `M'`, the composition of `f` with the extension of `I'` at `y` is continuously differentiable on the preimage of the source of this extension under `f`. Here, both manifolds, `M` and `M'`, are modeled on normed add commutative groups `E` and `E'` over a nontrivially normed field `𝕜`, and their topological spaces are `H` and `H'` respectively.
More concisely: A smooth function between smooth manifolds is continuously differentiable up to order n if and only if it is continuous and the composition with the extension of the target manifold at each point is continuously differentiable on the preimage of the extension's source under the function.
|
contMDiffOn_iff_target
theorem contMDiffOn_iff_target :
∀ {𝕜 : 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] [inst_6 : SmoothManifoldWithCorners I M]
{E' : Type u_5} [inst_7 : NormedAddCommGroup E'] [inst_8 : NormedSpace 𝕜 E'] {H' : Type u_6}
[inst_9 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [inst_10 : TopologicalSpace M']
[inst_11 : ChartedSpace H' M'] [inst_12 : SmoothManifoldWithCorners I' M'] {f : M → M'} {s : Set M} {n : ℕ∞},
ContMDiffOn I I' n f s ↔
ContinuousOn f s ∧
∀ (y : M'),
ContMDiffOn I (modelWithCornersSelf 𝕜 E') n (↑(extChartAt I' y) ∘ f) (s ∩ f ⁻¹' (extChartAt I' y).source)
This theorem states that for a given function `f` between two smooth manifolds `M` and `M'` with ModelWithCorners `I` and `I'` respectively, and a set `s` in `M`, the function `f` is continuously differentiable on `s` if and only if two conditions are met. First, `f` is continuous on `s`, and second, for every point `y` in `M'`, the function `f`, when composed with the extension chart at `y` and restricted to `s` intersected with the preimage of the extension chart at `y`'s source under `f`, is continuously differentiable. The continuous differentiability in the second condition is defined with respect to the model with corners of `𝕜` and `E'` and the same `n`, which is the number of times derivatives are allowed to be taken.
More concisely: A smooth function between smooth manifolds with ModelWithCorners is continuously differentiable on a subset if and only if it is continuous on that subset and the restriction of its compositions with extension charts is continuously differentiable with respect to the corresponding ModelWithCorners.
|
ContMDiff.continuous
theorem ContMDiff.continuous :
∀ {𝕜 : 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'} {n : ℕ∞}, ContMDiff I I' n f → Continuous f
The theorem `ContMDiff.continuous` states that for any function `f` from a manifold `M` to another manifold `M'`, given certain conditions on the underlying field, additional vector spaces, and topological spaces (including the charted spaces), if `f` is continuously differentiable to any order `n` (possibly infinite), then `f` is also a continuous function. This means that any function that has derivatives of all orders (up to `n`) that are continuous also preserves the property of continuity itself.
More concisely: If a continuously differentiable function `f` from manifold `M` to manifold `M'` satisfies given conditions, then `f` is continuous.
|
contMDiffOn_iff
theorem contMDiffOn_iff :
∀ {𝕜 : 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] [inst_6 : SmoothManifoldWithCorners I M]
{E' : Type u_5} [inst_7 : NormedAddCommGroup E'] [inst_8 : NormedSpace 𝕜 E'] {H' : Type u_6}
[inst_9 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [inst_10 : TopologicalSpace M']
[inst_11 : ChartedSpace H' M'] [inst_12 : SmoothManifoldWithCorners I' M'] {f : M → M'} {s : Set M} {n : ℕ∞},
ContMDiffOn I I' n f s ↔
ContinuousOn f s ∧
∀ (x : M) (y : M'),
ContDiffOn 𝕜 n (↑(extChartAt I' y) ∘ f ∘ ↑(extChartAt I x).symm)
((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source))
This theorem states that for any nontrivially normed field 𝕜, normed add commutative group E and E', normed spaces 𝕜 E and 𝕜 E', topological spaces H, M, H', M', model with corners I, I', and charted spaces H M, H' M', equipped with smooth manifolds with corners I M and I' M', and for any function f from M to M' defined on a set s and for any natural number or infinity n, the function f is continuously differentiable on set s with respect to the modelled corners I and I' and order n if and only if the function f is continuous on set s and for every point x in M and y in M', the composition of the extended chart at I' y, function f, and the inverse of the extended chart at I x is continuously differentiable with respect to 𝕜 and order n on the intersection of the target of the extended chart at I x and the preimage of the intersection of set s and the preimage of the source of the extended chart at I' y under the inverse operation of the extended chart at I x.
More concisely: For any nontrivially normed field 𝕜, normed add commutative groups E and E', smooth manifolds with corners I M, I' M', and functions f from M to M' defined on a set s, the function f is continuously differentiable of order n on s with respect to the indicated corners if and only if the composition of the extended charts at I' y, f, and the inverse of the extended chart at I x is continuously differentiable of order n with respect to 𝕜 for all x in M and y in M'.
|
contMDiffWithinAt_iff_contMDiffOn_nhds
theorem contMDiffWithinAt_iff_contMDiffOn_nhds :
∀ {𝕜 : 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] [inst_6 : SmoothManifoldWithCorners I M]
{E' : Type u_5} [inst_7 : NormedAddCommGroup E'] [inst_8 : NormedSpace 𝕜 E'] {H' : Type u_6}
[inst_9 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [inst_10 : TopologicalSpace M']
[inst_11 : ChartedSpace H' M'] [inst_12 : SmoothManifoldWithCorners I' M'] {f : M → M'} {s : Set M} {x : M}
{n : ℕ}, ContMDiffWithinAt I I' (↑n) f s x ↔ ∃ u ∈ nhdsWithin x (insert x s), ContMDiffOn I I' (↑n) f u
The theorem `contMDiffWithinAt_iff_contMDiffOn_nhds` states that a function `f` is `C^n` (n-times continuously differentiable) within a set `s` at a point `x` in a manifold `M` for a given natural number `n`, if and only if it is `C^n` on a neighborhood `u` of this point `x` such that `u` is in the "neighborhood within" filter of `x` in the augmented set `s` (i.e., `s` after inserting `x`). Here, specific conditions on the types of the spaces `𝕜`, `E`, `H`, `M`, `E'`, `H'`, and `M'` are assumed, including the requirements that the spaces `M` and `M'` are smooth manifolds with corners with models `I` and `I'`, respectively.
More concisely: A function `f` is `C^n` differentiable within a set `s` at a point `x` in a smooth manifold `M` if and only if it is `C^n` on a neighborhood `u` of `x` in `s` that lies in the "neighborhood within" filter of `x` in `M`, where `𝕜`, `E`, `H`, `M`, `E'`, `H'`, and `M'` are smooth manifolds with corners satisfying certain conditions.
|
contMDiffOn_iff_of_subset_source'
theorem contMDiffOn_iff_of_subset_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] [inst_6 : SmoothManifoldWithCorners I M]
{E' : Type u_5} [inst_7 : NormedAddCommGroup E'] [inst_8 : NormedSpace 𝕜 E'] {H' : Type u_6}
[inst_9 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [inst_10 : TopologicalSpace M']
[inst_11 : ChartedSpace H' M'] [inst_12 : SmoothManifoldWithCorners I' M'] {f : M → M'} {s : Set M} {n : ℕ∞}
{x : M} {y : M'},
s ⊆ (extChartAt I x).source →
Set.MapsTo f s (extChartAt I' y).source →
(ContMDiffOn I I' n f s ↔
ContDiffOn 𝕜 n (↑(extChartAt I' y) ∘ f ∘ ↑(extChartAt I x).symm) (↑(extChartAt I x) '' s))
This theorem states that, given a non-trivial normed field `𝕜`, normed additive commutative groups `E` and `E'`, topological spaces `H`, `M`, `H'` and `M'`, models with corners `I` and `I'`, charted spaces `M` and `M'` with smooth manifolds, a function `f` from `M` to `M'`, a set `s` in `M`, and points `x` in `M` and `y` in `M'`, if the set `s` is a subset of the source of the exterior chart at `x` and the function `f` maps the set `s` into the source of the exterior chart at `y`, then the continuity of the `n` times differentiability of `f` on the set `s` is equivalent to the `n` times continuity differentiability of the composition of the inverse of the exterior chart at `x` with `f` and the exterior chart at `y` applied on the image of the set `s` under the exterior chart at `x`.
More concisely: Given a non-trivial normed field `𝕜`, a function `f` between smooth manifolds `M` and `M'`, and sets `s` in `M` and `I` in their respective charts, the `n`-times differentiability of `f` on `s` is equivalent to the `n`-times continuity differentiability of the composite of the inverse charts and `f` on the image of `s`.
|
contDiffWithinAtProp_id
theorem contDiffWithinAtProp_id :
∀ {𝕜 : 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) {n : ℕ∞}
(x : H), ContDiffWithinAtProp I I n id Set.univ x
The theorem `contDiffWithinAtProp_id` states that for any nontrivially normed field `𝕜`, normed additive commutative group `E`, normed space `E` over `𝕜`, topological space `H`, and a model with corners `I` of `H` with values in `E` over `𝕜`, along with an arbitrary element `n` from the set of natural numbers plus infinity (`ℕ∞`), and an element `x` from the topological space `H`, the identity function is continuously differentiable within the universal set at the point `x`. In other words, the identity function is smooth at any point in the topological space `H`.
More concisely: For any nontrivially normed field `𝕜`, normed additive commutative group `E` over `𝕜`, and a topological space `H` with a model of corners `I` in the normed space `E`, the identity function is continuously differentiable at every point `x` in `H`.
|
contMDiffOn_iff_of_subset_source
theorem contMDiffOn_iff_of_subset_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] [inst_6 : SmoothManifoldWithCorners I M]
{E' : Type u_5} [inst_7 : NormedAddCommGroup E'] [inst_8 : NormedSpace 𝕜 E'] {H' : Type u_6}
[inst_9 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [inst_10 : TopologicalSpace M']
[inst_11 : ChartedSpace H' M'] [inst_12 : SmoothManifoldWithCorners I' M'] {f : M → M'} {s : Set M} {n : ℕ∞}
{x : M} {y : M'},
s ⊆ (chartAt H x).source →
Set.MapsTo f s (chartAt H' y).source →
(ContMDiffOn I I' n f s ↔
ContinuousOn f s ∧
ContDiffOn 𝕜 n (↑(extChartAt I' y) ∘ f ∘ ↑(extChartAt I x).symm) (↑(extChartAt I x) '' s))
This theorem states that given a pair of topological spaces (models of smooth manifolds) `M` and `M'` equipped with their respective charted spaces and smooth manifolds with corners, if we have a function `f` from `M` to `M'` defined on a set `s` within `M`, and `s` lies entirely in a single chart of `M`, and `f` maps `s` into a single chart of `M'`, then the smoothness of `f` on `s` can be characterized by its continuity on `s` and the smoothness of the composition of `f` with the inverse of the chart at `x` in `M` and the chart at `y` in `M'` when restricted to the image of `s` under the chart at `x`. This means that we can check the smoothness of `f` purely in the charted spaces, which simplifies the verification process.
In more mathematical terms, given `M` and `M'` are smooth manifolds with corners modeled on Euclidean spaces `E` and `E'` respectively, a function `f: M → M'` is of class `C^n` on a set `s ⊆ M` (i.e., `ContMDiffOn I I' n f s`) if and only if `f` is continuous on `s` and the function `f` composed with the inverse of the chart at `x` in `M` and the chart at `y` in `M'` (expressed as `(extChartAt I' y) ∘ f ∘ (extChartAt I x).symm`) is of class `C^n` when restricted to the image of `s` under the chart at `x` (expressed as `(extChartAt I x) '' s`). The condition `s ⊆ (chartAt H x).source` ensures that `s` lies entirely in a single chart of `M`, and `Set.MapsTo f s (chartAt H' y).source` ensures that `f` maps `s` into a single chart of `M'`.
More concisely: Given smooth manifolds with corners M and M', a function f: M -> M' is of class C^n on a set s subseteq M if and only if f is continuous on s and the composition of f with the inverse of the charts at x in M and y in M', restricted to the image of s under the chart at x, is of class C^n.
|
contMDiffWithinAt_iff
theorem contMDiffWithinAt_iff :
∀ {𝕜 : 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'} {s : Set M} {x : M} {n : ℕ∞},
ContMDiffWithinAt I I' n f s x ↔
ContinuousWithinAt f s x ∧
ContDiffWithinAt 𝕜 n (↑(extChartAt I' (f x)) ∘ f ∘ ↑(extChartAt I x).symm)
(↑(extChartAt I x).symm ⁻¹' s ∩ Set.range ↑I) (↑(extChartAt I x) x)
This theorem states that for a function `f` from a manifold `M` to another manifold `M'`, both embedded in normed spaces with nontrivial normed fields, the function is smooth within a subset `s` of `M` at a point `x` if and only if two conditions are met. Firstly, the function `f` must be continuous at the point `x` within the subset `s`. Secondly, the composition of the function `f` and the inverse of the chart at `x`, followed by the chart at `f(x)`, should be smooth within the intersection of the preimage of `s` under the inverse of the chart at `x` and the range of the chart, evaluated at the chart of `x`.
More concisely: A function `f: M → M'` between manifolds, embedded in normed spaces with nontrivial fields, is smooth at `x ∈ M` within a subset `s ∈ M` if and only if `f` is continuous at `x` in `s` and the composite of `f`, the inverse chart at `x`, and the chart at `f(x)` is smooth on the intersection of the inverse chart's preimage and the chart's range.
|
contMDiffAt_iff_contMDiffOn_nhds
theorem contMDiffAt_iff_contMDiffOn_nhds :
∀ {𝕜 : 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] [inst_6 : SmoothManifoldWithCorners I M]
{E' : Type u_5} [inst_7 : NormedAddCommGroup E'] [inst_8 : NormedSpace 𝕜 E'] {H' : Type u_6}
[inst_9 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [inst_10 : TopologicalSpace M']
[inst_11 : ChartedSpace H' M'] [inst_12 : SmoothManifoldWithCorners I' M'] {f : M → M'} {x : M} {n : ℕ},
ContMDiffAt I I' (↑n) f x ↔ ∃ u ∈ nhds x, ContMDiffOn I I' (↑n) f u
The theorem `contMDiffAt_iff_contMDiffOn_nhds` states that, given a nontrivially normed field `𝕜`, a normed additive commutative group `E`, a normed space `𝕜 E`, a topological space `H`, a model with corners `I` in `𝕜 E H`, a topological space `M`, a charted space `M` modelled on `H`, a smooth manifold with corners `I M`, and similar structures `E'`, `H'`, `I'`, `M'` for the target of a function `f`, along with a point `x` in `M` and a natural number `n` -- a function `f` is `C^n` at the point `x` if and only if there exists a neighborhood `u` of `x` such that `f` is `C^n` on this neighborhood `u`. Here "C^n" is a notation common in differential geometry, and it refers to a function being continuously differentiable `n` times. The neighborhood of `x` is defined in the context of the topology of `M`.
More concisely: A function between smooth manifolds with corners is `C^n` at a point if and only if there exists a neighborhood of that point where the function is `C^n`.
|
ContMDiffAt.contMDiffWithinAt
theorem ContMDiffAt.contMDiffWithinAt :
∀ {𝕜 : 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'} {s : Set M} {x : M} {n : ℕ∞}, ContMDiffAt I I' n f x → ContMDiffWithinAt I I' n f s x
The theorem `ContMDiffAt.contMDiffWithinAt` states that for any non-trivially normed field `𝕜`, given normed add commutative groups `E` and `E'` with normed spaces over `𝕜`, topological spaces `H`, `M`, `H'`, and `M'`, model structures `I` and `I'` with corners from `𝕜` and `E` to `H` and from `𝕜` and `E'` to `H'` respectively, a charted space structure over `M` with model `I` and chart `H`, a charted space structure over `M'` with model `I'` and chart `H'`, a function `f` from `M` to `M'`, a set `s` of elements of `M`, a point `x` in `M`, and a natural number `n`, if the function `f` is continuously differentiable at the point `x` to the `n`-th order, then it is also continuously differentiable within the set `s` at the point `x` to the `n`-th order.
More concisely: If `f: M → M'` is a function continuously differentiable to order `n` at `x ∈ M` between charted spaces over normed groups `E` and `E'` with normed spaces over a non-trivially normed field `𝕜`, then `f` is continuously differentiable to order `n` within any set `s ∈ M` at `x`.
|
ContMDiff.contMDiffAt
theorem ContMDiff.contMDiffAt :
∀ {𝕜 : 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} {n : ℕ∞}, ContMDiff I I' n f → ContMDiffAt I I' n f x
This theorem, `ContMDiff.contMDiffAt`, states that for any nontrivially normed field 𝕜, normed add commutative groups E and E', normed spaces over 𝕜 E and E', topological spaces H, M, H', and M', models with corners I and I' over these spaces, a map `f` from M to M', a point `x` in M, and a natural number or infinity `n`, if the map `f` is continuously differentiable up to order `n` in the sense of the manifolds M and M', then `f` is also continuously differentiable at the point `x` up to the same order `n`. In other words, if a function is continuously differentiable everywhere in a manifold, it is also continuously differentiable at any specific point in the manifold.
More concisely: If a function is continuously differentiable up to order n on a manifold, then it is continuously differentiable up to the same order at any point in the manifold.
|
contMDiffWithinAt_iff_of_mem_source
theorem contMDiffWithinAt_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] [inst_6 : SmoothManifoldWithCorners I M]
{E' : Type u_5} [inst_7 : NormedAddCommGroup E'] [inst_8 : NormedSpace 𝕜 E'] {H' : Type u_6}
[inst_9 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [inst_10 : TopologicalSpace M']
[inst_11 : ChartedSpace H' M'] [inst_12 : SmoothManifoldWithCorners I' M'] {f : M → M'} {s : Set M} {x : M}
{n : ℕ∞} {x' : M} {y : M'},
x' ∈ (chartAt H x).source →
f x' ∈ (chartAt H' y).source →
(ContMDiffWithinAt I I' n f s x' ↔
ContinuousWithinAt f s x' ∧
ContDiffWithinAt 𝕜 n (↑(extChartAt I' y) ∘ f ∘ ↑(extChartAt I x).symm)
(↑(extChartAt I x).symm ⁻¹' s ∩ Set.range ↑I) (↑(extChartAt I x) x'))
This theorem states that smoothness within a set at a certain point for a function between smooth manifolds can be reformulated as continuity within this set at the same point, and smoothness in any chart containing that point. In more detail, given a function `f` from manifold `M` to manifold `M'`, a set `s` in `M`, a point `x'` in `M`, and a point `y` in `M'`, if `x'` lies in the source of the preferred chart at `x` and `f(x')` lies in the source of the preferred chart at `y`, then the smoothness of `f` within `s` at `x'` is equivalent to the continuity of `f` within `s` at `x'` and the smoothness of the composition of the extended charts at `y` and `x` (with the latter inverted) with `f`, within the intersection of the preimage of `s` under the inverted extended chart at `x` and the range of the identity map on manifold `M`, at the image of `x` under the extended chart at `x`.
More concisely: Given a smooth function between manifolds and points lying in the domains of their preferred charts, smoothness within a set at a point is equivalent to continuity within that set and smoothness of the composite of the inverse chart transformations and the function on the intersections of their domains.
|
contMDiffWithinAt_iff_image
theorem contMDiffWithinAt_iff_image :
∀ {𝕜 : 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] [inst_6 : SmoothManifoldWithCorners I M]
{E' : Type u_5} [inst_7 : NormedAddCommGroup E'] [inst_8 : NormedSpace 𝕜 E'] {H' : Type u_6}
[inst_9 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [inst_10 : TopologicalSpace M']
[inst_11 : ChartedSpace H' M'] [inst_12 : SmoothManifoldWithCorners I' M'] {e : PartialHomeomorph M H}
{e' : PartialHomeomorph M' H'} {f : M → M'} {s : Set M} {n : ℕ∞} {x : M},
e ∈ SmoothManifoldWithCorners.maximalAtlas I M →
e' ∈ SmoothManifoldWithCorners.maximalAtlas I' M' →
s ⊆ e.source →
x ∈ e.source →
f x ∈ e'.source →
(ContMDiffWithinAt I I' n f s x ↔
ContinuousWithinAt f s x ∧
ContDiffWithinAt 𝕜 n (↑(e'.extend I') ∘ f ∘ ↑(e.extend I).symm) (↑(e.extend I) '' s)
(↑(e.extend I) x))
This theorem provides an alternative formulation of `contMDiffWithinAt_iff_of_mem_maximalAtlas` when the set `s` is a subset of `e.source`. For any normed field 𝕜, topological spaces E, H, M, E', H', M', models with corners I and I', partial homeomorphisms e and e', function f from M to M', set s of elements in M, natural number (possibly infinite) n, and point x in M, if e and e' are elements of the maximal atlas of the smooth manifolds with corners I M and I' M', s is a subset of e.source, x is an element of e.source, and f(x) is an element of e'.source, then the function f is continuously differentiable within s at x if and only if f is continuous at x within s and the composition of e'.extend I', f, and the inverse of e.extend I is continuously differentiable at the image of x under e.extend I within the image of s under e.extend I.
More concisely: Given a smooth manifold with corners I M, a subset s of its source set, and continuous functions e, e', f between their corresponding source sets, if s is contained in the domain of e, e and e' are in the maximal atlas, x is in s, and f(x) is in the domain of e', then f is continuously differentiable at x within s if and only if f is continuous at x within s and the composition of e'.extend I', f, and e.extend I|^(-1) is continuously differentiable at e.extend I(x) within the image of s under e.extend I.
|
contMDiffWithinAt_iff_target
theorem contMDiffWithinAt_iff_target :
∀ {𝕜 : 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'} {s : Set M} {x : M} {n : ℕ∞},
ContMDiffWithinAt I I' n f s x ↔
ContinuousWithinAt f s x ∧ ContMDiffWithinAt I (modelWithCornersSelf 𝕜 E') n (↑(extChartAt I' (f x)) ∘ f) s x
This theorem states that for any given non-trivial normed field 𝕜, normed addition-commutative groups E and E', normed spaces over 𝕜, topological spaces H, M, H', and M', charted spaces with model corners, a function f from M to M', a set s of elements of M, a point x in M and a natural number n, the function f is continuously differentiable within the set s at the point x if and only if the function f is continuous at the point x within the set s and the composition of the extended chart at the point (f x) with the function f is continuously differentiable within the set s at the point x, where the smoothness of the latter function is considered in the context of the vector space E' equipped with its standard model with corners.
More concisely: A function between charted normed spaces is continuously differentiable at a point if and only if it is continuous at that point and the composition of its extended chart and the function is continuously differentiable in the vector space sense.
|
contMDiffAt_iff_contMDiffAt_nhds
theorem contMDiffAt_iff_contMDiffAt_nhds :
∀ {𝕜 : 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] [inst_6 : SmoothManifoldWithCorners I M]
{E' : Type u_5} [inst_7 : NormedAddCommGroup E'] [inst_8 : NormedSpace 𝕜 E'] {H' : Type u_6}
[inst_9 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [inst_10 : TopologicalSpace M']
[inst_11 : ChartedSpace H' M'] [inst_12 : SmoothManifoldWithCorners I' M'] {f : M → M'} {x : M} {n : ℕ},
ContMDiffAt I I' (↑n) f x ↔ ∀ᶠ (x' : M) in nhds x, ContMDiffAt I I' (↑n) f x'
This theorem states that given a nontrivially 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` and `I'` for `𝕜 E H` and `𝕜 E' H'` respectively, charted spaces `H M` and `H' M'`, smooth manifolds with corners `I M` and `I' M'`, a function `f` from `M` to `M'`, a point `x` in `M`, and a natural number `n`, the function `f` is `C^n` continuous at point `x` if and only if `f` is `C^n` continuous at all points in every neighborhood of `x`. Note that this does not hold for `n = ∞`, meaning that `f` being `C^∞` at `x` implies that `f` is `C^n` on some neighborhood of `x`, but this neighborhood can depend on `n`.
More concisely: Given a nontrivially normed field `𝕜`, normed spaces `𝕜 E` and `𝕜 E'`, and smooth manifolds with corners `I M` and `I' M'`, a function `f: M -> M'` is `C^n` continuous at a point `x in M` if and only if it is `C^n` continuous at all points in every neighborhood of `x`. (This holds for finite `n` but not for `n = ∞`.)
|
contMDiffWithinAt_iff'
theorem contMDiffWithinAt_iff' :
∀ {𝕜 : 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'} {s : Set M} {x : M} {n : ℕ∞},
ContMDiffWithinAt I I' n f s x ↔
ContinuousWithinAt f s x ∧
ContDiffWithinAt 𝕜 n (↑(extChartAt I' (f x)) ∘ f ∘ ↑(extChartAt I x).symm)
((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source))
(↑(extChartAt I x) x)
This theorem states that for any nontrivially normed field `𝕜`, normed additive commutative groups `E` and `E'`, topological spaces `H`, `M` and `H'`, `M'`, models with corners `I` and `I'`, a function `f : M → M'`, a set `s : Set M`, a point `x : M`, and a smoothness degree `n : ℕ∞`, the smoothness of `f` within the set `s` at the point `x` is equivalent to `f` being continuous at `x` within `s` and the smoothness within the target of the extended chart at `x` composed with `f` and the inverse of the extended chart at `x`, restricted to the preimage of `s` intersected with the preimage of the source of the extended chart at `f(x)`, at the point corresponding to `x` in the extended chart. This reformulation restricts the set to lie within the domain/codomain of the corresponding charts. Despite the complexity of this form, it can be useful for rewriting the goal in proofs.
More concisely: For any nontrivially normed field `𝕜`, the smoothness of a function `f` from one normed additive commutative group to another at a point `x` with respect to a smoothness degree `n`, within the preimage of a set under the corresponding charts, is equivalent to `f` being continuous at `x` within that set and the smoothness of the composite of `f`, the inverse of the extended chart at `x`, and the extended chart at `f(x)` on the preimages of that set and the source of the chart at `f(x)`.
|
ContMDiffOn.continuousOn
theorem ContMDiffOn.continuousOn :
∀ {𝕜 : 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'} {s : Set M} {n : ℕ∞}, ContMDiffOn I I' n f s → ContinuousOn f s
This theorem states that if `f` is a function from a manifold `M` to another manifold `M'`, and `f` is continuously differentiable up to order `n` within a set `s` in `M`, then `f` is continuous on `s`. Here, `𝕜` represents the underlying field (which is a normed field), `E` and `E'` are the normed vector spaces associated with the manifolds, and `H` and `H'` are the model spaces of the manifolds. The manifolds `M` and `M'` are equipped with topologies and are also charted, meaning they have associated atlas of charts. The `ModelWithCorners` objects `I` and `I'` supply the differential structure on `M` and `M'`.
More concisely: If `f` is a continuously differentiable up to order `n` function from a manifold `M` to another manifold `M'` over a normed field, then `f` is continuous on every set `s` in `M`.
|
contDiffWithinAt_localInvariantProp
theorem contDiffWithinAt_localInvariantProp :
∀ {𝕜 : 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 : ℕ∞),
(contDiffGroupoid ⊤ I).LocalInvariantProp (contDiffGroupoid ⊤ I') (ContDiffWithinAtProp I I' n)
This theorem states that being `C^n` (having `n` continuous derivatives) in the model space is a property that is local and invariant under smooth maps. Hence, this property can be uplifted to manifolds smoothly. This is established for any non-trivially normed field, any normed additive commutative group, any normed space, and any topological space that are given as inputs. The theorem also requires a model with corners `I` and `I'` for the spaces and a natural number `n` to define the degree of differentiability. The local invariant property is then defined in terms of the groupoid of all `C^n` maps and the property of being `C^n` within a set.
More concisely: The property of being `C^n` (having `n` continuous derivatives) is a local and invariant property under smooth maps, allowing its uplift to manifolds in any non-trivially normed field, normed additive commutative group, normed space, and topological space.
|
ContMDiff.of_le
theorem ContMDiff.of_le :
∀ {𝕜 : 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'} {m n : ℕ∞}, ContMDiff I I' n f → m ≤ n → ContMDiff I I' m f
The theorem `ContMDiff.of_le` states that given any nontrivially normed field `𝕜`, normed additive commutative groups `E` and `E'`, normed spaces 𝕜 `E` and 𝕜 `E'`, topological spaces `H`, `M`, `H'`, `M'`, models with corners `I` (for the manifold `M` with values in `E`) and `I'` (for the manifold `M'` with values in `E'`), charts for these manifolds `M` and `M'`, and a function `f` from `M` to `M'`, if `f` is `n` times continuously differentiable (`ContMDiff`), then `f` is also `m` times continuously differentiable for any `m` less than or equal to `n`.
More concisely: If `f` is `n` times continuously differentiable from `M` to `M'` between normed spaces, then `f` is also `m` times continuously differentiable for any `m` less than or equal to `n`.
|
ContMDiff.contMDiffOn
theorem ContMDiff.contMDiffOn :
∀ {𝕜 : 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'} {s : Set M} {n : ℕ∞}, ContMDiff I I' n f → ContMDiffOn I I' n f s
The theorem `ContMDiff.contMDiffOn` asserts that for every nontrivially normed field `𝕜`, normed add-commutative groups `E` and `E'`, normed spaces `𝕜E` and `𝕜E'`, topological spaces `H`, `M`, `H'`, `M'`, models with corners `I` and `I'`, and charted spaces `H'M'` and `HM`, if a function `f` from `M` to `M'` is continuously differentiable to any order `n`, then it is also continuously differentiable to the same order `n` on any subset `s` of `M`. In other words, if a function is continuously differentiable everywhere, it remains continuously differentiable when restricted to any subset of its domain.
More concisely: If a function is continuously differentiable of order `n` on a normed space, then it is also continuously differentiable of order `n` on any subset of its domain.
|
ContMDiffWithinAt.of_insert
theorem ContMDiffWithinAt.of_insert :
∀ {𝕜 : 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'} {s : Set M} {x : M} {n : ℕ∞},
ContMDiffWithinAt I I' n f (insert x s) x → ContMDiffWithinAt I I' n f s x
This theorem, known as an alias of the forward direction of `contMDiffWithinAt_insert_self`, states that for any nontrivial normed field `𝕜`, a normed additive commutative group `E` which forms a normed space over `𝕜`, a topological space `H`, a model with corners `I` of `𝕜`, `E` and `H`, a topological space `M` equipped with a charted space structure `H M`, a normed additive commutative group `E'` which forms a normed space over `𝕜`, a topological space `H'`, a model with corners `I'` of `𝕜`, `E'` and `H'`, a topological space `M'` equipped with a charted space structure `H' M'`, a function `f` from `M` to `M'`, a set `s` of `M`, an element `x` of `M`, and a natural number `n` or infinity, if the function `f` is continuously differentiable `n` times at all points in the set formed by inserting `x` into `s` around `x`, then `f` is continuously differentiable `n` times at all points in `s` around `x`.
More concisely: If a function between charted normed spaces is continuously differentiable of order n at all points in a set around a point x, then it is continuously differentiable of order n at x within that set.
|
ContMDiffOn.of_le
theorem ContMDiffOn.of_le :
∀ {𝕜 : 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'} {s : Set M} {m n : ℕ∞}, ContMDiffOn I I' n f s → m ≤ n → ContMDiffOn I I' m f s
The theorem `ContMDiffOn.of_le` states that, for all types `𝕜`, `E`, `H`, `I`, `M`, `E'`, `H'`, `I'`, `M'`, `f`, `s`, `m` and `n`, if the space `𝕜` is a nontrivially normed field, `E` and `E'` are normed additive commutative groups, `E` and `E'` are normed over `𝕜`, `H`, `H'`, `M`, and `M'` are topological spaces, `I` and `I'` are models with corners over `𝕜`, `E`, `H`, `E'` and `H'` respectively, `M` and `M'` are charted spaces over `H` and `H'` respectively, `f` is a function from `M` to `M'`, `s` is a set in `M`, and `n` is a smoothness level, if `f` is `n` times continuously differentiable on `s`, and `m` is less than or equal to `n`, then `f` is `m` times continuously differentiable on `s`.
More concisely: If `𝕜` is a nontrivially normed field, `f` is `n` times continuously differentiable on a set `s` in the charted spaces `M` and `M'` over topological spaces `H` and `H'`, respectively, then `f` is `m` times continuously differentiable on `s` for any `m` less than or equal to `n`.
|
contMDiffOn_of_locally_contMDiffOn
theorem contMDiffOn_of_locally_contMDiffOn :
∀ {𝕜 : 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'} {s : Set M} {n : ℕ∞},
(∀ x ∈ s, ∃ u, IsOpen u ∧ x ∈ u ∧ ContMDiffOn I I' n f (s ∩ u)) → ContMDiffOn I I' n f s
The theorem `contMDiffOn_of_locally_contMDiffOn` states that being `$C^n$`-smooth (meaning a function is continuously differentiable `n` times) is a local property. In other words, if for every point `x` in a set `s`, we can find an open set `u` containing `x` such that the function `f` is `$C^n$`-smooth on the intersection of `s` and `u`, then `f` is `$C^n$`-smooth on `s`. Here, `f` is a function from a smooth manifold `M` to another smooth manifold `M'`, both equipped with a model (`I` and `I'`, respectively) including topological, normed real vector spaces `E` and `E'`, and `s` is a subset of `M`. The property of being `$C^n$`-smooth is defined in the context of these models which provide the necessary structure for differentiability.
More concisely: If for every point in a subset `s` of smooth manifolds `M` and `M'`, there exists an open set `u` containing that point such that the function `f` from `M` to `M'` is continuously differentiable up to order `n` on `s ∩ u`, then `f` is continuously differentiable up to order `n` on `s`.
|
contMDiff_iff
theorem contMDiff_iff :
∀ {𝕜 : 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] [inst_6 : SmoothManifoldWithCorners I M]
{E' : Type u_5} [inst_7 : NormedAddCommGroup E'] [inst_8 : NormedSpace 𝕜 E'] {H' : Type u_6}
[inst_9 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [inst_10 : TopologicalSpace M']
[inst_11 : ChartedSpace H' M'] [inst_12 : SmoothManifoldWithCorners I' M'] {f : M → M'} {n : ℕ∞},
ContMDiff I I' n f ↔
Continuous f ∧
∀ (x : M) (y : M'),
ContDiffOn 𝕜 n (↑(extChartAt I' y) ∘ f ∘ ↑(extChartAt I x).symm)
((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' (f ⁻¹' (extChartAt I' y).source))
This theorem states that for any non-trivially normed field `𝕜`, normed add commutative groups `E` and `E'`, normed spaces `𝕜 E` and `𝕜 E'`, topological spaces `H`, `M`, `H'`, and `M'`, charted spaces `H M`, `H' M'`, models with corners `I` and `I'`, and a smooth manifold with corners `M` and `M'`, a function `f` from `M` to `M'`, and a natural number `n`, `f` is continuously differentiable up to order `n` if and only if `f` is continuous and for every `x` in `M` and `y` in `M'`, the composition of the extended chart at `I' y`, `f`, and the inverse of the extended chart at `I x` is continuously differentiable on the intersection of the target of the extended chart at `I x` and the preimage of the preimage of `f` under the source of the extended chart at `I' y`.
More concisely: A smooth function between manifolds with corners is continuously differentiable up to order n if and only if, for every pair of points, the composition of the extended charts at those points and the inverse of the other chart is continuously differentiable on their intersection and preimage under the other chart.
|