LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-luna)

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 pointwise L2 box is weakly sequentially closed

Statement

Let $E$ and $Q_{a d} (q_{a}, q_{b})$ be as in Closed pointwise box of L2 controls. If $q_{n} \in Q_{a d}$ and $q_{n} ⇀ q$ weakly in $L^{2} (E)$ , then $q \in Q_{a d}$ .

Facts & Assumptions

Given: A bounded measurable $E$ , $q_{a}, q_{b} \in L^{2} (E)$ with $q_{a} \leq q_{b}$ almost everywhere, a sequence $q_{n} \in Q_{a d}$ , and weak convergence $q_{n} ⇀ q$ .

[F1]

$Q_{a d} = {r \in L^{2} (E) : q_{a} \leq r \leq q_{b} a.e.}$ (Closed pointwise box of L2 controls).

[F2]

On finite-measure $E$ , Hölder with exponents $2, 2$ makes products of $L^{2} (E)$ functions integrable (Holder's inequality for integrals, including the endpoint cases).

[F3]

A nonnegative measurable function has integral zero exactly when it vanishes almost everywhere (A nonnegative measurable function has integral $0$ exactly when it vanishes almost everywhere).

Proof

1.1F1F2F3givenalgebra

Let $A = {x \in E : q (x) < q_{a} (x)}$ . Since $E$ is bounded, choose $M \geq 1$ with $E \subset (- M, M)^{d}$ . The single-box cover in the definition of Lebesgue outer measure gives $μ (E) \leq (2 M)^{d} < \infty$ , so $1_{A} \in L^{2} (E)$ . If $A$ had positive measure, $f = (q_{a} - q) 1_{A}$ would be nonnegative, integrable by [F2], and positive on a set of positive measure. Thus [F3] gives $\int_{E} f > 0$ . Weak convergence tested against $1_{A}$ gives $\int_{A} (q - q_{a}) = \lim_{n \to \infty} \int_{A} (q_{n} - q_{a}) \geq 0$ , contradicting $\int_{A} (q - q_{a}) = - \int_{E} f < 0$ . Therefore $q \geq q_{a}$ almost everywhere.

2.1F1F2F3step 1.1givenalgebra∎

Let $B = {x \in E : q (x) > q_{b} (x)}$ . As in step 1.1, $1_{B} \in L^{2} (E)$ . If $B$ had positive measure, $f = (q - q_{b}) 1_{B}$ would be nonnegative, integrable by [F2], and positive on a set of positive measure. Thus [F3] gives $\int_{E} f > 0$ . Weak convergence tested against $1_{B}$ gives $\int_{B} (q - q_{b}) = \lim_{n} \int_{B} (q_{n} - q_{b}) \leq 0$ , contradicting $\int_{B} (q - q_{b}) = \int_{E} f > 0$ . Therefore $q \leq q_{b}$ almost everywhere, and [F1] gives $q \in Q_{a d}$ .

Depends on

Used by

Existence, uniqueness, and variational inequality for elliptic PDE control Theorem

Dependency tree · two levels

20 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

Hannes Meinlschmidt, Optimization with Partial Differential Equations, FAU lecture notes (standard reference, not scraped)