Mathlib Map

Map · 26

real analysis

MSC 26 · Real functions

8,686 declarations (8,207 theorems, 479 definitions) across 190 files. 23 of the 57 famous theorems listed for this area are in Mathlib (40%). 13 open conjectures here are stated in Lean.

Files are assigned to areas by a language model reading each file's documentation. Report a file that is in the wrong area.

Subareas4

  • 26A Functions of one variable 6,789
  • 26B Functions of several variables 1,441
  • 26D Inequalities in real analysis 409
  • 26C Polynomials, rational functions in real analysis 47

Famous theorems23 of 57

From the 1000+ theorems project, which classifies each theorem by MSC area.

Not yet in Mathlib · 34

In Mathlib · 23

From the 100 theorems list5

Open conjectures stated in Lean13

Statements without proofs, collected by the Formal Conjectures project.

Undergraduate topics still missing38 of 115

From Mathlib's own undergraduate checklist.

Single Variable Real Analysis · 14 of 74

  • Numerical series › Convergence of real-valued series
  • Numerical series › summation of comparison relations
  • Numerical series › error estimation
  • Numerical series › absolute convergence
  • Numerical series › products of series
  • Differentiability › piecewise $C^k$ functions
  • Taylor-like theorems › Taylor's theorem with little-o remainder
  • Taylor-like theorems › Taylor series expansions
  • Integration › integral over a segment of piecewise continuous functions
  • Integration › improper integrals
  • Integration › absolute vs conditional convergence of improper integrals
  • Integration › comparison test for improper integrals
  • Sequences and series of functions › normal convergence
  • Convexity › continuity and differentiability of convex functions › differentiability

Multivariable calculus · 24 of 41

  • Differential calculus › partial derivatives
  • Differential calculus › Jacobian matrix
  • Differential calculus › Hessian matrix
  • Differential calculus › $k$-th order partial derivatives
  • Differential calculus › Taylor's theorem with little-o remainder
  • Differential equations › maximal solutions
  • Differential equations › exit theorem of a compact subspace
  • Differential equations › autonomous differential equations
  • Differential equations › phase portraits
  • Differential equations › qualitative behavior
  • Differential equations › stability of equilibrium points (linearisation theorem)
  • Differential equations › linear differential systems
  • Differential equations › method of constant variation (Duhamel’s formula)
  • Differential equations › constant coefficient case
  • Differential equations › solving systems of differential equations of order $> 1$
  • Submanifolds of $\R^n$ › local graphs
  • Submanifolds of $\R^n$ › local parameterization
  • Submanifolds of $\R^n$ › local equation
  • Submanifolds of $\R^n$ › tangent space
  • Submanifolds of $\R^n$ › position with respect to the tangent plane
  • Submanifolds of $\R^n$ › gradient
  • Submanifolds of $\R^n$ › line integral
  • Submanifolds of $\R^n$ › curve length
  • Submanifolds of $\R^n$ › Lagrange multipliers

Structures defined here2

Typeclasses defined in this area's files, most assumed first.

Files190

Largest first. The code after each file is its assigned subarea.