Euclidean coordinates for positive-definite real Clifford forms

The positive-definite real Clifford form is the squared Euclidean norm after passing between function and Euclidean-space coordinates. Consequently, its unit quadric is identified with the Euclidean unit sphere.

Main results

• TauCeti.realCliffordForm_zero_euclideanSpaceEquiv_eq_norm_sq identifies the positive-definite real Clifford form with the squared Euclidean norm in Euclidean coordinates.
• TauCeti.norm_euclideanSpaceEquiv_symm_eq_one_of_realCliffordForm_zero_eq_one sends unit-quadric vectors to Euclidean unit vectors.
• TauCeti.realCliffordForm_zero_euclideanSpaceEquiv_eq_one sends Euclidean unit vectors to the unit quadric.

@[simp]

theorem TauCeti.realCliffordForm_zero_euclideanSpaceEquiv_eq_norm_sq {n : ℕ} (u : EuclideanSpace ℝ (Fin n)) : (realCliffordForm n 0) ((EuclideanSpace.equiv (Fin n) ℝ) u) = ‖u‖ ^ 2

The positive-definite real Clifford form is the squared Euclidean norm in Euclidean coordinates.

theorem TauCeti.norm_euclideanSpaceEquiv_symm_eq_one_of_realCliffordForm_zero_eq_one {n : ℕ} {v : Fin n → ℝ} (hv : (realCliffordForm n 0) v = 1) : ‖(EuclideanSpace.equiv (Fin n) ℝ).symm v‖ = 1

A vector on the unit quadric of the positive-definite real Clifford form has Euclidean norm one in Euclidean coordinates.

theorem TauCeti.realCliffordForm_zero_euclideanSpaceEquiv_eq_one {n : ℕ} (u : ↑(Metric.sphere 0 1)) : (realCliffordForm n 0) ((EuclideanSpace.equiv (Fin n) ℝ) ↑u) = 1

Every Euclidean unit vector lies on the unit quadric of the positive-definite real Clifford form after passing to Euclidean coordinates.