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∘ Tuple.sort f.

Main declarations

• Tuple.sort: given f : Fin n → α→ α, produces a permutation on Fin n
• Tuple.monotone_sort: f ∘ Tuple.sort f∘ Tuple.sort f is monotone

ink

def Tuple.graph {n : ℕ} {α : Type u_1} [inst : 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 => (f i, i)) Finset.univ

ink

def Tuple.graph.proj {n : ℕ} {α : Type u_1} [inst : LinearOrder α] {f : Fin n → α} : { x // x ∈ Tuple.graph f } → α

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

Equations

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

ink

@[simp]

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

ink

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

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

Equations

• One or more equations did not get rendered due to their size.

ink

@[simp]

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

ink

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

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

Equations

• Tuple.graphEquiv₂ f = Finset.orderIsoOfFin (Tuple.graph f) (_ : Finset.card (Tuple.graph f) = n)

ink

def Tuple.sort {n : ℕ} {α : Type u_1} [inst : 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 = Equiv.trans (Tuple.graphEquiv₂ f).toEquiv (Equiv.symm (Tuple.graphEquiv₁ f))

ink

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

ink

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

ink

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

ink

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

ink

theorem Tuple.unique_monotone {n : ℕ} {α : Type u_1} [inst : PartialOrder α] {f : Fin n → α} {σ : Equiv.Perm (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.

ink

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

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

ink

theorem Tuple.eq_sort_iff {n : ℕ} {α : Type u_1} [inst : LinearOrder α] {f : Fin n → α} {σ : Equiv.Perm (Fin n)} : σ = Tuple.sort f ↔ Monotone (f ∘ ↑σ) ∧ ∀ (i j : Fin n), i < j → f (↑σ i) = f (↑σ j) → ↑σ i < ↑σ j

A permutation σ equals sort f if and only if f ∘ σ∘ σ is monotone and 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.

ink

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

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

ink

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

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

ink

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

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

ink

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

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

ink

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

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