Finite sums of truncations of natural numbers

For a finite family c of natural numbers, the truncated sums ∑ l, min k (c l) count the boxes in the first k columns of the Young diagram with rows c l. Their second differences count the members of the family in a range: for p < q, the combination of the truncated sums at p + 1, q - 1, p and q is the number of members strictly between p and q.

Main results

• Finset.sum_min_add_sum_min_eq: the second-difference identity for truncated sums.
• Finset.exists_ne_forall_sum_min_lt: if the column counts of a family b are at most those of a family a with the same sum, and strictly smaller for some k, then two distinct members a j ≤ a i of a keep the inequality strict for all a j ≤ k ≤ a i. Moving a box between these two rows is the key step in generating dominance of partitions by box moves.

theorem Finset.sum_min_add_sum_min_eq {α : Type u_1} (u : Finset α) (c : α → ℕ) {p q : ℕ} (hpq : p < q) : ∑ l ∈ u, min (p + 1) (c l) + ∑ l ∈ u, min (q - 1) (c l) = ∑ l ∈ u, min p (c l) + ∑ l ∈ u, min q (c l) + {l ∈ u | p < c l ∧ c l < q}.card

For p < q, the second differences of the truncated sums ∑ l, min k (c l) at p and q count the members of the family c strictly between p and q.

theorem Finset.exists_ne_forall_sum_min_lt {ι : Type u_2} {κ : Type u_3} {s : Finset ι} {t : Finset κ} {a : ι → ℕ} {b : κ → ℕ} (hsum : ∑ l ∈ t, b l = ∑ l ∈ s, a l) (hle : ∀ (k : ℕ), ∑ l ∈ t, min k (b l) ≤ ∑ l ∈ s, min k (a l)) (hlt : ∃ (k : ℕ), ∑ l ∈ t, min k (b l) < ∑ l ∈ s, min k (a l)) : ∃ i ∈ s, ∃ j ∈ s, i ≠ j ∧ a j ≤ a i ∧ ∀ (k : ℕ), a j ≤ k → k ≤ a i → ∑ l ∈ t, min k (b l) < ∑ l ∈ s, min k (a l)

A pair of rows realising a strict inequality of column counts. Let a and b be finite families of natural numbers with the same sum, such that for every k the column count ∑ min k (b l) of b is at most the column count ∑ min k (a l) of a, strictly for some k. Then a has two distinct members a j ≤ a i such that the inequality is strict for every k with a j ≤ k ≤ a i. Moving one box from row j to row i lowers the column count of a by one exactly for a j ≤ k ≤ a i, so the result still has column counts at least those of b.