LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge 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.

The shifted solution operator is compact on $L^{2}$

Statement

Assume the Axiom of Choice, inherited through the compact-embedding supplier named below, together with Countable Choice. Let $Ω \subseteq R^{n}$ be open and bounded, and let $K_{μ}$ be the shifted solution operator of The shifted elliptic solution operator for a fixed $μ \geq β$ . Then $K_{μ}$ , regarded as an operator on $L^{2} (Ω)$ , is compact: $∥ K_{μ} f ∥_{H_{0}^{1}} \leq α^{- 1} ∥ f ∥_{L^{2}}$ (The Lax--Milgram solution operator has norm at most $1 / α$ ) and $H_{0}^{1} (Ω) ↪ L^{2} (Ω)$ is compact (Compactness of $W_{0}^{1, p} (Ω) ↪ L^{p} (Ω)$ on bounded open sets at $p = 2$ ), so $K_{μ}$ maps bounded subsets of $L^{2} (Ω)$ to relatively compact subsets of $L^{2} (Ω)$ . No regularity of $\partial Ω$ is assumed.

Facts & Assumptions

Given: the Axiom of Choice and Countable Choice; a bounded open set $Ω \subseteq R^{n}$ ; a fixed $μ \geq β$ ; the shifted solution operator $K_{μ} : L^{2} (Ω) \to H_{0}^{1} (Ω)$ with coercivity constant $α = θ / 2$ .

[F1]

$K_{μ}$ is well defined and linear, and for every $f \in L^{2} (Ω)$ one has $∥ K_{μ} f ∥_{H_{0}^{1}} \leq α^{- 1} ∥ f ∥_{L^{2}}$ (The shifted elliptic solution operator, The Lax--Milgram solution operator has norm at most $1 / α$ ).

[F2]

$H_{0}^{1} (Ω) = W_{0}^{1, 2} (Ω)$ , and for bounded open $Ω$ the inclusion $W_{0}^{1, 2} (Ω) ↪ L^{2} (Ω)$ is compact: 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, Zero-boundary Sobolev space as a norm closure, Integer-order Sobolev spaces and their norms, The space $L^{p} (μ)$ as the quotient by null functions).

[F3]

Compositions: if $T : X \to Y$ is compact and $B : Z \to X$ is bounded linear, then $T \circ B : Z \to Y$ is compact (Compositions with a compact operator are compact, Compact linear operator).

Proof

technique · direct

1.1F1given

The map $K_{μ} : L^{2} (Ω) \to H_{0}^{1} (Ω)$ is linear and bounded with operator bound $∥ K_{μ} ∥ \leq α^{- 1}$ by [F1], so it maps bounded subsets of $L^{2} (Ω)$ to bounded subsets of $H_{0}^{1} (Ω)$ .

1.2F2given

The inclusion $ι : H_{0}^{1} (Ω) \to L^{2} (Ω)$ is compact by [F2], because $Ω$ is bounded and open and $p = 2$ is admissible.

2.1F3step 1.1step 1.2given∎

The $L^{2}$ realization of $K_{μ}$ is the composite $ι \circ K_{μ}$ . By step 1.1 the first factor is bounded linear and by step 1.2 the second is compact, so [F3] makes the composite compact; hence bounded subsets of $L^{2} (Ω)$ are mapped into relatively compact subsets of $L^{2} (Ω)$ . No boundary regularity was used, and the Axiom of Choice is inherited through the Rellich supplier [F2].

Depends on

Used by

Dependency tree · two levels

54 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 (UC Davis, revised 18 June 2014, complete 242-page notes) (standard reference, not scraped)
Gerald Teschl, Partial Differential Equations: From Classical to Modern (2025 archived author manuscript, complete 392 pages) (standard reference, not scraped)
Haim Brezis, Functional Analysis, Sobolev Spaces and Partial Differential Equations (Springer Universitext, 2011, complete 614-page text) (standard reference, not scraped)

The shifted solution operator is compact on L2L2