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 Lecture 8 Notes The `by_cases` Tactic, Induction |
||
Week 6, 10/07, 10/10 |
Lecture 9 Notes Construction of Naturals (Induction), Finite Sums, Convergent implies Bounded Lecture 10 Notes Limit of products is product of Limits; the Algebraic Limit Theorem the Order Limit Theorem; Subsequences If Convergent, any Subsequence has same limit |
||
Week 7, 10/14, 10/17 |
Lecture 11 Notes Cauchy Sequences! If a sequence has a limit, then it's Cauchy; The sum of Cauchy sequences is Cauchy; If a sequence is Cauchy, then it's bounded. Lecture 12 Notes If a sequence is Monotonic (non-decreasing) and Bounded, then it is Cauchy! |
||
Week 8, 10/21, 10/24 |
Lecture 13 Notes Orbits, "Fancy" Choose, Peaks, Unbounded Peaks, and Monotone Subsequences. |
||
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 |