@[reducible, inline]

noncomputable abbrev Matrix.qNorm {n : ℕ} (Q : Matrix (Fin n) (Fin n) ℝ) (hQ : Q.PosDef) (x : Fin n → ℝ) : ℝ

The source-facing Q-norm on ℝ^n induced by the canonical owner Matrix.toNormedAddCommGroup.

theorem euclideanSpace_norm_eq_sqrt_sum_sq {n : ℕ} (x : EuclideanSpace ℝ (Fin n)) : ‖x‖ = √(∑ i : Fin n, x.ofLp i ^ 2)

The Euclidean norm on ℝ^n is the square root of the sum of the coordinate squares.

theorem norm_eq_sqrt_dotProduct_mulVec_of_posDef {n : ℕ} (Q : Matrix (Fin n) (Fin n) ℝ) (hQ : Q.PosDef) (x : Fin n → ℝ) : have qSeminormed := Q.toSeminormedAddCommGroup ⋯; have qNormed := Q.toNormedAddCommGroup hQ; ‖x‖ = √(x ⬝ᵥ Q.mulVec x)

If ℝ^n is endowed with the Q-inner product associated to a positive definite matrix Q, then the induced Euclidean norm is the Q-norm √(xᵀ Q x).

theorem qNorm_sq_eq_qInner_self {n : ℕ} (Q : Matrix (Fin n) (Fin n) ℝ) (hQ : Q.PosDef) (x : Fin n → ℝ) : Q.qNorm hQ x ^ 2 = Q.qInner hQ x x

In the Q-geometry, the squared Q-norm is the Q-inner self-pairing.