mfderiv_coe_sphere_injective
theorem mfderiv_coe_sphere_injective :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] {n : ℕ}
[inst_2 : Fact (FiniteDimensional.finrank ℝ E = n + 1)] (v : ↑(Metric.sphere 0 1)),
Function.Injective
⇑(mfderiv (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) (modelWithCornersSelf ℝ E) Subtype.val v)
This theorem states that the differential of the inclusion of a unit sphere in a Euclidean space `E` at a point `v` on the sphere is an injective continuous linear map. Here, `E` is an inner product space over the real numbers with a normed additive commutative group structure and its finite-dimensional rank is `n + 1`. The differential is taken in the context of two models with corners, one modeling the tangent space at `v` and the other modeling `E`. The term "injective" means that if the differential maps two different points from the tangent space to the same point in `E`, then those two points must have been the same to begin with.
More concisely: The differential of the inclusion map of the unit sphere in a real Euclidean space of dimension n+1 is an injective, continuous linear map.
|
contMDiff_coe_sphere
theorem contMDiff_coe_sphere :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] {n : ℕ}
[inst_2 : Fact (FiniteDimensional.finrank ℝ E = n + 1)],
ContMDiff (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) (modelWithCornersSelf ℝ E) ⊤ Subtype.val
This theorem states that the inclusion map (represented by `coe` or `Subtype.val` in Lean), which takes a point from the sphere in a Euclidean space `E` to `E` itself, is smooth (i.e., continuously differentiable). Here, the sphere is considered within an `n`-dimensional real or complex Euclidean space (`EuclideanSpace ℝ (Fin n)`), and `E` is assumed to be a normed add commutative group and an inner product space over the reals, with a dimension equal to `n + 1`. The smoothness of the inclusion map is asserted with respect to the model with corners associated with these Euclidean spaces.
More concisely: The inclusion map from the unit sphere in an `(n+1)`-dimensional Euclidean space over the reals or complexes to the Euclidean space itself is smooth with respect to the model with corners.
|
contMDiff_neg_sphere
theorem contMDiff_neg_sphere :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] {n : ℕ}
[inst_2 : Fact (FiniteDimensional.finrank ℝ E = n + 1)],
ContMDiff (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n)))
⊤ fun x => -x
The theorem `contMDiff_neg_sphere` asserts that the antipodal map, which maps any point on a sphere to its diametrically opposite point, is infinitely continuously differentiable ("smooth") for a real sphere embedded in a Euclidean vector space of dimension `n+1`. The smoothness is stated with respect to the `modelWithCornersSelf` model, which is a technical object capturing the notion of a manifold (the sphere in this case) embedded in a normed vector space. The theorem is general in the sense that it holds for all dimensions `n` of the sphere.
More concisely: The antipodal map on the real sphere of dimension `n` in a Euclidean vector space is infinitely continuously differentiable.
|
contMDiff_expMapCircle
theorem contMDiff_expMapCircle :
ContMDiff (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin 1))) ⊤ ⇑expMapCircle
This theorem states that the map `fun t ↦ exp (t * I)` from the real numbers `ℝ` to the unit circle in the complex numbers `ℂ` is smoothly differentiable. In other words, the function that takes a real number `t` and maps it to the exponential of the product of `t` and the imaginary unit `I` is smooth. This smoothness is defined in the context of the model with corners (a concept in differential geometry) associated with the real numbers and the standard real Euclidean space of dimension 1. The function is smooth at all levels, as indicated by the symbol `⊤` (top).
More concisely: The function `t ↦ exp (t * I)` from the real numbers to the unit circle in the complex numbers is smoothly differentiable with respect to the model with corners on the real numbers and the standard real Euclidean space of dimension 1.
|
ContMDiff.codRestrict_sphere
theorem ContMDiff.codRestrict_sphere :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] {F : Type u_2}
[inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {H : Type u_3} [inst_4 : TopologicalSpace H]
{I : ModelWithCorners ℝ F H} {M : Type u_4} [inst_5 : TopologicalSpace M] [inst_6 : ChartedSpace H M]
[inst_7 : SmoothManifoldWithCorners I M] {n : ℕ} [inst_8 : Fact (FiniteDimensional.finrank ℝ E = n + 1)] {m : ℕ∞}
{f : M → E},
ContMDiff I (modelWithCornersSelf ℝ E) m f →
∀ (hf' : ∀ (x : M), f x ∈ Metric.sphere 0 1),
ContMDiff I (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) m
(Set.codRestrict (fun x => f x) (Metric.sphere 0 1) hf')
This theorem states that if we have a continuously differentiable function `f`, mapping from a manifold `M` to a Euclidean space `E` and all values of `f` lie on the unit sphere, then the function `f` can be restricted to a continuously differentiable function from `M` to the sphere. Here, the manifold `M` is equipped with a smooth structure from a ModelWithCorners `I`, and the dimension of the Euclidean space `E` is `n + 1`. The sphere is considered as a manifold of dimension `n`, embedded in `E`, equipped with the standard Euclidean space structure.
More concisely: If `f` is a continuously differentiable function from a manifold `M` to a Euclidean space `E` of dimension `n+1`, such that all values of `f` lie on the unit sphere in `E`, then `f` can be restricted to a continuously differentiable function from `M` to the unit sphere in `E`.
|
range_mfderiv_coe_sphere
theorem range_mfderiv_coe_sphere :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] {n : ℕ}
[inst_2 : Fact (FiniteDimensional.finrank ℝ E = n + 1)] (v : ↑(Metric.sphere 0 1)),
LinearMap.range
(mfderiv (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) (modelWithCornersSelf ℝ E) Subtype.val v) =
(Submodule.span ℝ {↑v}).orthogonal
The theorem `range_mfderiv_coe_sphere` asserts the following: Given a normed additive commutative group `E` with an inner product space over the real numbers and a natural number `n` such that the finite rank of `E` over the real numbers equals `n + 1`. Consider the differential of the inclusion of the unit sphere in `E` at any point `v` on the sphere as a continuous linear map from the tangent space at `v` to `E`. The theorem states that the range of this map equals the orthogonal complement of the singleton set `{v}` in `E`.
It should be noted that there is a definitional equivalence between `E` and the tangent space to `E` at any point `(v:E)`. Generally, this definitional equivalence is not canonical, but in this specific context (the tangent space of a vector space), it can be considered canonical.
More concisely: Given a normed inner product space E of finite real dimension n+1, the differential of the inclusion of the unit sphere in E at any point v maps the tangent space at v to the orthogonal complement of {v} in E.
|