How 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.
A uniform derivative bound gives a uniform Taylor remainder bound
Statement
Let , and suppose has derivatives through order on the closed interval between and , with the usual endpoint continuity. If throughout that interval, then
Facts & Assumptions
Given: The stated regularity and derivative bound.
The Lagrange remainder formula is The Lagrange and Cauchy forms of Taylor's remainder.
Absolute value respects products and powers (Basic properties of the absolute value), and factorials are positive (The factorial and the falling factorial , defined by recursion in , Canonical naturals are positive and strictly increasing, The canonical natural of a field).
Proof
If , then , so the estimate is immediate. If , [L1] gives for some point strictly between and .
In the case , take absolute values in step 1.1, use , and divide by the positive factorial. Together with the case , this proves the estimate.
Depends on
- The Lagrange and Cauchy forms of Taylor's remainder
- Basic properties of the absolute value
- The factorial $n!$ and the falling factorial $n^{\underline{k}}$, defined by recursion in $\mathbb{N}$
- The canonical natural $\iota(n) = n \cdot 1_F$ of a field
- Canonical naturals are positive and strictly increasing
Used by
- The Taylor polynomial of (1-x)⁻¹ at 0 has the exact geometric remainder xⁿ⁺¹/(1-x) Example
- Characteristic exponential for a continuous local martingale with deterministic clock Lemma
- Second-order characteristic-function expansion Lemma
- Multidimensional Ito formula for Brownian-driven processes Theorem
- One-dimensional Ito formula Theorem
- Taylor-series representation by vanishing remainders Theorem
Dependency tree · two levels
28 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
- MIT OpenCourseWare 18.100B Real Analysis, Spring 2025 lecture notes (standard reference, not scraped)
- Taylor's theorem (Wikipedia): Lagrange remainder and error estimate (standard reference, not scraped)