Fundamental Theorem of Calculus · Landmark Theorems in Mathlib

8 min read Original article ↗

Existing in Mathlib · Analysis

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.

Oriented integration of the derivative recovers the endpoint change, with every analytic hypothesis and the reversed-endpoint behavior kept visible. Explanatory diagram.
Detailed visual description

The endpoint-difference equation dominates the upper poster. A ribbon carries accumulation from a to b and a smaller reversed copy shows the sign reversal. A hypothesis strip names completeness, the unordered closed interval differentiability condition, and interval integrability before a reading guide and exact-scope footer.

Statement structure

Statement and scope

Statement map for Fundamental Theorem of CalculusUnder differentiability and integrability hypotheses, the oriented interval integral of a derivative equals the endpoint difference. Claim boundary: 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. The pinned upstream declaration is intervalIntegral.integral_deriv_eq_sub. The complete formal statement is available in the Exact Mathlib statement section.Mathematical readingUnder differentiabilityand integrabilityhypotheses, the orientedinterval integral of aderivative equals theendpoint difference.Claim boundaryThis page presentsMathlib'sendpoint-difference formover the unorderedclosed interval Set.uIcca b with an orientedinterval integral. Itrequires pointwisedifferentiability thereand IntervalIntegrable(deriv f); it is notevery formulation of theFundamental Theorem ofCalculus.Pinned declarationmathlib ·intervalIntegral.integral_deriv_eq_subStatement map for Fundamental Theorem of CalculusUnder differentiability and integrability hypotheses, the oriented interval integral of a derivative equals the endpoint difference. Claim boundary: 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. The pinned upstream declaration is intervalIntegral.integral_deriv_eq_sub. The complete formal statement is available in the Exact Mathlib statement section.Mathematical readingUnder differentiabilityand integrabilityhypotheses, the orientedinterval integral of aderivative equals theendpoint difference.Claim boundaryThis page presentsMathlib'sendpoint-difference formover the unorderedclosed interval Set.uIcca b with an orientedinterval integral. Itrequires pointwisedifferentiability thereand IntervalIntegrable(deriv f); it is notevery formulation of theFundamental Theorem ofCalculus.Pinned declarationmathlib ·intervalIntegral.integral_deriv_eq_sub

Read the exact Mathlib declaration

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

For f(t)=t² on [0,2], integrating f′(t)=2t gives 4=f(2)−f(0). Explanatory scientific diagram.
Detailed visual description

The scientific schematic gives one explicit instance of the endpoint-difference theorem: the derivative 2t accumulates from 0 to 2 to the same value as the change in t².

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.

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

    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.

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

    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.

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

    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.

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

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

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

    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.

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

    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.

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

    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.

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

    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