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) r × Set.Ioi (0 : ℝ), r > 0. One may think about it as generalization of polar coordinates to any normed space.

We also specialize this definition to the case r = 1 and prove

source

noncomputable def homeomorphSphereProd (E : Type u_2) [NormedAddCommGroup E] [NormedSpace ℝ E] (r : ℝ) (hr : 0 < r) :

↑{0}ᶜ ≃ₜ ↑(Metric.sphere 0 r) × ↑(Set.Ioi 0)

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

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

In the case of the unit sphere r = , 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 homeomorphSphereProd_symm_apply_coe (E : Type u_2) [NormedAddCommGroup E] [NormedSpace ℝ E] (r : ℝ) (hr : 0 < r) (x : ↑(Metric.sphere 0 r) × ↑(Set.Ioi 0)) :

↑((homeomorphSphereProd E r hr).symm x) = ↑x.2 • ↑x.1

source

@[simp]

theorem homeomorphSphereProd_apply_snd_coe (E : Type u_2) [NormedAddCommGroup E] [NormedSpace ℝ E] (r : ℝ) (hr : 0 < r) (x : ↑{0}ᶜ) :

↑((homeomorphSphereProd E r hr) x).2 = ‖↑x‖ / r

source

@[simp]

theorem homeomorphSphereProd_apply_fst_coe (E : Type u_2) [NormedAddCommGroup E] [NormedSpace ℝ E] (r : ℝ) (hr : 0 < r) (x : ↑{0}ᶜ) :

↑((homeomorphSphereProd E r hr) x).1 = r • ‖↑x‖⁻¹ • ↑x

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. See also homeomorphSphereProd for a version that works for a sphere of any positive radius.

Equations