LemmaStatement: 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.

Cell averages give a strong recovery sequence for compact convex controls

Statement

Assume the Axiom of Countable Choice.

Assume the constraint set in Finite-horizon bounded-control linear-quadratic ODE problem is only the pointwise box $F = U_{c}$ . For the uniform mesh $0 = t_{0} < \dots < t_{N} = T$ , $h = T / N$ , define $P_{N} u$ on $[t_{j}, t_{j + 1})$ by $h^{- 1} \int_{t_{j}}^{t_{j + 1}} u (s) d s$ . Then $P_{N} u \in U_{c}$ for every $u \in U_{c}$ , $P_{N} u$ is piecewise constant, and $∥ P_{N} u - u ∥_{L^{2}} \to 0$ as $N \to \infty$ . This recovery statement need not hold for additional state or terminal constraints unless they are separately shown to be preserved or approximated.

Facts & Assumptions

Given: Countable Choice, $T > 0$ , a nonempty compact convex $U_{c} \subset R^{m}$ , its admissible control set, and the uniform meshes in Time meshes and piecewise-constant control parameterization.

[F1]

Finite linear combinations of interval indicators are dense in scalar $L^{2} (R)$ under Countable Choice; applying this componentwise gives density of finite vector-valued interval step functions, and extending by zero applies it on $(0, T)$ (Finite linear combinations of box indicators are dense in $L^{p} (R^{n})$ for $1 \leq p < \infty$ , The Axiom of Countable Choice ( ${A C}_{ω}$ )).

[F2]

The componentwise Lebesgue vector integral is linear. For $h \in L^{2} (I; R^{m})$ on a cell $I$ of length $h_{I}$ , put $I_{h} = \int_{I} h$ . If $I_{h} \neq 0$ , then $q = I_{h} / ∥ I_{h} ∥_{2}$ satisfies $∥ I_{h} ∥_{2} = \int_{I} q^{T} h \leq \int_{I} ∥ h ∥_{2} \leq \sqrt{h_{I}} ∥ h ∥_{L^{2} (I)}$ , using pointwise Euclidean Cauchy--Schwarz, monotonicity, scalar Cauchy--Schwarz, and componentwise linearity; the zero case is immediate (The Lebesgue integral is linear on $L^{1} (μ)$ , Cauchy-Schwarz $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥_{2} ∥ y ∥_{2}$ with its equality case, the triangle inequality for $∥ \cdot ∥_{2}$ , the parallelogram law and polarisation, Cauchy-Schwarz inequality for $L^{2}$ , The modulus of an integral is bounded by the integral of the modulus, Monotonicity and nonnegative homogeneity of the nonnegative integral).

[F3]

A continuous distance function attains its minimum on the nonempty compact set $U_{c}$ (A continuous real-valued function on a nonempty compact metric space is bounded and attains a greatest and a least value).

[F4]

For $v, w \in L^{2} (0, T; R^{m})$ , the pointwise Euclidean triangle inequality gives $∥ v + w ∥_{2} \leq ∥ v ∥_{2} + ∥ w ∥_{2}$ . Squaring, integrating by monotonicity, and applying scalar Minkowski to the scalar functions $∥ v (\cdot) ∥_{2}$ and $∥ w (\cdot) ∥_{2}$ yields $∥ v + w ∥_{L^{2}} \leq ∥ ∥ v (\cdot) ∥_{2} + ∥ w (\cdot) ∥_{2} ∥_{L^{2}} \leq ∥ v ∥_{L^{2}} + ∥ w ∥_{L^{2}}$ (Cauchy-Schwarz $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥_{2} ∥ y ∥_{2}$ with its equality case, the triangle inequality for $∥ \cdot ∥_{2}$ , the parallelogram law and polarisation, Monotonicity and nonnegative homogeneity of the nonnegative integral, Minkowski's inequality for integrals, including $p = \infty$ ).

Proof

1.1F2F3givenalgebra

On each interval $I_{j} = [t_{j}, t_{j + 1}]$ , let $m_{j} = h^{- 1} \int_{I_{j}} u (s) d s$ . If $m_{j} \notin U_{c}$ , compactness and [F3] give a nearest point $y \in U_{c}$ . For every $c \in U_{c}$ , the segment $y + θ (c - y)$ belongs to $U_{c}$ for $0 \leq θ \leq 1$ ; minimality of $y$ gives $∥ m_{j} - y - θ (c - y) ∥_{2}^{2} \geq ∥ m_{j} - y ∥_{2}^{2}$ . Divide by $θ > 0$ and let $θ ↓ 0$ to get $(m_{j} - y)^{T} (c - y) \leq 0$ . With $q_{0} = m_{j} - y \neq 0$ , this implies $q_{0}^{T} m_{j} > \sup_{c \in U_{c}} q_{0}^{T} c$ . But $q_{0}^{T} u (s) \leq \sup_{c \in U_{c}} q_{0}^{T} c$ almost everywhere, so integration contradicts the strict inequality. Thus every cell average lies in $U_{c}$ and $P_{N} u$ is pointwise admissible.

1.2F2F3F4algebra

For any $w \in L^{2}$ , [F2] on a cell $I_{j}$ gives $h ∥ h^{- 1} \int_{I_{j}} w ∥_{2}^{2} \leq \int_{I_{j}} ∥ w (s) ∥_{2}^{2} d s$ ; summing proves $∥ P_{N} w ∥_{2} \leq ∥ w ∥_{2}$ . For an interval indicator, $P_{N}$ agrees with it on cells not meeting an endpoint, and at most two endpoint cells contribute to the squared error, at most $2 h$ . By linearity of $P_{N}$ and the triangle inequality [F4], $P_{N} s \to s$ for every finite linear combination $s$ of interval indicators.

2.1F1F4step 1.2algebra∎

Fix $u \in L^{2}$ and $ε > 0$ . By [F1] choose such an interval step function $s$ with $∥ u - s ∥_{2} < ε$ . The contraction bound in step 1.2 and the triangle inequality [F4] give $∥ P_{N} u - u ∥_{2} \leq 2 ε + ∥ P_{N} s - s ∥_{2}$ . Taking $N \to \infty$ yields ${lim sup}_{N} ∥ P_{N} u - u ∥_{2} \leq 2 ε$ . Since $ε$ is arbitrary, $P_{N} u \to u$ strongly in $L^{2}$ .

Depends on

Used by

Dependency tree · two levels

67 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.3 (standard reference, not scraped)
J. Monnier, Optimal Control of ODEs: The Linear-Quadratic (LQ) Case, course notes, Chapter 2 §2.4 (standard reference, not scraped)