strict_mono_subseq

Stream: Is there code for X?

[Alex J. Best]

I'm trying to brush up some old code that includes:

import order.monotone
variables {γ : Type*} [preorder γ] [decidable_rel ((≤) : γ → γ → Prop)]

def strict_mono_subseq {f : ℕ → γ} (h : ∀ n, ∃ m, f n < f (n + m)) : ℕ → ℕ
| 0       := 0
| (n + 1) := strict_mono_subseq n + nat.find (h (strict_mono_subseq n))

lemma strict_mono_subseq_spec (f : ℕ → γ) (h : ∀ n, ∃ m, f n < f (n + m)) :
  strict_mono (f ∘ (strict_mono_subseq h)) := strict_mono_nat_of_lt_succ (λ n, nat.find_spec (h (strict_mono_subseq h n)))

and I noticed we now have docs#filter.strict_mono_subseq_of_tendsto_at_top, however the library lemma assumes linear_order whereas the application I have is to submodules which only form a partial order (though it is true that in the application the values of f are in a chain I believe) so I was wondering if there is a natural way to combine use-cases, so I have a few related questions

1. Is there a lemma/def like the one here that takes a strictly monotone subsequence in the library given these seemingly weaker assumptions?
2. Can / should the library lemma strict_mono_subseq_of_tendsto_at_top be generalized to cover something closer to the lemma / def above?
3. Is the assumption (h : ∀ n, ∃ m, f n < f (n + m)) something nice when expressed in filter-language, it seems weaker than tendsto f at_top at_top?

[Yaël Dillies]

A few things:

• I'm pretty sure that filter.strict_mono_subseq_of_tendsto_at_top can be generalized.
• You condition ∀ n, ∃ m, f n < f (n + m) still seems too strong. I think the correct hypothesis is "eventually strictly monotone", which does remind me that @Filippo A. E. Nuccio was looking for a definition of "eventually monotone".

[Yaël Dillies]

In some sense, you don't need the order to be linear, you just need it to be linear close to infinity. This is what happens with submodules because you have a maximal element.

[Filippo A. E. Nuccio]

Just for completeness, in the proof I was working on, I had a sequence $a_n$ that I wanted to state to be "eventually monotone". I new an index $n_0$ such that $n\mapsto a_n$ was monotone for all $n\geq n_0$ and ended up definining $b_n$ to be $a_n$ for $n\geq n_0$ and constantlu equal to $\min (a_n \mid n\leq n_0)$. So, $b_n$ was "really monotone" and I applied some limit-lemma of the form "tendsto.eventually" to deduce properties of $a_n$ from those of $b_n$.