## 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
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