help with sequences

Stream: maths

[Koundinya Vajjha]

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]

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

[Koundinya Vajjha]

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

[Koundinya Vajjha]

See hypothesis hfs.

[Kenny Lau]

hfs?

[Koundinya Vajjha]

In the snippet.

[Kevin Buzzard]

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

[Koundinya Vajjha]

hah no that's a theta not zero.

[Kevin Buzzard]

ha ha I should put my glasses on :-)

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Koundinya Vajjha]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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?