Antitone finitely supported sequences

A finitely supported sequence f : ℕ →₀ α that is antitone takes only nonnegative values, and it is determined by how many times it takes each nonzero value: it lists its nonzero values in nonincreasing order, followed by zeros. Sorted, zero-padded sequences of this kind are how Mathlib records singular values (LinearMap.singularValues), so this is the uniqueness principle used to identify two such sequences from their multiplicities. Nonnegativity holds in any preorder, and uniqueness requires only a partial order on the values.

Main declarations

• Finsupp.nonneg_of_antitone: an antitone finitely supported sequence is nonnegative.
• Finsupp.eq_of_antitone_of_ncard_eq: two antitone finitely supported sequences that take every nonzero value equally often are equal.

theorem Finsupp.nonneg_of_antitone {α : Type u_1} [Zero α] [Preorder α] {f : ℕ →₀ α} (hf : Antitone ⇑f) (i : ℕ) : 0 ≤ f i

An antitone finitely supported sequence takes only nonnegative values.

theorem Finsupp.eq_of_antitone_of_ncard_eq {α : Type u_1} [Zero α] [PartialOrder α] {f g : ℕ →₀ α} (hf : Antitone ⇑f) (hg : Antitone ⇑g) (h : ∀ (a : α), a ≠ 0 → {i : ℕ | f i = a}.ncard = {i : ℕ | g i = a}.ncard) : f = g

An antitone finitely supported sequence is determined by how many times it takes each nonzero value.