The radial retraction onto a closed ball

In a real normed space, TauCeti.radialRetraction r scales a vector x by min 1 (r / ‖x‖). When 0 ≤ r, it fixes the closed ball of radius r and pushes everything outside it to the sphere of radius r along the ray through the origin. It is the standard device for turning a map that is only Lipschitz near the origin into a globally Lipschitz map agreeing with it near the origin, and it is used that way to cut off the nonlinearity of a differential equation outside a small ball around an equilibrium.

For 0 ≤ r, the retraction is 2-Lipschitz in any normed space, and 2 is the constant carried by TauCeti.lipschitzWith_radialRetraction; it is not optimal in every space (in a Hilbert space the retraction is the metric projection onto a convex set, hence 1-Lipschitz) but the exact constant never matters for cutting off, where one is free to shrink the radius instead.

Main declarations

• TauCeti.radialRetraction: scaling by min 1 (r / ‖x‖); when 0 ≤ r, this is the retraction onto the closed ball of radius r centred at the origin.
• TauCeti.norm_radialRetraction: for 0 ≤ r, its norm is min ‖x‖ r.
• TauCeti.radialRetraction_eventuallyEq_id: inside the open ball, it agrees locally with the identity.
• TauCeti.lipschitzWith_radialRetraction: for 0 ≤ r, it is 2-Lipschitz.
• LipschitzOnWith.comp_radialRetraction: precomposing with it makes a map that is Lipschitz on the closed ball of radius r globally Lipschitz, with twice the constant.

References

• D. G. de Figueiredo, L. A. Karlovitz, On the radial projection in normed spaces, Bull. Amer. Math. Soc. 73 (1967), 364–368.

noncomputable def TauCeti.radialRetraction {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (r : ℝ) (x : E) : E

Scale x by min 1 (r / ‖x‖). When 0 ≤ r, this is the radial retraction onto the closed ball of radius r centred at the origin: vectors of norm at most r are fixed and the others are pulled back along their ray to the sphere of radius r.

Equations

• TauCeti.radialRetraction r x = min 1 (r / ‖x‖) • x

@[simp]

theorem TauCeti.radialRetraction_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (r : ℝ) : radialRetraction r 0 = 0

@[simp]

theorem TauCeti.radialRetraction_of_norm_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {r : ℝ} {x : E} (h : ‖x‖ ≤ r) : radialRetraction r x = x

The radial retraction fixes the closed ball of radius r.

theorem TauCeti.radialRetraction_eventuallyEq_id {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {r : ℝ} {x : E} (hx : ‖x‖ < r) : radialRetraction r =ᶠ[nhds x] id

The radial retraction agrees with the identity on a neighborhood of every point in the open ball.

theorem TauCeti.radialRetraction_of_le_norm {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {r : ℝ} {x : E} (h : r ≤ ‖x‖) : radialRetraction r x = (r / ‖x‖) • x

Outside the closed ball of radius r the radial retraction scales by r / ‖x‖.

@[simp]

theorem TauCeti.norm_radialRetraction {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {r : ℝ} (hr : 0 ≤ r) (x : E) : ‖radialRetraction r x‖ = min ‖x‖ r

For nonnegative radius, the radial retraction has norm min ‖x‖ r.

theorem TauCeti.radialRetraction_mem_closedBall {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {r : ℝ} (hr : 0 ≤ r) (x : E) : radialRetraction r x ∈ Metric.closedBall 0 r

theorem TauCeti.radialRetraction_radialRetraction {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {r : ℝ} (hr : 0 ≤ r) (x : E) : radialRetraction r (radialRetraction r x) = radialRetraction r x

The radial retraction is idempotent for nonnegative radius.

theorem TauCeti.mapsTo_radialRetraction {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {r : ℝ} (hr : 0 ≤ r) : Set.MapsTo (radialRetraction r) Set.univ (Metric.closedBall 0 r)

theorem TauCeti.lipschitzWith_radialRetraction {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {r : ℝ} (hr : 0 ≤ r) : LipschitzWith 2 (radialRetraction r)

The radial retraction onto a closed ball is 2-Lipschitz.

theorem LipschitzOnWith.comp_radialRetraction {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [PseudoEMetricSpace F] {f : E → F} {c : NNReal} {r : ℝ} (hf : LipschitzOnWith c f (Metric.closedBall 0 r)) (hr : 0 ≤ r) : LipschitzWith (c * 2) (f ∘ TauCeti.radialRetraction r)

Precomposing with the radial retraction turns a map that is Lipschitz on the closed ball of radius r into a globally Lipschitz map, at the cost of doubling the constant. The new map still agrees with the old one on that ball, by TauCeti.radialRetraction_of_norm_le.