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.

The L2 projection onto a cellwise constant box clips cell averages

Statement

Assume Countable Choice. Let $E$ be a bounded polyhedral open control domain and let $T_{h}$ be a finite matching affine simplicial mesh of $E$ as in Matching affine simplicial meshes and shape regularity. Let $U_{h} \subset L^{2} (E)$ be the subspace of functions constant on each cell. Let the bounds $q_{a}, q_{b}$ in Closed pointwise box of L2 controls be constant on each cell and satisfy $q_{a} \leq q_{b}$ . Put $Q_{h} = U_{h} \cap Q_{a d} (q_{a}, q_{b})$ . For $r \in L^{2} (E)$ define

(P_{Q_{h}} r) ∣_{K} = {clip}_{[q_{a} ∣_{K}, q_{b} ∣_{K}]} (\frac{1}{∣ K ∣} \int_{K} r (x) d x), K \in T_{h},

where ${clip}_{[a, b]} (s) = \min {b, \max {a, s}}$ . Then $P_{Q_{h}} r$ is the unique $L^{2} (E)$ -nearest point in $Q_{h}$ to $r$ , and $P_{Q_{h}}$ is nonexpansive: $∥ P_{Q_{h}} r - P_{Q_{h}} s ∥_{L^{2} (E)} \leq ∥ r - s ∥_{L^{2} (E)}$ .

Facts & Assumptions

Given: Countable Choice; the finite matching partition into nondegenerate simplices; $r \in L^{2} (E)$ ; and cellwise constant ordered bounds.

[F1]

The continuous box consists of the $L^{2}$ functions between its bounds almost everywhere (Closed pointwise box of L2 controls); intersecting it with $U_{h}$ gives independent closed intervals for the cell values.

[F2]

The mesh is a finite collection of nondegenerate cells with disjoint interiors covering $E$ up to measure-zero facets (Matching affine simplicial meshes and shape regularity).

[F3]

Every facet lies in an affine hyperplane, and every affine hyperplane is Lebesgue null; hence the finite union of mesh facets is null (Every affine hyperplane of $R^{n}$ , and hence every proper linear subspace, is Lebesgue null).

[F4]

Hölder with exponents $2, 2$ shows that each $L^{2} (K)$ function is integrable on a finite-measure cell, so the cell averages are finite (Holder's inequality for integrals, including the endpoint cases).

Proof

1.1F2F4givenalgebra

For a cell $K$ , [F4] makes ${\overset{ˉ}{r}}_{K} = ∣ K ∣^{- 1} \int_{K} r$ finite. For any constant value $z_{K}$ , $\int_{K} ∣ z_{K} - r ∣^{2} = ∣ K ∣ ∣ z_{K} - {\overset{ˉ}{r}}_{K} ∣^{2} + \int_{K} ∣ r - {\overset{ˉ}{r}}_{K} ∣^{2},$ because the cross term vanishes by $\int_{K} (r - {\overset{ˉ}{r}}_{K}) = 0$ . The second term is independent of $z_{K}$ .

2.1F1step 1.1algebra

Among real $z_{K} \in [q_{a} ∣_{K}, q_{b} ∣_{K}]$ , the square $∣ z_{K} - {\overset{ˉ}{r}}_{K} ∣^{2}$ is uniquely minimized by the clipped value: if ${\overset{ˉ}{r}}_{K}$ is below the interval the nearest endpoint is the lower bound; if it is inside, it is itself; if it is above, the nearest endpoint is the upper bound. Thus the displayed cell value uniquely minimizes the cell integral, and it lies in the required interval by [F1].

3.1F1F2F3step 2.1algebra

The cell choices are independent, so summing the cellwise minima from step 2.1 over the partition up to its null facets [F3] proves that $P_{Q_{h}} r$ is the unique global minimizer. For $v \in Q_{h}$ , convexity makes $p + t (v - p)$ feasible, where $p = P_{Q_{h}} r$ and $0 < t \leq 1$ . Minimality gives $∥ p + t (v - p) - r ∥_{2}^{2} - ∥ p - r ∥_{2}^{2} = 2 t (p - r, v - p)_{2} + t^{2} ∥ v - p ∥_{2}^{2} \geq 0.$ Divide by $2 t$ and let $t ↓ 0$ to obtain the projection variational inequality $(p - r, v - p)_{2} \geq 0$ .

4.1F4step 3.1algebra∎

Let $p = P_{Q_{h}} r$ and $q = P_{Q_{h}} s$ . Apply the variational inequality from step 3.1 with $v = q$ and $v = p$ , respectively. Adding gives $∥ p - q ∥_{2}^{2} \leq (r - s, p - q)_{2}$ . Hölder with exponents $2, 2$ then yields $∥ p - q ∥_{2} \leq ∥ r - s ∥_{2}$ when $p \neq q$ ; if $p = q$ the inequality is immediate.

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

Eduardo Casas and Fredi Tröltzsch, Error estimates for linear-quadratic elliptic control problems (standard reference, not scraped)