Alphabeta MathHow statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
Mean value theorem on a closed real interval
Statement
Let be continuous on and differentiable on , with . Then there is such that
Facts & Assumptions
Given: A field satisfying Dedekind-complete ordered real field, real endpoints , and continuous on and differentiable on as defined in Continuity and derivative on a real interval.
Continuity and derivative on a real interval: continuity is the relative epsilon-delta condition; differentiability is existence of the finite two-sided difference-quotient limit.
Rolle's theorem from attained extrema: a continuous function on differentiable on with equal endpoint values has an interior point with derivative zero.
Proof
Let and define . The function is continuous on and differentiable on by [F1], and . Applying [L1] gives with .
Differentiating the displayed affine expression gives . Thus ; multiplying by proves the identity.
Depends on
Used by
- Direct midpoint quadrature loses order on a half-order singularity Example
- A positive far-panel quadrature residual and normalized cluster combination Lemma
- A positive midpoint enclosure for Boys functions on bounded arguments Lemma
- An interval Jacobian encloses a vector mean-value matrix Lemma
- Cartesian Gaussian moments and exponent-parameter derivatives Lemma
- Local quadratic coordinate at a simple stationary point Lemma
- Local stationary expansion for a quadratic phase Lemma
- Range-reduced exponential, logarithm and arctangent series have certified tails Lemma
- Taylor's Lagrange remainder follows from repeated Rolle steps Lemma
- The fundamental theorem of calculus and integration by parts Lemma
- Trigonometric identities, Machin's formula and reduced Taylor tails Lemma
- Weierstrass log-Gamma series converges to a Gamma branch Lemma
- Absolute convergence and local parameter domination for Gaussian basis integrals Theorem
- Boys integral, power series, recurrence, and incomplete-gamma representation Theorem
- Certified real elementary-function evaluations enclose their ranges Theorem
- Floater–Hormann error bounds for a bounded-variation highest derivative Theorem
- Scalar interval Newton exclusion and strict inclusion certificates Theorem
Dependency tree · two levels
4 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.
Sources
- Michael C. Colding, MIT 18.100B Real Analysis, Lecture 16 (standard reference, not scraped)