Documentation

Mathlib.Analysis.NormedSpace.SphereNormEquiv

Homeomorphism between a normed space and sphere times (0, +∞) #

In this file we define a homeomorphism between nonzero elements of a normed space E and Metric.sphere (0 : E) 1 × Set.Ioi (0 : ℝ). One may think about it as generalization of polar coordinates to any normed space.

source
noncomputable def homeomorphUnitSphereProd (E : Type u_1) [NormedAddCommGroup E] [NormedSpace ℝ E] :
↑{0}ᶜ ≃ₜ ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)

The natural homeomorphism between nonzero elements of a normed space E and Metric.sphere (0 : E) 1 × Set.Ioi (0 : ℝ).

The forward map sends ⟨x, hx⟩ to ⟨‖x‖⁻¹ • x, ‖x‖⟩, the inverse map sends (x, r) to r • x.

One may think about it as generalization of polar coordinates to any normed space.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem homeomorphUnitSphereProd_apply_snd_coe (E : Type u_1) [NormedAddCommGroup E] [NormedSpace ℝ E] (x : ↑{0}ᶜ) :
    ↑((homeomorphUnitSphereProd E) x).2 = ‖↑x‖
    source
    @[simp]
    theorem homeomorphUnitSphereProd_apply_fst_coe (E : Type u_1) [NormedAddCommGroup E] [NormedSpace ℝ E] (x : ↑{0}ᶜ) :
    ↑((homeomorphUnitSphereProd E) x).1 = ‖↑x‖⁻¹ • ↑x
    source
    @[simp]
    theorem homeomorphUnitSphereProd_symm_apply_coe (E : Type u_1) [NormedAddCommGroup E] [NormedSpace ℝ E] (x : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)) :
    ↑((homeomorphUnitSphereProd E).symm x) = ↑x.2 • ↑x.1