## Stream: new members

### Topic: Defining auxiliary sequences in tutorial

#### Carlo Cabrera (May 17 2020 at 21:14):

I'm working through the tutorials, and one part has me wanting to try to figure out how to apply the squeeze theorem to show that a sequence has a certain limit. See the following example.

example (x : ℝ) (u : ℕ → ℝ) (h : ∀ n, u n ≤ x) (h' : ∀ n : ℕ, x - 1 /(n+1) ≤ u n) :
(seq_limit u x) :=
begin
let v : ℕ → ℝ := λ n, x,
have seq_v : ∀ n : ℕ, v n = x,
intro n,
linarith,
let w : ℕ → ℝ := λ n, x - 1 / (n + 1),
have seq_w : ∀ n : ℕ, w n = x - 1 / (n + 1),
sorry,
sorry
end


I have the sequence u, and it is sandwiched between two other convergent sequences. However, I need to define these two other sequences, and the way I'm doing it now doesn't seem to be the right way. In particular, the way I've defined v seems to not be too transparent for Lean, though I've managed to convince it that it has the property that I need. Unfortunately, what I did for v doesn't work for w.

Can anyone point me in the right direction? Thank you.

#### Carlo Cabrera (May 17 2020 at 21:22):

I guess I should be using choose here? That seems to be how one of the exercises constructed a sequence, but my hypotheses don't seem to have the right form for choose.

#### Rob Lewis (May 17 2020 at 21:27):

When you're looking for help here it's best to post a #mwe so that people can try out your code.

#### Rob Lewis (May 17 2020 at 21:28):

But I can see this one: seq_v and seq_w are true by definition. You can prove both of these with intro, refl.

#### Carlo Cabrera (May 17 2020 at 21:34):

Rob Lewis said:

But I can see this one: seq_v and seq_w are true by definition. You can prove both of these with intro, refl.

I thought that was an #mwe! In any case, you're right. It does work. I could swear I tried refl first, because I knew it was true by definition, but it seems I had not. Thanks for taking the time to address my silly question.

#### Kevin Buzzard (May 17 2020 at 21:34):

A mwe will run for me if I just cut and paste what you posted. This doesn't.

#### Kevin Buzzard (May 17 2020 at 21:35):

Oh! Maybe set v : ℕ → ℝ := λ n, x with seq_v might do everything for you in one go.

#### Carlo Cabrera (May 17 2020 at 21:37):

Kevin Buzzard said:

A mwe will run for me if I just cut and paste what you posted. This doesn't.

Yes, it does rely on the definition of seq_limit in the tutorial. Thought that was fine. Sorry about that! I have not yet managed to track down the definition of the limit of a sequence in mathlib.

#### Rob Lewis (May 17 2020 at 21:37):

Kevin Buzzard said:

Oh! Maybe set v : ℕ → ℝ := λ n, x with seq_v might do everything for you in one go.

Not quite, it will give you the unapplied version v = lambda n, ... instead of forall n, v n = ...

#### Carlo Cabrera (May 17 2020 at 21:55):

Edit: Fixed now.

Here is the #mwe.

import data.real.basic

def seq_limit (u : ℕ → ℝ) (l : ℝ) : Prop := ∀ ε > 0, ∃ N, ∀ n ≥ ℕ, abs (u n - l) ≤ ε

example (x : ℝ) (u : ℕ → ℝ) (h : ∀ n, u n ≤ x) (h' : ∀ n : ℕ, x - 1 /(n+1) ≤ u n) :
(seq_limit u x) :=
begin
let v : ℕ → ℝ := λ n, x,
have seq_v : ∀ n : ℕ, v n = x := by intro; refl,
let w : ℕ → ℝ := λ n, x - 1 / (n + 1),
have seq_w : ∀ n : ℕ, w n = x - 1 / (n + 1) := by intro; refl,
end


I feel like there should be a better way to define the auxiliary sequences I need, but I suppose proceeding with the example as written will work.

#### Kevin Buzzard (May 17 2020 at 21:59):

Why do you need to even define the sequences?

#### Carlo Cabrera (May 17 2020 at 22:04):

I would like to use the squeeze theorem (defined earlier in the tutorial) to conclude. I don't need the squeeze theorem to finish the proof; I was just thinking it would be good to know how to use it. (I know I don't state the squeeze theorem in the example, but I don't think that's necessary for the question. I can include the statement if it's needed.)

#### Kevin Buzzard (May 17 2020 at 22:06):

Why not just apply the squeeze theorem and then deal with all the inputs later?

#### Kevin Buzzard (May 17 2020 at 22:07):

If a function needs ten inputs and then spits out a proof of theorem X, and your goal is theorem X then you can just apply the function anyway

#### Kevin Buzzard (May 17 2020 at 22:07):

You'll just end up with ten goals

#### Kevin Buzzard (May 17 2020 at 22:08):

It's this weird backwards way that computer scientists think about proofs

#### Carlo Cabrera (May 17 2020 at 22:12):

Good question. Part of the reason is that I don't even understand the tactic state after applying the squeeze theorem. These ?m_1s show up in the goals of my tactic state. I think those ?m_1s are meant to be the sequences I wanted to define.

#### Kevin Buzzard (May 17 2020 at 22:13):

Maybe you should apply it and just fill in some of the easy inputs

#### Kevin Buzzard (May 17 2020 at 22:13):

What is the type of the squeeze theorem?

#### Kevin Buzzard (May 17 2020 at 22:14):

Just fill in the first few inputs which have round brackets

And apply that

#### Carlo Cabrera (May 17 2020 at 22:16):

Here is the type, which is what I get when I #check squeeze. (That's what you meant, right?)

squeeze :
seq_limit ?M_1 ?M_4 →
seq_limit ?M_3 ?M_4 →
(∀ (n : ℕ), ?M_1 n ≤ ?M_2 n) → (∀ (n : ℕ), ?M_2 n ≤ ?M_3 n) → seq_limit ?M_2 ?M_4


Sadly the first few inputs seem to require furnishing the sequences I wanted to define.

#### Kevin Buzzard (May 17 2020 at 22:18):

Why not skip the first two inputs by putting underscores and then fill in the next two with h and h'

#### Kevin Buzzard (May 17 2020 at 22:18):

And then you can refine it

#### Carlo Cabrera (May 17 2020 at 22:19):

Kevin Buzzard said:

Why not skip the first two inputs by putting underscores and then fill in the next two with h and h'

Yup, I realised that just after sending my last message. :) That also works. Thank you!

#### Mario Carneiro (May 17 2020 at 22:19):

You can also #check @squeeze so that it doesn't do the metavariable thing

#### Mario Carneiro (May 17 2020 at 22:19):

and supply the appropriate construction with @squeeze _ _ (my sequence) _ _ _ _ _

#### Carlo Cabrera (May 17 2020 at 22:22):

Mario Carneiro said:

You can also #check @squeeze so that it doesn't do the metavariable thing

Nice tip, thank you.

Last updated: May 09 2021 at 19:11 UTC