English
Product PosDef is equivalent to both components being PosDef under a partial order.
Русский
PosDef произведения эквивалентна тому, что обе компоненты PosDef.
LaTeX
$$Under [PartialOrder P] and [AddLeftMono P], (Q1.prod Q2).PosDef iff Q1.PosDef ∧ Q2.PosDef.$$
Lean4
theorem posDef_prod_iff [PartialOrder P] [AddLeftMono P] {Q₁ : QuadraticMap R M₁ P} {Q₂ : QuadraticMap R M₂ P} :
(Q₁.prod Q₂).PosDef ↔ Q₁.PosDef ∧ Q₂.PosDef :=
by
simp_rw [posDef_iff_nonneg, nonneg_prod_iff]
constructor
· rintro ⟨⟨hle₁, hle₂⟩, ha⟩
obtain ⟨ha₁, ha₂⟩ := anisotropic_of_prod ha
exact ⟨⟨hle₁, ha₁⟩, ⟨hle₂, ha₂⟩⟩
· rintro ⟨⟨hle₁, ha₁⟩, ⟨hle₂, ha₂⟩⟩
refine ⟨⟨hle₁, hle₂⟩, ?_⟩
rintro ⟨x₁, x₂⟩ (hx : Q₁ x₁ + Q₂ x₂ = 0)
rw [add_eq_zero_iff_of_nonneg (hle₁ x₁) (hle₂ x₂), ha₁.eq_zero_iff, ha₂.eq_zero_iff] at hx
rwa [Prod.mk_eq_zero]
