The dominance order on finite vectors

A vector a : Fin n → M dominates g when the two have the same total and every leading partial sum ∑_{j < k} a j is at most that of g. For monotone vectors of natural numbers, a is then the more spread out of the two. This is the order along which the monomials of a Hecke ring are triangular in its diagonal double cosets.

Dominance is reflexive and transitive, and it is antisymmetric when addition is left cancellative, since the leading partial sums determine the vector. In an ordered cancellative monoid, adding a common vector to both sides neither creates nor destroys dominance.

For vectors of natural numbers, TauCeti.dominanceDefect g sums the defects of the leading partial sums of g from its total. It strictly decreases down the dominance order, so induction on it is induction along that order.

Main definitions

• TauCeti.Dominates: the dominance order on Fin n → M.
• TauCeti.dominanceDefect: a natural-number measure strictly decreasing down that order.

Main results

• TauCeti.Dominates.antisymm: dominance is antisymmetric.
• TauCeti.Dominates.add_right, TauCeti.Dominates.of_add_right: dominance is compatible with adding a common vector.
• TauCeti.Dominates.dominanceDefect_lt: the defect strictly decreases down the order.

def TauCeti.Dominates {M : Type u_1} {n : ℕ} [AddCommMonoid M] [LE M] (a g : Fin n → M) : Prop

a dominates g: the two vectors have the same total and every leading partial sum of a is at most that of g. For monotone vectors of natural numbers, a is the more spread out of the two.

theorem TauCeti.dominates_def {M : Type u_1} {n : ℕ} [AddCommMonoid M] [LE M] {a g : Fin n → M} : Dominates a g ↔ ∑ i : Fin n, g i = ∑ i : Fin n, a i ∧ ∀ (k : ℕ) (hk : k ≤ n), ∑ j : Fin k, a (Fin.castLE hk j) ≤ ∑ j : Fin k, g (Fin.castLE hk j)

The defining property of TauCeti.Dominates.

theorem TauCeti.Dominates.refl {M : Type u_1} {n : ℕ} [AddCommMonoid M] [Preorder M] (a : Fin n → M) : Dominates a a

Every vector dominates itself.

theorem TauCeti.Dominates.trans {M : Type u_1} {n : ℕ} [AddCommMonoid M] [Preorder M] {a g h : Fin n → M} (hag : Dominates a g) (hgh : Dominates g h) : Dominates a h

Dominance is transitive.

theorem TauCeti.Dominates.antisymm {M : Type u_1} {n : ℕ} [AddCommMonoid M] [PartialOrder M] [IsLeftCancelAdd M] {a g : Fin n → M} (hag : Dominates a g) (hga : Dominates g a) : a = g

Dominance is antisymmetric when addition is left cancellative: the leading partial sums determine the vector.

theorem TauCeti.Dominates.add_right {M : Type u_1} {n : ℕ} [AddCommMonoid M] [Preorder M] [AddRightMono M] {a g : Fin n → M} (h : Dominates a g) (f : Fin n → M) : Dominates (a + f) (g + f)

Adding a common vector preserves dominance.

theorem TauCeti.Dominates.of_add_right {M : Type u_1} {n : ℕ} [AddCommMonoid M] [PartialOrder M] [IsOrderedCancelAddMonoid M] {a g f : Fin n → M} (h : Dominates (a + f) (g + f)) : Dominates a g

In an ordered cancellative monoid, a common summand can be cancelled from a dominance.

def TauCeti.dominanceDefect {n : ℕ} (g : Fin n → ℕ) : ℕ

The defects of the leading partial sums of g from its total, summed. It strictly decreases down the dominance order (TauCeti.Dominates.dominanceDefect_lt), so induction on it is induction along that order.

theorem TauCeti.dominanceDefect_def {n : ℕ} (g : Fin n → ℕ) : dominanceDefect g = ∑ k : Fin (n + 1), (∑ i : Fin n, g i - ∑ j : Fin ↑k, g (Fin.castLE ⋯ j))

The defining equation of TauCeti.dominanceDefect.

theorem TauCeti.Dominates.dominanceDefect_lt {n : ℕ} {a g : Fin n → ℕ} (h : Dominates a g) (hne : a ≠ g) : dominanceDefect g < dominanceDefect a

The defect strictly decreases down the dominance order. If a dominates g and a ≠ g, then dominanceDefect g < dominanceDefect a.