monotone -> strict_mono

Stream: general

[Alex J. Best]

Is there anything like

variables {γ : Type*} [preorder γ]

noncomputable def strict_monotone_inc_subseq {f : ℕ → γ} (h : ∀ n, ∃ m, f n < f (n + m)) : ℕ → ℕ
| 0       := 0
| (n + 1) := (strict_monotone_inc_subseq n) + classical.some (h (strict_monotone_inc_subseq n))

in mathlib? I.e. creating a strictly monotone subsequence of a sequence that is not eventually monotone decreasing.

the important property being

lemma strict_monotone_inc_subseq_spec (f : ℕ → γ) (h : ∀ n, ∃ m, f n < f (n + m)) :
  strict_mono (f ∘ (strict_monotone_inc_subseq h)) :=
begin
    refine strict_mono.nat _,
    intro n,
    rw comp_app,
    rw comp_app,
    rw [strict_monotone_inc_subseq],

    convert classical.some_spec (h (strict_monotone_inc_subseq h n)),
    simp only [add_comm],
end

[Yury G. Kudryashov]

We have directed.sequence in data/equiv/encodable.

[Yury G. Kudryashov]

Though it doesn't ensure that the sequence itself is monotone.

[Yury G. Kudryashov]

It might be a good idea to create a version for nat with more guaranteed properties, then define the encodable version using it.

[Yury G. Kudryashov]

On the other hand, the encodable version gives you a (strict) monotone sequence with a prescribed rate of convergence to infinity.

[Yury G. Kudryashov]

Or you can get the nat version from directed.sequence applied to the relation λ m n, m < n ∧ f m < f n.

[Yury G. Kudryashov]

Not sure if we already have a nat version.