Symmetric matrix quadratic forms on the standard simplex

This file records the expansion of a symmetric matrix quadratic form along a line and the first-order inequality at a minimizer on the standard simplex.

Main results

• Matrix.IsSymm.dotProduct_mulVec_add_smul: over a commutative semiring, expands the quadratic form of a symmetric matrix along a line.
• Matrix.IsSymm.mulVec_apply_le_of_isMinOn: over a linearly ordered field, at a simplex minimizer, a coordinate of M y in the support of y is no larger than any other coordinate of M y.

theorem Matrix.IsSymm.dotProduct_mulVec_add_smul {n : Type u_1} {R : Type u_2} [Fintype n] [CommSemiring R] {M : Matrix n n R} (hM : M.IsSymm) (y d : n → R) (t : R) : (y + t • d) ⬝ᵥ M.mulVec (y + t • d) = y ⬝ᵥ M.mulVec y + 2 * t * d ⬝ᵥ M.mulVec y + t ^ 2 * d ⬝ᵥ M.mulVec d

The quadratic form of a symmetric matrix along the line through y in the direction d.

theorem Matrix.IsSymm.mulVec_apply_le_of_isMinOn {n : Type u_1} {R : Type u_2} [Fintype n] [Field R] [LinearOrder R] [IsStrictOrderedRing R] {M : Matrix n n R} (hM : M.IsSymm) {y : n → R} (hy : 0 ≤ y ∧ ∑ k : n, y k = 1) (hmin : IsMinOn (fun (z : n → R) => z ⬝ᵥ M.mulVec z) {z : n → R | 0 ≤ z ∧ ∑ k : n, z k = 1} y) {i : n} (hi : 0 < y i) (j : n) : M.mulVec y i ≤ M.mulVec y j

At a minimizer y of the quadratic form of a symmetric matrix on the standard simplex, the entry (M y)ᵢ at a coordinate in the support of y is the smallest entry of M y.