LemmaStatement: 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.

Projection onto a closed convex set is nonexpansive

Statement

Let $d \in N$ , including $d = 0$ . Let $C \subseteq R^{d}$ be nonempty, closed, and convex, and let $P_{C} (y)$ denote the unique nearest point in $C$ to $y$ . Then $∥ P_{C} (u) - P_{C} (v) ∥_{2} \leq ∥ u - v ∥_{2} (u, v \in R^{d}) .$

Facts & Assumptions

Given: The set $C$ and points $u, v$ in the Statement.

[F1]

For $d \geq 1$ , Metric projection onto a closed convex set satisfies the variational inequality: if $p = P_{C} (y)$ , then $⟨ y - p, z - p ⟩ \leq 0$ for every $z \in C$ .

[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: $∣ ⟨ a, b ⟩ ∣ \leq ∥ a ∥_{2} ∥ b ∥_{2}$ .

[F3]

The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ : $R^{0}$ consists of its single zero vector, whose norm is $0$ .

Proof

1.1F3given

If $d = 0$ , then the nonempty set $C \subseteq R^{0} = {0}$ is ${0}$ , so $P_{C}$ is the constant zero map and the claimed inequality is $0 \leq 0$ .

1.2F1givenalgebra

Now assume $d \geq 1$ . Put $p = P_{C} (u)$ and $q = P_{C} (v)$ . Applying [F1] first with $(y, z) = (u, q)$ and then with $(y, z) = (v, p)$ gives $⟨ u - p, p - q ⟩ \geq 0$ and $⟨ q - v, p - q ⟩ \geq 0$ . Therefore $⟨ u - v, p - q ⟩ = ⟨ u - p, p - q ⟩ + ∥ p - q ∥_{2}^{2} + ⟨ q - v, p - q ⟩ \geq ∥ p - q ∥_{2}^{2} .$

2.1F2step 1.2givenalgebra∎

By [F2], $∥ p - q ∥_{2}^{2} \leq ∥ u - v ∥_{2} ∥ p - q ∥_{2}$ . If $p = q$ the result is immediate; otherwise divide by the positive number $∥ p - q ∥_{2}$ .

Depends on

Used by

Dependency tree · two levels

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