Alphabeta Math
LemmaStatement: Literature-sourcedProof: 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.

The L2 projection onto a pointwise box is clipping

Statement

Let Qad=Qad(qa,qb)⊂L2(E;R) be as in Closed pointwise box of L2 controls, and let r∈L2(E). Define

PQadr(x)=min⁡{qb(x),max⁡{qa(x),r(x)}}a.e.

Then PQadr is the unique minimizer of ∥q−r∥L2(E) over q∈Qad. Equivalently, q=PQadr if and only if

(q−r,v−q)L2(E)≥0(v∈Qad).

Facts & Assumptions

Given: The finite-measure control domain, the bounds qa,qb∈L2(E) with qa≤qb almost everywhere, and r∈L2(E).

[F1]

The admissible set consists of the L2 functions satisfying qa≤q≤qb almost everywhere (Closed pointwise box of L2 controls).

Proof

1.1F1givenalgebra

Put q(x)=min⁡{qb(x),max⁡{qa(x),r(x)}}. This function is measurable and lies between qa and qb; therefore q∈Qad and q∈L2(E). For real numbers a≤b, the clipped value c=min⁡{b,max⁡{a,s}} satisfies (c−s)(t−c)≥0 for every t∈[a,b]: if s<a, then c=a and both factors are nonnegative; if a≤s≤b, then c=s and the product is zero; if s>b, then c=b and both factors are nonpositive. Applying this pointwise with s=r(x) and t=v(x) and integrating gives (q−r,v−q)L2≥0 for every v∈Qad.

2.1F1step 1.1givenalgebra∎

For any v∈Qad, ∥v−r∥22−∥q−r∥22=∥v−q∥22+2(q−r,v−q)2≥∥v−q∥22. Thus q minimizes the distance and equality can hold only when v=q in L2. Conversely, if q is a distance minimizer, then for any v∈Qad and 0<t≤1, q+t(v−q)∈Qad. Expanding ∥q+t(v−q)−r∥22≥∥q−r∥22, dividing by 2t, and letting t↓0 gives (q−r,v−q)2≥0.

Depends on

Used by

Dependency tree · two levels

4 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