Distance between radial projections onto the unit sphere

Proved

DbarRegularity.norm_inv_norm_smul_sub_le

by Mazecto · Oct 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

analysisnormed-spaces

Let $E$ be a real normed space, $u,v\in E$ and $v\ne0$ . Then

\Bigl\|\frac{u}{\|u\|}-\frac{v}{\|v\|}\Bigr\|\;\le\;\frac{2\,\|u-v\|}{\|v\|},

with the convention $u/\|u\|=0$ for $u=0$ .

Formalization Note. $u/\|u\|$ is written ‖u‖⁻¹ • u; in Lean (0 : ℝ)⁻¹ = 0, which gives the convention at $u=0$ , where the bound reads $1\le2$ .

Preamble

import Mathlib.Analysis.Normed.Module.Basic
import Mathlib.Analysis.SpecialFunctions.Pow.Real

Formal statement

namespace DbarRegularity

/-- Distance between the radial projections to the unit sphere: for `v ≠ 0`,
`|u/|u| - v/|v|| ≤ 2 |u - v| / |v|` (with `0/|0| = 0`). -/
theorem norm_inv_norm_smul_sub_le {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    (u v : E) (hv : v ≠ 0) :
    ‖‖u‖⁻¹ • u - ‖v‖⁻¹ • v‖ ≤ 2 * ‖u - v‖ / ‖v‖ := by sorry

end DbarRegularity

Source

E. M. Stein, Singular Integrals and Differentiability Properties of Functions, Princeton Mathematical Series 30, Princeton University Press (1970), Chapter II, § 4.2, Theorem 3, p. 39

View graph