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.

Cell averaging preserves constant box bounds and has an H1 error bound

Statement

Assume Countable Choice. Let $E \subset R^{d}$ be a nonempty bounded polyhedral open control domain, and let ${T_{h}}$ be a family of matching affine simplicial meshes of $E$ as in Matching affine simplicial meshes and shape regularity. Set $h = \max_{K \in T_{h}} diam (K)$ . For every $q \in L^{2} (E)$ define

(Π_{h} q) ∣_{K} = ∣ K ∣^{- 1} \int_{K} q .

Then $Π_{h}$ is the $L^{2}$ orthogonal projection onto the cellwise-constant space. For every $q \in H^{1} (E)$ ,

∥ q - Π_{h} q ∥_{L^{2} (E)} \leq C h ∣ q ∣_{H^{1} (E)},

where $C$ depends only on dimension and the fixed reference simplex. If additionally the box bounds $q_{a}, q_{b}$ are constant on each cell and $q \in Q_{a d}$ , then $Π_{h} q \in Q_{a d}$ .

Facts & Assumptions

Given: Countable Choice; the affine simplex mesh convention; $q \in L^{2} (E)$ for orthogonal projection and $q \in H^{1} (E)$ for the error estimate; and, only for box preservation, cellwise-constant bounds with $q_{a} \leq q \leq q_{b}$ almost everywhere.

[F1]

A cell map is an affine bijection from the fixed reference simplex, and the cells have disjoint interiors (Matching affine simplicial meshes and shape regularity).

[F2]

Affine pullback transports weak derivatives and Sobolev seminorms by the matrix and determinant factors (Affine pullback of weak derivatives and Sobolev seminorms).

[F3]

On the reference simplex, subtracting the cell mean leaves an $L^{2}$ norm bounded by a constant times the $H^{1}$ seminorm (Poincare–Wirtinger inequality on a reference simplex).

[F4]

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

[F5]

Change of variables holds for nonnegative measurable integrands; applying it to the positive and negative parts gives the formula for the integrable real function $q$ (A C^1 diffeomorphism satisfies the change-of-variables formula for nonnegative Lebesgue measurable functions).

[F6]

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

[A1]

Countable Choice is the stated hypothesis of [F2] and [F3] (The Axiom of Countable Choice ( ${A C}_{ω}$ )).

Proof

1.1F1F4F6givenalgebra

By [F4], the cell means are finite, and finitely many finite cell values define an element of the cellwise-constant subspace of $L^{2} (E)$ . For every cellwise-constant $c$ , $\int_{K} (q - Π_{h} q) c ∣_{K} = 0$ by the mean identity. Summing over cells, ignoring the null facets by [F6], gives $(q - Π_{h} q, c)_{U} = 0$ , proving the orthogonal-projection property for all $q \in L^{2} (E)$ . If additionally $q_{a} ∣_{K} \leq q \leq q_{b} ∣_{K}$ , integration and division by $∣ K ∣ > 0$ place each mean in that interval; hence $Π_{h} q \in Q_{a d}$ .

1.2A1F1F2F3F4F5F6givenalgebra

Fix a cell $K$ with affine map $F_{K} (\hat{x}) = b_{K} + A_{K} \hat{x}$ and write $\hat{q} = q \circ F_{K}$ . By [F5], change of variables applied to $q^{+}$ and $q^{-}$ gives the signed integral formula; [F6] lets us ignore the cell facets. Hence $(Π_{h} q) ∣_{K} \circ F_{K} = {\hat{q}}_{{\hat{S}}_{d}}$ , the mean of $\hat{q}$ on the reference simplex. By [F3], $∥ q - Π_{h} q ∥_{L^{2} (K)} = ∣ \det A_{K} ∣^{1 / 2} ∥ \hat{q} - {\hat{q}}_{{\hat{S}}_{d}} ∥_{L^{2} ({\hat{S}}_{d})} \leq C ∣ \det A_{K} ∣^{1 / 2} ∣ \hat{q} ∣_{H^{1} ({\hat{S}}_{d})} .$ By [F2], $∣ \hat{q} ∣_{H^{1} ({\hat{S}}_{d})} \leq C ∥ A_{K} ∥ ∣ \det A_{K} ∣^{- 1 / 2} ∣ q ∣_{H^{1} (K)}$ , and $∥ A_{K} ∥ \leq C_{d} h_{K}$ from the fixed reference simplex geometry. Thus $∥ q - Π_{h} q ∥_{L^{2} (K)} \leq C h_{K} ∣ q ∣_{H^{1} (K)}$ .

2.1F1F6step 1.2algebra∎

Square the cell estimates in step 1.2 and sum over cells; the interiors are disjoint and their omitted facets are null by [F6]. Since $h_{K} \leq h$ , the sum is at most $C^{2} h^{2} ∣ q ∣_{H^{1} (E)}^{2}$ . Taking square roots proves the global bound.

Depends on

Used by

Piecewise-constant control with shape-regular finite elements has O(h) error Theorem

Dependency tree · two levels

50 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)
Michael Hinze, A Variational Discretization Concept in Control Constrained Optimization (standard reference, not scraped)