LemmaStatement: Literature-sourcedProof: AI-generatedPipeline-generatedjudge pass (gpt-6-luna)

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.

Finite geometric error bound from a one-step recurrence

Statement

Let $T > 0$ , $N \in N$ with $N \geq 1$ , $h = T / N > 0$ , $p \in R$ with $p \geq 1$ , and $C_{0}, C, L \geq 0$ . Real powers of the positive base $h$ are as in Real powers for positive bases, with the zero-base positive-exponent convention. If nonnegative real numbers $e_{0}, \dots, e_{N}$ satisfy $e_{0} \leq C_{0} h^{p}, e_{n + 1} \leq (1 + L h) e_{n} + C h^{p + 1} (0 \leq n < N),$ then, when $L > 0$ , $\max_{0 \leq n \leq N} e_{n} \leq (C_{0} \exp (L T) + C \frac{\exp (L T) - 1}{L}) h^{p},$ and, when $L = 0$ , $\max_{0 \leq n \leq N} e_{n} \leq (C_{0} + C T) h^{p} .$

Facts & Assumptions

Given: The constants, step size, and nonnegative error sequence in the Statement.

[A1]

$T > 0$ , $N \geq 1$ , $h = T / N$ , $p \geq 1$ , $C_{0}, C, L \geq 0$ , and the stated initial and recurrence inequalities hold.

[F1]

The real exponential is $\exp (x) = \sum_{n = 0}^{\infty} x^{n} / n!$ , with $e : = \exp (1)$ and $\exp (0) = 1$ (The real exponential function and the number $e$ by a power series).

[F2]

For every real $x$ , $1 + x \leq \exp (x)$ ( $1 + x \leq \exp (x)$ for every real $x$ , hence $(1 - p)^{m} \leq \exp (- m p)$ ).

[F3]

If $0 \leq a \leq b$ , then $a^{n} \leq b^{n}$ for every natural $n$ (Monotonicity of $x \mapsto x^{n}$ and of $n \mapsto a^{n}$ ); natural powers satisfy $a^{0} = 1$ and $a^{n + 1} = a^{n} a$ (Integer powers $a^{m}$ ).

[F4]

$\exp (x + y) = \exp (x) \exp (y)$ for real $x, y$ (The exponential addition formula $\exp (x + y) = \exp (x) \exp (y)$ ).

[F5]

The real exponential is strictly increasing (The exponential function is strictly increasing).

[F6]

Finite sums satisfy additivity and scaling (Laws of finite sums and finite products, Finite sums and finite products, by recursion).

[F7]

Finite sums telescope as $\sum_{j < n} (c_{j + 1} - c_{j}) = c_{n} - c_{0}$ (Laws of finite sums and finite products).

[F8]

For $h > 0$ and $p \in R$ , $h^{p + 1} = h^{p} h$ : The exponent, product, quotient, and iterated-power laws for positive real bases and real exponents gives $h^{p + 1} = h^{p} h^{1}$ , and Real powers for positive bases, with the zero-base positive-exponent convention and The natural logarithm as the inverse of the exponential function give $h^{1} = \exp (\log h) = h$ .

Proof

1.1A1inductionalgebra

Put $a : = 1 + L h$ and $b : = C h^{p + 1}$ . By induction on $n$ , the recurrence gives $e_{n} \leq a^{n} e_{0} + b \sum_{j = 0}^{n - 1} a^{j}$ for $0 \leq n \leq N$ : the sum is empty at $n = 0$ , where the bound is equality in the first term, and substituting the bound at $n$ into $e_{n + 1} \leq a e_{n} + b$ appends the term $b a^{n}$ .

2.1A1F1F2F3F4F5F6F7F8step 1.1algebra∎

If $L > 0$ , then $a - 1 = L h$ and [F6, F7] give $(a - 1) \sum_{j < n} a^{j} = \sum_{j < n} (a^{j + 1} - a^{j}) = a^{n} - 1$ , so $\sum_{j < n} a^{j} = (a^{n} - 1) / (L h)$ . By [F2], $a = 1 + L h \leq \exp (L h)$ . If $n = 0$ then $a^{n} = \exp (L h)^{n} = 1$ ; if $n \geq 1$ , [F3] gives $a^{n} \leq \exp (L h)^{n}$ . Induction using [F1] and [F4] gives $\exp (L h)^{n} = \exp (n L h)$ for every natural $n$ . Since $n \leq N$ , $n L h \leq L T$ , and [F5] gives $a^{n} \leq \exp (L T)$ . Substitution in step 1.1, using [F8] to simplify the real-power factor, yields $e_{n} \leq (C_{0} \exp (L T) + C \frac{\exp (L T) - 1}{L}) h^{p}$ . If $L = 0$ , then $a = 1$ and step 1.1 gives $e_{n} \leq C_{0} h^{p} + n C h^{p + 1} = C_{0} h^{p} + C h^{p} (n h) \leq (C_{0} + C T) h^{p}$ by [F8], because $n \leq N$ and $N h = T$ . Taking the maximum proves both cases.

Depends on

Used by

Dependency tree · two levels

50 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

Ernst Hairer and Gerhard Wanner, Introduction à l’Analyse Numérique, Chapter III: Équations Différentielles Ordinaires (standard reference, not scraped)
Mark Embree, Lecture Notes on Numerical Analysis (standard reference, not scraped)