English
Let R be a linearly ordered commutative semiring with a ≥ 0 and d ≥ 0. Then 4 a b ≤ (a + b)^2 for all a,b.
Русский
Пусть R — упорядоченное коммутативное полукольцо; тогда 4ab ≤ (a+b)^2 при a≥0, b≥0.
LaTeX
$$$$4 a b \\le (a + b)^2 \\quad\\text{whenever } a \\ge 0,\\; b \\ge 0.$$$$
Lean4
/-- Binary, squared, and division-free **arithmetic mean-geometric mean inequality**
(aka AM-GM inequality) for linearly ordered commutative semirings. -/
theorem four_mul_le_sq_add [ExistsAddOfLE R] [MulPosStrictMono R] [AddLeftReflectLE R] [AddLeftMono R] (a b : R) :
4 * a * b ≤ (a + b) ^ 2 := by
calc
4 * a * b
_ = 2 * a * b + 2 * a * b := by rw [mul_assoc, two_add_two_eq_four.symm, add_mul, mul_assoc]
_ ≤ a ^ 2 + b ^ 2 + 2 * a * b := by gcongr; exact two_mul_le_add_sq _ _
_ = a ^ 2 + 2 * a * b + b ^ 2 := by rw [add_right_comm]
_ = (a + b) ^ 2 := (add_sq a b).symm
