TheoremStatement: AI-adaptedProof: Literature-sourced

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.

General Banach-triple Aubin–Lions–Simon compactness

Statement

Assume Countable Choice. Let $X, B, Y$ be Banach spaces over the same scalar field $K \in {R, C}$ , with $X$ compactly embedded into $B$ and $B$ continuously embedded into $Y$ , and let $0 < T < \infty$ and $1 \leq p < \infty$ . A family bounded in $L^{p} (0, T; X)$ whose distributional time derivatives are bounded in $L^{1} (0, T; Y)$ is relatively compact in $L^{p} (0, T; B)$ .

Relative compactness means that the closure of the family in the displayed $L^{p} (0, T; B)$ norm is compact. The embeddings are compatible injective linear maps; the time spaces consist of strongly measurable almost-everywhere classes for Lebesgue measure on $(0, T)$ , with Bochner norms. The derivative is represented by a strongly measurable $Y$ -valued integrable function satisfying the Bochner distributional identity against scalar smooth compactly supported time tests.

Statement references

The Axiom of Countable Choice (AC_ω)

Compatible compact Banach triples

Bochner spaces and bounded inclusion of value spaces

Distributional time derivatives with values in a Banach space

Facts & Assumptions

Given: Countable Choice, the three Banach spaces over the same scalar field, $0 < T < \infty$ and the finite exponent in the Statement; boundedness means a common finite supremum of the displayed Bochner norms. The localized complex Sobolev example in [F2] and [F4] additionally assumes the Axiom of Choice.

Goal: Record the independently established general compactness input and its exact applicability.

[F1]

Under Countable Choice (The Axiom of Countable Choice (AC_ω)) and $0 < T < \infty$ , the compatibility maps in Compatible compact Banach triples identify every $u \in L^{p} (0, T; X)$ as a $B$ -valued and $Y$ -valued class by Bochner spaces and bounded inclusion of value spaces. On this finite interval it is also in $L^{1} (0, T; Y)$ . Thus the identity defining its derivative in Distributional time derivatives with values in a Banach space is meaningful. Countable Choice is retained to meet these helper contracts; no necessity assertion for Simon's theorem is made.

[F2]

