Zulip Chat Archive

Stream: new members

Topic: bounding limits cont'd


view this post on Zulip Alex Kontorovich (Oct 07 2020 at 17:57):

Hello, Can I please get some help on what theorem I can use to prove this?

theorem cau_lim_le (f : cau_seq  abs) (g : cau_seq  abs) : ( j,  i, j  i  f i  g i)  f.lim  g.lim :=
begin
    intros,
    sorry,
end

Thank you!

view this post on Zulip Alex J. Best (Oct 07 2020 at 20:19):

I'm not an expert on this part of the library so hopefully someone can chime in with a better way, but I tried to use the lemma
le_of_tendsto_of_tendsto which phrases everything in terms of docs#filter.eventually, it takes a little work to line that up with the form you have though.

import topology.metric_space.cau_seq_filter
theorem cau_lim_le (f : cau_seq  abs) (g : cau_seq  abs) : ( j,  i, j  i  f i  g i)  f.lim  g.lim :=
begin
  intros,
  refine le_of_tendsto_of_tendsto (cau_seq.tendsto_limit _) (cau_seq.tendsto_limit _) _,
  rwa [filter.eventually_le, filter.eventually_at_top],
end

view this post on Zulip Alex Kontorovich (Oct 07 2020 at 23:46):

Thank you!!!

view this post on Zulip Yury G. Kudryashov (Oct 08 2020 at 02:19):

cau_seq.tendsto_limit is the main way to deal with cau_seqs. E.g., this will require very few modifications once we port exp to analytic functions.

view this post on Zulip Yury G. Kudryashov (Oct 08 2020 at 02:20):

We have many theorems about tendsto and much less about cau_seq.


Last updated: May 13 2021 at 06:15 UTC