## Stream: general

### Topic: monotone -> strict_mono

#### Alex J. Best (Jan 01 2020 at 13:23):

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)),
end


#### Yury G. Kudryashov (Jan 01 2020 at 13:42):

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

#### Yury G. Kudryashov (Jan 01 2020 at 13:43):

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

#### Yury G. Kudryashov (Jan 01 2020 at 13:44):

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 (Jan 01 2020 at 13:45):

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

#### Yury G. Kudryashov (Jan 01 2020 at 13:51):

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 (Jan 01 2020 at 13:52):

Not sure if we already have a nat version.

Last updated: May 14 2021 at 13:24 UTC