Zulip Chat Archive

Stream: new members

Topic: sequence limit lemmas


Anatole Dedecker (Jun 22 2020 at 17:15):

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 (Jun 22 2020 at 17:17):

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 (Jun 22 2020 at 17:22):

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 (Jun 22 2020 at 17:24):

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

Patrick Massot (Jun 22 2020 at 17:25):

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

Reid Barton (Jun 22 2020 at 17:26):

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 (Jun 22 2020 at 17:26):

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

Patrick Massot (Jun 22 2020 at 17:26):

Reid, we need a conditionaly complete version

Reid Barton (Jun 22 2020 at 17:27):

I was just planning to use ereal

Reid Barton (Jun 22 2020 at 17:27):

but I agree such a version would be more convenient

Reid Barton (Jun 22 2020 at 17:29):

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

Kevin Buzzard (Jun 22 2020 at 17:32):

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 (Jun 22 2020 at 17:33):

Actually that one is pretty readable.

Patrick Massot (Jun 22 2020 at 17:33):

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

Kevin Buzzard (Jun 22 2020 at 17:34):

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 (Jun 22 2020 at 17:39):

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 (Jun 22 2020 at 17:41):

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 (Jun 22 2020 at 18:03):

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 (Jun 22 2020 at 18:15):

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

Anatole Dedecker (Jun 22 2020 at 18:16):

Yes, that's where I am !

Patrick Massot (Jun 22 2020 at 18:38):

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 (Jun 22 2020 at 18:39):

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


Last updated: Dec 20 2023 at 11:08 UTC