Analysis in Mathlib: Calculus, Measures, and Spaces

Analysis in Mathlib spans the Mathlib/Analysis/ and Mathlib/MeasureTheory/ directories and represents one of the deepest and most extensively verified bodies of mathematics in any proof assistant. The development covers real and complex analysis from first principles — derivatives, integrals, power series — through the full machinery of measure theory (sigma-algebras, Lebesgue and Bochner integration, Fubini’s theorem), functional analysis (normed and Banach spaces, the Hahn-Banach theorem, the open mapping theorem), and Hilbert space theory including the Fréchet-Riesz representation and the spectral theorem for self-adjoint operators. The analysis library integrates tightly with Mathlib’s topology layer: continuity, convergence, and compactness arguments all flow through the unified Filter abstraction.

Real and Complex Analysis

Basic Number Types

#check Real     -- ℝ, the real numbers (as a Cauchy completion of ℚ)
#check Complex  -- ℂ = ℝ × ℝ with i² = -1
#check EReal    -- Extended reals ℝ ∪ {-∞, +∞}

Derivatives and Differentiability

Mathlib formalizes derivatives for functions between general normed spaces using the Fréchet derivative, with one-dimensional derivatives as a special case.

-- Fréchet derivative at a point
#check HasFDerivAt      -- f has Fréchet derivative f' at x
#check DifferentiableAt -- f is Fréchet-differentiable at x
#check DifferentiableOn -- f is differentiable on a set

-- One-dimensional derivative
#check HasDerivAt       -- f has derivative f' at x (scalar case)
#check deriv            -- The derivative function ℝ → ℝ

-- Chain rule
#check HasFDerivAt.comp
-- (hg : HasFDerivAt g g' (f x)) → (hf : HasFDerivAt f f' x) →
--   HasFDerivAt (g ∘ f) (g'.comp f') x

Mean Value Theorem

#check exists_ratio_deriv_eq_ratio_slope
-- ∃ c ∈ (a, b), (f b - f a) / (b - a) = deriv f c

Rolle's Theorem

#check exists_deriv_eq_zero
-- f a = f b → ∃ c ∈ (a, b), deriv f c = 0

Inverse Function Theorem

#check HasStrictFDerivAt.to_localInverse

Implicit Function Theorem

#check ImplicitFunctionData.implicitFunction

-- Higher-order smoothness: Cᵏ functions
#check ContDiff        -- f is k-times continuously differentiable

-- Taylor's theorem
-- (see Mathlib.Analysis.Calculus.Taylor)

-- Local extrema
#check IsLocalMin.fderiv_eq_zero  -- Fermat's theorem

Special Functions

#check Real.exp    -- Exponential function
#check Real.log    -- Natural logarithm
#check Real.sin    -- Sine
#check Real.cos    -- Cosine
#check Real.arcsin -- Arcsine
#check Real.sinh   -- Hyperbolic sine

Measure Theory and Integration

Measure theory lives in Mathlib.MeasureTheory and provides the rigorous foundations for integration used throughout analysis and probability.

Sigma-Algebras and Measures

-- Measurable spaces and sigma-algebras
#check MeasurableSpace     -- Type class: a sigma-algebra on α
#check Measurable          -- f : α → β is measurable
#check BorelSpace          -- The Borel sigma-algebra from a topology

-- Measures
#check MeasureTheory.Measure        -- A countably additive measure
#check MeasureTheory.Measure.pi     -- Product of finitely many measures
#check Real.measureSpace            -- Lebesgue measure on ℝ
#check MeasureTheory.Measure.hausdorffMeasure  -- Hausdorff measure

Integration

-- Bochner integral (vector-valued)
#check MeasureTheory.integral       -- ∫ x, f x ∂μ
#check MeasureTheory.Integrable     -- f is Bochner-integrable

-- Lebesgue integral (non-negative functions)
#check MeasureTheory.lintegral      -- ∫⁻ x, f x ∂μ

