English
The inverse stereographic' map expressed in Euclidean coordinates involves the same U as above and norm terms; the expression is given by combining U.symm x with v and quadratic norm terms.
Русский
Обратная карта stereographic' выражена через тот же базис U и норму; выражение содержит u и норму в квадратичных коэффициентах.
LaTeX
$$$((\\text{stereographic'}\\ n v).symm\\ toFun' x) = (\\|U^{-1}x\\|^2 + 4)^{-1} · (4 · U^{-1}x) + (\\|U^{-1}x\\|^2 + 4)^{-1} · (\\|U^{-1}x\\|^2 - 4) · v$$$
Lean4
theorem stereographic'_symm_apply {n : ℕ} [Fact (finrank ℝ E = n + 1)] (v : sphere (0 : E) 1)
(x : EuclideanSpace ℝ (Fin n)) :
((stereographic' n v).symm x : E) =
let U : (ℝ ∙ (v : E))ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) :=
(OrthonormalBasis.fromOrthogonalSpanSingleton n (ne_zero_of_mem_unit_sphere v)).repr
(‖(U.symm x : E)‖ ^ 2 + 4)⁻¹ • (4 : ℝ) • (U.symm x : E) +
(‖(U.symm x : E)‖ ^ 2 + 4)⁻¹ • (‖(U.symm x : E)‖ ^ 2 - 4) • v.val :=
by simp [stereographic, stereographic', ← Submodule.coe_norm]
