monotone increasing or decreasing subsequence

Stream: Is there code for X?

[Kevin Buzzard]

Do we have either this definition or some form of this theorem? It came up in #6208.

import order.basic

def antitone {α β : Type*} [preorder α] [preorder β]
  (f : α → β) := ∀⦃a b⦄, a ≤ b → f b ≤ f a

example (α : Type) [linear_order α] (f : ℕ → α) : ∃ φ : ℕ → ℕ,
strict_mono φ ∧ (monotone (f ∘ φ) ∨ antitone (f ∘ φ)) := sorry

The proof I know is sketched in my review of the PR: you do a case split on whether the set {n | \forall m > n, f m < f n} is finite or infinite. The Bolzano-Weierstrass theorem for R follows without too much trouble from this (because a monotonic bounded sequence converges) and this was the proof I learnt as an undergrad, however we seem to have some fancier proof of BW in mathlib.

The reason it's relevant is that if furthermore f is injective then one can guarantee that f ∘ φ is strict mono or antimono, and deduce that if alpha is an infinite linearly ordered type then at least one of alpha and its order-dual must be not well-founded -- the naturals inject into any infinite type.

[Eric Wieser]

I imagine antitone follows from some application of order_dual

[Kevin Buzzard]

Sure, but I still need a name for it because if I only have f ∘ φ then it's hard to get my hands on the order_dual unless you want the usual @ _-fest.

[Eric Wieser]

import order.basic

def antitone {α β : Type*} [preorder α] [preorder β]
  (f : α → β) := ∀⦃a b⦄, a ≤ b → f b ≤ f a

def antitone' {α β : Type*} [preorder α] [preorder β]
  (f : α → β) := @monotone α (order_dual β) _ _ f

example {α β : Type*} [preorder α] [preorder β] (f : α → β):
  antitone' f = antitone f := rfl

[Eric Wieser]

So I don't know if we have a name, but you can pick up all the existing lemmas by using that antitone' definition

[Kevin Buzzard]

Sure, but if you don't define it then you'll just get the @ _-fest in the statement of the theorem.

[Eric Wieser]

I agree - I'm just saying we have a full implementation, it just doesn't have a usable name yet :)

[Kevin Buzzard]

Anyway, I would be happy to have the example phrased in whatever way, the real question is whether it's there already.

[Aaron Anderson]

I added a version of this theorem in #6208, and used it again in #6226.

[Aaron Anderson]

If it turns out it does already exist, I'd be happy to use the existing form, but I don't think it does, and it saved me a lot of code in those two PRs.

[Aaron Anderson]

My formulation refers to a general relation, and so doesn't need antitone to be defined, but there are some good corollaries that could be defined using monotone, etc.