Radial projection to the unit sphere

This file packages pointwise normalization of a continuous nowhere-zero map as a continuous map to the unit sphere.

noncomputable def TauCeti.normalizeToSphere {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {Y : Type u_2} [TopologicalSpace Y] (f : Y → E) (hf : Continuous f) (h0 : ∀ (y : Y), f y ≠ 0) : C(Y, ↑(Metric.sphere 0 1))

Radial projection sends a continuous nowhere-zero map into a real normed space continuously to its unit sphere.

Equations

• TauCeti.normalizeToSphere f hf h0 = { toFun := fun (y : Y) => ⟨NormedSpace.normalize (f y), ⋯⟩, continuous_toFun := ⋯ }

@[simp]

theorem TauCeti.coe_normalizeToSphere_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {Y : Type u_2} [TopologicalSpace Y] (f : Y → E) (hf : Continuous f) (h0 : ∀ (y : Y), f y ≠ 0) (y : Y) : ↑((normalizeToSphere f hf h0) y) = NormedSpace.normalize (f y)

The underlying vector of normalizeToSphere f hf h0 y is the normalization of f y.