CorollaryStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-6.1-sol)

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 bounded map into $H_{0}^{1}$ yields a compact $L^{2}$ operator

Statement

Assume the Axiom of Choice. Let $Ω \subset R^{n}$ be a bounded open set and $T : L^{2} (Ω) \to H_{0}^{1} (Ω)$ a bounded linear operator. Then $ι T : L^{2} (Ω) \to L^{2} (Ω)$ is compact, where $ι : H_{0}^{1} (Ω) ↪ L^{2} (Ω)$ is the inclusion. No boundary regularity of $Ω$ is needed.

Facts & Assumptions

Given: the Axiom of Choice, a bounded open set $Ω \subseteq R^{n}$ , and a bounded linear operator $T : L^{2} (Ω) \to H_{0}^{1} (Ω)$ , with $ι : H_{0}^{1} (Ω) \to L^{2} (Ω)$ the inclusion.

[F1]

Zero-boundary Rellich theorem. $W_{0}^{1, 2} (Ω) = H_{0}^{1} (Ω)$ is compactly embedded in $L^{2} (Ω)$ : every sequence bounded in $H_{0}^{1} (Ω)$ has a subsequence converging in $L^{2} (Ω)$ . (Compactness of $W_{0}^{1, p} (Ω) ↪ L^{p} (Ω)$ on bounded open sets, Compactly embedded normed spaces, The notation $H^{k}$ and the reserved zero-boundary symbol)

[F2]

Bounded operators map bounded sequences to bounded sequences. If $(f_{j})$ satisfies $∥ f_{j} ∥_{L^{2}} \leq M$ , then $∥ T f_{j} ∥_{H_{0}^{1}} \leq ∥ T ∥ M$ for the operator norm of A bounded linear operator between normed spaces. (A bounded linear operator between normed spaces)

[F3]

Compactness is the sequential extraction criterion. A bounded operator $S$ is compact exactly when the image of every bounded sequence has a convergent subsequence. (Compact linear operator, Compactly embedded normed spaces)

Proof

technique · direct

1.1F1F2given

Let $(f_{j})$ be bounded in $L^{2} (Ω)$ with $∥ f_{j} ∥_{L^{2}} \leq M$ . By [F2], $(T f_{j})$ is bounded in $H_{0}^{1} (Ω)$ , so [F1] supplies a subsequence with $T f_{j_{k}} \to g$ in $L^{2} (Ω)$ , that is, $ι T f_{j_{k}} \to g$ .

2.1F1F3step 1.1∎

Since every bounded sequence in $L^{2} (Ω)$ has an image under $ι T$ with a convergent subsequence, [F3] makes $ι T$ a compact operator. The inclusion $ι$ is bounded because $∥ u ∥_{L^{2}} \leq ∥ u ∥_{H_{0}^{1}}$ , and the Axiom of Choice is inherited through the Rellich theorem [F1].

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

29 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

John K. Hunter, Notes on Partial Differential Equations, complete 242-page 2014 notes (standard reference, not scraped)

A bounded map into H01H01​ yields a compact L2L2 operator