Zulip Chat Archive

Stream: Is there code for X?

Topic: monotone increasing or decreasing subsequence


view this post on Zulip Kevin Buzzard (Feb 16 2021 at 00:17):

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.

view this post on Zulip Eric Wieser (Feb 16 2021 at 00:18):

I imagine antitone follows from some application of order_dual

view this post on Zulip Kevin Buzzard (Feb 16 2021 at 00:19):

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.

view this post on Zulip Eric Wieser (Feb 16 2021 at 00:19):

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

view this post on Zulip Eric Wieser (Feb 16 2021 at 00:19):

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

view this post on Zulip Kevin Buzzard (Feb 16 2021 at 00:20):

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

view this post on Zulip Eric Wieser (Feb 16 2021 at 00:20):

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

view this post on Zulip Kevin Buzzard (Feb 16 2021 at 00:22):

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

view this post on Zulip Aaron Anderson (Feb 16 2021 at 02:52):

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

view this post on Zulip Aaron Anderson (Feb 16 2021 at 02:54):

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.

view this post on Zulip Aaron Anderson (Feb 16 2021 at 02:59):

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.


Last updated: May 16 2021 at 05:21 UTC