LemmaStatement: 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 certified projection variational residual bounds the projection error

Statement

Let $d \in N$ , including $d = 0$ . Let $C \subseteq R^{d}$ be nonempty, closed, and convex. If $y \in R^{d}$ , $ε \geq 0$ , and $p \in C$ satisfy $\sup_{z \in C} ⟨ y - p, z - p ⟩ \leq ε^{2},$ then $∥ p - P_{C} (y) ∥_{2} \leq ε$ .

Facts & Assumptions

Given: The set $C$ , input $y$ , tolerance $ε$ , and feasible candidate $p$ in the Statement.

[F1]

For $d \geq 1$ , Every point has a unique nearest point in a nonempty closed Euclidean convex set supplies the unique nearest point $q = P_{C} (y) \in C$ ; Metric projection onto a closed convex set satisfies the variational inequality gives $⟨ y - q, z - q ⟩ \leq 0$ for every $z \in C$ .

[F2]

The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ : $R^{0} = {0}$ and its Euclidean norm and inner product are zero.

Proof

1.1F2given

If $d = 0$ , then $C = {0}$ , $y = p = P_{C} (y) = 0$ , and the residual supremum is $0 \leq ε^{2}$ ; the asserted distance is $0 \leq ε$ .

1.2F1givenalgebra

Now assume $d \geq 1$ . Put $q = P_{C} (y)$ and $d_{0} = p - q$ . The residual bound at $z = q$ gives $⟨ y - p, d_{0} ⟩ \geq - ε^{2}$ . By [F1] with $z = p$ , $⟨ y - q, d_{0} ⟩ \leq 0$ . Since $y - q = (y - p) + d_{0}$ , this also gives $⟨ y - p, d_{0} ⟩ + ∥ d_{0} ∥_{2}^{2} \leq 0$ .

2.1step 1.2givenalgebra∎

Combining the two bounds yields $∥ d_{0} ∥_{2}^{2} \leq ε^{2}$ . Both sides are nonnegative, so $∥ p - P_{C} (y) ∥_{2} = ∥ d_{0} ∥_{2} \leq ε$ . This also covers $ε = 0$ .

Depends on

Used by

Dependency tree · two levels

21 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)