TheoremStatement: AI-adaptedProof: AI-adaptedPipeline-generatedprecheck pass

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.

A certified projected-gradient residual bounds distance to the control-mesh optimum

Statement

Assume Countable Choice. Let $U_{h}$ be a finite-dimensional cellwise-constant control space with nonempty box $Q_{h}$ , and restrict the exact reduced objective $\hat{J}$ of Linear coercive elliptic PDE control problem and reduced objective to $Q_{h}$ . Let $q_{h}^{*}$ be its minimizer and let $L_{h} \geq ∥ S ∣_{U_{h}} ∥^{2} + α$ , where $S$ is the linear part of the continuous state-to-observation map and $α > 0$ . Assume the residual- and projection-evaluation routines satisfy the finite-return admissibility conditions in Finite-budget projected-gradient loop with state-adjoint residual certificates. Then that finite-budget algorithm terminates in finite time after at most $N$ iterations and at most $N$ calls to each routine, returning \texttt{inconclusive}, \texttt{budget-exhausted}, or \texttt{certified}. Every \texttt{certified} return at $q \in Q_{h}$ with reported bound $ρ = \tilde{ρ} + δ / L_{h}$ satisfies $∥ q - P_{Q_{h}} (q - \nabla \hat{J} (q) / L_{h}) ∥_{U} \leq ρ \leq τ$ , and consequently $∥ q - q_{h}^{*} ∥_{U} \leq (L_{h} / α) ρ = (L_{h} / α) \tilde{ρ} + δ / α$ . This bounds distance to the control-mesh minimizer of the exact PDE objective; it is not an error estimate between that minimizer and the unrestricted PDE optimum.

Facts & Assumptions

Given: Countable Choice; a nonempty finite-dimensional cellwise-constant box $Q_{h}$ ; the exact reduced objective; $α > 0$ ; a valid $L_{h}$ ; and residual- and projection-evaluation routines satisfying the finite-return admissibility conditions in the algorithm definition.

[F1]

The FE state and adjoint residuals give $∥ g (q_{k}) - {\tilde{g}}_{k} ∥_{U} \leq ∥ B ∥ ε_{p, k}$ (State and adjoint Strang bounds give a reduced-gradient error certificate).

[F2]

The projection onto the cellwise box clips cell averages and is nonexpansive (The L2 projection onto a cellwise constant box clips cell averages).

[F3]

The exact reduced objective has gradient $g = \nabla \hat{J}$ and Hessian $S^{*} S + α I$ (Reduced gradient and coercive Hessian for linear elliptic tracking control).

[F4]

The Hessian bound in [F3] implies $α$ -strong convexity of $\hat{J}$ (Reduced gradient and coercive Hessian for linear elliptic tracking control).

[F5]

A continuous function on a compact finite-dimensional box attains its minimum (Semicontinuous extreme value theorem on compact Euclidean sets).

[F6]

A self-adjoint endomorphism of a finite-dimensional real-inner-product space has an orthonormal eigenbasis (Real spectral theorem: a self-adjoint endomorphism of a finite-dimensional real inner product space has an orthonormal eigenbasis).

[F7]

The algorithm issues \texttt{certified} only when the computed residual plus the adjoint-gradient error bound is at most $τ$ (Finite-budget projected-gradient loop with state-adjoint residual certificates).

[F8]

The algorithm performs at most $N$ iterations; its admissible residual and projection routines each return in finite time with either their exact valid outputs or failure, and the definition returns the stated failure or exhaustion status when certification does not succeed (Finite-budget projected-gradient loop with state-adjoint residual certificates).

[A2]

The algorithm supplies a certified bound $β_{B} \geq ∥ B ∥$ (Finite-budget projected-gradient loop with state-adjoint residual certificates).

[A3]

The algorithm sets $δ_{k} = β_{B} ε_{p, k}$ (Finite-budget projected-gradient loop with state-adjoint residual certificates).

[A1]

Countable Choice is used through the state-adjoint well-posedness and Hilbert-space Riesz results in [F1] and [F3] (The Axiom of Countable Choice ( ${A C}_{ω}$ )).

Proof

1.1A1A2A3F1F2givenalgebra

