English
Let R be a linearly ordered commutative semiring with a ≥ 0, b ≥ 0, and a chosen r with r^2 = a b. Then 2 r ≤ a + b.
Русский
Пусть R — упорядоченное коммутативное полукольцо; если a ≥ 0, b ≥ 0 и r^2 = ab, то 2r ≤ a + b.
LaTeX
$$$$a \\ge 0,\\; b \\ge 0,\\; r^2 = a b \\Rightarrow 2 r \\le a + b.$$$$
Lean4
/-- Binary and division-free **arithmetic mean-geometric mean inequality**
(aka AM-GM inequality) for linearly ordered commutative semirings. -/
theorem two_mul_le_add_of_sq_eq_mul [ExistsAddOfLE R] [MulPosStrictMono R] [PosMulStrictMono R] [AddLeftReflectLE R]
[AddLeftMono R] {a b r : R} (ha : 0 ≤ a) (hb : 0 ≤ b) (ht : r ^ 2 = a * b) : 2 * r ≤ a + b :=
by
apply nonneg_le_nonneg_of_sq_le_sq (Left.add_nonneg ha hb)
conv_rhs => rw [← pow_two]
convert four_mul_le_sq_add a b using 1
rw [mul_mul_mul_comm, two_mul, two_add_two_eq_four, ← pow_two, ht, mul_assoc]
