TheoremStatement: AI-adaptedProof: AI-adaptedPipeline-generatedprecheck pass

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 square-root global error bound for projected Euler with certified projection tolerances

Statement

Assume the hypotheses of Existence and uniqueness for projected dynamics and convergence of projection Euler under countable and dependent choice, including Countable Choice and Dependent Choice, and let $x$ be its unique solution. Let $D$ be any finite bound for the diameter of $C$ , set $M = ∥ f (0, x_{0}) ∥_{2} + L (T + D), C_{0} = 8 M^{2} + L^{2} (1 + M)^{2} T, K_{e r r} = \sqrt{C_{0} T e^{(2 L + 1) T}} .$ For $h = T / N$ , let $X_{h}$ be the affine interpolant of the exact projection Euler recurrence. If a complete run of Projected Euler with certified inexact projection solves returns nodes ${\tilde{x}}_{k}$ with certified residuals $\sup_{z \in C} ⟨ {\tilde{x}}_{k} + h f (t_{k}, {\tilde{x}}_{k}) - {\tilde{x}}_{k + 1}, z - {\tilde{x}}_{k + 1} ⟩ \leq ε_{k}^{2},$ and ${\tilde{X}}_{h}$ is their affine interpolant, then $\sup_{0 \leq t \leq T} ∥ {\tilde{X}}_{h} (t) - x (t) ∥_{2} \leq K_{e r r} \sqrt{h} + e^{L T} \sum_{k = 0}^{N - 1} ε_{k} .$ In particular, the exact-projection branch has uniform error $O (\sqrt{h})$ . Certified projection errors with $\sum_{k} ε_{k} = O (\sqrt{h})$ retain that rate; no rate follows from an uncertified solver tolerance alone.

Facts & Assumptions

Given: The data, Countable Choice and Dependent Choice assumptions of Existence and uniqueness for projected dynamics and convergence of projection Euler under countable and dependent choice, and a completed inexact projected-Euler run with the residual certificates in the Statement.

[A1]

The Axiom of Countable Choice ( ${A C}_{ω}$ ) is assumed as in [F1] to obtain the exact solution $x$ ; the estimates use no additional countable choices.

[A2]

The axiom of dependent choice: a relation in which every element is related to something admits an $N$ -indexed chain is assumed as in [F1] to obtain the exact solution $x$ ; the estimates use no additional dependent choices.

[F1]

Existence and uniqueness for projected dynamics and convergence of projection Euler under countable and dependent choice: there is a unique absolutely continuous $x$ satisfying $f (t, x) - \dot{x} \in N_{C} (x)$ almost everywhere.

[F2]

The convex normal-cone operator is maximal monotone and its resolvent is projection: $N_{C}$ is monotone.

[F3]

Projection onto a closed convex set is nonexpansive: $P_{C}$ is nonexpansive.

[F4]

A certified projection variational residual bounds the projection error: a feasible candidate with variational residual at most $ε^{2}$ is within distance $ε$ of its exact projection.

[F5]

Projected Euler with certified inexact projection solves: a completed run returns feasible nodes with the residual certificates specified in the algorithm Definition.

[F6]

$C^{1}$ implies Lipschitz, Lipschitz implies absolutely continuous, and absolutely continuous implies continuous and bounded variation and Every function of bounded variation is differentiable almost everywhere: Lipschitz curves are absolutely continuous and differentiable almost everywhere.

[F7]

The product of two absolutely continuous functions is absolutely continuous and Fundamental theorem of calculus for absolutely continuous functions: products of AC components are AC with the product derivative a.e., and the derivative integrates to the endpoint difference.

[F8]

Cauchy-Schwarz $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥_{2} ∥ y ∥_{2}$ with its equality case, the triangle inequality for $∥ \cdot ∥_{2}$ , the parallelogram law and polarisation: $∣ ⟨ a, b ⟩ ∣ \leq ∥ a ∥_{2} ∥ b ∥_{2}$ .

[F9]

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

[F10]

Gronwall's integral inequality with variable and constant coefficients: if $u \geq 0$ is continuous and $u (t) \leq A + \int_{0}^{t} b u$ for constants $A, b \geq 0$ , then $u (t) \leq A e^{b t}$ .

[F11]

Projected contact dynamics and explicit projection Euler step: the outward cone is $N_{C} (x) = {n : ⟨ n, z - x ⟩ \leq 0 for every z \in C}$ , and an exact projection step satisfies $x_{k + 1} = P_{C} (x_{k} + h f (t_{k}, x_{k}))$ .

[F12]

Heine-Borel in $R^{n}$ : with the Euclidean metric a subset of $R^{n}$ is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line: because $d \geq 1$ , compact $C \subseteq R^{d}$ is closed, as well as bounded.

Proof

1.1A1A2F1F3F6F8F11F12givenchoosealgebra

