Zulip Chat Archive

Stream: general

Topic: monotone -> strict_mono


view this post on Zulip 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)),
    simp only [add_comm],
end

view this post on Zulip Yury G. Kudryashov (Jan 01 2020 at 13:42):

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

view this post on Zulip Yury G. Kudryashov (Jan 01 2020 at 13:43):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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