Analysis · existing Mathlib theorem

Fundamental Theorem of Calculus

Let a function from the real line into a complete real normed vector space be differentiable throughout the closed interval between two endpoints. If its derivative is interval-integrable, then integrating that derivative from the first endpoint to the second gives the function's final value minus its initial value.

derivatives
interval integrals
endpoint values
normed spaces

Four separate status axes

Upstream indexedPinned source bytes verified locally

Locally reproducedExact upstream declaration replayed

Reviewed pageCurrent public presentation reviewed

Accepted Atlas resultNot recorded for the preferred artifact

These states distinguish upstream identity, local reproduction, review, and Atlas acceptance. This page is part of the public, read-only Mathlib landmark collection.

Formal orientation

Statement map

This deterministic map orients the reader from the mathematical summary to the pinned declaration and exact checked form. The HTML statement below is authoritative.

The theorem at a glance

Fundamental Theorem of Calculus at a glance

A source-bound editorial overview of the exact Mathlib formulation. The image is explanatory; the statement map, formal type, and pinned source remain authoritative.

An ivory theorem poster shows an oriented interval from a to b, a derivative-accumulation ribbon, the endpoint difference formula, a reversed-orientation echo, and the theorem's completeness, differentiability, and integrability hypotheses. — Oriented integration of the derivative recovers the endpoint change, with every analytic hypothesis and the reversed-endpoint behavior kept visible.

A smooth curve spans two endpoints above layered blue and green signed accumulation, ending at one vertical endpoint difference. — Accumulating the derivative across an oriented interval produces the function's endpoint change.

Complementary intuition

A mathematical landmark

The theorem makes differentiation and integration inverse processes under precise analytic hypotheses. It is a central organizing principle of calculus and analysis.

The low-text schematic gives the theorem a visual identity; it does not replace the source-bound poster or exact statement.

Authoritative formal type

Exact Mathlib statement

intervalIntegral.integral_deriv_eq_sub {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} [CompleteSpace E] {f : ℝ → E} (hderiv : ∀ x ∈ Set.uIcc a b, DifferentiableAt ℝ f x) (hint : IntervalIntegrable (deriv f) MeasureTheory.volume a b) : ∫ (y : ℝ) in a..b, deriv f y = f b - f a

Selected evidence declaration text

theorem intervalIntegral.integral_deriv_eq_sub {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} [CompleteSpace E] {f : ℝ → E} (hderiv : ∀ x ∈ Set.uIcc a b, DifferentiableAt ℝ f x) (hint : IntervalIntegrable (deriv f) MeasureTheory.volume a b) : ∫ (y : ℝ) in a..b, deriv f y = f b - f a

Proof architecture

How Mathlib proves FTC-2 for integrable derivatives

8 curated stages

The checked route proves the difficult real inequality through Vitali--Caratheodory approximation and closed-interval propagation, obtains the reverse inequality by negation, lifts the real identity through separating continuous dual functionals, handles interval orientation, and finally specializes the result to the derivative of a differentiable function.

These source-anchored stages explain the retained Mathlib proof route. They are generated explanations, not proof evidence or an extracted Lean proof-term dependency graph.