For the localized Sobolev application assume the Axiom of Choice (The Axiom of Choice), which includes Countable Choice. Let $G \subset R^{n}$ , $n \geq 1$ , be a nonempty bounded open set with smooth boundary, $B = L^{2} (G; C)$ and $Y = (H_{0}^{2} (G))^{'}$ , with the full weak-derivative $H^{2}$ norm and conjugate-dual convention of The L2 pivot injects into the local negative Sobolev space. That supplier makes $Y$ Banach and the $L^{2}$ pivot an injective continuous linear map $B \to Y$ . The space $B$ is Banach by L² with the integral pairing is a Hilbert space. If a complex Banach space $X$ embeds compactly into $B$ , these maps give the triple in Compatible compact Banach triples.

[F3]

At $p = 2$ , a bound $\sup_{u} ∥ u ∥_{L^{2} (0, T; X)} < \infty$ and strongly measurable distributional derivative representatives with $\sup_{u} ∥ \partial_{t} u ∥_{L^{\infty} (0, T; Y)} \leq M < \infty$ give the exact derivative hypothesis $\sup_{u} ∥ \partial_{t} u ∥_{L^{1} (0, T; Y)} \leq T M$ by Finite-time bounds for Banach-valued derivatives, under the Countable Choice and positive finite interval already assumed. The derivative remains valued in the local negative space; it is not identified with the exterior Dirichlet spectral negative scale.

[F4]

In [F2] define $X = H^{1 / 2} (G)$ by the restriction convention of Restriction Bessel-potential spaces on polyhedral domains, applicable to this nonempty open set with $s = 1 / 2$ . Thus its elements are restrictions of complex whole-space Bessel-potential completion classes, with norm $∥ u ∥_{X} = \inf_{U ∣_{G} = u} ∥ U ∥_{H^{1 / 2} (R^{n})}$ . This $X$ is Banach: the whole-space space is complete by Every real-order Bessel-potential completion is Hilbert, and restriction $R : H^{1 / 2} (R^{n}) \to L^{2} (G)$ is linear with $∥ R U ∥_{2} \leq ∥ U ∥_{H^{1 / 2}}$ by the restriction definition's $L^{2}$ realization. Its kernel $N$ is a linear subspace and is closed: if $U_{j} \in N$ and $U_{j} \to U$ in the whole-space norm, the bound gives $∥ R U ∥_{2} \leq ∥ U - U_{j} ∥_{H^{1 / 2}} \to 0$ . The quotient by $N$ is Banach by A quotient of a Banach space by a closed subspace is Banach, and $U + N \mapsto R U$ is a linear bijection onto $X$ with exactly the displayed quotient norm. Completeness therefore transfers to $X$ . All three cited inputs require only Countable Choice, available under [F2]. Consequently one may take this $X$ once its bounded-domain compact embedding into $L^{2} (G)$ has independently been supplied; no global exterior compact embedding is asserted here.

External input

Imported result: Simon, §8, assumption (8.1), printed p.84, and Corollary 4, first clause, printed p.85 (scanned PDF leaf 11). For Banach spaces with compatible compact $X ↪ B$ and continuous $B ↪ Y$ embeddings, a family bounded in $L^{p} (0, T; X)$ whose derivatives are bounded in $L^{1} (0, T; Y)$ is relatively compact in $L^{p} (0, T; B)$ , for $0 < T < \infty$ and $1 \leq p < \infty$ . This is an external mathematical input, not a locally reconstructed proof of the general theorem.

Application of the contract: Under the stated choice and interval hypotheses, [F1] matches Simon's Banach-triple and distributional-derivative hypotheses using Compatible compact Banach triples, Bochner spaces and bounded inclusion of value spaces and Distributional time derivatives with values in a Banach space. In the local example, [F2] supplies the Banach space $B$ by L² with the integral pairing is a Hilbert space and the Banach space $Y$ and pivot injection by The L2 pivot injects into the local negative Sobolev space, under the additional Axiom of Choice (The Axiom of Choice). For the specific fractional choice, [F4] supplies the definition and Banach property of $X$ using Restriction Bessel-potential spaces on polyhedral domains, Every real-order Bessel-potential completion is Hilbert and A quotient of a Banach space by a closed subspace is Banach. Its compact embedding is still a separate condition. With that condition, the $L^{2} (X)$ bound and the derivative bound in [F3], Finite-time bounds for Banach-valued derivatives gives the required $L^{1} (Y)$ bound. Applying the imported clause then yields relative compactness in $L^{2} (0, T; L^{2} (G))$ . Countable Choice (The Axiom of Countable Choice (AC_ω)) meets the general helper hypotheses. The general Statement itself requires exactly the displayed $L^{1} (Y)$ derivative norm, including $p = 1$ , and is not restricted to an evolution triple.

Actual source reading: In this adjudication the independent original PDF was opened online and its retained scanned leaf 11, printed pp.84–85, was visually read for (8.1) and the finite- $p$ clause of Corollary 4. The general compactness proof, surrounding intermediate proofs and earlier theorems were not reconstructed or fully checked. The separate $p = \infty$ clause is not used. The elementary closed-kernel application in [F4] is local reasoning from the declared library inputs, rather than part of the imported Simon statement.

Depends on

Used by · 2

Dependency tree · 2 levels

Each result is drawn at its shortest distance from this item. Arrows run from prerequisites to the items that use them; this item has a heavier outline. External source nodes link directly to the cited text. The view shows up to two dependency steps; open a prerequisite to continue.

External dependencies

Jacques Simon, Compact sets in the space L^p(0,T;B), Annali di Matematica Pura ed Applicata 146 (1987), 65–96 · §8, embedding assumption (8.1), printed p.84, and Corollary 4 first clause, printed p.85; scanned PDF leaf 11 (zero-based page 10)

For Banach spaces X compactly embedded in B and B continuously embedded in Y, a family bounded in L^p(0,T;X), 1<=p<infinity, whose distributional derivatives form a bounded family in L^1(0,T;Y), is relatively compact in L^p(0,T;B).

Hypotheses: 0<T<infinity; X,B,Y Banach over a fixed scalar field with injective continuous embeddings X into B into Y and X into B compact; finite p>=1; strongly measurable L^p(X) functions and distributional derivatives represented by a uniformly L^1(Y)-bounded family. No reflexivity, density or evolution-triple identification is required.

Reading limits: During this adjudication, opened the independent 17-leaf scanned PDF online and visually read the retained scan escalation-support/simon-leaf-11.png in the frozen run (zero-based PDF page 10), printed pp.84–85, for §8 embedding assumption (8.1) and Corollary 4, finite-p clause. This imports that clause without reconstructing its proof or the surrounding intermediate results and earlier compactness theorems. The separate p=infinity clause, requiring derivative exponent r>1, is not used. Independently read the declared library definition and completeness suppliers for the local restriction space; the closed-kernel argument in [F4] is a local application of those suppliers. The local compact embedding remains a separate condition.

Sources

Jacques Simon, Compact sets in the space L^p(0,T;B), Annali di Matematica Pura ed Applicata 146 (1987), 65–96 · §8, embedding assumption (8.1), printed p.84, and Corollary 4 first clause, printed p.85; scanned PDF leaf 11 (zero-based page 10)