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.
The Taylor polynomial of at has the exact geometric remainder
Example
For and , whenever .
Facts & Assumptions
Given: The geometric function.
Finite geometric sums follow from Laws of finite sums and finite products. Derivative algebra, the chain rule, and the natural-power derivative give the successive derivatives of ; factorial arithmetic is preserved by the canonical embedding (Sums, scalar multiples, products and quotients: , , , and when , The chain rule, in one line from Carathéodory: if is differentiable at and is differentiable at , then is differentiable at with , For a natural the function is differentiable everywhere with derivative ; for it is the constant , with derivative ; for a natural the function is differentiable at every with derivative ; consequently every polynomial function is differentiable at every real, with the derivative computed term by term, The factorial and the falling factorial , defined by recursion in , The canonical natural of a field, Canonical naturals are positive and strictly increasing), and induction is The principle of mathematical induction.
The Taylor objects and bound are Taylor polynomials and their remainders and A uniform derivative bound gives a uniform Taylor remainder bound.
Verification
Induction gives , hence .
Multiplying by telescopes to . Subtracting from gives the stated remainder.
This exact expression agrees with the qualitative estimate supplied by [L2] on every closed interval avoiding .
Depends on
- Taylor polynomials and their remainders
- A uniform derivative bound gives a uniform Taylor remainder bound
- Laws of finite sums and finite products
- Sums, scalar multiples, products and quotients: $(f+g)'(c) = f'(c) + g'(c)$, $(\alpha f)'(c) = \alpha f'(c)$, $(fg)'(c) = f'(c)g(c) + f(c)g'(c)$, and $(f/g)'(c) = \bigl(f'(c)g(c) - f(c)g'(c)\bigr)/g(c)^{2}$ when $g(c) \ne 0$
- The chain rule, in one line from Carathéodory: if $g$ is differentiable at $c$ and $f$ is differentiable at $g(c)$, then $f \circ g$ is differentiable at $c$ with $(f \circ g)'(c) = f'(g(c))\,g'(c)$
- For a natural $n \ge 1$ the function $x \mapsto x^{n}$ is differentiable everywhere with derivative $\iota(n)\,x^{\,n-1}$; for $n = 0$ it is the constant $1$, with derivative $0$; for a natural $n \ge 1$ the function $x \mapsto x^{-n}$ is differentiable at every $x \ne 0$ with derivative $-\iota(n)\,x^{-n-1}$; consequently every polynomial function is differentiable at every real, with the derivative computed term by term
- 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
- The principle of mathematical induction
Used by
Nothing in the library uses this result yet.
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 97 results over 27 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.
Sources
- MIT OpenCourseWare 18.100B Real Analysis, Spring 2025 lecture notes (standard reference, not scraped)
- J. Lebl, Basic Analysis I, Taylor's theorem and related calculus (standard reference, not scraped)