Course Description: The primary aim of this course is to teach you the rigorous foundations of calculus — foundations which were omitted in earlier calculus courses. We will give precise definitions of the concept of a limit and of such concepts as the continuity and differentiability of functions, and will prove some of the many consequences which may be deduced from these definitions. A secondary aim is to improve your skills in reading and understanding mathematics written by others and in writing precise definitions and rigorous proofs of your own.
More information: is available on the Course Info Page.
Week | Lecture 1 Video | Lecture 2 Video | Topics/Content/Notes/Other |
---|---|---|---|
Week 1, 09/02, 09/05 |
Lecture 1 Notes Newton, Leibniz, Cauchy, Fourier, Lean tactics: exact, rfl, rewrite, ring_nf, use, intro, specialize, choose Lecture 2 Notes Newton's computation of π Formal definition of the limit of a sequence |
||
Week 2, 09/09, 09/12 | Installing Lean locally (VS Code etc), GitHub (Issues, Pull Requests) |
Lecture 3 Notes Archimedean Property, Casting/Coercion, bound, linarith, field_simp, exact_mod_cast |
|
Week 3, 09/16, 09/19 |
MIDTERM 1 REVIEW, and |
Lecture 4 Notes Non-convergence of (-1)^n, triangle inequality. Lecture 5 Notes Doubling a sequence doubles the limit. |
|
Week 4, 09/23, 09/26 | MIDTERM 1 |
Lecture 6 Notes Limit of a Sum is the the Sum of the Limits, dealing with conjunction/disjunction (And and Or) in the Goal and Hypotheses, and the Squeeze Theorem |
|
Week 5, 09/30, 10/03 |
Lecture 7 Notes Limit is Unique, Convergent Sequence stays away from zero, Limit of Abs Value is the the Abs Value of the Limit, Limit of Reciprocal is Reciprocal of the Limit |
||
Week 6, 10/07, 10/10 | |||
Week 7, 10/14, 10/17 | |||
Week 8, 10/21, 10/24 | |||
Week 9, 10/28, 10/31 | MIDTERM II | ||
Week 10, 11/04, 11/07 | |||
Week 11, 11/11, 11/14 | |||
Week 12, 11/18, 11/21 | |||
Week 13, WED 11/26 (FRI schedule) | HAPPY THANKSGIVING! | ||
Week 14, 12/02, 12/05 | |||
Week 15, 12/09 | FINAL REVIEW |