high scores

Stream: Is there code for X?

[Patrick Massot]

Sébastien, do you know whether the high scores lemma you discussed in Orsay is in mathlib ?

[Sebastien Gouezel]

I don't think it is, at least I never noticed it.

[Sebastien Gouezel]

Using nat.find, it should be pretty straightforward. The Isabelle proof I gave is very clunky as it does everything by hand, using only infs and sups.

[Patrick Massot]

Do we have some form of:

class unbounded_above (α : Type*) [has_lt α] : Prop :=
(exists_gt : ∀ a : α, ∃ b, a < b)

This seems needed for the statement of the high scores lemma if we want a rather general sequence target.

[Patrick Massot]

Of course I don't mind using a data carrying version (adding a function taking a and outputting b).

[Mario Carneiro]

there is order.unbounded although it is stated a bit differently

[Patrick Massot]

Where is that?

[Patrick Massot]

I see only def unbounded (r : α → α → Prop) (s : set α) : Prop := ∀ a, ∃ b ∈ s, ¬ r b a. Is that what you mean?

[Patrick Massot]

Maybe this discussion is too abstract. I'd like to read comments about:

import order.filter

open filter

lemma exists_le_of_tendsto_at_top {α : Type*} [decidable_linear_order α]
  {β : Type*} [preorder β] {u : α → β} (h : tendsto u at_top at_top) :
∀ a b, ∃ a' ≥ a, b ≤ u a' :=
begin
  intros a b,
  rw tendsto_at_top at h,
  haveI : nonempty α := ⟨a⟩,
  cases mem_at_top_sets.mp (h b) with a' ha',
  exact ⟨max a a', le_max_left _ _, ha' _ $ le_max_right _ _⟩,
end

class unbounded_above (α : Type*) [has_lt α] : Prop :=
(exists_gt : ∀ a : α, ∃ b, a < b)

instance linear_ordered_semiring.unbounded_above {R : Type*} [linear_ordered_semiring R] :
  unbounded_above R := ⟨λ a, ⟨a+1, lt_add_one a⟩⟩

lemma exists_lt_of_tendsto_at_top {α : Type*} [decidable_linear_order α]
  {β : Type*} [preorder β] [unbounded_above β] {u : α → β} (h : tendsto u at_top at_top) :
∀ a b, ∃ a' ≥ a, b < u a' :=
begin
  intros a b,
  cases unbounded_above.exists_gt b with b' hb',
  rcases exists_le_of_tendsto_at_top h a b' with ⟨a', ha', ha''⟩,
  exact ⟨a', ha', lt_of_lt_of_le hb' ha''⟩
end

lemma high_scores {β : Type*} [decidable_linear_order β] [unbounded_above β] {u : ℕ → β}
  (hu : tendsto u at_top at_top) : ∀ N, ∃ n ≥ N, ∀ k < n, u k < u n :=
begin
  intros N,
  let A := finset.image u (finset.range $ N+1), -- A = {u 0, ..., u N}
  have Ane : A.nonempty,
    from ⟨u 0, finset.mem_image_of_mem _ (finset.mem_range.mpr $ nat.zero_lt_succ _)⟩,
  let M := finset.max' A Ane,
  have ex : ∃ n ≥ N, M < u n,
    from exists_lt_of_tendsto_at_top hu _ _,
  obtain ⟨n, hnN, hnM, hn_min⟩ : ∃ n, N ≤ n ∧ M < u n ∧ ∀ k, N ≤ k → k < n → u k ≤ M,
  { use nat.find ex,
    rw ← and_assoc,
    split,
    { simpa using nat.find_spec ex },
    { intros k hk hk',
      simpa [hk] using nat.find_min ex hk' } },
  use [n, hnN],
  intros k hk,
  by_cases H : k ≤ N,
  { have : u k ∈ A,
      from finset.mem_image_of_mem _ (finset.mem_range.mpr $ nat.lt_succ_of_le H),
    have : u k ≤ M,
      from finset.le_max' A Ane (u k) this,
    exact lt_of_le_of_lt this hnM },
  { push_neg at H,
    calc u k ≤ M   : hn_min k (le_of_lt H) hk
         ... < u n : hnM },
end

[Patrick Massot]

@Sebastien Gouezel

[Sebastien Gouezel]

It's called no_top_order

[Patrick Massot]

Ah

[Patrick Massot]

I knew it was bound to exist :wink:

[Patrick Massot]

The preorder requirement in the definition of no_top_order is ridiculous.

[Mario Carneiro]

that's our weakest well behaved order typeclass

[Patrick Massot]

But has_lt is enough here!

[Mario Carneiro]

if you want less than that you should go for the piecemeal is_irrefl etc typeclasses

[Patrick Massot]

:stuck_out_tongue:

[Patrick Massot]

Anyway, let's go back to serious stuff. no_top_order is indeed what I was looking for. Any other observation about that high scores stuff?

[Mario Carneiro]

it occurs to me that the statement of high_scores could be stated using order.unbounded, although I'm not sure if the result is more or less readable

[Patrick Massot]

In my intended use, the sequence target is either nat or real.

[Sebastien Gouezel]

I think your code is nice. How do you feel it compare to the Isabelle proof wrt to length and readability? For the record, here is the Isabelle code:

lemma high_scores:
  fixes u::"nat ⇒ real" and i::nat
  assumes "u ⇢ ∞"
  shows "∃n ≥ i. ∀l ≤ n. u l ≤ u n"
proof -
  define M where "M = Max {u l|l. l < i}"
  define n where "n = Inf {m. u m > M}"
  have "eventually (λm. u m > M) sequentially"
    using assms by (simp add: filterlim_at_top_dense tendsto_PInfty_eq_at_top)
  then have "{m. u m > M} ≠ {}" by fastforce
  then have "n ∈ {m. u m > M}" unfolding n_def using Inf_nat_def1 by metis
  then have "u n > M" by simp
  have "n ≥ i"
  proof (rule ccontr)
    assume " ¬ i ≤ n"
    then have *: "n < i" by simp
    have "u n ≤ M" unfolding M_def apply (rule Max_ge) using * by auto
    then show False using ‹u n > M› by auto
  qed
  moreover have "u l ≤ u n" if "l ≤ n" for l
  proof (cases "l = n")
    case True
    then show ?thesis by simp
  next
    case False
    then have "l < n" using ‹l ≤ n› by auto
    then have "l ∉ {m. u m > M}"
      unfolding n_def by (meson bdd_below_def cInf_lower not_le zero_le)
    then show ?thesis using ‹u n > M› by auto
  qed
  ultimately show ?thesis by auto
qed

[Patrick Massot]

I think it's pretty comparable. The only painful part in Lean is finding the lemmas. Basically every intermediate assumption should be proved by automation. Some of it already is (by library_search).

[Patrick Massot]

I also wish nat.find had a less cryptic name.