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 exponential function is smooth and
Statement
The real exponential function is , and for every , In particular .
Facts & Assumptions
Given: The exponential power series.
A real power series may be differentiated termwise inside its radius (Inside its radius a real power series may be differentiated term by term, and the differentiated series has the same radius), and its sum is smooth there (A power-series sum is infinitely differentiable inside its radius and satisfies at its centre).
The radius is infinite, , and the canonical embedding preserves products and sends positive naturals to nonzero reals (The exponential series converges absolutely for every real argument, The factorial and the falling factorial , defined by recursion in , The canonical natural of a field, Canonical naturals are positive and strictly increasing).
Proof
Termwise differentiation gives .
Reindex and cancel using the factorial recurrence. The series becomes .
Smoothness follows from [L1] and the infinite radius; iterating step 2.1 gives every higher derivative.
Depends on
- The exponential series converges absolutely for every real argument
- Inside its radius a real power series may be differentiated term by term, and the differentiated series has the same radius
- A power-series sum is infinitely differentiable inside its radius and satisfies $a_n=f^{(n)}(c)/\iota(n!)$ at its centre
- 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 exponential is not uniformly continuous on ℝ Counterexample
- A nonzero smooth compactly supported bump Example
- Fubini computes ∫₀¹∫₋₁¹ xexp(xy) dx dy by reversing the order Example
- The one-sided flat function is C^∞ with identically zero Taylor series Example
- Addition formulas, identities, parity, and derivatives of the hyperbolic functions Theorem
- Continuity and derivatives of positive-base real powers Theorem
- Landau's root limit: log x is the limit of 2ⁿ times (x^(1/2ⁿ) minus 1) Theorem
- Regular normalized multiplicative Cauchy equations characterize the exponential Theorem
- The exponential function is strictly increasing Theorem
- The exponential is the unique solution of y'=y with y(0)=1 Theorem
- The natural logarithm has derivative 1/x and equals the integral from 1 to x of 1/t Theorem
- The power-series, product-limit, IVP, functional-equation, and Picard definitions agree Theorem
- The two-point convexity inequality for the exponential function Theorem
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 97 results over 16 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)
- J. K. Hunter, An Introduction to Real Analysis, Chapter 10 (standard reference, not scraped)
- J. Lebl, Basic Analysis, Analytic Functions (standard reference, not scraped)