Existing in Mathlib · Analysis

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

Exact theorem

Exact Mathlib statement

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

The theorem at a glance

Fundamental Theorem of Calculus at a glance

A visual guide to the theorem's hypotheses, structure, and conclusion; the exact statement gives the formal detail.

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.

Statement structure

From hypotheses to conclusion

This map summarizes the statement's structure; the exact Mathlib declaration remains authoritative.

The curve f of t equals t squared on zero to two sits above increasing derivative bars for 2t, whose area is four. — For f(t)=t² on [0,2], integrating f′(t)=2t gives 4=f(2)−f(0).

Why it matters

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.

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`.

ProofAtlas record

What has been checked

Upstream indexedPinned source bytes verified locally

Locally reproducedExact upstream declaration replayed

Reviewed pageCurrent public presentation reviewed

Accepted Atlas resultNot recorded for the preferred artifact

Mathlib is the source of the theorem; the local Lean replay and page review are separate.

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.

Source and local evidence

Where the theorem comes from

Existing declaration: intervalIntegral.integral_deriv_eq_sub in mathlib
Relationship: The checked artifact is the upstream declaration itself
Local Lean evidence: artifact.library.mathlib.fundamental-theorem-calculus.v001
Source: Open the pinned upstream reference

Exact Mathlib statement

Fundamental Theorem of Calculus at a glance

From hypotheses to conclusion

A mathematical landmark

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

What has been checked

No new theorem is claimed

Where the theorem comes from