Radial contraction of bundled smooth embeddings

A radial contraction with nonnegative parameter can precompose a smooth embedding from a finite-dimensional real normed space or postcompose an embedding into that space. The bundled operations preserve every regularity at most ∞; coercion and application lemmas describe their underlying functions.

Since a radial contraction preserves every orientation of E at its centre (TauCeti.isOrientationPreservingAt_radialContraction_self), precomposing an embedding with a radial contraction about the origin keeps it orientation-preserving at the origin (TauCeti.SmoothEmbedding.isOrientationPreservingAt_compRadialContraction).

noncomputable def TauCeti.SmoothEmbedding.compRadialContraction {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {n : WithTop ℕ∞} {F : Type u_2} {H : Type u_3} {N : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] [TopologicalSpace H] {J : ModelWithCorners ℝ F H} [TopologicalSpace N] [ChartedSpace H N] (f : SmoothEmbedding (modelWithCornersSelf ℝ E) J n E N) (hn : n ≤ ↑⊤) {κ : ℝ} (hκ : 0 ≤ κ) : SmoothEmbedding (modelWithCornersSelf ℝ E) J n E N

A smooth embedding of E precomposed with the radial contraction about 0 with parameter κ ≥ 0, preserving any regularity n ≤ ∞.

@[simp]

theorem TauCeti.SmoothEmbedding.coe_compRadialContraction {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {n : WithTop ℕ∞} {F : Type u_2} {H : Type u_3} {N : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] [TopologicalSpace H] {J : ModelWithCorners ℝ F H} [TopologicalSpace N] [ChartedSpace H N] (f : SmoothEmbedding (modelWithCornersSelf ℝ E) J n E N) (hn : n ≤ ↑⊤) {κ : ℝ} (hκ : 0 ≤ κ) : ⇑(f.compRadialContraction hn hκ) = ⇑f ∘ radialContraction 0 κ

@[simp]

theorem TauCeti.SmoothEmbedding.compRadialContraction_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {n : WithTop ℕ∞} {F : Type u_2} {H : Type u_3} {N : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] [TopologicalSpace H] {J : ModelWithCorners ℝ F H} [TopologicalSpace N] [ChartedSpace H N] (f : SmoothEmbedding (modelWithCornersSelf ℝ E) J n E N) (hn : n ≤ ↑⊤) {κ : ℝ} (hκ : 0 ≤ κ) (x : E) : (f.compRadialContraction hn hκ) x = f (radialContraction 0 κ x)

theorem TauCeti.SmoothEmbedding.range_compRadialContraction_subset {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {n : WithTop ℕ∞} {F : Type u_2} {H : Type u_3} {N : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] [TopologicalSpace H] {J : ModelWithCorners ℝ F H} [TopologicalSpace N] [ChartedSpace H N] (f : SmoothEmbedding (modelWithCornersSelf ℝ E) J n E N) (hn : n ≤ ↑⊤) {κ : ℝ} (hκ : 0 ≤ κ) : Set.range ⇑(f.compRadialContraction hn hκ) ⊆ Set.range ⇑f

Precomposing with a radial contraction does not enlarge the image of an embedding.

noncomputable def TauCeti.SmoothEmbedding.transRadialContraction {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {n : WithTop ℕ∞} {E₀ : Type u_5} {H₀ : Type u_6} {M : Type u_7} [NormedAddCommGroup E₀] [NormedSpace ℝ E₀] [TopologicalSpace H₀] {I : ModelWithCorners ℝ E₀ H₀} [TopologicalSpace M] [ChartedSpace H₀ M] (f : SmoothEmbedding I (modelWithCornersSelf ℝ E) n M E) (c : E) (hn : n ≤ ↑⊤) {κ : ℝ} (hκ : 0 ≤ κ) : SmoothEmbedding I (modelWithCornersSelf ℝ E) n M E

A smooth embedding into E followed by the radial contraction about c with parameter κ ≥ 0, preserving any regularity n ≤ ∞.

@[simp]

theorem TauCeti.SmoothEmbedding.coe_transRadialContraction {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {n : WithTop ℕ∞} {E₀ : Type u_5} {H₀ : Type u_6} {M : Type u_7} [NormedAddCommGroup E₀] [NormedSpace ℝ E₀] [TopologicalSpace H₀] {I : ModelWithCorners ℝ E₀ H₀} [TopologicalSpace M] [ChartedSpace H₀ M] (f : SmoothEmbedding I (modelWithCornersSelf ℝ E) n M E) (c : E) (hn : n ≤ ↑⊤) {κ : ℝ} (hκ : 0 ≤ κ) : ⇑(f.transRadialContraction c hn hκ) = radialContraction c κ ∘ ⇑f

@[simp]

theorem TauCeti.SmoothEmbedding.transRadialContraction_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {n : WithTop ℕ∞} {E₀ : Type u_5} {H₀ : Type u_6} {M : Type u_7} [NormedAddCommGroup E₀] [NormedSpace ℝ E₀] [TopologicalSpace H₀] {I : ModelWithCorners ℝ E₀ H₀} [TopologicalSpace M] [ChartedSpace H₀ M] (f : SmoothEmbedding I (modelWithCornersSelf ℝ E) n M E) (c : E) (hn : n ≤ ↑⊤) {κ : ℝ} (hκ : 0 ≤ κ) (x : M) : (f.transRadialContraction c hn hκ) x = radialContraction c κ (f x)

theorem TauCeti.SmoothEmbedding.isOrientationPreservingAt_compRadialContraction {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {n : WithTop ℕ∞} {X : Type u_8} [TopologicalSpace X] [ChartedSpace E X] [IsManifold (modelWithCornersSelf ℝ E) 1 X] {ι : Type u_9} [Fintype ι] (f : SmoothEmbedding (modelWithCornersSelf ℝ E) (modelWithCornersSelf ℝ E) n E X) (hn : n ≤ ↑⊤) {κ : ℝ} (hκ : 0 ≤ κ) {o : Manifold.Orientation (modelWithCornersSelf ℝ E) E ι} {oM : Manifold.Orientation (modelWithCornersSelf ℝ E) X ι} (hf : o.IsOrientationPreservingAt oM (⇑f) 0) : o.IsOrientationPreservingAt oM (⇑(f.compRadialContraction hn hκ)) 0

Precomposing an embedding of E with a radial contraction about the origin keeps it orientation-preserving at the origin.