## Stream: maths

### Topic: help with sequences

#### 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.

#### 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, ...
?

#### 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

#### Koundinya Vajjha (Jul 22 2019 at 12:31):

See hypothesis hfs.

hfs?

In the snippet.

#### 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.

#### Koundinya Vajjha (Jul 22 2019 at 12:39):

hah no that's a theta not zero.

#### Kevin Buzzard (Jul 22 2019 at 12:39):

ha ha I should put my glasses on :-)

#### 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?

#### Kevin Buzzard (Jul 22 2019 at 12:42):

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

#### Koundinya Vajjha (Jul 22 2019 at 12:42):

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

#### 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.

#### Kevin Buzzard (Jul 22 2019 at 12:43):

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

#### 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