Zulip Chat Archive

Stream: maths

Topic: generalizing lemmas about monotone nat -> nat functions

Jakub Kądziołka (Mar 07 2022 at 17:11):

In #12443 I proved the following, very specific lemma:

lemma fib_between (n : ℕ) : ∃ k : ℕ, fib k ≤ n ∧ n < fib k.succ :=

This is obviously be generalized, but I'm not exactly sure how much. So far I've split it into two lemmas: an unbounded monotone function satisfies this property, and a strictly monotone function is unbounded. However so far I'm only stating it for ℕ → ℕ functions, and I'm having trouble stating exactly what kind of an ordered set is necessary. At least for ℤ one could state something similar, but the f 0 ≤ n assumption then becomes problematic...

lemma ex_le_lt_of_mono_of_unbounded
  (f : ℕ → ℕ) (Hmono : monotone f)
  (Hunbounded : set.unbounded (≤) (set.range f))
  (n : ℕ) (Hlow: f 0 ≤ n):
  ∃ k : ℕ, f k ≤ n ∧ n < f k.succ :=
begin
  by_contra' next : ∀ k : ℕ, f k ≤ n → f k.succ ≤ n,
  have all_bounded : ∀ k : ℕ, f k ≤ n,
  { intro k, induction k with k IH,
    exact Hlow, exact next k IH },
  have bounded : set.bounded (≤) (set.range f),
  { use n, assume (v : ℕ) (Hv : v ∈ set.range f),
    obtain ⟨k, Hk⟩ : ∃ k, f k = v := by simp at Hv; exact Hv,
    rw ← Hk, apply all_bounded },
  have not_unbounded : ¬ set.unbounded (≤) (set.range f) := by rwa set.not_unbounded_iff,
  contradiction
end

lemma arg_le_strict_mono {f : ℕ → ℕ} {Hmono : strict_mono f} {n : ℕ} : n ≤ f n :=
begin
  induction n with n IH,
  { apply zero_le },
  { suffices : n < f n.succ, tauto,
    calc n ≤ f n : IH
    ...    < f n.succ : Hmono _,
    rw lt_succ_iff }
end

lemma unbounded_of_strict_mono
  (f : ℕ → ℕ) (Hmono : strict_mono f) : set.unbounded (≤) (set.range f) :=
begin
  by_contra',
  have bounded : set.bounded (≤) (set.range f) := by rwa set.not_unbounded_iff at this,
  obtain ⟨m, Hm⟩ : ∃ m, ∀ v ∈ set.range f, v ≤ m := bounded,
  have : m + 1 ≤ m :=
    calc m.succ ≤ f m.succ : by apply arg_le_strict_mono; assumption
    ...         ≤ m        : Hm (f m.succ) (set.mem_range_self _),
  linarith
end

Yaël Dillies (Mar 07 2022 at 17:20):

Your arg_le_strict_mono is docs#strict_mono.id_le. For the strict_mono -> unbounded part, you need no_max_orderon the domain and something like eventually docs#well_founded on the codomain. For the unbounded -> exists_between part, you need docs#linear_order + docs#succ_order on the domain.