Zulip Chat Archive

I am getting myself in a total tangle with 05_sequence_limits.lean (https://github.com/leanprover-community/tutorials/blob/master/src/exercises/05_sequence_limits.lean), and specifically the squeezing theorem. I can see the proof, but I just seem to have a sprawling mess of facts and calcs that feels very bad. I don't actually have a MWE: would it be alright if I posted what I have?

The thing which is the actual sticking point is moving from |v n - u n| = v n - u n, where I have as a hypothesis (h : ∀ n, u n ≤ v n). This feels "obviously true" but I don't know how to get it. Maybe I want to do something else... but, in short, I'm all in knots. It's this sort of messy epsilon-chasing that I always found tiresome about real analysis anyway...

Wrenna Robson (Aug 21 2020 at 23:11):

Actually, I do have a MWE, if I just sorry out the tangled bit. But it's still a mess!

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

example (hu : seq_limit u l) (hw : seq_limit w l)
(h : ∀ n, u n ≤ v n)
(h' : ∀ n, v n ≤ w n) : seq_limit v l :=
begin
  intros ε ε_pos,
  cases hu (ε/3) (by linarith) with N₁ hN₁,
  cases hw (ε/3) (by linarith) with N₂ hN₂,
  use max N₁ N₂,
  intros n hn,
  rw ge_max_iff at hn,
  have fact₁ : |u n - l| ≤ ε/3,
    from hN₁ n (by linarith),
  have fact₂ : |w n - l| ≤ ε/3,
    from hN₂ n (by linarith),
  have fact₃ : |u n - w n| ≤ 2*ε/3,
  {
    calc
    |u n - w n| = |(u n - l) + (l - w n)|  : by ring
            ... ≤ |u n - l| + |l - w n|    : by apply abs_add
            ... = |u n - l| + |w n - l|    : by rw abs_sub (w n)
            ... ≤ 2*ε/3                    : by linarith,
  },
  have fact₄ : |v n - u n| ≤ |u n - w n|,
  {
    sorry,
  },
  calc
  |v n - l| ≤ |(v n - u n) + (u n - l)| : by ring
        ... ≤ |v n - u n| + |u n - l|   : by apply abs_add
        ... ≤ ε                         : by linarith,
end

Kevin Buzzard (Aug 21 2020 at 23:47):

You've done the hard work by the time you've got to the use max line. I'm not at a computer right now but if you rewrite abs_le then linarith should be able to do everything

Patrick Massot (Aug 22 2020 at 00:02):

@Wrenna Robson you're making this a lot more complicated that it needs to be. You should think more carefully about the strategy, and have a look at the solution if you're really stuck. If you really want to prove this fourth fact your can use rw [abs_of_nonneg, abs_of_nonpos] ; linarith [h n, h' n] } but probably those lemmas have not been discussed since they are not needed.

Wrenna Robson (Aug 22 2020 at 00:50):

Yes, I feel like I'm overblowing it!
@Kevin Buzzard which line? the fourth?

Wrenna Robson (Aug 22 2020 at 00:57):

@Patrick Massot hmm! having looked at the solution, I see that, in fact my actual on-paper proof was over-complex. Which in a sense is a relief!

Patrick Massot (Aug 22 2020 at 07:54):

Yes, this is what I meant by "you're making this a lot more complicated that it needs to be". I'm sorry it wasn't clear I was referring to the pen and paper proof rather than Lean code.