English
For a pi Q, nonnegativity of all coordinates is equivalent to nonnegativity of each component on its domain.
Русский
Для pi Q, неотрицательность на всем пространстве эквивалентна неотрицательности для каждой компоненты на её области определения.
LaTeX
$$$ (\\forall x, 0 \\le \\pi Q x) \\iff \\forall i x, 0 \\le Q_i x. $$$
Lean4
theorem nonneg_pi_iff {P} [Fintype ι] [AddCommMonoid P] [PartialOrder P] [IsOrderedAddMonoid P] [Module R P]
{Q : ∀ i, QuadraticMap R (Mᵢ i) P} : (∀ x, 0 ≤ pi Q x) ↔ ∀ i x, 0 ≤ Q i x :=
by
simp_rw [pi, sum_apply, comp_apply, LinearMap.proj_apply]
constructor
-- TODO: does this generalize to a useful lemma independent of `QuadraticMap`?
· intro h i x
classical
convert h (Pi.single i x) using 1
rw [Finset.sum_eq_single_of_mem i (Finset.mem_univ _) fun j _ hji => ?_, Pi.single_eq_same]
rw [Pi.single_eq_of_ne hji, map_zero]
· rintro h x
exact Finset.sum_nonneg fun i _ => h i (x i)
