Zulip Chat Archive

Stream: maths

Topic: help with sequences


view this post on Zulip Koundinya Vajjha (Jul 22 2019 at 12:28):

I am trying to prove that if a sequence x converges to θ then inc_seq_of x also converges to θ , where inc_seq_of x is as follows:

noncomputable def inc_seq_of  (x :   nnreal) :   nnreal
| 0 := x 0
| (nat.succ n) := max (x (nat.succ n)) (inc_seq_of n)

I am stuck in a proof where the state is the following:

x :   nnreal,
θ : nnreal,
hfs :  (n : ), x n  θ,
s : set nnreal,
h :  (s : set nnreal), is_open s  θ  s  ( (a : ),  (b : ), b  a  x b  s),
hs :  (t : set nnreal) (H : t  s), is_open t  θ  t
  (a : ),  (b : ), b  a  inc_seq_of x b  s

I need to somehow pick an open interval around θ and work with that. Are there any lemmas saying something like this? I can't seem to understand how to use the basic open sets of nnreal in a proof.

view this post on Zulip Kenny Lau (Jul 22 2019 at 12:29):

x = 1, 1/2, 1/3, 1/4, 1/5, ...
inc_seq_of x = 1, 1, 1, 1, 1, ...
?

view this post on Zulip Koundinya Vajjha (Jul 22 2019 at 12:31):

Sorry I should have mentioned that my sequence converges to a point which is bigger than or equal to every term

view this post on Zulip Koundinya Vajjha (Jul 22 2019 at 12:31):

See hypothesis hfs.

view this post on Zulip Kenny Lau (Jul 22 2019 at 12:32):

hfs?

view this post on Zulip Koundinya Vajjha (Jul 22 2019 at 12:32):

In the snippet.

view this post on Zulip Kevin Buzzard (Jul 22 2019 at 12:39):

You know x n is a nnreal which is <= 0? Just prove it's zero and then prove everything is zero.

view this post on Zulip Koundinya Vajjha (Jul 22 2019 at 12:39):

hah no that's a theta not zero.

view this post on Zulip Kevin Buzzard (Jul 22 2019 at 12:39):

ha ha I should put my glasses on :-)

view this post on Zulip Kevin Buzzard (Jul 22 2019 at 12:41):

Why don't you just prove that x n <= inc_Seq_of x n <= theta and then use the sandwich theorem?

view this post on Zulip Kevin Buzzard (Jul 22 2019 at 12:42):

http://wwwf.imperial.ac.uk/~buzzard/docs/lean/sandwich.html

view this post on Zulip Koundinya Vajjha (Jul 22 2019 at 12:42):

oh wow I didn't know we had the sandwich theorem!

view this post on Zulip Kevin Buzzard (Jul 22 2019 at 12:43):

We have things like the definition of e^x as a power series; we will surely have oodles of lemmas about sequences and series converging.

view this post on Zulip Kevin Buzzard (Jul 22 2019 at 12:43):

But I don't know this part of mathlib at all.

view this post on Zulip Kevin Buzzard (Jul 24 2019 at 19:03):

I don't think your goal is true in the proof you're stuck in. You can prove that for all sufficiently large n, x n \in t, but if x 0 equals theta - 0.1, and all the other x_i are <= theta-0.2, and theta-0.1 is not in t then aren't you in trouble?


Last updated: May 12 2021 at 07:17 UTC