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.

Mesh-consistent LQR minimizers converge to the unique continuous minimizer

Statement

Assume the axiom branch of A bounded-control linear-quadratic ODE has a unique minimizer, and let $u^{*}$ be the unique minimizer of the LQR objective $J$ on a nonempty convex weakly sequentially closed feasible set $F \subseteq U_{c}$ . For each mesh index $N$ , let $F_{N} \subseteq F$ be nonempty, and let $J_{N}$ be the discrete transcription objective. Assume there are $ε_{N} \to 0$ such that $∣ J_{N} (v) - J (v) ∣ \leq ε_{N}$ for every $v \in F_{N}$ . Assume also a recovery sequence $v_{N} \in F_{N}$ with $∥ v_{N} - u^{*} ∥_{L^{2}} \to 0$ . If $u_{N}$ is a global minimizer of $J_{N}$ on $F_{N}$ , then $u_{N} ⇀ u^{*}$ in $L^{2}$ and $x_{u_{N}} \to x_{u^{*}}$ uniformly.

For the control-only case $F = U_{c}$ and piecewise-constant mesh controls, the cell-average lemma supplies the strong recovery sequence. If active path or terminal constraints are present, preservation or recovery of those constraints is an additional hypothesis; node sampling alone does not establish continuous-path feasibility. This theorem is conditional on a uniform objective consistency bound; an embedded adaptive RK difference alone does not provide that bound.

Facts & Assumptions

Given: The LQR data, its unique minimizer, feasible discrete sets, uniform consistency, recovery controls, and global discrete minimizers.

[F1]

The continuous LQR minimizer exists uniquely under the stated closedness and choice-axiom hypotheses (A bounded-control linear-quadratic ODE has a unique minimizer).

[F2]

The control set $U_{c}$ is bounded in $L^{2}$ because $U_{c}$ is compact, and is weakly sequentially closed under Countable Choice (supplied by the theorem's axiom branch) (Finite-horizon bounded-control linear-quadratic ODE problem, Under Countable Choice, pointwise compact convex control constraints are weakly closed in L2).

[F3]

A bounded sequence in a real reflexive Banach space has a weakly convergent subsequence under the ultrafilter lemma, Dependent Choice, and Hahn–Banach (A bounded sequence in a reflexive Banach space has a weakly convergent subsequence).

[F4]

The LQR objective is weakly sequentially lower semicontinuous on $U_{c}$ (Under Countable Choice, the LQR objective is weakly lower semicontinuous).

[F5]

Weakly convergent controls in $U_{c}$ have uniformly convergent states (Weakly convergent bounded controls have uniformly convergent states).

[F6]

The state map is affine and bounded from $L^{2}$ to the supremum norm, so the LQR objective is continuous under strong $L^{2}$ convergence (The bounded measurable linear ODE has a unique affine state map, Finite-horizon bounded-control linear-quadratic ODE problem).

[A1]

The ultrafilter lemma, Dependent Choice, and Hahn–Banach are assumed for [F3] and real Hilbert-space reflexivity (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, $L^{2}$ with the integral pairing is a Hilbert space, Hilbert spaces are reflexive).

Proof

1.1F2F3A1givenalgebra

Since $u_{N} \in F_{N} \subseteq U_{c}$ and $U_{c}$ is compact, $\sup_{N} ∥ u_{N} ∥_{2} \leq \sqrt{T} \sup_{c \in U_{c}} ∥ c ∥_{2} < \infty$ . Real $L^{2}$ is reflexive by [A1], so [F3] gives a weakly convergent subsequence from every subsequence of $(u_{N})$ .

2.1F1F4F6givenstep 1.1algebra

Let a subsequence $u_{N_{k}}$ converge weakly to $\overset{ˉ}{u}$ . Because each $u_{N_{k}} \in F$ and $F$ is weakly sequentially closed, $\overset{ˉ}{u} \in F$ . By [F4] and consistency, $J (\overset{ˉ}{u}) \leq {lim inf}_{k} J (u_{N_{k}}) \leq {lim sup}_{k} (J_{N_{k}} (u_{N_{k}}) + ε_{N_{k}})$ . Global discrete minimality gives $J_{N_{k}} (u_{N_{k}}) \leq J_{N_{k}} (v_{N_{k}}) \leq J (v_{N_{k}}) + ε_{N_{k}}$ . To see $J (v_{N_{k}}) \to J (u^{*})$ , [F6] gives $∥ x_{v_{N_{k}}} - x_{u^{*}} ∥_{\infty} \leq C ∥ v_{N_{k}} - u^{*} ∥_{2} \to 0$ ; the control quadratic difference is bounded by $\frac{M}{2} (∥ v_{N_{k}} ∥_{2} + ∥ u^{*} ∥_{2}) ∥ v_{N_{k}} - u^{*} ∥_{2}$ , and state and terminal quadratic differences tend to zero by the corresponding bounded-quadratic estimate and uniform state convergence. Hence $J (v_{N_{k}}) \to J (u^{*})$ , so $J (\overset{ˉ}{u}) \leq J (u^{*})$ .

3.1F1step 1.1step 2.1algebra

Since $\overset{ˉ}{u} \in F$ and $u^{*}$ is the unique minimizer there, step 2.1 forces $\overset{ˉ}{u} = u^{*}$ . Every subsequence therefore has a weakly convergent subsubsequence whose limit is $u^{*}$ . If the full sequence failed to converge weakly to $u^{*}$ , some bounded linear functional and some positive tolerance would witness failure along a subsequence; a weakly convergent subsubsequence from step 1.1 would contradict that witness. Thus $u_{N} ⇀ u^{*}$ .

4.1F5step 3.1∎

Apply [F5] to the weakly convergent admissible controls from step 3.1 to obtain $x_{u_{N}} \to x_{u^{*}}$ uniformly on $[0, T]$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

82 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

S. Gros and M. Diehl, Numerical Optimal Control, draft course manuscript, Chapter 13 §§13.1–13.4 (standard reference, not scraped)
J. Monnier, Optimal Control of ODEs: The Linear-Quadratic (LQ) Case, course notes, Chapter 2 §§2.4–2.5.1 (standard reference, not scraped)