-- L^p spaces
#check MeasureTheory.Lp    -- The Banach space Lᵖ(μ)
#check MeasureTheory.UniformIntegrable  -- Uniform integrability

Dominated Convergence

#check MeasureTheory.tendsto_integral_of_dominated_convergence

Monotone Convergence

#check MeasureTheory.lintegral_iInf_ae

Fubini's Theorem

#check MeasureTheory.integral_prod
-- ∫ (x, y), f x y ∂(μ.prod ν) =
--   ∫ x, ∫ y, f x y ∂ν ∂μ

Fundamental Theorem of Calculus

-- Part 1 (differentiation of integral)
#check intervalIntegral.integral_hasFDerivAt_of_tendsto_ae
-- Part 2 (Newton-Leibniz)
#check intervalIntegral.integral_eq_sub_of_hasDeriv_right_of_le

-- Change of variables
#check MeasureTheory.integral_image_eq_integral_abs_det_fderiv_smul

-- Convolution
#check MeasureTheory.convolution
#check ContDiffBump.convolution_tendsto_right  -- Approximation by convolution

-- Haar measure on locally compact groups
#check MeasureTheory.Measure.haarMeasure

Mathlib’s Bochner integral works for functions valued in any Banach space, not just ℝ or ℂ. This generality is used extensively in probability theory and functional analysis.

Functional Analysis

Normed and Banach Spaces

-- Normed spaces
#check NormedSpace       -- A module over a normed field with compatible norm
#check NormedAddCommGroup -- Additive group with a norm

-- Continuous linear maps
#check ContinuousLinearMap   -- L : E →L[𝕜] F  (bounded linear operator)
#check LinearMap.mkContinuous -- Bound a linear map to get a continuous one

-- Norms of operators
-- ‖L‖ = sup { ‖L x‖ / ‖x‖ | x ≠ 0 }

Hahn-Banach Theorem

Every bounded linear functional on a subspace extends to the whole space.

#check exists_extension_norm_eq

Banach Open Mapping

A surjective bounded linear map between Banach spaces is open.

#check ContinuousLinearMap.isOpenMap

Banach-Steinhaus

Pointwise-bounded families of operators are uniformly bounded.

#check banach_steinhaus

Closed Graph Theorem

A linear map with closed graph between Banach spaces is continuous.

#check LinearMap.continuous_of_isClosed_graph

-- Dual space
#check StrongDual                       -- The strong dual E'
#check NormedSpace.inclusionInDoubleDualLi  -- Canonical inclusion E ↪ E''

-- Absolutely convergent series
#check Summable.of_norm   -- ∑ ‖aₙ‖ < ∞ → ∑ aₙ converges in a Banach space

Hilbert Spaces

-- Inner product spaces
#check InnerProductSpace    -- Hilbert space structure (real or complex)

-- Cauchy-Schwarz inequality
#check inner_mul_inner_self_le
-- |⟪x, y⟫| ≤ ‖x‖ * ‖y‖  (actually the squared version)

-- Orthogonal projection
#check Submodule.orthogonalProjectionOnto
#check Submodule.orthogonal   -- The orthogonal complement K⊥

-- Fréchet-Riesz representation theorem
#check InnerProductSpace.toDual
-- E ≃ₗᵢ[𝕜] E'  (isometric isomorphism with dual)

-- Existence of Hilbert basis
#check exists_hilbertBasis

-- Spectral theorem for self-adjoint operators
#check IsSelfAdjoint
#check LinearMap.IsSymmetric.eigenvectorBasis_apply_self_apply

-- Lax-Milgram theorem
#check IsCoercive.continuousLinearEquivOfBilin

Asymptotics

-- Big-O and little-o notation
#check Asymptotics.IsO       -- f = O(g) as x → a
#check Asymptotics.IsLittleO -- f = o(g) as x → a

-- Examples:
-- sin x = O(x) as x → 0
-- sin x = o(1) as x → ∞  (not quite right, but illustrates usage)

Convexity

#check ConvexOn        -- f is convex on a set
#check StrictConvexOn  -- Strict convexity

