TheoremStatement: AI-adaptedProof: AI-generatedPipeline-generated

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 bounded-control linear-quadratic ODE has a unique minimizer

Statement

Assume the ultrafilter lemma, Dependent Choice, and Hahn–Banach. For the LQR data of Finite-horizon bounded-control linear-quadratic ODE problem, if the feasible-control set $F$ is nonempty, convex, and weakly sequentially closed, then $J$ attains its minimum on $F$ at a unique control $u^{*}$ . The direct-method branch uses exactly these three principles; Dependent Choice also supplies Countable Choice for the $L^{2}$ Hilbert-space/reflexivity suppliers. No use of the full Axiom of Choice is asserted.

Facts & Assumptions

Given: The LQR data, a nonempty convex weakly sequentially closed $F \subseteq U_{c}$ , the ultrafilter lemma, Dependent Choice, and Hahn–Banach.

[A1]

The ultrafilter lemma, Dependent Choice and Hahn–Banach are the exact axiom assumptions of the direct-method supplier; the uses below are weak-subsequence extraction and the stated reflexivity route (The ultrafilter extension principle (UL/BPI), The axiom of dependent choice: a relation in which every element is related to something admits an $N$ -indexed chain, The real dominated-extension principle as an additional hypothesis over ZF).

[F1]

Under Countable Choice, real $L^{2} (0, T; R^{m})$ with its integral pairing is a Hilbert space ( $L^{2}$ with the integral pairing is a Hilbert space).

[F2]

A real Hilbert space is reflexive under Countable Choice (Hilbert spaces are reflexive).

[F3]

Dependent Choice implies Countable Choice (Dependent choice implies countable choice).

[F4]

Under the ultrafilter lemma, Dependent Choice and Hahn–Banach, a proper coercive weakly sequentially lower-semicontinuous functional on a nonempty weakly sequentially closed subset of a real reflexive Banach space attains its infimum (The direct method in a reflexive Banach space).

[F5]

Under Countable Choice (supplied by Dependent Choice through [F3]), the pointwise control set is weakly sequentially closed; additional path/terminal constraints are included only through the assumed weakly sequentially closed set $F$ (Under Countable Choice, pointwise compact convex control constraints are weakly closed in L2, Finite-horizon bounded-control linear-quadratic ODE problem).

[F6]

The quadratic objective $J$ is weakly lower semicontinuous (Under Countable Choice, the LQR objective is weakly lower semicontinuous).

[F7]

The state map is unique, affine, and bounded from $L^{2}$ to continuous states (The bounded measurable linear ODE has a unique affine state map).

Proof

1.1A1F1F2F3

By [A1] and [F3], Countable Choice is available. Hence [F1] makes $L^{2} (0, T; R^{m})$ a real Hilbert space and [F2] makes it reflexive.

1.2F5F7givenalgebra

The set $F$ is nonempty by hypothesis and weakly sequentially closed by [F5]. For $u \in F$ , every state and terminal quadratic term in $J$ is nonnegative, while $R (t) ⪰ r I$ gives $J (u) \geq \frac{r}{2} ∥ u ∥_{2}^{2}$ . The cost is finite on $F$ by [F7], so $J$ is proper and coercive there.

2.1A1F1F2F4F6step 1.1step 1.2

By [F6], $J$ is weakly sequentially lower semicontinuous on $F$ . The axioms in [A1] and the reflexivity and admissibility checks in steps 1.1–1.2 verify every hypothesis of [F4]; therefore there exists $u^{*} \in F$ with $J (u^{*}) = \inf_{u \in F} J (u)$ .

3.1F1F5F7step 1.2step 2.1algebra∎

The state map is affine by [F7]. For $0 < θ < 1$ , each positive-semidefinite quadratic state or terminal form satisfies $q (θ a + (1 - θ) b) = θ q (a) + (1 - θ) q (b) - θ (1 - θ) q (a - b) \leq θ q (a) + (1 - θ) q (b)$ . The control form satisfies $\frac{1}{2} ⟨ R (θ u + (1 - θ) v), θ u + (1 - θ) v ⟩ = \frac{θ}{2} ⟨ R u, u ⟩ + \frac{1 - θ}{2} ⟨ R v, v ⟩ - \frac{θ (1 - θ)}{2} ⟨ R (u - v), u - v ⟩$ . If $u \neq v$ , then $⟨ R (u - v), u - v ⟩ \geq r ∥ u - v ∥_{2}^{2} > 0$ , so $J$ is strictly convex on the convex set $F$ . Two distinct minimizers would have a feasible strict convex combination with smaller cost, contradicting the minimum value established in step 2.1. Thus $u^{*}$ is unique.

Remarks

The source notes' direct-method outline is not used as a substitute for lower semicontinuity: Under Countable Choice, the LQR objective is weakly lower semicontinuous proves that requirement for this objective. The proof does not claim an axiom-minimal version without the three principles in [A1].

Depends on

Used by

Mesh-consistent LQR minimizers converge to the unique continuous minimizer Theorem

Dependency tree · two levels

71 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

J. Monnier, Optimal Control of ODEs: The Linear-Quadratic (LQ) Case, course notes, Chapter 2 §§2.4–2.5.1 (standard reference, not scraped)
W. W. Hager, Runge-Kutta methods in optimal control and the transformed adjoint system, Numerische Mathematik 87 (2000) (standard reference, not scraped)