Radial contractions of a finite-dimensional real normed space

The radial contraction of E about c with parameter κ ≥ 0 is y ↦ c + (1 + κ d(y, c)²)^(-1/2) • (y - c), where d = Euclidean.dist is the distance of the inner product structure that toEuclidean transports to E. It is jointly smooth in κ and y, it is the identity for κ = 0, and it moves no point away from c for d when κ ≥ 0. For r > 0 and κ = r⁻² it is Mathlib's OpenPartialHomeomorph.univBall after an affine normalization, so it maps E homeomorphically, with a smooth inverse, onto the Euclidean ball Euclidean.ball c r. Its derivative at the centre is the identity.

The Euclidean distance replaces the norm of E because its square is smooth, which the square of an arbitrary norm need not be.

These maps shrink an embedding of E into a prescribed neighbourhood of its centre without changing its derivative there; they are used to reduce the disc theorem in a manifold to the Euclidean disc theorem.

Main definitions

• TauCeti.radialContraction: the radial contraction about a point with a given parameter.

Main results

• TauCeti.euclideanDist_radialContraction_le: a radial contraction moves no point away from its centre when κ ≥ 0.
• TauCeti.radialContraction_mem_ball: for r > 0 and κ = r⁻² it takes values in the Euclidean ball of radius r.
• TauCeti.contDiffOn_radialContraction: joint smoothness in the parameter and the point.
• TauCeti.exists_radialContraction_eq_openPartialHomeomorph: for a positive parameter it is an open partial homeomorphism defined on all of E, smooth in both directions.
• TauCeti.hasFDerivAt_radialContraction_self: its derivative at the centre is the identity, so precomposing with it does not change derivatives at the centre (TauCeti.fderiv_comp_radialContraction_self).

The construction transports Mathlib's OpenPartialHomeomorph.univBall and its smoothness (contDiffOn_univBall_symm).

noncomputable def TauCeti.radialContraction {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (c : E) (κ : ℝ) (y : E) : E

The radial contraction of E about c with parameter κ. For κ ≥ 0, the point y moves towards c by the factor (1 + κ d(y, c)²)^(-1/2), for the Euclidean distance d(y, c) = ‖toEuclidean (y - c)‖. For κ = 0 it is the identity. For r > 0 and κ = r⁻² it is a diffeomorphism of E onto Euclidean.ball c r.

@[simp]

theorem TauCeti.radialContraction_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (c y : E) : radialContraction c 0 y = y

@[simp]

theorem TauCeti.radialContraction_self {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (c : E) (κ : ℝ) : radialContraction c κ c = c

theorem TauCeti.toEuclidean_radialContraction {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (c : E) (κ : ℝ) (y : E) : toEuclidean (radialContraction c κ y) = toEuclidean c + (√(1 + κ * ‖toEuclidean (y - c)‖ ^ 2))⁻¹ • toEuclidean (y - c)

The radial contraction read in toEuclidean: the image of y - c is rescaled by the contraction factor.

theorem TauCeti.euclideanDist_radialContraction_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (c y : E) {κ : ℝ} (hκ : 0 ≤ κ) : Euclidean.dist (radialContraction c κ y) c ≤ Euclidean.dist y c

A radial contraction with κ ≥ 0 moves no point away from the centre in Euclidean distance.

theorem TauCeti.toEuclidean_radialContraction_eq_univBall {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (c y : E) {r : ℝ} (hr : 0 < r) : toEuclidean (radialContraction c (r⁻¹ ^ 2) y) = ↑(OpenPartialHomeomorph.univBall (toEuclidean c) r) (r⁻¹ • toEuclidean (y - c))

For a positive parameter, the radial contraction read in toEuclidean is univBall read after the affine normalization y ↦ r⁻¹ • toEuclidean (y - c), where κ = r⁻².

theorem TauCeti.radialContraction_mem_ball {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (c y : E) {r : ℝ} (hr : 0 < r) : radialContraction c (r⁻¹ ^ 2) y ∈ Euclidean.ball c r

For r > 0 and κ = r⁻², the radial contraction lands in the Euclidean ball of radius r about the centre.

theorem TauCeti.range_radialContraction {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (c : E) {r : ℝ} (hr : 0 < r) : Set.range (radialContraction c (r⁻¹ ^ 2)) = Euclidean.ball c r

For r > 0 and κ = r⁻², the range is the whole Euclidean ball of radius r.

@[simp]

theorem TauCeti.exists_radialContraction_eq_iff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (c y : E) {r : ℝ} (hr : 0 < r) : (∃ (x : E), radialContraction c (r ^ 2)⁻¹ x = y) ↔ y ∈ Euclidean.ball c r

Membership in the range of a positive radial contraction is membership in its ball.

theorem TauCeti.contDiffOn_radialContraction {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (c : E) : ContDiffOn ℝ (↑⊤) (fun (q : ℝ × E) => radialContraction c q.1 q.2) {q : ℝ × E | 0 < 1 + q.1 * ‖toEuclidean (q.2 - c)‖ ^ 2}

The radial contraction is jointly smooth in the parameter and the point, wherever 1 + κ d(y, c)² is positive.

theorem TauCeti.contDiff_radialContraction {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (c : E) {κ : ℝ} (hκ : 0 ≤ κ) : ContDiff ℝ (↑⊤) (radialContraction c κ)

A radial contraction with nonnegative parameter is smooth.

theorem TauCeti.exists_radialContraction_eq_openPartialHomeomorph {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (c : E) {κ : ℝ} (hκ : 0 < κ) : ∃ (Θ : OpenPartialHomeomorph E E), Θ.source = Set.univ ∧ ContDiffOn ℝ (↑⊤) (↑Θ) Θ.source ∧ ContDiffOn ℝ (↑⊤) (↑Θ.symm) Θ.target ∧ ↑Θ = radialContraction c κ

For a positive parameter, the radial contraction is the restriction to all of E of an open partial homeomorphism onto a Euclidean ball, which is smooth in both directions.

theorem TauCeti.isEmbedding_radialContraction {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (c : E) {κ : ℝ} (hκ : 0 ≤ κ) : Topology.IsEmbedding (radialContraction c κ)

A radial contraction with nonnegative parameter is a topological embedding.

theorem TauCeti.hasFDerivAt_radialContraction_self {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (c : E) (κ : ℝ) : HasFDerivAt (radialContraction c κ) (ContinuousLinearMap.id ℝ E) c

A radial contraction has derivative the identity at its centre.

theorem TauCeti.fderiv_comp_radialContraction_self {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {h : E → F} (c : E) (κ : ℝ) (hh : DifferentiableAt ℝ h c) : fderiv ℝ (h ∘ radialContraction c κ) c = fderiv ℝ h c

Precomposing with a radial contraction does not change the derivative at its centre.