Permutation to make a function monotone

Stream: Is there code for X?

[Heather Macbeth]

I thought that docs#finset.sort might do something like this, but apparently it outputs a list ... how can I get a permutation?

import data.fin.basic

variables {n : ℕ}
variables {α : Type*} [linear_order α]

def sort (f : fin n → α) : equiv.perm (fin n) := sorry

lemma monotone_sort (f : fin n → α) : monotone (f ∘ sort f) := sorry

[Kyle Miller]

There's docs#finset.order_iso_of_fin, which is close. I found a way to use it by constructing the graph of a function and sorting that lexicographically.

import data.fin.basic
import data.finset.sort
import order.lexicographic

variables {n : ℕ}
variables {α : Type*} [linear_order α]

def graph (f : fin n → α) : finset (lex α (fin n)) :=
finset.univ.image (λ i, (f i, i))

def graph.proj {f : fin n → α} : graph f → α := λ p, p.1.1

@[simp] lemma graph.card (f : fin n → α) : (graph f).card = n :=
begin
  rw [graph, finset.card_image_of_injective],
  simp,
  rintros ⟨i, hi⟩ ⟨j, hj⟩,
  simp,
end

/-- The induced map into the graph -/
def graph_equiv₁ (f : fin n → α) : fin n ≃ graph f :=
{ to_fun := λ i, ⟨(f i, i), by simp [graph]⟩,
  inv_fun := λ p, p.1.2,
  left_inv := λ i, by simp,
  right_inv := λ ⟨⟨x, i⟩, h⟩, by simpa [graph] using h }

@[simp] lemma proj_equiv₁' (f : fin n → α) : graph.proj ∘ graph_equiv₁ f = f := rfl

/-- putting the graph in sorted order -/
def graph_equiv₂ (f : fin n → α) : fin n ≃o graph f :=
finset.order_iso_of_fin _ (by simp)

/-- The permutation that puts `f` in sorted order. -/
def sort (f : fin n → α) : equiv.perm (fin n) :=
(graph_equiv₂ f).to_equiv.trans (graph_equiv₁ f).symm

lemma self_comp_sort (f : fin n → α) : f ∘ sort f = graph.proj ∘ graph_equiv₂ f :=
begin
  rw [sort],
  nth_rewrite 0 [←proj_equiv₁' f],
  change graph.proj ∘ ((graph_equiv₁ f) ∘ (graph_equiv₁ f).symm) ∘ (graph_equiv₂ f).to_equiv = _,
  simp,
end

lemma monotone_sort (f : fin n → α) : monotone (f ∘ sort f) :=
begin
  rw [self_comp_sort],
  intros i j h,
  simp,
  have h' := (order_iso.le_iff_le (graph_equiv₂ f)).mpr h,
  generalize hx : graph_equiv₂ f i = x,
  generalize hy : graph_equiv₂ f j = y,
  rw [hx, hy] at h',
  obtain ⟨⟨x, I⟩, hI⟩ := x,
  obtain ⟨⟨y, J⟩, hJ⟩ := y,
  simp [graph.proj],
  cases h',
  apply le_of_lt, assumption,
  refl,
end

[Heather Macbeth]

@Kyle Miller Wow, that's much more elaborate than I anticipated. Thank you! Could you PR it? (Or I could PR myself if you prefer.)

By the way, I was wondering whether the following would also work: use docs#multiset.map to consider the range of f as a multiset in α, sort this using docs#multiset.sort, and then somehow transfer back to give a sorting of fin n. I've never used lists or multisets so I don't know how much work would be needed there.

[Yury G. Kudryashov]

Kyle used lex to remember the index of each element while sorting on its value.

[Kyle Miller]

The lex trick is to be able to distinguish each of the images of f, which seems like the main difficulty with sort. I'd originally tried doing things with lists directly, but it was extremely unpleasant.

Here's a commutative diagram that organizes what's going on in the construction:

image.png

[Kyle Miller]

Looking at this diagram more carefully, I realized I didn't take advantage of docs#monotone.comp. This can replace the last lemma:

lemma monotone_proj (f : fin n → α) : monotone (graph.proj : graph f → α) :=
begin
  simp [graph.proj],
  rintro ⟨⟨x, i⟩, hx⟩ ⟨⟨y, j⟩, hy⟩,
  rintro (h|h),
  simp,
  exact le_of_lt ‹_›,
  simp,
end

lemma monotone_sort (f : fin n → α) : monotone (f ∘ sort f) :=
begin
  rw [self_comp_sort],
  apply monotone.comp,
  apply monotone_proj,
  apply order_iso.monotone,
end

[Kyle Miller]

I'm also not sure how all of this should relate to docs#function.graph, which gives a relation. If you uncurry that relation and turn it into a set, its docs#set.to_finset would be equal to graph.

[Kyle Miller]

@Heather Macbeth Would you mind PRing sort and monotone_sort?

[Heather Macbeth]

Sure, happy to (listing you as the author of course). Thanks again! By the way, the purpose here is to convert from a basis of eigenvectors to a basis of eigenvectors ordered by eigenvalue :)

[Kevin Buzzard]

what if the eigenvalues are complex ? ;-)

[Heather Macbeth]

Good thing they're not! :)
https://github.com/leanprover-community/mathlib/blob/d59f9ece9c74e1e04d1a506ea85fbfb9536a2af0/src/analysis/inner_product_space/spectrum.lean#L61

[Yaël Dillies]

It just occurred to me that this result is a corollary of #17932. Because a function f : α → β monovaries with itself, the results in this PR give that there's some linear order on α according to which f is monotone. But then we can use the fact that perm α acts transitively on linear_order α to get the desired permutation.