theorem exists_Q_of_linearEquiv_diag {n : ℕ} (A : (Fin n → ℝ) ≃ₗ[ℝ] Fin n → ℝ) (d : Fin n → ℝ) : ∃ (Q : (Fin n → ℝ) →ₗ[ℝ] Fin n → ℝ), (∀ (x y : Fin n → ℝ), Q x ⬝ᵥ y = x ⬝ᵥ Q y) ∧ ∀ (x : Fin n → ℝ), x ⬝ᵥ Q x = ∑ i : Fin n, d i * A x i ^ 2

Given a linear equivalence A and diagonal weights d, build a dot-product symmetric linear map Q whose quadratic form is x ↦ ∑ i, d i * (A x i)^2.