Schurs_Inequality
Provedalgebrainequalitiesproofwiki
For nonneg reals x, y, z and positive natural number t, x^t(x-y)(x-z) + y^t(y-x)(y-z) + z^t(z-x)(z-y) >= 0.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Schurs_Inequality (x y z : ℝ) (hx : 0 ≤ x) (hy : 0 ≤ y) (hz : 0 ≤ z) (t : ℕ) (ht : 0 < t) : x ^ t * (x - y) * (x - z) + y ^ t * (y - x) * (y - z) + z ^ t * (z - x) * (z - y) ≥ 0 := by sorry
Source