Finite layer-cake decomposition

Section 5 lifts inequalities for hereditary families to inequalities for nonnegative decreasing weights by layer cake. On a finite space, integration can be replaced by repeatedly subtracting the smallest positive weight from its support. The support is a lower set, and each step strictly shrinks it.

theorem Chvatal.sum_mul_antitone_nonneg_of_lowerSets {α : Type u_1} [Fintype α] [Preorder α] (c : α → ℝ) (hc : ∀ (D : Finset α), IsLowerSet ↑D → 0 ≤ ∑ x ∈ D, c x) (ω : α → ℝ) (hω : ∀ (x : α), 0 ≤ ω x) (hanti : Antitone ω) : 0 ≤ ∑ x : α, c x * ω x

The finite layer-cake principle used in Section 5 (Proposition 5.3): if a signed function has nonnegative sum on every lower set, then its scalar product with every nonnegative antitone weight is nonnegative. This also covers an empty underlying type.