sequence limit lemmas

Stream: new members

[Anatole Dedecker]

Hello everyone, hope you're having a great day ! Today's problem is : I am struggling to find in mathlib some lemmas I'm used to rely on when working with limits of sequences of real numbers. More precisely, I can't find these lemmas :

import order.filter.basic
import topology.basic
import topology.instances.real

open filter
open topological_space

lemma monotone_tendsto (u : ℕ → ℝ) (h : monotone u) : tendsto u at_top at_top ∨ (∃ l : ℝ, tendsto u at_top (nhds l)) := by {
    sorry,
}

lemma lim_le_of_almost_le (u : ℕ → ℝ) (x l : ℝ) (hle : ∃ N, ∀ n ≥ N, x ≤ u n) (hu : tendsto u at_top (nhds l)) : x ≤ l := by {
    sorry,
}

I would be able to prove them quite easily if I were using epsilon-delta-limits, but I want to use mathlib as much as possible for the little project I'm working on, and I am not yet familiar with working with filters. These lemmas seem so important to me that I'm sure there are almost identical (probably more generic) lemmas in the lib, but the search is very hard : as a first year undergraduate, I only know properties of sequences of real numbers, and I don't know what structure allows which property, which makes it very inconvenient to search in the lib : should I search in filter ? topology ? topology.metric_space, and so on... So I thought people here would be able to help. Thanks in advance !

[Kevin Buzzard]

You know that there will be some lemma which says that this whole tendsto filter business is equivalent to the usual epsilon-delta definition? So you could just rewrite and then prove it yourself. However it would not surprise me at all if there was some direct fancy filter proof which is two incomprehensible lines too :-)

[Kevin Buzzard]

e.g.

lemma monotone_tendsto (u : ℕ → ℝ) (h : monotone u) : tendsto u at_top at_top ∨ (∃ l : ℝ, tendsto u at_top (nhds l)) :=
begin
  simp_rw metric.tendsto_nhds,
  rw tendsto_at_top,
  -- etc
  sorry
end

[Patrick Massot]

The second one is ge_of_tendsto at_top_ne_bot hu $ eventually_at_top.mpr hle

[Patrick Massot]

I don't think the first one is stated in this way, but it should be easy to deduce from existing lemmas.

[Reid Barton]

Maybe from

lemma tendsto_at_top_supr_nat [topological_space α] [complete_linear_order α] [order_topology α]
  (f : ℕ → α) (hf : monotone f) : tendsto f at_top (𝓝 (⨆i, f i)) :=

[Patrick Massot]

Also, you don't need all those imports, importing is transitive.

[Patrick Massot]

Reid, we need a conditionaly complete version

[Reid Barton]

I was just planning to use ereal

[Reid Barton]

but I agree such a version would be more convenient

[Reid Barton]

well, possibly more convenient depending on what happens at the use of monotone_tendsto.

[Kevin Buzzard]

Patrick Massot said:

The second one is ge_of_tendsto at_top_ne_bot hu $ eventually_at_top.mpr hle

sorry, one incomprehensible line :-)

[Patrick Massot]

Actually that one is pretty readable.

[Patrick Massot]

It's pretty easy to guess what each piece refers to, and to understand how this is relevant.

[Kevin Buzzard]

Maybe not to someone who's just done your tutorials and nothing else :-) (but actually I know Anatole has done a bunch of other stuff, I'm sure he can figure out what's going on by hovering to look at the types and thinking hard).

[Kevin Buzzard]

In fact @Anatole Dedecker you might want to try the widgets version of the VS Code extension here, search for messages by Edward Ayers containing a .vsix link and download the most recent; then follow instructions here. Then you'll be able to click on every term in Patrick's proof and see what is going on at each step even more easily than just doing all the unification yourself.

[Patrick Massot]

You don't need that, since a couple of week you can move your cursor in a proof term to see what each subterm is proving.

[Anatole Dedecker]

Thanks to everyone ! Now I just have to update my installation of mathlib, because I don't have these lemmas :sweat_smile: Guess I'll do a fresh install distinct from the math114 installation, as I was planning to do anyway

[Patrick Massot]

https://leanprover-community.github.io/install/debian.html

[Anatole Dedecker]

Yes, that's where I am !

[Patrick Massot]

One can answer your intial question by:

import topology.instances.real

open filter topological_space set
open_locale topological_space

lemma tendsto_at_top_supr_of_bdd {ι  : Type*} [nonempty ι] [semilattice_sup ι]
  {α : Type*} [topological_space α] [conditionally_complete_linear_order α] [order_topology α]
  {f : ι → α} (h_mono : monotone f) (hbdd : bdd_above $ range f) : tendsto f at_top (𝓝 (⨆i, f i)) :=
begin
  rw tendsto_order,
  split,
  { intros a h,
    rw eventually_at_top,
    cases exists_lt_of_lt_csupr h with N hN,
    exact ⟨N, λ i hi, lt_of_lt_of_le hN (h_mono hi)⟩ },
  { intros a h,
    apply univ_mem_sets',
    intros n,
    exact lt_of_le_of_lt (le_csupr hbdd n) h },
end

lemma tendsto_at_top_of_monotone {ι  : Type*} [nonempty ι] [semilattice_sup ι]
  {α : Type*} [linear_order α] [topological_space α] [order_topology α] {u : ι → α}
  (h : monotone u) (H : ¬bdd_above (range u)) : tendsto u at_top at_top :=
begin
    rw tendsto_at_top,
    intro b,
    rw mem_at_top_sets,
    rw not_bdd_above_iff at H,
    rcases H b with ⟨_, ⟨N, rfl⟩, hN⟩,
    exact ⟨N, λ n hn, le_of_lt (lt_of_lt_of_le hN $ h hn)⟩,
end

lemma monotone_tendsto (u : ℕ → ℝ) (h : monotone u) : tendsto u at_top at_top ∨ (∃ l : ℝ, tendsto u at_top (nhds l)) :=
begin
  classical,
  by_cases H : bdd_above (range u),
  { right,
    exact ⟨supr u, tendsto_at_top_supr_of_bdd h H⟩ },
  { left,
    exact tendsto_at_top_of_monotone h H },
end

lemma lim_le_of_almost_le (u : ℕ → ℝ) (x l : ℝ) (hle : ∃ N, ∀ n ≥ N, x ≤ u n) (hu : tendsto u at_top (nhds l)) : x ≤ l :=
ge_of_tendsto at_top_ne_bot hu $ eventually_at_top.mpr hle

The first two lemmas should be in https://leanprover-community.github.io/mathlib_docs/topology/algebra/ordered.html (feel free to open a PR). The last lemma already is, and the remaining one is too weak, you should replace the existential with the "explicit" description of the limit.

[Patrick Massot]

And of course both ℕ and ℝ can be generalized as in the previous lemmas.