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
Archimedean Property, Casting/Coercion,
bound, linarith,
field_simp, exact_mod_cast
Non-convergence of (-1)^n, triangle inequality.
Lecture 5 Notes
Doubling a sequence doubles the limit.
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
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
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
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!
Orbits, "Fancy" Choose, Peaks, Unbounded Peaks, and Monotone Subsequences.
Lecture 14 Notes
Bolzano-Weierstrass
The Construction of the Real Numbers!
Completion of Metric Spaces is Complete!
Lecture 17 Notes
Series, Series Having a Limit, Series Converging,
Convergence Implies Terms Decay,
Leibniz Series,
Series Order Theorem,
Basel Problem,
Cesaro Summation
Infinite Summation is not Commutative!
Absolute Convergence implies Convergence
Alternating Series Test
Lecture 19 Notes
If the series converges Absolutely, then Infinite Summation is Commutative!
If not, then infinite summation is as non-commutative as possible!
(Riemann Rearrangement Theorem.)
Functions!! Function Limits,
Continuity,
Sequential Criterion for Limits
Lecture 21 Notes
Sequential Limit Converges iff Function Limit does;
Derivatives! at a Point;
Derivative as a Function;
Continuity Everywhere
Pointwise vs Uniform Convergence
Composition of Continuous functions is Continuous
Uniform Limit of Continuous functions is Continuous
Integration! Riemann Sums
Area of a Parallelogram
Riemann Sums Refinement
Riemann Sums converge, as long as f is Uniformly Continuous
f is uniformly continuous, as long as the set is Compact
Lecture 24 Notes
Compact, Open, Closed Sets
Least Upper Bound (supremum), Existence
Heine-Borel Theorem
Countable/Uncountable Infinities,
Limits of Integrals is Integral of Limits,
Intermediate Value Theorem!! :)