isometryEquivWeightedSumSquares — Mathlib

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₁]

Похожие утверждения