Analysis

Squeeze Theorem

When two bounding sequences converge to the same limit, any sequence caught between them must follow

lean4-proofanalysisvisualization

Monotone Convergence Theorem

A bounded monotone sequence of reals always converges — the supremum is the limit

lean4-proofanalysisvisualization

Cauchy Criterion

A sequence converges if and only if its terms eventually become arbitrarily close to each other — no candidate limit required

lean4-proofanalysisvisualization

Monotone Class Theorem

A pi-system closed under intersection generates the same sigma-algebra as the lambda-system it generates

lean4-proofanalysisvisualizationmeasure-theory

Fatou's Lemma

The integral of the liminf of nonnegative measurable functions is at most the liminf of their integrals

lean4-proofanalysisvisualizationmeasure-theory

Dominated Convergence Theorem

Pointwise convergence plus a uniform integrable dominating bound lets you pass the limit inside the integral

lean4-proofanalysisvisualizationmeasure-theory

Fubini's Theorem

For integrable functions on a product measure space the iterated integrals in either order both equal the double integral

lean4-proofanalysisvisualizationmeasure-theory

Lebesgue Differentiation Theorem

For locally integrable f, the ball averages of f converge to f(x) at almost every point x

lean4-proofanalysisvisualizationmeasure-theory

Absolutely Continuous Functions

A function is absolutely continuous iff it is the integral of its derivative — the bridge between differentiation and Lebesgue integration

lean4-proofanalysisvisualizationmeasure-theory

Arzelà–Ascoli Theorem

A family of continuous functions on a compact space is precompact iff it is equicontinuous and uniformly bounded

lean4-proofanalysisvisualizationtopology