Hlawka's inequality and its generalisation by Djoković

Hlawka's inequality ‖x+y‖ + ‖y+z‖ + ‖z+x‖ ≤ ‖x‖ + ‖y‖ + ‖z‖ + ‖x+y+z‖ in a real inner product space, and its generalisation (Djoković 1963; Smiley–Smiley 1964): for n ≥ 3 vectors, with d_k the sum of the norms of all k-element subsums, d_2 + ⋯ + d_{n-1} ≤ (2^(n-2) - 1) (d_1 + d_n). The general case is equivalent to 4F ≤ 2^n (d_1 + d_n), where F sums the norms of the subsums over all subsets; it is proved by strong induction on the number of vectors, merging two of them, x a and x b, into x a + x b: the subsets containing both or neither form the merged family, and each subset T containing exactly one of them is handled by Hlawka's inequality for (Σ_T, x a, x b).

Main results

• Hlawka.norm_add_add_le: Hlawka's inequality for three vectors
• Hlawka.generalised: d_2 + ... + d_(n-1) <= (2^(n-2) - 1)(d_1 + d_n) for n >= 3 vectors

References

• D. Ž. Djoković, Generalizations of Hlawka's inequality, Glasnik Mat.-Fiz. Astronom. 18 (1963), 169–175.
• D. M. Smiley and M. F. Smiley, The polygonal inequalities, Amer. Math. Monthly 71 (1964), 755–760.

theorem Hlawka.norm_add_add_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (x y z : E) : ‖x + y‖ + ‖y + z‖ + ‖z + x‖ ≤ ‖x‖ + ‖y‖ + ‖z‖ + ‖x + y + z‖

Hlawka's inequality (n = 3).

theorem Hlawka.generalised {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} (hn : 3 ≤ n) (x : Fin n → E) : ∑ k ∈ Finset.Icc 2 (n - 1), ∑ S ∈ Finset.powersetCard k Finset.univ, ‖∑ i ∈ S, x i‖ ≤ (2 ^ (n - 2) - 1) * (∑ i : Fin n, ‖x i‖ + ‖∑ i : Fin n, x i‖)

Generalised Hlawka inequality (Djoković 1963; Smiley–Smiley 1964). For n ≥ 3 vectors of a real inner product space, write d_k for the sum of the norms of all k-element subsums. Then d_2 + ⋯ + d_{n-1} ≤ (2^(n-2) - 1) (d_1 + d_n). For n = 3 this is Hlawka's inequality ‖x+y‖ + ‖y+z‖ + ‖z+x‖ ≤ ‖x‖ + ‖y‖ + ‖z‖ + ‖x+y+z‖.