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

Choice-free residual error bound for piecewise-C1 ODE reconstructions

Statement

Let $d \geq 1$ and $a < T$ , let $D \subseteq R \times R^{d}$ be open, let $f : D \to R^{d}$ be continuous, and let $y$ be an exact solution of $y^{'} = f (t, y)$ on $[a, T]$ . Let $U : [a, T] \to R^{d}$ be continuous and $C^{1}$ on each member of a finite partition (continuously differentiable on each closed panel, with one-sided endpoint derivatives), with graph in $D$ . Let $ℓ, ρ : [a, T] \to [0, \infty)$ be continuous on each partition interval, with one-sided endpoint values, and suppose on every open panel $⟨ U - y, f (t, U) - f (t, y) ⟩ \leq ℓ (t) ∥ U - y ∥_{2}^{2}, ∥ U^{'} (t) - f (t, U (t)) ∥_{2} \leq ρ (t) .$ Then for every $t \in [a, T]$ , $∥ U (t) - y (t) ∥_{2} \leq e^{\int_{a}^{t} ℓ (v) d v} ∥ U (a) - y (a) ∥_{2} + \int_{a}^{t} e^{\int_{s}^{t} ℓ (v) d v} ρ (s) d s .$ The proof uses only finite-piece ordinary calculus and no choice axiom. The general absolutely continuous case is treated separately.

Facts & Assumptions

Given: The exact solution, reconstruction, finite partition, nonnegative piecewise-continuous coefficient and residual envelope in the Statement.

[F1]

First-order systems, initial value problems, and solutions on intervals: the exact solution is differentiable and satisfies $y^{'} = f (t, y)$ .

[F2]

Cauchy-Schwarz $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥_{2} ∥ y ∥_{2}$ with its equality case, the triangle inequality for $∥ \cdot ∥_{2}$ , the parallelogram law and polarisation: the Euclidean inner product satisfies Cauchy–Schwarz and its norm is nonnegative.

[F3]

The chain rule, in one line from Carathéodory: if $g$ is differentiable at $c$ and $f$ is differentiable at $g (c)$ , then $f \circ g$ is differentiable at $c$ with $(f \circ g)^{'} (c) = f^{'} (g (c)) g^{'} (c)$ and Sums, scalar multiples, products and quotients: $(f + g)^{'} (c) = f^{'} (c) + g^{'} (c)$ , $(α f)^{'} (c) = α f^{'} (c)$ , $(f g)^{'} (c) = f^{'} (c) g (c) + f (c) g^{'} (c)$ , and $(f / g)^{'} (c) = (f^{'} (c) g (c) - f (c) g^{'} (c)) / g (c)^{2}$ when $g (c) \neq 0$ : the chain and product rules apply to differentiable functions.

[F4]

The exponential function is smooth and $(\exp)^{'} = \exp$ and The exponential is positive and satisfies $\exp (- x) = 1 / \exp (x)$ : $e^{x}$ is positive and has derivative $e^{x}$ .

[F5]

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 gives the derivative of the integral of a continuous function. 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)$ gives $g (v) - g (u) = \int_{u}^{v} g^{'} (s) d s$ for $g \in C^{1} [u, v]$ , using one-sided endpoint derivatives.

[F6]

Square roots exist: a unique $\sqrt{a} \geq 0$ with $(\sqrt{a})^{2} = a$ ; the positives are ${x^{2} : x \neq 0}$ , Sums, scalar multiples, products and quotients: $(f + g)^{'} (c) = f^{'} (c) + g^{'} (c)$ , $(α f)^{'} (c) = α f^{'} (c)$ , $(f g)^{'} (c) = f^{'} (c) g (c) + f (c) g^{'} (c)$ , and $(f / g)^{'} (c) = (f^{'} (c) g (c) - f (c) g^{'} (c)) / g (c)^{2}$ when $g (c) \neq 0$ , and Derivative of an inverse: if $f$ is continuous and injective on a nondegenerate interval $I$ and differentiable at $c \in I$ with $f^{'} (c) \neq 0$ , then the inverse $g$ is differentiable at $f (c)$ with $g^{'} (f (c)) = 1 / f^{'} (c)$ ; and if $f^{'} (c) = 0$ then $g$ is not differentiable at $f (c)$ : the positive square root on $(0, \infty)$ is the inverse of $x \mapsto x^{2}$ on $(0, \infty)$ and has derivative $1 / (2 \sqrt{x})$ there.

[F7]

The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ : the Euclidean inner product is symmetric and bilinear, and $∥ e ∥_{2}^{2} = ⟨ e, e ⟩$ .

Proof

1.1givenF1F2F3F6F7algebra

On one open partition panel put $e = U - y$ , $q_{ε} = (∥ e ∥_{2}^{2} + ε^{2})^{1 / 2}$ for $ε > 0$ , and $r = U^{'} - f (t, U)$ . The functions are $C^{1}$ there, so [F3], [F6], and [F7] give $q_{ε}^{'} = ⟨ e, e^{'} ⟩ / q_{ε}$ . Since $e^{'} = r + f (t, U) - f (t, y)$ , the hypotheses and [F2] yield $q_{ε}^{'} \leq ℓ \frac{∥ e ∥_{2}^{2}}{q_{ε}} + ρ \frac{∥ e ∥_{2}}{q_{ε}} \leq ℓ q_{ε} + ρ$ , using $ℓ \geq 0$ , $∥ e ∥_{2} \leq q_{ε}$ , and $∥ e ∥_{2}^{2} \leq q_{ε}^{2}$ .

2.1F3F4F5step 1.1algebra

Let $Λ (t) = \int_{a}^{t} ℓ (v) d v$ and multiply the differential inequality by $e^{- Λ (t)}$ . On each panel, [F3]–[F5] give $(e^{- Λ} q_{ε})^{'} \leq e^{- Λ} ρ$ . Integrate on each full or partial panel and add the finitely many inequalities; continuity at the partition nodes cancels the intermediate endpoint terms. This gives $q_{ε} (t) \leq e^{Λ (t)} q_{ε} (a) + \int_{a}^{t} e^{Λ (t) - Λ (s)} ρ (s) d s$ .

3.1step 2.1algebra∎

Let $ε ↓ 0$ . Since $q_{ε} (t) \to ∥ U (t) - y (t) ∥_{2}$ and $q_{ε} (a) \to ∥ U (a) - y (a) ∥_{2}$ , while the integral term is independent of $ε$ , the inequality in step 2.1 passes to the limit. Replacing $Λ (t) - Λ (s)$ by $\int_{s}^{t} ℓ (v) d v$ gives the claimed estimate.

Depends on

Used by

A validated rational residual-tube certificate encloses an exact ODE solution Theorem

Dependency tree · two levels

70 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

Donald Estep, A Posteriori Error Bounds and Global Error Control for Approximation of Ordinary Differential Equations, SIAM Journal on Numerical Analysis 32 (1995) (standard reference, not scraped)
Ernst Hairer, course notes, Chapter III: Équations Différentielles Ordinaires (standard reference, not scraped)