Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-6.1-sol)
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.

The metric projection onto a closed convex set is nonexpansive

Statement

Assume the Axiom of Countable Choice (The Axiom of Countable Choice (ACω)). Let H be a real Hilbert space (Hilbert space) and let K⊆H be nonempty, closed and convex, with metric projection PK:H→K, the unique nearest point map of Projection onto a nonempty closed convex set. Then for all x,y∈H ∥PKx−PKy∥≤∥x−y∥, and PK is firmly nonexpansive in the equivalent forms ⟨PKx−PKy, x−y⟩≥∥PKx−PKy∥2,⟨(x−PKx)−(y−PKy), PKx−PKy⟩≥0.

Facts & Assumptions

Given: A real Hilbert space H, a nonempty closed convex set K⊆H, and points x,y∈H; Countable Choice is available.

[A1]

The Axiom of Countable Choice (ACω): Countable Choice, consumed by the existence-and-uniqueness theorem for nearest points.

[F1]

Projection onto a nonempty closed convex set: under Countable Choice the nearest point PKz of K to z exists and is unique for every z∈H.

[F2]

The projection onto a closed convex set is characterised by a variational inequality: for u∈K one has u=PKz if and only if ⟨u−z,v−u⟩≥0 for every v∈K.

[F3]

Real and complex inner-product spaces and their induced length: the inner product is real-valued on a real inner product space, symmetric and linear in each argument, with ∥w∥2=⟨w,w⟩.

[F4]

Cauchy–Schwarz: ∣⟨u,v⟩∣≤∥u∥∥v∥, with equality exactly for linearly dependent vectors: ∣⟨u,v⟩∣≤∥u∥∥v∥ for all vectors u,v of a real or complex inner product space.

Proof

technique · direct

Given: A real Hilbert space H, a nonempty closed convex set K⊆H, and points x,y∈H, with Countable Choice available.

1.1A1F1F2

Put u:=PKx and v:=PKy, both well defined by [F1]. By [F2] applied to u=PKx with the admissible point v∈K one has ⟨u−x,v−u⟩≥0, and applied to v=PKy with the admissible point u∈K one has ⟨v−y,u−v⟩≥0.

2.1step 1.1F3algebra

Adding the two inequalities of step 1.1 and using u−v=−(v−u) twice gives 0≤⟨u−x,v−u⟩+⟨v−y,u−v⟩=⟨u−x,v−u⟩−⟨v−y,v−u⟩=⟨(u−x)−(v−y),v−u⟩=⟨(u−v)−(x−y),v−u⟩=−∥u−v∥2−⟨x−y,v−u⟩=−∥u−v∥2+⟨x−y,u−v⟩, that is ⟨PKx−PKy,x−y⟩=⟨u−v,x−y⟩≥∥u−v∥2 by symmetry of the real inner product, the first firmly nonexpansive form.

3.1step 2.1F3F4algebra

If u=v the nonexpansiveness inequality is trivial; otherwise [F4] gives ∥u−v∥2≤⟨u−v,x−y⟩≤∥u−v∥ ∥x−y∥, and division by the positive number ∥u−v∥ yields ∥PKx−PKy∥=∥u−v∥≤∥x−y∥.

4.1step 2.1A1F3algebra∎

Finally, ⟨(x−u)−(y−v),u−v⟩=⟨x−y,u−v⟩−∥u−v∥2 [F3], so the inequality of step 2.1 is exactly the equivalent form ⟨(x−PKx)−(y−PKy),PKx−PKy⟩≥0; this completes the proof of both nonexpansiveness statements for arbitrary x,y and arbitrary admissible K, with Countable Choice used only through the existence of the projections [A1].

Depends on

Used by

Dependency tree · two levels

32 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