One-dimensional Hlawka inequality
ProvedHlawka1D.hlawka_1dhlawka-schatteninequalitysharp-constant
For real numbers : . The one-dimensional case of Hlawka's inequality; the base case for the proof that the sharp diagonal Hlawka constant of is .
Preamble
import Mathlib
Formal statement
theorem Hlawka1D.hlawka_1d : ∀ a b c : ℝ, |a + b| + |b + c| + |c + a| ≤ |a| + |b| + |c| + |a + b + c| := by sorry
Source
Hlawka's inequality (1944); 1D case used as base for the p=2 sharp Hlawka constant proof