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.

Under Countable Choice, pointwise compact convex control constraints are weakly closed in L2

Statement

Assume the Axiom of Countable Choice.

Let $U_{c} \subset R^{m}$ be nonempty, compact and convex, and let $U_{c}$ be the pointwise admissible set in Finite-horizon bounded-control linear-quadratic ODE problem. If $u_{k} \in U_{c}$ and $u_{k} ⇀ u$ weakly in real $L^{2} (0, T; R^{m})$ , then $u \in U_{c}$ . Thus $U_{c}$ is weakly sequentially closed.

Facts & Assumptions

Given: Countable Choice, a finite horizon $T > 0$ , a nonempty compact convex set $U_{c} \subset R^{m}$ , its pointwise admissible set $U_{c}$ , and a weakly convergent sequence in real $L^{2} (0, T; R^{m})$ .

[A1]

Countable Choice ensures the Lebesgue outer measure construction is a measure on its sigma-algebra (The Axiom of Countable Choice ( ${A C}_{ω}$ ), Assuming countable choice, $L (R^{n})$ is a sigma-algebra containing every elementary set and $λ_{n}$ is a complete measure extending elementary volume).

[F1]

$U_{c} = {u \in L^{2} : u (t) \in U_{c} for almost every t}$ (Finite-horizon bounded-control linear-quadratic ODE problem). The pairing $\int q^{T} w$ is well-defined for vector-valued $L^{2}$ classes and bounded by $∥ q ∥_{2} ∥ w ∥_{2}$ : apply Euclidean Cauchy--Schwarz pointwise and scalar $L^{2}$ Cauchy--Schwarz to the norm functions (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}$ ).

[F2]

Weak convergence means convergence under every bounded linear functional; by [F1], $w \mapsto \int_{E} q^{T} w$ is bounded on $L^{2}$ whenever $E \subset [0, T]$ is measurable (Weak convergence of nets and sequences).

[F3]

A continuous real function on a nonempty compact metric space attains its minimum (A continuous real-valued function on a nonempty compact metric space is bounded and attains a greatest and a least value).

[F4]

The Lebesgue integral is linear on $L^{1}$ , and the nonnegative integral is monotone (The Lebesgue integral is linear on $L^{1} (μ)$ , Monotonicity and nonnegative homogeneity of the nonnegative integral).

[F5]

Rational open boxes form a countable basis of the product topology, and on $R^{m}$ that topology is the Euclidean metric topology ( $Q^{n}$ is a countable dense subset of $R^{n}$ , and rational open boxes form a countable basis, For $n \geq 1$ the product topology on $n$ copies of the usual topology of $R$ is the metric topology of $d_{\infty}$ on $R^{n}$ , and hence also of $d_{1}$ and $d_{2}$ , so $R^{n}$ as a product and $R^{n}$ as a metric space are one space).

[F6]

Under Countable Choice, Lebesgue measurable sets form a sigma-algebra and a countable union of measurable null sets is null, by countable subadditivity (Assuming countable choice, $L (R^{n})$ is a sigma-algebra containing every elementary set and $λ_{n}$ is a complete measure extending elementary volume, Finite and countable subadditivity of measures).

Given: The set and sequence in the Statement.

Proof

Given: The set and sequence in the Statement.

1.1F1F3F5choosealgebra

For $q \in R^{m}$ set $h (q) = \sup_{c \in U_{c}} q^{T} c$ , which is finite because $U_{c}$ is compact and hence bounded. If $z \notin U_{c}$ , [F3] gives a nearest point $y \in U_{c}$ to $z$ . For each $c \in U_{c}$ and $0 < θ \leq 1$ , convexity gives $y + θ (c - y) \in U_{c}$ ; minimality of $y$ implies $∥ z - y - θ (c - y) ∥_{2}^{2} \geq ∥ z - y ∥_{2}^{2}$ , and division by $θ$ followed by $θ ↓ 0$ gives $(z - y)^{T} (c - y) \leq 0$ . Thus $q_{0} = z - y$ satisfies $q_{0}^{T} z - h (q_{0}) \geq ∥ z - y ∥_{2}^{2} > 0$ . If $M_{c} = \sup_{c \in U_{c}} ∥ c ∥_{2}$ , then $∣ h (q) - h (q_{0}) ∣ \leq M_{c} ∥ q - q_{0} ∥_{2}$ and $∣ (q - q_{0})^{T} z ∣ \leq ∥ q - q_{0} ∥_{2} ∥ z ∥_{2}$ . By [F5], rational vectors are dense in Euclidean $R^{m}$ , so one can choose rational $q$ close enough to $q_{0}$ that $q^{T} z > h (q)$ . Therefore a point $z$ belongs to $U_{c}$ exactly when $q^{T} z \leq h (q)$ for every rational vector $q$ .

1.2A1F1F2F4givenalgebra

Fix a rational $q$ . Every $u_{k}$ is in $U_{c}$ , so $h (q) - q^{T} u_{k} (t) \geq 0$ almost everywhere. For any measurable $E \subseteq [0, T]$ , the test function $q 1_{E}$ lies in $L^{2}$ because $T < \infty$ ; weak convergence, [F2], and [F4] give $\int_{E} q^{T} u d t = \lim_{k} \int_{E} q^{T} u_{k} d t \leq h (q) ∣ E ∣$ . If $q^{T} u > h (q)$ on a set of positive measure, then for some integer $r \geq 1$ the measurable set $E_{r} = {t : q^{T} u (t) \geq h (q) + 1 / r}$ has positive measure, contradicting the integral inequality with $E = E_{r}$ . Hence $q^{T} u (t) \leq h (q)$ almost everywhere.

2.1A1F1F5F6step 1.1step 1.2algebra∎

The rational vectors form a countable set by [F5], so the exceptional null sets from step 1.2 have a null union by [A1, F6]. Outside that union all rational support inequalities hold simultaneously; step 1.1 then gives $u (t) \in U_{c}$ almost everywhere. This is exactly $u \in U_{c}$ .

Depends on

Used by

Dependency tree · two levels

93 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.3.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)