ExampleConstruction: AI-adaptedVerification: 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 distributed heat source has an exact box-constrained optimum

Statement

Assume Countable Choice. Let $E = Ω = (0, 1)$ , $V = H_{0}^{1} (0, 1)$ , $U = H = L^{2} (0, 1)$ , and $a (u, v) = \int_{0}^{1} (u^{'} v^{'} + u v) d x$ . Let $B q$ be the $L^{2}$ load functional $v \mapsto \int_{0}^{1} q v d x$ , set $f = 0$ , $q_{a} = 0$ , $q_{b} = 1$ , and $α = 1$ . Put $q_{*} (x) = \frac{1}{2} \sin (π x)$ and $u_{*} (x) = q_{*} (x) / (π^{2} + 1)$ , which solve the state equation. Set $p_{*} (x) = - q_{*} (x)$ and $u_{d} (x) = u_{*} (x) + \frac{1}{2} (π^{2} + 1) \sin (π x)$ . Define $J (q) = \frac{1}{2} ∥ u (q) - u_{d} ∥_{L^{2}}^{2} + \frac{1}{2} ∥ q ∥_{L^{2}}^{2}$ . Then $q_{*}$ is the unique optimal control, and its adjoint is $p_{*}$ .

Facts & Assumptions

Given: The one-dimensional coercive elliptic control problem, the admissible box $0 \leq q \leq 1$ , and the exactly defined target $u_{d}$ .

[F1]

The state and adjoint equations have unique weak solutions under the bounded coercive form hypotheses (Well-posedness of elliptic control state and adjoint equations).

[F2]

For $α > 0$ , an admissible $q$ satisfying $(B^{*} p (q) + α q, v - q)_{U} \geq 0$ for every $v \in Q_{a d}$ is the unique minimizer (Existence, uniqueness, and variational inequality for elliptic PDE control).

Verification

1.1F1givenalgebra

The form is the full $H^{1}$ inner product, so it is bounded and coercive with constants one, and $∣ ⟨ B q, v ⟩ ∣ \leq ∥ q ∥_{2} ∥ v ∥_{H^{1}}$ . Since $f = 0$ , $- u_{*}^{''} + u_{*} = q_{*}$ , and $u_{*} (0) = u_{*} (1) = 0$ , integration by parts first for compactly supported smooth tests and then by $H_{0}^{1}$ density gives $a (u_{*}, v) = (q_{*}, v)_{L^{2}}$ for every $v \in H_{0}^{1} (0, 1)$ ; uniqueness in [F1] identifies the state. Since $- p_{*}^{''} + p_{*} = - \frac{1}{2} (π^{2} + 1) \sin (π x) = u_{*} - u_{d}$ and $p_{*}$ has zero boundary values, the same argument verifies the adjoint equation.

2.1F2step 1.1givenalgebra∎

The load identity gives $(B^{*} p_{*}, r)_{U} = ⟨ B r, p_{*} ⟩ = (p_{*}, r)_{U}$ for every $r \in U$ , hence $B^{*} p_{*} = p_{*}$ . Since $0 \leq q_{*} \leq 1 / 2$ , it is admissible, and $B^{*} p_{*} + α q_{*} = p_{*} + q_{*} = 0$ . Thus its variational inequality holds with equality for every admissible comparison control, and [F2] makes $q_{*}$ the unique minimizer.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

22 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)
Hannes Meinlschmidt, Optimization with Partial Differential Equations, FAU lecture notes (standard reference, not scraped)