TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 2026-08-01

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.

Picard iteration from $1$ produces the exponential partial sums

Statement

Define $u_{0} (x) = 1$ and $u_{r + 1} (x) = 1 + \int_{0}^{x} u_{r} (t) d t$ . Then $u_{r} (x) = \sum_{k = 0}^{r} \frac{x^{k}}{ι (k!)}$ and $u_{r} \to \exp$ uniformly on every bounded interval. Moreover, $\exp (x) = 1 + \int_{0}^{x} \exp (t) d t,$ and differentiating this integral equation recovers $\exp^{'} = \exp$ and $\exp (0) = 1$ .

Facts & Assumptions

Given: The displayed recursion with the oriented integral of The integral with oriented limits: $\int_{a}^{a} f : = 0$ and $\int_{b}^{a} f : = - \int_{a}^{b} f$ .

[L1]

For $k \in N$ , the derivative of $t^{k + 1} / ι (k + 1)$ is $t^{k}$ (For a natural $n \geq 1$ the function $x \mapsto x^{n}$ is differentiable everywhere with derivative $ι (n) x^{n - 1}$ ; for $n = 0$ it is the constant $1$ , with derivative $0$ ; for a natural $n \geq 1$ the function $x \mapsto x^{- n}$ is differentiable at every $x \neq 0$ with derivative $- ι (n) x^{- n - 1}$ ; consequently every polynomial function is differentiable at every real, with the derivative computed term by term), so the second fundamental theorem evaluates its oriented integral (The second fundamental theorem: if $G$ is differentiable on $[a, b]$ with $G^{'} = f$ and $f$ is integrable, then $\int_{a}^{b} f = G (b) - G (a)$ , The integral with oriented limits: $\int_{a}^{a} f : = 0$ and $\int_{b}^{a} f : = - \int_{a}^{b} f$ ); the integral is linear over finite sums (Integrable functions on $[a, b]$ form a set closed under sums and scalar multiples, and $\int_{a}^{b} (λ f + μ g) = λ \int_{a}^{b} f + μ \int_{a}^{b} g$ ), and the factorial recurrence is The factorial $n!$ and the falling factorial $n^{\underline{k}}$ , defined by recursion in $N$ .

[L2]

The exponential series has infinite radius (The exponential series converges absolutely for every real argument, The real exponential function and the number $e$ by a power series), and a power series converges uniformly on compact subintervals of its interval of convergence (A power series converges absolutely and uniformly on every closed interval strictly inside its interval of convergence).

[L3]

Polynomial functions are continuous (Sums, scalar multiples, products, absolute values, maxima, minima and quotients with nonvanishing denominator of continuous functions are continuous, as are constants, the identity and every polynomial function); uniform limits of continuous real functions are continuous (The uniform limit of continuous real-valued functions on a metric space is continuous); continuous functions on compact intervals are integrable (A continuous function on $[a, b]$ is Riemann integrable, by Heine-Cantor and Riemann's criterion); uniform limits interchange with Riemann integration (A uniform limit of Riemann-integrable functions is Riemann integrable, and its integral is the limit of their integrals); and the first fundamental theorem differentiates an integral of a continuous function (The first fundamental theorem: if $f$ is integrable on $[a, b]$ and continuous at $c$ , then $F^{'} (c) = f (c)$ ; in particular a continuous $f$ has $F$ as a primitive).

Proof

technique · induction

1.1

At $r = 0$ , $u_{0} = 1$ , the stated finite sum.

basegiven

1.2

If the formula holds at $r$ , integrate its finite sum termwise from $0$ to $x$ . By [L1], the integral of $t^{k} / ι (k!)$ is $x^{k + 1} / ι ((k + 1)!)$ , giving the formula at $r + 1$ .

ihL1given

2.1

Hence the iterates are precisely the partial sums of the exponential series. Its infinite radius and [L2] give uniform convergence on every bounded interval.

step 1.1step 1.2L2given

3.1

Fix $x$ and work on the compact interval with endpoints $0$ and $x$ . The polynomial iterates are continuous and integrable there, and step 2.1 gives uniform convergence to $\exp$ . Thus [L3] lets the integrals in $u_{r + 1} (x) = 1 + \int_{0}^{x} u_{r} (t) d t$ pass to the limit, giving $\exp (x) = 1 + \int_{0}^{x} \exp (t) d t$ , with the orientation supplied by The integral with oriented limits: $\int_{a}^{a} f : = 0$ and $\int_{b}^{a} f : = - \int_{a}^{b} f$ when $x < 0$ .

step 2.1L3given

4.1

Step 2.1 and [L3] make $\exp$ continuous. The first fundamental theorem applied to step 3.1 gives $\exp^{'} (x) = \exp (x)$ , and setting $x = 0$ gives $\exp (0) = 1$ .

step 2.1step 3.1L3discharge-induction∎

Depends on

Used by

Dependency tree · two levels

96 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 full lecture notes (standard reference, not scraped)
J. Lebl, Basic Analysis, Analytic Functions (standard reference, not scraped)
J. Lebl, Basic Analysis, Picard's Theorem (standard reference, not scraped)
University of Pennsylvania MATH 3600, Section 34 (standard reference, not scraped)

Picard iteration from 11 produces the exponential partial sums