Radial coordinates in a seminormed space

The positive-norm locus of a real seminormed space is homeomorphic to any sphere of positive radius times the positive real numbers. The inverse map is scalar multiplication, so these coordinates give product neighbourhoods of the sphere even when the seminorm has a nonzero kernel.

TauCeti.homeomorphSphereProdOfNormPos and its unit-sphere specialization TauCeti.homeomorphUnitSphereProdOfNormPos generalize Mathlib's homeomorphSphereProd and homeomorphUnitSphereProd: the positive-norm locus replaces the complement of the origin. The construction follows those homeomorphisms, with the domain and the proof that the inverse lands in it adapted to seminorms.

Reparametrizing the radius by an open embedding ρ : Y → ℝ with positive values gives an open embedding (u, y) ↦ ρ y • u of sphere (0 : E) 1 × Y into E (Topology.IsOpenEmbedding.smul_coe_sphere). With Y = ℝ and ρ an increasing homeomorphism onto an interval of radii, such as t ↦ r * exp t or the logistic sigmoid, this is a product neighbourhood of a round sphere: a bicollar whose zero slice is the sphere of radius ρ 0. TauCeti.polar uses the exponential radius exp (t - 1), so that time 1 corresponds to the unit sphere and times at most 1 parametrize the punctured closed unit ball.

noncomputable def TauCeti.homeomorphSphereProdOfNormPos (E : Type u_1) [SeminormedAddCommGroup E] [NormedSpace ℝ E] (r : ℝ) (hr : 0 < r) : ↑{x : E | 0 < ‖x‖} ≃ₜ ↑(Metric.sphere 0 r) × ↑(Set.Ioi 0)

Radial coordinates on the positive-norm locus of a real seminormed space, using the sphere of radius r > 0. The forward map sends x to (r • ‖x‖⁻¹ • x, ‖x‖ / r) and the inverse sends (u, d) to d • u.

@[simp]

theorem TauCeti.homeomorphSphereProdOfNormPos_apply_fst_coe (E : Type u_1) [SeminormedAddCommGroup E] [NormedSpace ℝ E] (r : ℝ) (hr : 0 < r) (x : ↑{x : E | 0 < ‖x‖}) : ↑((homeomorphSphereProdOfNormPos E r hr) x).1 = r • ‖↑x‖⁻¹ • ↑x

@[simp]

theorem TauCeti.homeomorphSphereProdOfNormPos_apply_snd_coe (E : Type u_1) [SeminormedAddCommGroup E] [NormedSpace ℝ E] (r : ℝ) (hr : 0 < r) (x : ↑{x : E | 0 < ‖x‖}) : ↑((homeomorphSphereProdOfNormPos E r hr) x).2 = ‖↑x‖ / r

@[simp]

theorem TauCeti.homeomorphSphereProdOfNormPos_symm_apply_coe (E : Type u_1) [SeminormedAddCommGroup E] [NormedSpace ℝ E] (r : ℝ) (hr : 0 < r) (p : ↑(Metric.sphere 0 r) × ↑(Set.Ioi 0)) : ↑((homeomorphSphereProdOfNormPos E r hr).symm p) = ↑p.2 • ↑p.1

noncomputable def TauCeti.homeomorphUnitSphereProdOfNormPos (E : Type u_1) [SeminormedAddCommGroup E] [NormedSpace ℝ E] : ↑{x : E | 0 < ‖x‖} ≃ₜ ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)

Radial coordinates on the positive-norm locus of a real seminormed space, using the unit sphere. The forward map sends x to (‖x‖⁻¹ • x, ‖x‖) and the inverse sends (u, r) to r • u.

@[simp]

theorem TauCeti.homeomorphUnitSphereProdOfNormPos_apply_fst_coe (E : Type u_1) [SeminormedAddCommGroup E] [NormedSpace ℝ E] (x : ↑{x : E | 0 < ‖x‖}) : ↑((homeomorphUnitSphereProdOfNormPos E) x).1 = ‖↑x‖⁻¹ • ↑x

@[simp]

theorem TauCeti.homeomorphUnitSphereProdOfNormPos_apply_snd_coe (E : Type u_1) [SeminormedAddCommGroup E] [NormedSpace ℝ E] (x : ↑{x : E | 0 < ‖x‖}) : ↑((homeomorphUnitSphereProdOfNormPos E) x).2 = ‖↑x‖

@[simp]

theorem TauCeti.homeomorphUnitSphereProdOfNormPos_symm_apply_coe (E : Type u_1) [SeminormedAddCommGroup E] [NormedSpace ℝ E] (p : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)) : ↑((homeomorphUnitSphereProdOfNormPos E).symm p) = ↑p.2 • ↑p.1

theorem Topology.IsOpenEmbedding.smul_coe_sphere {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {Y : Type u_2} [TopologicalSpace Y] {ρ : Y → ℝ} (hρ : IsOpenEmbedding ρ) (hpos : ∀ (y : Y), 0 < ρ y) : IsOpenEmbedding fun (q : ↑(Metric.sphere 0 1) × Y) => ρ q.2 • ↑q.1

Polar coordinates with a reparametrized radius. If ρ : Y → ℝ is an open embedding with positive values, then (u, y) ↦ ρ y • u is an open embedding of sphere (0 : E) 1 × Y into E, onto the vectors whose norm lies in the range of ρ.

Exponential polar coordinates

noncomputable def TauCeti.polar {V : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] (q : ↑(Metric.sphere 0 1) × ℝ) : V

Polar coordinates on the complement of the origin, with time t on the sphere of radius exp (t - 1): time 1 is the unit sphere, and the times t ≤ 1 fill the punctured closed unit ball.

theorem TauCeti.polar_apply {V : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] (q : ↑(Metric.sphere 0 1) × ℝ) : polar q = Real.exp (q.2 - 1) • ↑q.1

The value of the exponential polar-coordinate map.

@[simp]

theorem TauCeti.norm_polar {V : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] (q : ↑(Metric.sphere 0 1) × ℝ) : ‖polar q‖ = Real.exp (q.2 - 1)

The radius in exponential polar coordinates.

theorem TauCeti.polar_ne_zero {V : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] (q : ↑(Metric.sphere 0 1) × ℝ) : polar q ≠ 0

Exponential polar coordinates avoid the origin.

theorem TauCeti.isOpenEmbedding_polar {V : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] : Topology.IsOpenEmbedding polar

Exponential polar coordinates embed the sphere times the real line openly.

theorem TauCeti.mem_range_polar {V : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] {v : V} (hv : v ≠ 0) : v ∈ Set.range polar

Every nonzero vector has exponential polar coordinates.