Sorting tuples by their values

Given an n-tuple f : Fin n → α where α is ordered, we may want to turn it into a sorted n-tuple. This file provides an API for doing so, with the sorted n-tuple given by f ∘ Tuple.sort f.

Main declarations

• Tuple.sort: given f : Fin n → α, produces a permutation on Fin n
• Tuple.monotone_sort: f ∘ Tuple.sort f is Monotone
• Tuple.sortDesc: given f : Fin n → α, produces a permutation on Fin n sorting into decreasing order
• Tuple.antitone_sortDesc: f ∘ Tuple.sortDesc f is Antitone
• Tuple.comp_sort_comp_rev_eq_comp_sortDesc: sorting descending equals sorting ascending, reversed

def Tuple.graph {n : ℕ} {α : Type u_1} [LinearOrder α] (f : Fin n → α) : Finset (Lex (α × Fin n))

graph f produces the finset of pairs (f i, i) equipped with the lexicographic order.

Equations

• Tuple.graph f = Finset.image (fun (i : Fin n) => (f i, i)) Finset.univ

def Tuple.graph.proj {n : ℕ} {α : Type u_1} [LinearOrder α] {f : Fin n → α} : ↥(graph f) → α

Given p : α ×ₗ (Fin n) := (f i, i) with p ∈ graph f, graph.proj p is defined to be f i.

Equations

• Tuple.graph.proj p = (↑p).1

@[simp]

theorem Tuple.graph.card {n : ℕ} {α : Type u_1} [LinearOrder α] (f : Fin n → α) : (graph f).card = n

def Tuple.graphEquiv₁ {n : ℕ} {α : Type u_1} [LinearOrder α] (f : Fin n → α) : Fin n ≃ ↥(graph f)

graphEquiv₁ f is the natural equivalence between Fin n and graph f, mapping i to (f i, i).

Equations