By [F12], compactness makes $C$ closed, so the projection and normal-cone hypotheses in [F11] and [F3] apply to the stated set. Let $X_{h}$ be the exact affine Euler interpolant, ${\overset{ˉ}{X}}_{h} (t) = x_{k + 1}$ on $[t_{k}, t_{k + 1})$ , $F_{h} (t) = f (t_{k}, x_{k})$ , and $n_{h} = F_{h} - {\dot{X}}_{h}$ . The projection variational inequality in [F11] gives $n_{h} (t) \in N_{C} ({\overset{ˉ}{X}}_{h} (t))$ . Nonexpansiveness [F3] gives $∥ {\dot{X}}_{h} ∥_{2} \leq M$ and $∥ {\overset{ˉ}{X}}_{h} - X_{h} ∥_{2} \leq h M$ , so $∥ n_{h} ∥_{2} \leq 2 M$ . For the exact solution put $n (t) = f (t, x (t)) - \dot{x} (t) \in N_{C} (x (t))$ . At almost every differentiability point, $x (t + s) \in C$ on both sides of $t$ ; the normal inequality with $z = x (t + s)$ , divided by positive and negative $s$ and passed to the limit, gives $⟨ n (t), \dot{x} (t) ⟩ = 0$ . Hence $∥ \dot{x} (t) ∥_{2}^{2} = ⟨ f (t, x (t)), \dot{x} (t) ⟩$ , so Cauchy–Schwarz [F8] gives $∥ \dot{x} (t) ∥_{2} \leq M$ and $∥ n (t) ∥_{2} \leq 2 M$ .

1.2F3F4F5F9givenalgebrainduction

By [F4] and [F5], each inexact node is within $ε_{k}$ of the exact projection of its own unprojected input. Comparing it with the exact node and using [F3] and the state-Lipschitz bound gives $∥ {\tilde{x}}_{k + 1} - x_{k + 1} ∥_{2} \leq (1 + h L) ∥ {\tilde{x}}_{k} - x_{k} ∥_{2} + ε_{k} .$ Iteration from the common initial point yields $\max_{k} ∥ {\tilde{x}}_{k} - x_{k} ∥_{2} \leq (1 + h L)^{N} \sum_{k} ε_{k}$ . By [F9], $(1 + h L)^{N} \leq e^{N h L} = e^{L T}$ .

2.1F1F2F6F7F8step 1.1givenalgebra

Put $e_{h} = X_{h} - x$ and $E_{h} = ∥ e_{h} ∥_{2}^{2}$ . By [F6]–[F7], $E_{h}$ is absolutely continuous and $E_{h}^{'} = 2 ⟨ {\dot{X}}_{h} - \dot{x}, e_{h} ⟩$ almost everywhere. Monotonicity [F2] at ${\overset{ˉ}{X}}_{h}$ and $x$ gives $⟨ n_{h} - n, {\overset{ˉ}{X}}_{h} - x ⟩ \geq 0$ . Since $∥ {\overset{ˉ}{X}}_{h} - X_{h} ∥_{2} \leq h M$ and $∥ n_{h} - n ∥_{2} \leq 4 M$ , differentiation yields $\frac{1}{2} E_{h}^{'} \leq L E_{h} + L h (1 + M) \sqrt{E_{h}} + 4 M^{2} h .$ Indeed, $∥ F_{h} - f (t, x) ∥_{2} \leq L (h + ∥ x_{k} - x (t) ∥_{2}) \leq L (∥ e_{h} ∥_{2} + h (1 + M))$ using the within-step displacement bound; [F8] bounds its inner product with $e_{h}$ .

3.1F7F10step 2.1givenalgebra

Since $(\sqrt{E_{h}} - L h (1 + M))^{2} \geq 0$ , we have $L h (1 + M) \sqrt{E_{h}} \leq \frac{1}{2} E_{h} + \frac{1}{2} L^{2} (1 + M)^{2} h^{2}$ . Thus $E_{h}^{'} \leq (2 L + 1) E_{h} + 8 M^{2} h + L^{2} (1 + M)^{2} h^{2} \leq (2 L + 1) E_{h} + C_{0} h,$ since $h \leq T$ . Integrating the inequality and using $E_{h} (0) = 0$ gives $E_{h} (t) \leq C_{0} h T + (2 L + 1) \int_{0}^{t} E_{h} (s) d s$ . By [F10], $\sup_{t} E_{h} (t) \leq C_{0} h T e^{(2 L + 1) T}$ , hence $\sup_{t} ∥ X_{h} (t) - x (t) ∥_{2} \leq K_{e r r} \sqrt{h}$ .

4.1step 3.1step 1.2givenalgebra∎

On each mesh cell, ${\tilde{X}}_{h} - X_{h}$ is the affine interpolation of its endpoint errors, so its norm is at most the larger endpoint norm. The triangle inequality with step 3.1 gives $\sup_{t} ∥ {\tilde{X}}_{h} (t) - x (t) ∥_{2} \leq K_{e r r} \sqrt{h} + e^{L T} \sum_{k} ε_{k},$ which is the claimed estimate. If $ε_{k} = 0$ all $k$ , or if their sum is $O (\sqrt{h})$ along a refining mesh, the stated $O (\sqrt{h})$ rate follows.

Depends on

Used by

Projected Euler for a constrained overdamped particle Example

Dependency tree · two levels

106 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

David E. Stewart, Dynamics with Inequalities: Impacts and Hard Constraints (standard reference, not scraped)
Dimitri P. Bertsekas, 6.253 Convex Analysis and Optimization, Complete Lecture Notes (standard reference, not scraped)