English
For any x : α → ℕ and list l of polynomials, 0 ≤ sumsq l x.
Русский
Для любого x : α → ℕ и списка полиномов l выполняется 0 ≤ sumsq l x.
LaTeX
$$$$ 0 \\le \\text{sumsq} \\; l \\; x $$$$
Lean4
theorem sumsq_eq_zero (x) : ∀ l, sumsq l x = 0 ↔ l.Forall fun a : Poly α => a x = 0
| [] => eq_self_iff_true _
| p :: ps => by
rw [List.forall_cons, ← sumsq_eq_zero _ ps]; rw [sumsq]
exact
⟨fun h : p x * p x + sumsq ps x = 0 =>
have : p x = 0 :=
eq_zero_of_mul_self_eq_zero <|
le_antisymm
(by
rw [← h]
have t := add_le_add_left (sumsq_nonneg x ps) (p x * p x)
rwa [add_zero] at t)
(mul_self_nonneg _)
⟨this, by simpa [this] using h⟩,
fun ⟨h1, h2⟩ => by rw [add_apply, mul_apply, h1, h2]; rfl⟩
