English
Let a and b be elements of a totally ordered field with a compatible quadratic form, and let ε > 0. Then 2ab ≤ ε a^2 + ε^(-1) b^2. This is a canonical inequality bounding the product by a weighted sum of squares.
Русский
Пусть a и b являются элементами полностью упорядоченного поля с совместимой квадратичной формой, и дано ε > 0. Тогда 2ab ≤ ε a^2 + ε^(-1) b^2. Это каноническое неравенство, ограничивающее произведение взвешенной суммой квадратов.
LaTeX
$$$\\forall a,b,ε>0:\\ 2ab\\le εa^2+ε^{-1}b^2$$$
Lean4
theorem two_mul_le_add_mul_sq {ε : α} (hε : 0 < ε) : 2 * a * b ≤ ε * a ^ 2 + ε⁻¹ * b ^ 2 :=
by
have h : 2 * (ε * a) * b ≤ (ε * a) ^ 2 + b ^ 2 := two_mul_le_add_sq (ε * a) b
calc
2 * a * b
_ = 2 * a * b * (ε * ε⁻¹) := by rw [mul_inv_cancel₀ hε.ne', mul_one]
_ = (2 * (ε * a) * b) * ε⁻¹ := by simp_rw [mul_assoc, mul_comm ε, mul_assoc]
_ ≤ ((ε * a) ^ 2 + b ^ 2) * ε⁻¹ := by gcongr; exact inv_nonneg.mpr hε.le
_ = ε * a ^ 2 + ε⁻¹ * b ^ 2 := by
rw [mul_comm _ ε⁻¹, mul_pow, mul_add, ← mul_assoc, pow_two, ← mul_assoc, inv_mul_cancel₀ hε.ne', one_mul]
