Multisets of natural numbers compared through their initial counts

A multiset s of natural numbers is determined by its initial counts countP (· ≤ n) s, the numbers of its elements of size at most n (Multiset.ext_countP_le). Its sum is read off the complementary counts: s.sum = ∑_{k < B} countP (k < ·) s for every bound B on the elements of s (Multiset.sum_eq_sum_range_countP_lt), each element x being counted once for every k < x.

Suppose that s and t have the same cardinality and that, for every n, t has at least as many elements of size at most n as s does. Then t is pointwise smaller than s after sorting, so t.sum ≤ s.sum, and equality of the sums forces s = t (Multiset.eq_of_forall_countP_le_le_of_sum_le).

This is the combinatorial step in comparing the degrees of homogeneous generators of two graded polynomial algebras A ⊆ B of the same dimension: algebraic independence bounds the number of generators of A of degree at most n by the corresponding number for B, and an independent computation of the sums of the degrees then shows that the two multisets of degrees coincide.

theorem Multiset.countP_le_eq_count_add_countP_lt (s : Multiset ℕ) (a : ℕ) : countP (fun (x : ℕ) => x ≤ a) s = count a s + countP (fun (x : ℕ) => x < a) s

The number of elements of size at most a is the multiplicity of a plus the number of elements smaller than a.

theorem Multiset.ext_countP_le {s t : Multiset ℕ} (h : ∀ (n : ℕ), countP (fun (x : ℕ) => x ≤ n) s = countP (fun (x : ℕ) => x ≤ n) t) : s = t

A multiset of natural numbers is determined by its initial counts. If, for every n, the multisets s and t have the same number of elements of size at most n, then s = t.

theorem Multiset.sum_eq_sum_range_countP_lt {s : Multiset ℕ} {B : ℕ} (hs : ∀ x ∈ s, x ≤ B) : s.sum = ∑ k ∈ Finset.range B, countP (fun (x : ℕ) => k < x) s

The sum of a multiset of natural numbers from its counts. If every element of s is at most B, then s.sum is the sum over k < B of the number of elements of s larger than k.

theorem Multiset.eq_of_forall_countP_le_le_of_sum_le {s t : Multiset ℕ} (hcard : s.card = t.card) (h : ∀ (n : ℕ), countP (fun (x : ℕ) => x ≤ n) s ≤ countP (fun (x : ℕ) => x ≤ n) t) (hsum : s.sum ≤ t.sum) : s = t

Equal sums and dominated initial counts force equality. Let s and t be multisets of natural numbers of the same cardinality such that, for every n, t has at least as many elements of size at most n as s. If s.sum ≤ t.sum, then s = t.