Radial contractions as local diffeomorphisms

On a finite-dimensional real normed space, the Euclidean radial contraction with a nonnegative parameter is a local diffeomorphism. Families of these contractions preserve manifold smoothness for every regularity at most ∞.

theorem TauCeti.isLocalDiffeomorph_radialContraction {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {n : WithTop ℕ∞} (c : E) (hn : n ≤ ↑⊤) {κ : ℝ} (hκ : 0 ≤ κ) : IsLocalDiffeomorph (modelWithCornersSelf ℝ E) (modelWithCornersSelf ℝ E) n (radialContraction c κ)

A radial contraction with nonnegative parameter is a local diffeomorphism.

theorem TauCeti.contMDiff_radialContraction {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {n : WithTop ℕ∞} {E' : Type u_2} {H' : Type u_3} {X : Type u_4} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] {J : ModelWithCorners ℝ E' H'} [TopologicalSpace X] [ChartedSpace H' X] (c : E) (hn : n ≤ ↑⊤) {κ : X → ℝ} {y : X → E} (hκ : ContMDiff J (modelWithCornersSelf ℝ ℝ) n κ) (hκ₀ : ∀ (x : X), 0 ≤ κ x) (hy : ContMDiff J (modelWithCornersSelf ℝ E) n y) : ContMDiff J (modelWithCornersSelf ℝ E) n fun (x : X) => radialContraction c (κ x) (y x)

A C^n family of radial contractions with nonnegative parameters, applied to a C^n family of points, is C^n for n ≤ ∞.