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

Existence, uniqueness, and variational inequality for elliptic PDE control

Statement

Assume Countable Choice and the setting of Linear coercive elliptic PDE control problem and reduced objective. Then J^ has a unique minimizer q∗∈Qad. It is characterized by

(B∗p(q∗)+αq∗,v−q∗)U≥0(v∈Qad),

where p(q∗) is the adjoint from Well-posedness of elliptic control state and adjoint equations. Conversely, every q∈Qad satisfying this variational inequality is the unique minimizer.

Facts & Assumptions

Given: Countable Choice, the nonempty pointwise box Qad⊂U, the bounded coercive state problem, and the reduced objective J^.

[F1]

Qad is nonempty, bounded, norm closed, and weakly sequentially closed (A pointwise L2 box is nonempty, bounded, closed, and convex, A pointwise L2 box is weakly sequentially closed).

[F2]

Every bounded sequence in the separable real Hilbert control space U=L2(E) has a weakly convergent subsequence (A bounded sequence in a separable Hilbert space has a weakly convergent subsequence, L2 controls on a bounded spatial region form a separable Hilbert space).

[F3]

The state map is affine with bounded linear part S, and J^(q+h)−J^(q)=(B∗p(q)+αq,h)U+12∥Sh∥H2+α2∥h∥U2 (Reduced gradient and coercive Hessian for linear elliptic tracking control).

[F4]

A Fréchet minimizer over a convex set has nonnegative directional derivative along every feasible segment; here that derivative is (B∗p(q)+αq,v−q)U (Reduced gradient and coercive Hessian for linear elliptic tracking control).

[A1]

Countable Choice permits the indexed selection of a minimizing sequence from the nonempty sets {q∈Qad:J^(q)<m+1/(n+1)} for n∈N (The Axiom of Countable Choice (ACω)).

Proof

1.1A1F1F2givenconstruct

The box is nonempty by [F1], so m:=inf⁡q∈QadJ^(q) is finite: J^≥0 and J^(qa)<∞. For every n∈N, the defining property of the infimum makes the set in [A1] nonempty. By Countable Choice choose qn∈Qad with J^(qn)<m+1/(n+1). Since J^(qn)≥α∥qn∥U2/2 and 1/(n+1)≤1, the sequence is bounded. By [F2], applied to its positive-indexed tail, a subsequence converges weakly to some q∈U, and [F1] gives q∈Qad.

1.2F4givenalgebra

If q∗ minimizes, fix v∈Qad. Convexity gives q∗+t(v−q∗)∈Qad for 0≤t≤1. Minimality makes the right directional quotient nonnegative for every t>0; letting t↓0 and using [F4] proves the variational inequality.

2.1F1F3step 1.1algebra

Write Ju(qn)−ud=Ju(0)−ud+Sqn. Bounded linear maps preserve weak convergence, so along the subsequence this state residual converges weakly in H to Ju(q)−ud; the controls converge weakly in U. The Hilbert norm is weakly lower semicontinuous: if z≠0, then ∥zn∥≥∣(zn,z/∥z∥)∣→∥z∥, while the case z=0 is immediate. Applying this to both squared norms in J^ gives J^(q)≤lim inf⁡nJ^(qn)=m. Thus q attains the infimum.

3.1F1F3step 2.1algebra

The exact expansion in [F3] shows strict convexity: for distinct q,r∈U and 0<t<1, J^(tq+(1−t)r)=tJ^(q)+(1−t)J^(r)−t(1−t)2(∥S(q−r)∥H2+α∥q−r∥U2). The last subtracted term is positive, so two different minimizers in the convex box cannot exist.

4.1F3step 3.1step 1.2givenalgebra∎

Conversely, if q satisfies the variational inequality, then for every v∈Qad the exact expansion [F3] gives J^(v)−J^(q)=(B∗p(q)+αq,v−q)U+12∥S(v−q)∥H2+α2∥v−q∥U2≥0. Thus q is a minimizer; step 3.1 gives uniqueness.

Remarks

The existence proof uses Countable Choice to select a minimizing sequence and the stated separable-Hilbert weak subsequence lemma. It uses no Axiom of Choice, Hahn–Banach separation, or reflexive-space compactness theorem.

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