# Zulip Chat Archive

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

.

#### Kenny Lau (Jul 22 2019 at 12:32):

hfs?

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

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