# Zulip Chat Archive

## Stream: maths

### Topic: Limits of product

#### Patrick Massot (Jan 29 2019 at 21:54):

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 (Jan 29 2019 at 21:54):

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 (Jan 29 2019 at 21:55):

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 (Jan 29 2019 at 21:56):

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 (Jan 29 2019 at 21:57):

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 (Jan 29 2019 at 21:59):

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 (Jan 29 2019 at 22:16):

Anyway, I can still prove the multiplication lemma:

#### Patrick Massot (Jan 29 2019 at 22:16):

-- 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 (Jan 29 2019 at 22:17):

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

#### Patrick Massot (Jan 29 2019 at 22:18):

How do you like my proofs?

#### Kevin Buzzard (Jan 29 2019 at 22:28):

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 (Jan 29 2019 at 22:33):

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

#### Patrick Massot (Jan 29 2019 at 22:33):

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

#### Kevin Buzzard (Jan 29 2019 at 22:34):

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

#### Kevin Buzzard (Jan 29 2019 at 22:34):

But I'll certainly look later.

Last updated: May 12 2021 at 06:14 UTC