English
On an orthogonal basis, the basis representation of Q is a sum of squares with the basis elements.
Русский
На ортогональном базисе представление Q является суммой квадратов по элементам базиса.
LaTeX
$$Q.basisRepr v = weightedSumSquares R (\i => Q(v_i))$$
Lean4
/-- On an orthogonal basis, the basis representation of `Q` is just a sum of squares. -/
theorem basisRepr_eq_of_iIsOrtho {R M} [CommRing R] [AddCommGroup M] [Module R M] [Invertible (2 : R)]
(Q : QuadraticForm R M) (v : Basis ι R M) (hv₂ : (associated (R := R) Q).IsOrthoᵢ v) :
Q.basisRepr v = weightedSumSquares _ fun i => Q (v i) :=
by
ext w
rw [basisRepr_apply, ← @associated_eq_self_apply R, map_sum, weightedSumSquares_apply]
refine sum_congr rfl fun j hj => ?_
rw [← @associated_eq_self_apply R, LinearMap.map_sum₂, sum_eq_single_of_mem j hj]
· rw [LinearMap.map_smul, LinearMap.map_smul₂, smul_eq_mul, associated_apply, smul_eq_mul, smul_eq_mul,
Module.End.smul_def, half_moduleEnd_apply_eq_half_smul]
ring_nf
· intro i _ hij
rw [LinearMap.map_smul, LinearMap.map_smul₂, hv₂ hij]
module
