Limits of product

Stream: maths

[Patrick Massot]

I think we should create a stream "Lean for teaching". This message is a follow up to the conversation around https://github.com/ImperialCollegeLondon/M1P1-lean. The question is: can we write the product rule for limits of sequence in the literate style that we want for writing a bilingual math/Lean elementary analysis textbook. I think Kevin's rule of sticking to the proofs taught at Imperial is a bit too rigid. I think we can still draw inspiration from the mathlib thousands-of-lemmas-style.

[Patrick Massot]

We clearly want to teach that:

lemma tendsto_iff_sub_tendsto_zero {a : ℕ → ℝ} {l : ℝ} :
  is_limit (λ n, a n - l) 0 ↔ is_limit a l :=
begin
  split ;
  { intros h ε εpos,
    rcases h ε εpos with ⟨N, H⟩,
    use N,
    intros n hn,
    simpa using H n hn }
end

(sorry that one isn't commented)

[Patrick Massot]

Then a very important trick that can be utterly confusing for beginners, so let's state it openly

-- In the definition of a limit, the final ε can be replaced
-- by a constant multiple of ε. We could assume this constant is positive
-- but we don't want to deal with this when applying the lemma.
lemma tendsto_of_mul_eps (a : ℕ → ℝ) (l : ℝ) (A : ℝ)
  (h : ∀ ε > 0, ∃ N, ∀ n ≥ N, | a n - l | < A*ε) : is_limit a l :=
begin
  -- Let ε be any positive number
  intros ε εpos,
  -- A is either non positive or positive
  cases le_or_gt A 0 with Anonpos Apos,
  { -- If A is non positive then our assumed bound quickly
    -- gives a contradiction.
    exfalso,
    -- Indeed we can apply our assumption to ε = 1 to get N such that
    -- ∀ (n : ℕ), n ≥ N → |a n - l| < A * 1
    rcases h 1 (by linarith) with ⟨N, H⟩,
    -- in particular this holds when n = N
    specialize H N (by linarith),
    -- but |a N - l| ≥ 0 so we get a contradiction
    have : |a N - l| ≥ 0, from abs_nonneg _,
    linarith },
  { -- Now assume A is positive. Our assumption h gives N such that
    -- ∀ n ≥ N, |a n - l| < A * (ε / A)
    rcases h (ε/A) (div_pos εpos Apos) with ⟨N, H⟩,
    -- we can simplify that A * (ε / A) and we are done.
    rw mul_div_cancel' _ (ne_of_gt Apos) at H,
    tauto }
end

[Kevin Buzzard]

I talked about this product of limits lemmas with the undergrads today in an informal course I'm giving. We reduced product of limits = limit of products to linearity of limits and the assertion that the product of null sequences is null. I think this is a nicer proof than the one I typed up.

[Patrick Massot]

Yeah, let's move towards the actual goal. Notice how the constant A from the preceding lemma is not instantiated before we get it. But Lean doesn't need to be told at the end!

lemma tendsto_bounded_mul_zero {a : ℕ → ℝ} {b : ℕ → ℝ} {A : ℝ} (Apos : A > 0)
  (hA : has_bound a A) (hB : is_limit b 0)
  : is_limit (a*b) 0 :=
begin
  -- Let's apply our variant of the definition of limits where the final
  -- ε gets multiplied by some constant to be determined
  apply tendsto_of_mul_eps,
  -- Let ε be any positive number
  intros ε εpos,
  -- by assumption hB, we get some N such that
  -- ∀ (n : ℕ), n ≥ N → |b n| < ε
  cases hB ε εpos with N H,
  simp at H,
  -- Let's use that N
  use N,
  -- And compute for any n ≥ N
  intros n nN,
  calc
  |(a * b) n - 0| = |a n * b n|    : by simp
              ... = |a n| * |b n|  : abs_mul _ _
              ... ≤ A*|b n|        : mul_le_mul_of_nonneg_right (hA n) (abs_nonneg _)
              ... < A*ε            : mul_lt_mul_of_pos_left (H n nN) Apos
end

[Patrick Massot]

Oh crap, I just noticed I left the Apos assumption that I intended to remove. I don't need it to apply tendsto_of_mul_eps but I need it in the last inequality above

[Patrick Massot]

Anyway, I can still prove the multiplication lemma:

[Patrick Massot]

-- The limit of the product is the product of the limits.
-- If aₙ → l and bₙ → m then aₙ * bₙ → l * m.
theorem tendsto_mul (a : ℕ → ℝ) (b : ℕ → ℝ) (l m : ℝ)
  (h1 : is_limit a l) (h2 : is_limit b m) :
  is_limit (a * b) (l * m) :=
begin
  -- We apply the difference criterion so we need to prove a*b - l*m goes to zero
  rw ←tendsto_iff_sub_tendsto_zero,

  -- The key idea is to introduce (a_n - l) and (b_n - m) in this difference
  have key : (λ n, (a*b) n - l*m) = (λ n, (a n)*(b n - m) + m*(a n - l)),
  by simp ; ring,
  rw key,

  -- By addition of limit, it then suffices to prove a_n * (b_n - m) and m*(a_n - l)
  -- both go to zero
  suffices : is_limit (λ n, a n * (b n - m)) 0 ∧ is_limit (λ n, m * (a n - l)) 0,
  { rw [show (0 : ℝ) = 0 + 0, by simp],
    exact tendsto_add _ _ _ _ this.left this.right},
  -- Let's tackle one after the other
  split,
  { -- Since a is convergent, it's bounded by some positive A
    rcases bounded_pos_of_convergent a ⟨l, h1⟩ with ⟨A, A_pos, hA⟩,
    -- We can reformulate the b convergence assumption as b_n - m goes to zero.
    have limb : is_limit (λ n, b n - m) 0,
     from tendsto_iff_sub_tendsto_zero.2 h2,
    -- So we can conclude using our lemma about product of a bounded sequence and a
    -- sequence converging to zero
    exact tendsto_bounded_mul_zero  A_pos hA limb },
  { -- It remains to prove m * (a_n - l) goes to zero
    -- If m = 0 this is obvious.
    by_cases Hm : m = 0,
    { simp [Hm, tendsto_const] },
    -- Otherwise we follow the same strategy as above.
    { -- We reformulate our convergence assumption on a as a_n - l goes to zero
      have lima : is_limit (λ n, a n - l) 0,
        from tendsto_iff_sub_tendsto_zero.2 h1,
      -- and conclude using the same lemma
      exact tendsto_bounded_mul_zero (abs_pos_iff.2 Hm) (has_bound_const m) lima } }
end

[Kevin Buzzard]

I am ultimately envisaging the text looking like LaTeX and you can click on it and open up the Lean.

[Patrick Massot]

How do you like my proofs?

[Kevin Buzzard]

I can only understand them if I look at them in Lean and I'm in the middle of something else right now :-) Nat subtraction :-/

[Patrick Massot]

https://github.com/ImperialCollegeLondon/M1P1-lean/pull/1

[Patrick Massot]

I'm a bit disappointed that you can look at them only in Lean. There are so many comments!

[Kevin Buzzard]

Maybe I mean "I'm sort of focussed on something else"

[Kevin Buzzard]

But I'll certainly look later.