• Tuple.graphEquiv₁ f = { toFun := fun (i : Fin n) => ⟨(f i, i), ⋯⟩, invFun := fun (p : ↥(Tuple.graph f)) => (↑p).2, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Tuple.proj_equiv₁' {n : ℕ} {α : Type u_1} [LinearOrder α] (f : Fin n → α) : graph.proj ∘ ⇑(graphEquiv₁ f) = f

def Tuple.graphEquiv₂ {n : ℕ} {α : Type u_1} [LinearOrder α] (f : Fin n → α) : Fin n ≃o ↥(graph f)

graphEquiv₂ f is an equivalence between Fin n and graph f that respects the order.

Equations

• Tuple.graphEquiv₂ f = (Tuple.graph f).orderIsoOfFin ⋯

def Tuple.sort {n : ℕ} {α : Type u_1} [LinearOrder α] (f : Fin n → α) : Equiv.Perm (Fin n)

sort f is the permutation that orders Fin n according to the order of the outputs of f.

Equations

• Tuple.sort f = (Tuple.graphEquiv₂ f).trans (Tuple.graphEquiv₁ f).symm

theorem Tuple.graphEquiv₂_apply {n : ℕ} {α : Type u_1} [LinearOrder α] (f : Fin n → α) (i : Fin n) : (graphEquiv₂ f) i = (graphEquiv₁ f) ((sort f) i)

theorem Tuple.self_comp_sort {n : ℕ} {α : Type u_1} [LinearOrder α] (f : Fin n → α) : f ∘ ⇑(sort f) = graph.proj ∘ ⇑(graphEquiv₂ f)

theorem Tuple.monotone_proj {n : ℕ} {α : Type u_1} [LinearOrder α] (f : Fin n → α) : Monotone graph.proj

theorem Tuple.monotone_sort {n : ℕ} {α : Type u_1} [LinearOrder α] (f : Fin n → α) : Monotone (f ∘ ⇑(sort f))

def Tuple.sortDesc {n : ℕ} {α : Type u_1} [LinearOrder α] (f : Fin n → α) : Equiv.Perm (Fin n)

sortDesc f is the permutation that orders Fin n according to the reverse order of the outputs of f, so that f ∘ sortDesc f is decreasing.

Unlike sort f ∘ Fin.revPerm, which also arranges f in decreasing order, sortDesc f is a stable sort: among indices with equal f-value it keeps their original order (isStable_sortDesc), whereas sort f ∘ Fin.revPerm reverses it and so is stable only when f is injective (isStable_sort_comp_rev_iff), in which case the two coincide (sort_comp_rev_eq_sortDesc_of_injective).

Equations

• Tuple.sortDesc f = Tuple.sort (⇑OrderDual.toDual ∘ f)

theorem Tuple.antitone_sortDesc {n : ℕ} {α : Type u_1} [LinearOrder α] (f : Fin n → α) : Antitone (f ∘ ⇑(sortDesc f))

theorem Tuple.lt_card_le_iff_apply_le_of_monotone {n : ℕ} {α : Type u_1} {j : Fin n} {f : Fin n → α} [Preorder α] {a : α} [DecidableLE α] (h_sorted : Monotone f) : ↑j < {i : Fin n | f i ≤ a}.card ↔ f j ≤ a

If f₀ ≤ f₁ ≤ f₂ ≤ ⋯ is a sorted n-tuple of elements of α, then for any j : Fin n and a : α we have j < #{i | fᵢ ≤ a} iff fⱼ ≤ a.

theorem Tuple.lt_card_ge_iff_apply_ge_of_antitone {n : ℕ} {α : Type u_1} {j : Fin n} {f : Fin n → α} [Preorder α] {a : α} [DecidableLE α] (h_sorted : Antitone f) : ↑j < {i : Fin n | a ≤ f i}.card ↔ a ≤ f j

theorem Tuple.lt_card_lt_iff_apply_lt_of_monotone {n : ℕ} {α : Type u_1} {j : Fin n} {f : Fin n → α} [Preorder α] {a : α} [DecidableLT α] (h_sorted : Monotone f) : ↑j < {i : Fin n | f i < a}.card ↔ f j < a

theorem Tuple.lt_card_gt_iff_apply_gt_of_antitone {n : ℕ} {α : Type u_1} {j : Fin n} {f : Fin n → α} [Preorder α] {a : α} [DecidableLT α] (h_sorted : Antitone f) : ↑j < {i : Fin n | a < f i}.card ↔ a < f j

theorem Tuple.unique_monotone {n : ℕ} {α : Type u_1} [PartialOrder α] {f : Fin n → α} {σ τ : Equiv.Perm (Fin n)} (hfσ : Monotone (f ∘ ⇑σ)) (hfτ : Monotone (f ∘ ⇑τ)) : f ∘ ⇑σ = f ∘ ⇑τ

If two permutations of a tuple f are both monotone, then they are equal.

theorem Tuple.unique_antitone {n : ℕ} {α : Type u_1} [PartialOrder α] {f : Fin n → α} {σ τ : Equiv.Perm (Fin n)} (hfσ : Antitone (f ∘ ⇑σ)) (hfτ : Antitone (f ∘ ⇑τ)) : f ∘ ⇑σ = f ∘ ⇑τ

If two permutations of a tuple f are both antitone, then they are equal.

theorem Tuple.eq_sort_iff' {n : ℕ} {α : Type u_1} [LinearOrder α] {f : Fin n → α} {σ : Equiv.Perm (Fin n)} : σ = sort f ↔ StrictMono ⇑(Equiv.trans σ (graphEquiv₁ f))

A permutation σ equals sort f if and only if the map i ↦ (f (σ i), σ i) is strictly monotone (w.r.t. the lexicographic ordering on the target).

theorem Tuple.eq_sort_iff {n : ℕ} {α : Type u_1} [LinearOrder α] {f : Fin n → α} {σ : Equiv.Perm (Fin n)} : σ = sort f ↔ Monotone (f ∘ ⇑σ) ∧ IsStable f ⇑σ

A permutation σ equals sort f if and only if f ∘ σ is monotone and σ is stable, i.e. whenever i ≤ j and f (σ i) = f (σ j), then σ i ≤ σ j. This means that sort f is the lexicographically smallest permutation σ such that f ∘ σ is monotone.

theorem Tuple.eq_sortDesc_iff {n : ℕ} {α : Type u_1} [LinearOrder α] {f : Fin n → α} {σ : Equiv.Perm (Fin n)} : σ = sortDesc f ↔ Antitone (f ∘ ⇑σ) ∧ IsStable f ⇑σ

A permutation σ equals sortDesc f if and only if f ∘ σ is antitone and σ is stable, i.e. σ breaks ties by increasing index. This is the descending analogue of eq_sort_iff.

theorem Tuple.sort_eq_refl_iff_monotone {n : ℕ} {α : Type u_1} [LinearOrder α] {f : Fin n → α} : sort f = Equiv.refl (Fin n) ↔ Monotone f

The permutation that sorts f is the identity if and only if f is monotone.

theorem Tuple.comp_sort_eq_comp_iff_monotone {n : ℕ} {α : Type u_1} [LinearOrder α] {f : Fin n → α} {σ : Equiv.Perm (Fin n)} : f ∘ ⇑σ = f ∘ ⇑(sort f) ↔ Monotone (f ∘ ⇑σ)

A permutation of a tuple f is f sorted if and only if it is monotone.

theorem Tuple.comp_perm_comp_sort_eq_comp_sort {n : ℕ} {α : Type u_1} [LinearOrder α] {f : Fin n → α} {σ : Equiv.Perm (Fin n)} : (f ∘ ⇑σ) ∘ ⇑(sort (f ∘ ⇑σ)) = f ∘ ⇑(sort f)

The sorted versions of a tuple f and of any permutation of f agree.

theorem Tuple.comp_perm_comp_sortDesc_eq_comp_sortDesc {n : ℕ} {α : Type u_1} [LinearOrder α] {f : Fin n → α} {σ : Equiv.Perm (Fin n)} : (f ∘ ⇑σ) ∘ ⇑(sortDesc (f ∘ ⇑σ)) = f ∘ ⇑(sortDesc f)

The sorted-descending versions of a tuple f and of any permutation of f agree.

theorem Tuple.comp_sort_comp_rev_eq_comp_sortDesc {n : ℕ} {α : Type u_1} [LinearOrder α] {f : Fin n → α} : f ∘ ⇑(sort f) ∘ Fin.rev = f ∘ ⇑(sortDesc f)

Sorting f in descending order is the same as sorting it in ascending order, then reversing.

theorem Tuple.comp_sortDesc_comp_rev_eq_comp_sort {n : ℕ} {α : Type u_1} [LinearOrder α] {f : Fin n → α} : f ∘ ⇑(sortDesc f) ∘ Fin.rev = f ∘ ⇑(sort f)

Sorting f in ascending order is the same as sorting it in descending order, then reversing.

theorem Tuple.sort_comp_rev_eq_sortDesc_of_injective {n : ℕ} {α : Type u_1} [LinearOrder α] {f : Fin n → α} (inj : Function.Injective f) : ⇑(sort f) ∘ Fin.rev = ⇑(sortDesc f)

When f is injective there are no ties, so sorting descending agrees with sorting ascending then reversing, already as an equality of permutations.

theorem Tuple.sortDesc_comp_rev_eq_sort_of_injective {n : ℕ} {α : Type u_1} [LinearOrder α] {f : Fin n → α} (inj : Function.Injective f) : ⇑(sortDesc f) ∘ Fin.rev = ⇑(sort f)

theorem Tuple.antitone_pair_of_not_sorted' {n : ℕ} {α : Type u_1} [LinearOrder α] {f : Fin n → α} {σ : Equiv.Perm (Fin n)} (h : f ∘ ⇑σ ≠ f ∘ ⇑(sort f)) : ∃ (i : Fin n) (j : Fin n), i < j ∧ (f ∘ ⇑σ) j < (f ∘ ⇑σ) i

If a permutation f ∘ σ of the tuple f is not the same as f ∘ sort f, then f ∘ σ has a pair of strictly decreasing entries.

theorem Tuple.antitone_pair_of_not_sorted {n : ℕ} {α : Type u_1} [LinearOrder α] {f : Fin n → α} (h : f ≠ f ∘ ⇑(sort f)) : ∃ (i : Fin n) (j : Fin n), i < j ∧ f j < f i

If the tuple f is not the same as f ∘ sort f, then f has a pair of strictly decreasing entries.

@[simp]

theorem Tuple.sort_perm {n : ℕ} (σ : Equiv.Perm (Fin n)) : sort ⇑σ = σ⁻¹

The sorted version of a permutation σ is its inverse σ⁻¹.

theorem Tuple.isStable_sort {n : ℕ} {α : Type u_1} [LinearOrder α] (f : Fin n → α) : IsStable f ⇑(sort f)

theorem Tuple.isStable_sortDesc {n : ℕ} {α : Type u_1} [LinearOrder α] (f : Fin n → α) : IsStable f ⇑(sortDesc f)

theorem Tuple.isStable_iff_imp {α : Type u_2} {γ : Type u_3} [Preorder α] (f : α → γ) (σ : Equiv.Perm α) : IsStable f ⇑σ ↔ ∀ ⦃i j : α⦄, f i = f j → σ⁻¹ i ≤ σ⁻¹ j → i ≤ j

IsStable f σ says exactly that σ⁻¹ reflects the order of any two indices sharing an f-value.

theorem Tuple.isStable_iff {α : Type u_2} {γ : Type u_3} [LinearOrder α] (f : α → γ) (σ : Equiv.Perm α) : IsStable f ⇑σ ↔ ∀ ⦃i j : α⦄, f i = f j → (i ≤ j ↔ σ⁻¹ i ≤ σ⁻¹ j)

IsStable f σ says exactly that σ⁻¹ preserves the order of any two indices sharing an f-value.

theorem Tuple.isStable_sort_comp_rev_iff {n : ℕ} {α : Type u_1} [LinearOrder α] {f : Fin n → α} : IsStable f (⇑(sort f) ∘ Fin.rev) ↔ Function.Injective f

sort f ∘ Fin.rev is a stable sort exactly when f is injective: on tied values it orders them by decreasing index, the opposite of the stable sortDesc f.

theorem Equiv.Perm.monotone_iff {n : ℕ} (σ : Perm (Fin n)) : Monotone ⇑σ ↔ σ = 1