sum_repr_sq_add_sum_repr_mul_polar

English

For a quadratic map Q, a chosen basis bm of M, and a vector x ∈ M, write x in coordinates relative to bm, x = ∑ i x_i bm_i. Then Q(x) can be recovered from the coordinate representation by summing the squared coordinates against Q applied to the basis vectors, and adding the pairwise interaction terms given by polarSym2 Q evaluated on pairs of basis vectors with coefficients x_i x_j. In formula: Q(x) = ∑ i x_i^2 Q(bm_i) + ∑_{i<j} x_i x_j polar(Q)(bm_i, bm_j).

Русский

Пусть Q— квадратичное отображение, bm — база для M, и x ∈ M. Разложим x по координатам: x = sum_i x_i bm_i. Тогда Q(x) восстанавливается из координат: сумма x_i^2 Q(bm_i) по i плюс пары взаимодействий: сумма по i<j of x_i x_j polar(Q)(bm_i, bm_j).

LaTeX

$$$ Q(x) = \\sum_i x_i^2\,Q(bm_i) + \\sum_{i

Lean4

/-- The quadratic version of `LinearMap.sum_repr_mul_repr_mul`. -/
theorem sum_repr_sq_add_sum_repr_mul_polar (Q : QuadraticMap R M N) (bm : Basis ι R M) (x : M) :
    linearCombination R (Q ∘ bm) (bm.repr x * bm.repr x) +
        ∑ p ∈ (bm.repr x).support.sym2 with ¬p.IsDiag, Sym2.mul (p.map (bm.repr x)) • polarSym2 Q (p.map bm) =
      Q x :=
  by rw [← apply_linearCombination, Basis.linearCombination_repr]

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