-- Characterization via second derivative
#check convexOn_of_deriv2_nonneg
-- f'' ≥ 0 on (a, b) → f convex on [a, b]

-- Jensen's inequality
#check ConvexOn.map_sum_le      -- Finite sum version
#check ConvexOn.map_integral_le -- Integral version

-- Carathéodory's theorem
#check convexHull_eq_union

Complex Analysis

-- Cauchy integral formula
#check DiffContOnCl.circleIntegral_sub_inv_smul

-- Liouville's theorem: bounded entire functions are constant
#check Differentiable.apply_eq_apply_of_bounded

-- Maximum modulus principle
#check Complex.eventually_eq_of_isLocalMax_norm

-- Principle of isolated zeros
#check AnalyticAt.eventually_eq_zero_or_eventually_ne_zero

-- Analytic continuation
#check AnalyticOnNhd.eqOn_of_preconnected_of_frequently_eq

-- Schwarz lemma
#check Complex.norm_le_norm_of_mapsTo_ball

-- Fundamental theorem of algebra
#check Complex.isAlgClosed   -- ℂ is algebraically closed

Fourier Analysis

-- Fourier transform
#check Real.fourier_eq                  -- Fourier transform as an integral
#check VectorFourier.fourierIntegral    -- General fourierIntegral definition

-- Inversion formula
#check Continuous.fourierInv_fourier_eq

-- Riemann-Lebesgue lemma
#check tendsto_integral_exp_inner_smul_cocompact

-- Parseval's formula for Fourier series
#check tsum_sq_fourierCoeff

Distribution Theory

#check TestFunction       -- Smooth compactly supported test functions
#check SchwartzMap        -- Schwartz space 𝒮(ℝⁿ)
#check Distribution       -- Distributions (generalized functions)
#check TemperedDistribution  -- Tempered distributions

The analysis contributors maintain detailed module-level docstrings. For any specific theorem, searching mathlib4_docs by identifier gives the exact statement, proof, and surrounding context.

Getting Started

Mathematics

Tactics

Contributing

Analysis in Mathlib: Calculus, Measures, and Spaces

Real and Complex Analysis

Basic Number Types

Derivatives and Differentiability

Mean Value Theorem

Rolle's Theorem

Inverse Function Theorem

Implicit Function Theorem

Special Functions

Measure Theory and Integration

Sigma-Algebras and Measures

Integration

Dominated Convergence

Monotone Convergence

Fubini's Theorem

Fundamental Theorem of Calculus

Functional Analysis

Normed and Banach Spaces

Hahn-Banach Theorem

Banach Open Mapping

Banach-Steinhaus

Closed Graph Theorem

Hilbert Spaces

Asymptotics

Convexity

Complex Analysis

Fourier Analysis

Distribution Theory

Build docs developers (and LLMs) love

Getting Started

Mathematics

Tactics

Contributing

Documentation Index

​Real and Complex Analysis

​Basic Number Types

​Derivatives and Differentiability

Mean Value Theorem

Rolle's Theorem

Inverse Function Theorem

Implicit Function Theorem

​Special Functions

​Measure Theory and Integration

​Sigma-Algebras and Measures

​Integration

Dominated Convergence

Monotone Convergence

Fubini's Theorem

Fundamental Theorem of Calculus

​Functional Analysis

​Normed and Banach Spaces

Hahn-Banach Theorem

Banach Open Mapping

Banach-Steinhaus

Closed Graph Theorem

​Hilbert Spaces

​Asymptotics

​Convexity

​Complex Analysis

​Fourier Analysis

​Distribution Theory

Build docs developers (and LLMs) love

Real and Complex Analysis

Basic Number Types

Derivatives and Differentiability

Special Functions

Measure Theory and Integration

Sigma-Algebras and Measures

Integration

Functional Analysis

Normed and Banach Spaces

Hilbert Spaces

Asymptotics

Convexity

Complex Analysis

Fourier Analysis

Distribution Theory