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.
The real exponential function and the number by a power series
Definition
For , define provided by the all-real convergence proved in The exponential series converges absolutely for every real argument ↗. Here is the factorial of The factorial and the falling factorial , defined by recursion in , is its nonzero real image (The canonical natural of a field, Canonical naturals are positive and strictly increasing), and powers and series are those of Integer powers and Series, partial sums, convergence and the sum, divergence, and the tail series.
This is a real power series centred at (A real power series about a centre, its interval of convergence, and its radius in ). No logarithm, irrational power, or differential equation enters the definition.
Depends on
- A real power series about a centre, its interval of convergence, and its radius in $[0,+\infty]$
- The factorial $n!$ and the falling factorial $n^{\underline{k}}$, defined by recursion in $\mathbb{N}$
- Integer powers $a^m$
- The canonical natural $\iota(n) = n \cdot 1_F$ of a field
- Canonical naturals are positive and strictly increasing
- Series, partial sums, convergence and the sum, divergence, and the tail series
Used by
- The elementary numerical bound 2<e<3 Corollary
- The exponential is positive and satisfies exp(-x)=1/exp(x) Corollary
- Real powers for positive bases, with the zero-base positive-exponent convention Definition
- The six hyperbolic functions and their natural domains Definition
- The log-free product limit (1-2/n)ⁿ→exp(-2) Example
- A geometric bound for tails of the exponential series Lemma
- The exponential series converges absolutely for every real argument Lemma
- exp(z+w)=exp z exp w, and the complex exponential extends the real exponential Theorem
- For every real x, (1+x/n)ⁿ→exp x Theorem
- Picard iteration from 1 produces the exponential partial sums Theorem
- Regular normalized multiplicative Cauchy equations characterize the exponential Theorem
- The exponential dominates every fixed nonnegative integer power at +∞ Theorem
- The exponential is the unique solution of y'=y with y(0)=1 Theorem
- The exponential tends to +∞ at +∞ and to 0 at -∞ Theorem
- The number e is irrational Theorem
- The power-series, product-limit, IVP, functional-equation, and Picard definitions agree Theorem
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 80 results over 15 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 full lecture notes (standard reference, not scraped)
- J. Lebl, Basic Analysis, Logarithm and Exponential (standard reference, not scraped)