English
Let R be a linearly ordered commutative semiring with appropriate additive-multiplicative monotonicity. If a ≥ 0, b ≥ 0 and 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 \\quad\\Rightarrow\\quad 2 r \\le a + b.$$$$
Lean4
/-- Binary, squared, and division-free **arithmetic mean-geometric mean inequality**
(aka AM-GM inequality) for linearly ordered commutative semirings. -/
theorem two_mul_le_add_sq [ExistsAddOfLE R] [MulPosStrictMono R] [AddLeftReflectLE R] [AddLeftMono R] (a b : R) :
2 * a * b ≤ a ^ 2 + b ^ 2 := by
simpa [fn_min_add_fn_max (fun x ↦ x * x), sq, two_mul, add_mul] using
mul_add_mul_le_mul_add_mul (@min_le_max _ _ a b) (@min_le_max _ _ a b)
