English
The positive definiteness of the product pi is equivalent to the positive definiteness of each component.
Русский
Положительная определённость произведения pi эквивалентна положительной определённости каждой компоненты.
LaTeX
$$$ (\\pi Q).\\mathrm{PosDef} \\iff \\forall i, Q_i.\\mathrm{PosDef}. $$$
Lean4
theorem posDef_pi_iff {P} [Fintype ι] [AddCommMonoid P] [PartialOrder P] [IsOrderedAddMonoid P] [Module R P]
{Q : ∀ i, QuadraticMap R (Mᵢ i) P} : (pi Q).PosDef ↔ ∀ i, (Q i).PosDef :=
by
simp_rw [posDef_iff_nonneg, nonneg_pi_iff]
constructor
· rintro ⟨hle, ha⟩
intro i
exact ⟨hle i, anisotropic_of_pi ha i⟩
· intro h
refine ⟨fun i => (h i).1, fun x hx => funext fun i => (h i).2 _ ?_⟩
rw [pi_apply, Finset.sum_eq_zero_iff_of_nonneg fun j _ => ?_] at hx
· exact hx _ (Finset.mem_univ _)
exact (h j).1 _