The hard real estimate allows an arbitrary margin
The hard real estimate allows an arbitrary margin
The real-valued upper estimate is reduced to proving endpoint growth is at most the comparison integral plus every positive error margin.
Open original image in a new tab
The real-valued upper estimate is reduced to proving endpoint growth is at most the comparison integral plus every positive error margin.
g b - g a <= integral a..b phi + epsilon, for every epsilon > 0
For the hard real direction of FTC-2 on an ordered interval, le_of_forall_pos_le_add reduces the required inequality to one with an arbitrary positive epsilon margin. The proof will remove that margin after replacing the comparison function by a better-behaved majorant.
A lower-semicontinuous majorant controls the integral
A lower-semicontinuous majorant controls the integral
Vitali--Caratheodory places an integrable lower-semicontinuous majorant strictly above the comparison function while keeping its integral within the chosen margin.
Open original image in a new tab
Vitali--Caratheodory places an integrable lower-semicontinuous majorant strictly above the comparison function while keeping its integral within the chosen margin.
phi x < G' x and integral G' < integral phi + epsilon
The source invokes exists_lt_lowerSemicontinuous_integral_lt to obtain an EReal-valued lower-semicontinuous function G'. It lies strictly above phi, its real part is integrable, it is finite almost everywhere, and its integral is less than the integral of phi plus epsilon.
A closed set records how far the estimate has propagated
A closed set records how far the estimate has propagated
Points where endpoint growth is bounded by the majorant integral form a closed subset of the interval containing the left endpoint.
Open original image in a new tab
Points where endpoint growth is bounded by the majorant integral form a closed subset of the interval containing the left endpoint.
s = {t | g t - g a <= integral a..t G'} inter Icc a b
Mathlib defines the propagation set by the partial-integral inequality and intersects it with the closed interval. Continuity of g and of the interval-integral primitive proves this set closed; the left endpoint belongs to it, preparing the continuous-induction step.
The majorant forces enough local integral growth
The majorant forces enough local integral growth
At a propagated point, a real comparison slope below the lower-semicontinuous majorant yields a local lower bound for the next integral slice.
Open original image in a new tab
At a propagated point, a real comparison slope below the lower-semicontinuous majorant yields a local lower bound for the next integral slice.
(u - t) * y <= integral t..u G' for nearby u > t
At a frontier point t, the proof chooses a real y strictly between g' t and G' t. Lower semicontinuity keeps G' above y immediately to the right, and monotonicity of the restricted integral shows that the next integral slice dominates the constant-height comparison integral.
Two local bounds advance the estimate
Two local bounds advance the estimate
The right derivative bounds function growth by the same comparison slope, so the propagated inequality extends to a new point.
Open original image in a new tab
The right derivative bounds function growth by the same comparison slope, so the propagated inequality extends to a new point.
g u - g t <= (u - t) * y <= integral t..u G'
The right-derivative hypothesis bounds g u - g t by the same real comparison slope used in the integral estimate. Combining the two local bounds and using additivity of adjacent interval integrals produces a point strictly to the right that still satisfies the propagation inequality.
Local advances fill the closed interval
Local advances fill the closed interval
Closedness and a rightward advance from every interior frontier propagate the estimate to the endpoint, where the error margin is removed.
Open original image in a new tab
Closedness and a rightward advance from every interior frontier propagate the estimate to the endpoint, where the error margin is removed.
g b - g a <= integral a..b phi
The closed-interval induction lemma turns the local extension property into inclusion of all of Icc a b in the propagation set. Evaluating at b and applying the majorant's integral bound removes epsilon. A closure argument then passes from the half-open derivative formulation to the interior derivative hypothesis.
The mirrored estimate closes to real equality
The mirrored estimate closes to real equality
Applying the established upper estimate to the negated function gives the reverse inequality; antisymmetry yields the real FTC identity.
Open original image in a new tab
Applying the established upper estimate to the negated function gives the reverse inequality; antisymmetry yields the real FTC identity.
integral a..b g' = g b - g a
Mathlib applies the proved upper estimate to -g, -g', and -phi to derive the reverse inequality for the original data. le_antisymm then combines the two bounds into the real-valued interval-integral identity.
Scalar dual views reassemble the selected theorem
Scalar dual views reassemble the selected theorem
Continuous real linear functionals reduce the vector-valued identity to the real theorem; interval orientation and differentiability then close the exact selected declaration.
Open original image in a new tab
Continuous real linear functionals reduce the vector-valued identity to the real theorem; interval orientation and differentiability then close the exact selected declaration.
integral a..b (deriv f) = f b - f a
SeparatingDual.eq_iff_forall_dual_eq reduces the vector-valued equality to its image under every continuous real linear functional. Such functionals commute with the interval integral and subtraction, so the real theorem applies. Mathlib then handles both interval orientations, converts full derivatives to right derivatives, and specializes DifferentiableAt to HasDerivAt in integral_deriv_eq_sub.

Claim boundary

No new theorem is claimed

This page presents Mathlib's endpoint-difference form over the unordered closed interval Set.uIcc a b with an oriented interval integral. It requires pointwise differentiability there and IntervalIntegrable (deriv f); it is not every formulation of the Fundamental Theorem of Calculus.

Proof Atlas did not originate the Fundamental Theorem of Calculus or Mathlib's declaration.
The hypotheses in the exact formal type are material and are not replaced by an unconditional slogan.
The page does not claim a new analytic argument.

Provenance

Origin and evidence stay separate

Existing declaration: intervalIntegral.integral_deriv_eq_sub in mathlib
Relationship: The checked artifact is the upstream declaration itself
Preferred checked artifact: artifact.library.mathlib.fundamental-theorem-calculus.v001
Source handling: Verified upstream reference; no mirrored source package

Statement map

Fundamental Theorem of Calculus at a glance

A mathematical landmark

Exact Mathlib statement

How Mathlib proves FTC-2 for integrable derivatives

The hard real estimate allows an arbitrary margin

A lower-semicontinuous majorant controls the integral

A closed set records how far the estimate has propagated

The majorant forces enough local integral growth

Two local bounds advance the estimate

Local advances fill the closed interval

The mirrored estimate closes to real equality

Scalar dual views reassemble the selected theorem

No new theorem is claimed

Origin and evidence stay separate