Put $g = \nabla \hat{J}$ , $T (q) = P_{Q_{h}} (q - g (q) / L_{h})$ , and ${\tilde{T}}_{k} = P_{Q_{h}} (q_{k} - {\tilde{g}}_{k} / L_{h})$ . By [F1], [A2], and [A3], $∥ g (q_{k}) - {\tilde{g}}_{k} ∥_{U} \leq ∥ B ∥ ε_{p, k} \leq δ_{k}$ . Nonexpansiveness [F2] gives $∥ T (q_{k}) - {\tilde{T}}_{k} ∥_{U} \leq δ_{k} / L_{h}$ . Since ${\tilde{ρ}}_{k} = ∥ q_{k} - {\tilde{T}}_{k} ∥_{U}$ , the triangle inequality gives $∥ q_{k} - T (q_{k}) ∥_{U} \leq {\tilde{ρ}}_{k} + δ_{k} / L_{h} = ρ_{k}$ .

1.2A1F2F3F6givenalgebra

Let $P_{U_{h}}$ be the orthogonal projection onto cellwise constants. The clipped-cell-average formula [F2] gives $P_{Q_{h}} (w) = P_{Q_{h}} (P_{U_{h}} w)$ . For $x, y \in U_{h}$ , [F3] yields $g (x) - g (y) = (S^{*} S + α I) (x - y)$ , so applying $P_{U_{h}}$ gives $H_{h} (x - y)$ , where $H_{h} = P_{U_{h}} (S^{*} S + α I) ∣_{U_{h}}$ . Its Rayleigh quotients lie in $[α, L_{h}]$ ; [F6] therefore implies $∥ I - H_{h} / L_{h} ∥ \leq 1 - α / L_{h}$ . Nonexpansiveness now gives $∥ T (x) - T (y) ∥_{U} \leq (1 - α / L_{h}) ∥ x - y ∥_{U}$ .

1.3A1F3F4F5givenalgebra

Since $Q_{h}$ is a nonempty compact box in finite-dimensional $U_{h}$ , [F5] gives a minimizer, and $α$ -strong convexity [F4] makes it unique. For any $v \in Q_{h}$ , the feasible segment from $q_{h}^{*}$ to $v$ and differentiability imply $(g (q_{h}^{*}), v - q_{h}^{*})_{U} \geq 0$ . Set $w = q_{h}^{*} - g (q_{h}^{*}) / L_{h}$ . Then $∥ w - v ∥_{U}^{2} - ∥ w - q_{h}^{*} ∥_{U}^{2} = ∥ v - q_{h}^{*} ∥_{U}^{2} + (2 / L_{h}) (g (q_{h}^{*}), v - q_{h}^{*})_{U} \geq 0$ . Thus $q_{h}^{*}$ is the unique nearest point in $Q_{h}$ to $w$ , so $T (q_{h}^{*}) = q_{h}^{*}$ .

2.1F7F8step 1.1givenalgebra

By [F7], a \texttt{certified} return is issued only when $ρ_{k} \leq τ$ , so step 1.1 proves the reported bound for the exact mapping residual. By [F8], each residual and projection call returns in finite time, and each is called at most $N$ times; the projection routine supplies the exact cell values and step norm used in step 1.1, and all remaining steps are finite scalar arithmetic and comparisons, so the algorithm terminates with one of its stated statuses.

2.2step 1.2step 1.3algebra

For $r = ∥ q - T (q) ∥_{U}$ , steps 1.2–1.3 and the triangle inequality imply $∥ q - q_{h}^{*} ∥_{U} \leq r + ∥ T (q) - T (q_{h}^{*}) ∥_{U} \leq r + (1 - α / L_{h}) ∥ q - q_{h}^{*} ∥_{U}$ . Rearranging yields $∥ q - q_{h}^{*} ∥_{U} \leq (L_{h} / α) r$ .

3.1step 1.1step 2.2algebra∎

On a \texttt{certified} return, step 1.1 gives $r \leq ρ = \tilde{ρ} + δ / L_{h}$ ; substituting into step 2.2 proves both displayed distance bounds.

Remarks

The objective in this theorem uses the exact continuous PDE state map and optimizes only over the finite-dimensional control box. Its finite-element state/adjoint solves are gradient approximations certified by the full Strang ledger in State and adjoint Strang bounds give a reduced-gradient error certificate.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

41 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

Michael Hinze, A Variational Discretization Concept in Control Constrained Optimization (standard reference, not scraped)