Strictly antitone sequences indexed by Fin n

A sequence f : Fin n → α is strictly antitone when it strictly decreases along the indices. This file records three facts about such sequences, used for beta-numbers of Young diagrams and the Pieri rule for Schur polynomials.

Over ℕ a strictly antitone sequence drops by at least one at each step, so it drops by at least the index gap: StrictAnti.add_sub_le_nat. This is what makes a strictly decreasing sequence of n natural numbers a sequence of beta-numbers of a Young diagram. The increasing analogue indexed by all of ℕ is StrictMono.add_le_nat.

Over any linear order, an injective sequence becomes strictly antitone after precomposition with a suitable permutation of the indices (Function.Injective.exists_strictAnti_comp), and over any partial order that permutation is unique (StrictAnti.perm_eq): sorting into decreasing order is possible and unambiguous. Mathlib's Tuple.sort sorts into increasing order; composing with the reversal Fin.revPerm turns it around.

Main results

• StrictAnti.add_sub_le_nat: a strictly antitone sequence of naturals drops by at least the index gap.
• Function.Injective.exists_strictAnti_comp: an injective sequence can be sorted into decreasing order.
• StrictAnti.perm_eq: the sorting permutation is unique.

theorem StrictAnti.add_sub_le_nat {n : ℕ} {η : Fin n → ℕ} (hη : StrictAnti η) {i j : Fin n} (hij : i ≤ j) : η j + (↑j - ↑i) ≤ η i

A strictly antitone sequence of naturals drops by at least the index gap: it loses at least one unit at each step, hence at least j - i units between the indices i ≤ j.

theorem Function.Injective.exists_strictAnti_comp {n : ℕ} {α : Type u_1} [LinearOrder α] {f : Fin n → α} (hf : Injective f) : ∃ (τ : Equiv.Perm (Fin n)), StrictAnti (f ∘ ⇑τ)

Sorting into decreasing order. Precomposing an injective sequence indexed by Fin n with a suitable permutation of the indices makes it strictly antitone.

theorem StrictAnti.perm_eq {n : ℕ} {α : Type u_1} [PartialOrder α] {f : Fin n → α} {τ₁ τ₂ : Equiv.Perm (Fin n)} (h₁ : StrictAnti (f ∘ ⇑τ₁)) (h₂ : StrictAnti (f ∘ ⇑τ₂)) : τ₁ = τ₂

The sorting permutation is unique. Two permutations of the indices that both make a sequence strictly antitone are equal.