TheoremStatement: AI-adaptedProof: 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.

A conditional binomial error bound for Parareal

Statement

Let $x_{n + 1} = F_{n} (x_{n})$ be the sequential fine trajectory and let $U_{n}^{k}$ be the exact-arithmetic table from Finite-budget Parareal correction sweeps. Let $D \subseteq X$ contain every $x_{n}$ and every iterate used in the requested sweeps. Suppose constants $a, b, M \geq 0$ satisfy, for every $0 \leq n < N$ and $u, v \in D$ , $∥ G_{n} (u) - G_{n} (v) ∥ \leq a ∥ u - v ∥, ∥ (F_{n} - G_{n}) (u) - (F_{n} - G_{n}) (v) ∥ \leq b ∥ u - v ∥,$ and $∥ U_{n}^{0} - x_{n} ∥ \leq M$ for all $0 \leq n \leq N$ . Use $(\binom{n}{k})$ for the number of $k$ -element subsets of an $n$ -element set, set it to $0$ for $k > n$ , and put $A = \max {1, a}$ . Then for every node $0 \leq n \leq N$ and completed sweep $k \geq 0$ , $∥ U_{n}^{k} - x_{n} ∥ \leq M (\binom{n}{k}) A^{n} b^{k},$ with $b^{0} = 1$ . The hypotheses include all comparison points; invariance of $D$ under $F_{n}, G_{n}$ alone does not ensure that corrected iterates stay in $D$ .

For a fixed horizon $T = N H$ , suppose $a \leq 1 + C_{a} H$ , $b \leq C_{b} H^{q + 1}$ for constants $C_{a}, C_{b} \geq 0$ and integer $q \geq 1$ , and one $M$ works uniformly as $N$ varies. Then, for each fixed $k \leq N$ , $∥ U_{N}^{k} - x_{N} ∥ \leq M (C_{b} T)^{k} \exp (C_{a} T) H^{q k} .$ Thus the exact-solve error is $O (H^{q k})$ at each fixed iteration $k$ under these uniform assumptions. Neither estimate includes finite-solver error; that effect requires a separate update-defect analysis.

Facts & Assumptions

Given: The exact Parareal recurrence, its sequential fine trajectory, a common comparison set, and the stated Lipschitz and initial-error bounds.

[F1]

Fine and coarse propagators on a common macro grid: the sequential fine trajectory is $x_{n + 1} = F_{n} (x_{n})$ from $x_{0}$ .

[F2]

Finite-budget Parareal correction sweeps: $U_{0}^{k} = x_{0}$ and $U_{n + 1}^{k + 1} = G_{n} (U_{n}^{k + 1}) + F_{n} (U_{n}^{k}) - G_{n} (U_{n}^{k})$ .

[F3]

A norm on a real vector space, the induced metric, and the dictionary with the metric axioms: the norm satisfies $∥ u + v ∥ \leq ∥ u ∥ + ∥ v ∥$ .

[F4]

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

[F5]

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

[F6]

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

[A1]

All fine and coarse evaluations are exact and defined, all comparison points lie in $D$ , the two Lipschitz inequalities hold on $D$ , and the coarse initial-row errors are at most $M$ .

[A2]

In the fixed-horizon branch, $H = T / N$ , $T > 0$ , $a \leq 1 + C_{a} H$ , $b \leq C_{b} H^{q + 1}$ , $q \geq 1$ , and the envelope $M$ is independent of $N$ .

Proof

1.1givenF1F2F3A1algebra

Put $e_{n}^{k} = U_{n}^{k} - x_{n}$ . Subtract $x_{n + 1} = F_{n} (x_{n})$ from the recurrence in [F2] and add and subtract $G_{n} (x_{n})$ ; this gives $e_{n + 1}^{k + 1} = G_{n} (U_{n}^{k + 1}) - G_{n} (x_{n}) + (F_{n} - G_{n}) (U_{n}^{k}) - (F_{n} - G_{n}) (x_{n})$ . By [A1] and the triangle inequality in [F3], $E_{n + 1}^{k + 1} \leq a E_{n}^{k + 1} + b E_{n}^{k}$ , where $E_{n}^{k} = ∥ e_{n}^{k} ∥$ .

1.2F2A1induction

At node $0$ , $E_{0}^{k} = 0$ for every $k$ by [F2]. At sweep $k = 0$ , [A1] gives $E_{n}^{0} \leq M \leq M A^{n}$ . These are the initial cases for induction on the node, simultaneously over all completed sweeps.

2.1step 1.1step 1.2A1inductionalgebra

Assume the bound holds at node $n$ . For the level-zero row at node $n + 1$ , [A1] gives $E_{n + 1}^{0} \leq M \leq M A^{n + 1}$ . For each $k \geq 0$ , [step 1.1] gives $E_{n + 1}^{k + 1} \leq M A^{n} b^{k + 1} (a (\binom{n}{k + 1}) + (\binom{n}{k})) \leq M A^{n + 1} b^{k + 1} ((\binom{n}{k + 1}) + (\binom{n}{k}))$ . The last inequality uses $a \leq A$ and $1 \leq A$ . Partitioning the $(k + 1)$ -element subsets of an $(n + 1)$ -element set according to whether they contain its final element gives $(\binom{n}{k + 1}) + (\binom{n}{k}) = (\binom{n + 1}{k + 1})$ , including the zero convention. Thus the bound holds at node $n + 1$ , and induction proves the first estimate.

3.1A2F4F5F6step 2.1constructalgebra∎

In the fixed-horizon branch, $A \leq 1 + C_{a} H \leq \exp (C_{a} H)$ by [A2], [F4], and the definition of $\exp$ in [F6]. Repeated use of [F5] gives $A^{N} \leq \exp (C_{a} N H) = \exp (C_{a} T)$ . Each $k$ -element subset of an $N$ -element set has a unique increasing $k$ -tuple, so $(\binom{N}{k}) \leq N^{k}$ . Substituting these bounds and $b \leq C_{b} H^{q + 1}$ into the first estimate gives $∥ U_{N}^{k} - x_{N} ∥ \leq M N^{k} \exp (C_{a} T) (C_{b} H^{q + 1})^{k} = M (C_{b} T)^{k} \exp (C_{a} T) H^{q k}$ . For fixed $T, k$ and uniform $M$ , this is $O (H^{q k})$ .

Depends on

Used by

Dependency tree · two levels

38 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

Martin J. Gander, 50 Years of Time Parallel Time Integration (standard reference, not scraped)
Martin J. Gander, Time Parallel Time Integration, Chapter 2: Methods Based on Multiple Shooting (standard reference, not scraped)
Ben S. Southworth, Necessary Conditions and Tight Two-Level Convergence Bounds for Parareal and Multigrid Reduction in Time (standard reference, not scraped)