Schur's cubic sum bounds a product of squared differences
ProvedWorkbookSource.base_20293lean-workbooksource-checked
The best result here is the following.
Let , and be positive numbers. Prove that:
Source: InternLM Lean-Workbook, record lean_workbook_20293 (Apache-2.0). Complete source proposition preserved; proof developed independently.
Preamble
import Mathlib open Real Nat
Formal statement
theorem WorkbookSource.base_20293 (a b c : ℝ) (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) : a * (a - b) * (a - c) + b * (b - a) * (b - c) + c * (c - a) * (c - b) ≥ (4 * (a - b) ^ 2 * (a - c) ^ 2 * (b - c) ^ 2) / (a ^ 3 + b ^ 3 + c ^ 3) := by sorry
Source