MathlibAnnex.Sphere.lipschitzWith_radialExtension
theorem
Separates radial variation from the change of unit direction to obtain the global bound with coefficient 1 + 2.
Statement
For real normed spaces and a bijective chord-metric isometry , define and for . Here and are the unit spheres. Then for every ,
Assumptions
The sphere distances are inherited from the ambient norms. The map is a bijective isometry, so it preserves these chord distances and sends unit vectors to unit vectors. No completeness, finite-dimensionality or nontriviality assumption is made.
Conclusion
The forward radial map is globally -Lipschitz. Applying the same theorem to gives the separately stated -Lipschitz bound for . Together with the inverse identities, this makes the radial bijection a homeomorphism with Lipschitz inverse.
The constant is a proved upper bound. This statement makes no optimality assertion and supplies no ambient distance-preserving or linear-extension conclusion. Both directions of the homeomorphism use the same radial maps as in the definitions.
Proof route
First assume , and put , . Split the difference at the smaller radius:
The first direction has norm one and preserves chord distances. Hence
The first bound is the reverse triangle inequality. The second uses the angular lemma with its three hypotheses , and . The following calculation gives its coefficient .
Proof steps
Set . The assumed order and positivity imply and . Scaling the normalized difference gives
Consequently .
The first summand satisfies . For the second,
The triangle inequality now yields , which is the required angular bound.
Insert this angular bound into the displayed radial decomposition. If the norm order is reversed, interchange and use the symmetry of and of the image distance. If one vector is zero, norm preservation gives the sharper equality , so the bound by follows; the two-zero case is immediate.
Main citations
- Exact
declaration and its source —
MathlibAnnex.Sphere.lipschitzWith_radialExtension - The
radial extension —
MathlibAnnex.Sphere.radialExtension - The
angular estimate at the smaller radius —
MathlibAnnex.Sphere.scaled_normalize_dist_le_two - The
radial and angular decomposition in the proof —
MathlibAnnex.Sphere.radialExtension_dist_le_three_of_norm_le - The
extension at zero —
MathlibAnnex.Sphere.radialExtension_zero - The
nonzero defining formula —
MathlibAnnex.Sphere.radialExtension_of_ne_zero - Norm
preservation —
MathlibAnnex.Sphere.radialExtension_norm - The
inverse Lipschitz estimate —
MathlibAnnex.Sphere.lipschitzWith_radialExtension_symm - Inverse
identities —
MathlibAnnex.Sphere.radialExtension_rightInverse - The
radial homeomorphism —
MathlibAnnex.Sphere.radialExtensionHomeomorph
Lean source signature (exact)
theorem lipschitzWith_radialExtension
(e : Metric.sphere (0 : X) 1 ≃ᵢ Metric.sphere (0 : Y) 1) :
LipschitzWith 3 (radialExtension e)| In the source | Mathematical meaning |
|---|---|
(e : Metric.sphere (0 : X) 1 ≃ᵢ Metric.sphere (0 : Y)
1) |
The same bijective chord-distance isometry , where and . The surrounding binders make real normed spaces. |
| In the source | Mathematical meaning |
|---|---|
radialExtension e |
The map , with and for . |
LipschitzWith 3 (radialExtension e) |
For every , . The nonnegative constant is the proved bound, not an extra input or an optimality claim. |
Exact surrounding binder context (separate excerpt)
namespace MathlibAnnex
namespace Sphere
universe u v
variable {X : Type u} {Y : Type v}
[NormedAddCommGroup X] [NormedSpace ℝ X]
[NormedAddCommGroup Y] [NormedSpace ℝ Y]Read exact source with highlighted declaration · Raw UTF-8 source · Card PDF · Back to Project
Exact content identity
Declaration: MathlibAnnex.Sphere.lipschitzWith_radialExtension
Accepted content SHA-256: 01fbb3907373edf7dcdd7cb95a51fbeb2b5c73335d05a1def4972ee8b752871b
Accepted source guide SHA-256: 87ed83f724d62dfbd967187494fe9beedd18d6a8a0bd678b0f56f3486cf1130a
Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73