English
Given an orthogonal basis, a quadratic form is isometrically equivalent to a weighted sum of squares with weights Q(v_i).
Русский
При ортогональном базисе квадратичная форма изометрически эквивалентна взвешенной сумме квадратов с весами $Q(v_i)$.
LaTeX
$$$Q$ is isometric to $\operatorname{weightedSumSquares} K (\lambda i. Q(v_i))$ whenever $(\operatorname{associated}(Q)).IsOrtho_i v$.$$
Lean4
/-- Given an orthogonal basis, a quadratic form is isometrically equivalent with a weighted sum of
squares. -/
noncomputable def isometryEquivWeightedSumSquares (Q : QuadraticForm K V) (v : Basis (Fin (Module.finrank K V)) K V)
(hv₁ : (associated (R := K) Q).IsOrthoᵢ v) : Q.IsometryEquiv (weightedSumSquares K fun i => Q (v i)) :=
by
let iso := Q.isometryEquivBasisRepr v
refine ⟨iso, fun m => ?_⟩
convert iso.map_app m
rw [basisRepr_eq_of_iIsOrtho _ _ hv₁]