English
In a suitable ordered ring, (a+b)^2 ≤ 2(a^2 + b^2).
Русский
В подходящем упорядоченном кольце (a+b)^2 ≤ 2(a^2 + b^2).
LaTeX
$$$ (a+b)^2 \le 2\,(a^2 + b^2).$$$
Lean4
theorem add_sq_le : (a + b) ^ 2 ≤ 2 * (a ^ 2 + b ^ 2) :=
by
calc
(a + b) ^ 2 = a ^ 2 + b ^ 2 + (a * b + b * a) := by
simp_rw [pow_succ', pow_zero, mul_one, add_mul, mul_add, add_comm (b * a), add_add_add_comm]
_ ≤ a ^ 2 + b ^ 2 + (a * a + b * b) := (add_le_add_left ?_ _)
_ = _ := by simp_rw [pow_succ', pow_zero, mul_one, two_mul]
cases le_total a b
· exact mul_add_mul_le_mul_add_mul ‹_› ‹_›
·
exact
mul_add_mul_le_mul_add_mul' ‹_›
‹_›
-- TODO: Use `gcongr`, `positivity`, `ring` once those tactics are made available here
