Zulip Chat Archive

Stream: Is there code for X?

Topic: Permutation to make a function monotone


Heather Macbeth (Nov 08 2021 at 03:46):

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 (Nov 08 2021 at 19:54):

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 (Nov 08 2021 at 20:08):

@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 (Nov 08 2021 at 20:13):

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

Kyle Miller (Nov 08 2021 at 20:44):

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 (Nov 08 2021 at 20:45):

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 (Nov 08 2021 at 20:48):

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 (Nov 08 2021 at 20:48):

@Heather Macbeth Would you mind PRing sort and monotone_sort?

Heather Macbeth (Nov 08 2021 at 20:49):

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 (Nov 08 2021 at 20:51):

what if the eigenvalues are complex ? ;-)

Heather Macbeth (Nov 08 2021 at 20:52):

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

Yaël Dillies (Dec 16 2022 at 17:48):

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.

Adrian Wüthrich (Feb 28 2024 at 10:00):

Are there sorted eigenvalues in mathlib now? In LinearMap.IsSymmetric.eigenvalues I found the TODO:

-- TODO Postcompose with a permutation so that these eigenvalues are listed in increasing order.
noncomputable irreducible_def eigenvalues (i : Fin n) :  :=
  @IsROrC.re 𝕜 _ <| (hT.direct_sum_isInternal.subordinateOrthonormalBasisIndex hn i
    hT.orthogonalFamily_eigenspaces').val
#align linear_map.is_symmetric.eigenvalues LinearMap.IsSymmetric.eigenvalues

Would the following be the right way to do it?

noncomputable def eigenvalues_sorted (i : Fin n) :  :=
  (eigenvalues hT hn  Tuple.sort (eigenvalues hT hn)) i

Last updated: May 02 2025 at 03:31 UTC