Is there anything to even say about calculus? Probably!

Calculus vs Analysis. Basically the same thing https://en.wikipedia.org/wiki/Calculus

Calc I

Stewart Book

Derivatives

Tangents and Secants

When do derivatives exists Continuity Moduli of continuity https://en.wikipedia.org/wiki/Lipschitz_continuity

Product Rule Chain Rule

Sequences Series Convergence Tests

Mean Value Theorem

Taylor Series

Infinitesimals

Integrals

Fundamental theorem of calculus - an antiderivatve F' = f Area under curve Riemann integral - break up into rectangles $ lim_{n \to \infty} \sum_{i=1}^n f(i / n) \Delta x_i $. Unpack this. Does limit exist?

Measure Theory

See also probability

https://en.wikipedia.org/wiki/Measure_(mathematics) sigma algebra - set of sets closed under

Lebesgue Measure

Lebesgue Integral

Measure theory for dummies - https://vannevar.ece.uw.edu/techsite/papers/documents/UWEETR-2006-0008.pdf

Multivariate

Partial Derivatives

Somewhat subtle actually. What does it mean to “fix” the other coordinates?

Vector Calc

Grad Div Curl are best understood via their definition as

Line integrals

Stokes theorem https://en.wikipedia.org/wiki/Stokes%27_theorem

Exterior Calculus

See also differential geometry

Calculus of Variations

Functional Derivative Path Integral

Analysis

Some book reccomendations:

Abbott understanding analysis Spivak Calculus Tao I and II Rudin Jay Cummings

real analysis in reverse

real induction instructors guide to real induction https://math.stackexchange.com/questions/4202/induction-on-real-numbers open-closed induction. Very interesting. http://ucsd-pl.github.io/veridrone/induction/2016/02/17/real-induction.html veridone notes

Soft analysis, hard analysis, and the finite convergence principle As cody says, competeness is infinite pigeonhole

Cauchy sequence sequences gets closer to itself rather than talking about limit value

https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Real/Basic.html#Real Cauchy completion of Q

Dirichlet cuts. Construct reals as sets of rationals. The cut property.

Ordered Fields

Completeness of Reals

least upper bound

Bolzano Weierstrauss

archimedean property

Constructive Analysis

https://en.wikipedia.org/wiki/Constructive_analysis

https://en.wikipedia.org/wiki/Apartness_relation apartness relatiobn

Bishop

Marshal

Computable Analysis

Interval Analysis Moore

Formalization

Harrison book Theorem Proving with Real Numbers https://link.springer.com/book/10.1007/978-1-4471-1591-5 https://ncatlab.org/nlab/show/Eudoxus+real+number#:~:text=Eudoxus%20real%20number%20refers%20to,the%20floor%20of%20r%20n%20. eudoxus reals https://golem.ph.utexas.edu/category/2023/09/constructing_the_real_numbers.html Constructing the Real Numbers as Nearly Multiplicative Sequences - riehl

https://www.cl.cam.ac.uk/~jrh13/papers/trybulec.pdf - formalizig basic complex analyis - harrison

https://link.springer.com/book/10.1007/978-981-15-7261-6 Formalization of Complex Analysis and Matrix Theory

acl2 hyperreals thesis

Limits

Hyperreals

see draft