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.

A posteriori ODE error bound from the continuous residual

Statement

Assume the Axioms of Countable Choice and Dependent Choice. Let $d \geq 1$ and $a < b$ , let $D \subseteq R \times R^{d}$ be open, let $f : D \to R^{d}$ be continuous, and let $y : [a, b] \to R^{d}$ be an exact solution of $y^{'} = f (t, y)$ whose graph lies in $D$ . Let $U : [a, b] \to R^{d}$ be componentwise absolutely continuous with graph in $D$ . Suppose $ℓ, ρ \in L^{1} [a, b]$ , $ρ \geq 0$ almost everywhere, and, for almost every $t$ , the points $U (t), y (t)$ satisfy

⟨ U (t) - y (t), f (t, U (t)) - f (t, y (t)) ⟩ \leq ℓ (t) ∥ U (t) - y (t) ∥_{2}^{2} .

Define $r (t) : = U^{'} (t) - f (t, U (t))$ wherever $U^{'}$ exists, and assume $∥ r (t) ∥_{2} \leq ρ (t)$ almost everywhere. Then, for every $t \in [a, b]$ ,

∥ U (t) - y (t) ∥_{2} \leq \exp ⁣ (\int_{a}^{t} ℓ (v) d v) ∥ U (a) - y (a) ∥_{2} + \int_{a}^{t} \exp ⁣ (\int_{s}^{t} ℓ (v) d v) ρ (s) d s .

The bound is a posteriori: it uses the residual of the actual reconstruction. An embedded Runge–Kutta difference alone does not supply the hypothesis $∥ r (t) ∥_{2} \leq ρ (t)$ .

Facts & Assumptions

Given: The domain, exact solution, reconstruction, integrable coefficient and residual bound in the Statement, and Countable Choice plus Dependent Choice.

[A1]

The Axiom of Countable Choice ( ${A C}_{ω}$ ) and The axiom of dependent choice: a relation in which every element is related to something admits an $N$ -indexed chain: the proof assumes both axioms only when applying the library's fundamental theorem for absolutely continuous functions.

[A2]

For almost every $t$ , $⟨ U (t) - y (t), f (t, U (t)) - f (t, y (t)) ⟩ \leq ℓ (t) ∥ U (t) - y (t) ∥_{2}^{2}$ .

[A3]

$r (t) = U^{'} (t) - f (t, U (t))$ satisfies $∥ r (t) ∥_{2} \leq ρ (t)$ almost everywhere, with $ℓ, ρ \in L^{1} [a, b]$ and $ρ \geq 0$ almost everywhere.

[L1]

The class $L^{1} (μ)$ of integrable functions and Integrable real and complex functions, and their integrals: $g \in L^{1} [a, b]$ means that $g$ is measurable and $\int_{a}^{b} ∣ g ∣ < \infty$ ; the measure is Lebesgue measure restricted to $[a, b]$ .

[F1]

Absolute continuity on a compact interval: absolute continuity on $[a, b]$ is the finite disjoint-interval increment condition.

[F2]

First-order systems, initial value problems, and solutions on intervals: a solution remains in the open time-state domain and satisfies $y^{'} = f (t, y)$ .

[F3]

Fundamental theorem of calculus for absolutely continuous functions: under Countable Choice and Dependent Choice, an absolutely continuous real function has integrable derivative almost everywhere and equals its initial value plus the integral of that derivative.

[F4]

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 norm satisfies the triangle inequality and $∣ ⟨ x, z ⟩ ∣ \leq ∥ x ∥_{2} ∥ z ∥_{2}$ .

[F5]

The indefinite integral of an $L^{1}$ function is absolutely continuous and The indefinite integral of an $L^{1}$ function is differentiable almost everywhere: if $g \in L^{1}$ , then its indefinite integral is absolutely continuous and has derivative $g$ almost everywhere.

[F6]

A Lipschitz function after an absolutely continuous function is absolutely continuous and The product of two absolutely continuous functions is absolutely continuous: Lipschitz composition and products preserve absolute continuity.

[F7]

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$ : at points of differentiability, the ordinary chain and product rules hold.

[F8]

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

[F9]

The mean value theorem, as the case $g (x) = x$ of Cauchy's: for $f$ continuous on $[a, b]$ with $a < b$ and differentiable on $(a, b)$ there is $c \in (a, b)$ with $f (b) - f (a) = f^{'} (c) (b - a)$ : a differentiable scalar function with derivative bounded in absolute value by $M$ on an interval is $M$ -Lipschitz there.

[F10]

The modulus of an integral is bounded by the integral of the modulus: for $g \in L^{1}$ , $∣ \int g ∣ \leq \int ∣ g ∣$ .

[F11]

Monotonicity and nonnegative homogeneity of the nonnegative integral: the nonnegative Lebesgue integral is monotone and homogeneous for nonnegative finite scalars.

[F12]

Arithmetic and lattice operations preserve measurability whenever they are defined: sums, scalar multiples, products and absolute values of measurable real-valued functions are measurable.

[F13]

The Lebesgue integral is linear on $L^{1} (μ)$ and Two integrable functions are equal almost everywhere exactly when all of their indefinite integrals agree: the Lebesgue integral is linear on $L^{1}$ and is unchanged by almost-everywhere modification.

[F14]

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

Proof

1.1givenF1F4F14algebra

Put $e : = U - y$ and $q (t) : = ∥ e (t) ∥_{2}$ . Each component $e_{i}$ is absolutely continuous by [F1]. Given $ϵ > 0$ , choose for each of the finitely many components a positive interval-length threshold that makes the sum of its increments less than $ϵ / d$ ; the minimum of these finitely many thresholds works for all components at once. For any finite disjoint interval family with total length below that minimum, [F4] gives $∣ q (v) - q (u) ∣ \leq ∥ e (v) - e (u) ∥_{2} \leq \sum_{i} ∣ e_{i} (v) - e_{i} (u) ∣$ , so the total increments of $q$ are below $ϵ$ . Thus $q$ is absolutely continuous by [F1].

2.1givenA1A2A3F2F3F4F14step 1.1algebra

By [F3], $q$ and each component of $e$ are differentiable almost everywhere; the finite intersection of these full-measure sets is still full measure. At such a point with $q > 0$ , differentiating $q^{2} = ⟨ e, e ⟩$ using [F14] gives $2 q q^{'} = 2 ⟨ e, e^{'} ⟩$ , hence $q^{'} = ⟨ e, e^{'} ⟩ / q$ . Since $e^{'} = r + f (t, U) - f (t, y)$ , [A2], [A3], and [F4] imply $q^{'} \leq ℓ q + ρ$ . At a differentiability point where $q = 0$ , the nonnegative function $q$ has a local minimum, so $q^{'} = 0$ and the same inequality holds.

3.1givenA1L1F5F6F7F8F9F10F11step 2.1algebra

Define $Λ (t) : = \int_{a}^{t} ℓ (v) d v$ and $w (t) : = \exp (- Λ (t))$ . By [F5], $Λ$ is absolutely continuous and $Λ^{'} = ℓ$ almost everywhere. [F10] and [F11] give $∣ Λ (t) ∣ \leq \int_{a}^{b} ∣ ℓ (v) ∣ d v = : M$ , and $∣ \frac{d}{d x} \exp (- x) ∣ = \exp (- x) \leq \exp (M)$ on $[- M, M]$ , so [F8] and [F9] make $x \mapsto \exp (- x)$ Lipschitz there. By [F6], $w$ and $w q$ are absolutely continuous. At almost every point, [F7]–[F8] give $(w q)^{'} = w (q^{'} - ℓ q) \leq w ρ$ .

4.1A1L1F3F11F12F13step 3.1algebra

The product $w ρ$ is measurable by [F12], and $∣ w ρ ∣ \leq \exp (M) ρ$ almost everywhere. Since $ρ \geq 0$ almost everywhere and $\int_{a}^{b} ρ < \infty$ , [F11] implies $\int_{a}^{b} ∣ w ρ ∣ < \infty$ ; [L1] gives $w ρ \in L^{1}$ . By [F3], $(w q)^{'} \in L^{1}$ , so $h : = w ρ - (w q)^{'}$ is in $L^{1}$ by [F13]. Step 3.1 says $h \geq 0$ almost everywhere. Since $0 \leq h^{+} \leq ∣ h ∣$ almost everywhere, [F11] and $h \in L^{1}$ give $\int_{a}^{b} h^{+} < \infty$ ; measurability follows from [F12], so [L1] gives $h^{+} \in L^{1}$ . Thus $h = h^{+}$ almost everywhere; [F13] gives $\int_{a}^{t} h = \int_{a}^{t} h^{+}$ , and [F11] gives $\int_{a}^{t} h^{+} \geq 0$ . Hence $\int_{a}^{t} (w q)^{'} \leq \int_{a}^{t} w ρ$ .

5.1A1F3F8step 4.1algebra∎

Apply [F3] to $w q$ on $[a, t]$ , and use $w (a) = 1$ and $w (t) > 0$ from [F8]. Step 4.1 gives $q (t) \leq \exp (Λ (t)) q (a) + \int_{a}^{t} \exp (Λ (t) - Λ (s)) ρ (s) d s$ . Substituting the definition of $Λ$ gives the asserted bound.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

95 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), 1–48 (standard reference, not scraped)
Ernst Hairer, course notes, Chapter III: Équations Différentielles Ordinaires (standard reference, not scraped)
Tobin A. Driscoll and Richard J. Braun, Fundamentals of Numerical Computation, Chapter 6, Adaptive Runge–Kutta (standard reference, not scraped)