bounding limits cont'd

Stream: new members

[Alex Kontorovich]

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!

[Alex J. Best]

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

[Alex Kontorovich]

Thank you!!!

[Yury G. Kudryashov]

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.

[Yury G. Kudryashov]

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