TheoremStatement: 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 first Dirichlet eigenvalue is monotone under domain inclusion

Statement

Assume the Axiom of Choice and Countable Choice. Let $Ω_{1} \subseteq Ω_{2} \subseteq R^{n}$ be nonempty bounded open sets, let $a^{i j}$ be measurable, essentially bounded and uniformly elliptic on $Ω_{2}$ with $a^{i j} = \overline{a^{j i}}$ , and for $i = 1, 2$ let $a^{(i)}$ be the principal Dirichlet form $a^{(i)} (u, v) = \int_{Ω_{i}} a^{i j} D_{j} u \overline{D_{i} v} d x$ on $H_{0}^{1} (Ω_{i})$ ; the model case $a^{i j} = δ^{i j}$ is the Dirichlet Laplacian. Let $λ_{k} (Ω_{i})$ be the eigenvalues of the corresponding symmetric elliptic Dirichlet operator (Discrete spectrum of a symmetric elliptic Dirichlet operator) . Then $λ_{k} (Ω_{2}) \leq λ_{k} (Ω_{1}) for every k \geq 1,$ in particular $λ_{1} (Ω_{2}) \leq λ_{1} (Ω_{1})$ : making the domain smaller raises the Dirichlet frequencies. The mechanism is that extension by zero maps $H_{0}^{1} (Ω_{1})$ isometrically into $H_{0}^{1} (Ω_{2})$ for the energy form and preserves the $L^{2}$ norm (Zero extension of W_0^{1,p} has no boundary derivative), so every $k$ -dimensional competitor in $H_{0}^{1} (Ω_{1})$ is a competitor in $H_{0}^{1} (Ω_{2})$ with the same Rayleigh quotient.

Facts & Assumptions

Given: the Axiom of Choice and Countable Choice; nonempty bounded open sets $Ω_{1} \subseteq Ω_{2} \subseteq R^{n}$ ; Hermitian uniformly elliptic coefficients $a^{i j}$ on $Ω_{2}$ ; the principal forms $a^{(1)}$ on $H_{0}^{1} (Ω_{1})$ and $a^{(2)}$ on $H_{0}^{1} (Ω_{2})$ ; and $k \geq 1$ .

[F1]

Zero extension: the extension operator $E$ sending a class $u \in W_{0}^{1, 2} (Ω_{1})$ to its zero extension is linear and isometric for the Sobolev norm, with weak derivatives the zero extensions of the weak derivatives (Zero extension of W_0^{1,p} has no boundary derivative, Zero-boundary Sobolev space as a norm closure, Integer-order Sobolev spaces and their norms).

[F2]

Because $Ω_{1} \subseteq Ω_{2}$ , the inclusion $C_{c}^{\infty} (Ω_{1}) \subseteq C_{c}^{\infty} (Ω_{2})$ induces $E (H_{0}^{1} (Ω_{1})) \subseteq H_{0}^{1} (Ω_{2})$ , and for $u \in H_{0}^{1} (Ω_{1})$ the integrals of the coefficient form over $Ω_{2}$ see only $Ω_{1}$ : $a^{(2)} (E u, E v) = a^{(1)} (u, v)$ and $∥ E u ∥_{L^{2} (Ω_{2})} = ∥ u ∥_{L^{2} (Ω_{1})}$ (Uniformly elliptic divergence-form operators and their sesquilinear forms, The $L^{2}$ operator associated with a symmetric elliptic form, Zero-boundary Sobolev space as a norm closure).

[F3]

Courant--Fischer: for $i = 1, 2$ and every $k \geq 1$ , $λ_{k} (Ω_{i}) = \min {\max_{u \in S ∖ {0}} a^{(i)} (u, u) / ∥ u ∥_{L^{2} (Ω_{i})}^{2} : S \subseteq H_{0}^{1} (Ω_{i}), \dim S = k}$ , the extrema being attained (The Courant-Fischer min-max principle for elliptic eigenvalues, Discrete spectrum of a symmetric elliptic Dirichlet operator, The Rayleigh principle for the first Dirichlet eigenvalue).

Proof

technique · direct

1.1F1F2givenalgebra

Isometry of the extension. By [F1] the map $E$ is linear and isometric for the Sobolev norm, and by [F2] its image lies in $H_{0}^{1} (Ω_{2})$ and the coefficient form and $L^{2}$ norm are preserved: for every $u \in H_{0}^{1} (Ω_{1})$ , $a^{(2)} (E u, E u) = a^{(1)} (u, u), ∥ E u ∥_{L^{2} (Ω_{2})}^{2} = ∥ u ∥_{L^{2} (Ω_{1})}^{2} .$ In particular the Rayleigh quotients agree, $a^{(2)} (E u, E u) / ∥ E u ∥_{L^{2} (Ω_{2})}^{2} = a^{(1)} (u, u) / ∥ u ∥_{L^{2} (Ω_{1})}^{2}$ for $u \neq 0$ .

2.1F3step 1.1givenalgebra∎

Min-max comparison. Fix $k \geq 1$ and let $S_{i}$ be the family of $k$ -dimensional subspaces of $H_{0}^{1} (Ω_{i})$ ; by [F3], $λ_{k} (Ω_{i}) = \min_{S \in S_{i}} \max_{u \in S ∖ {0}} Q_{i} (u)$ with $Q_{i}$ the corresponding Rayleigh quotient. The extension $E$ maps $S_{1}$ into $S_{2}$ (linear isometry preserves dimension), and the quotients agree on corresponding vectors by step 1.1, so $λ_{k} (Ω_{2}) \leq \min_{S \in S_{1}} \max_{u \in S ∖ {0}} Q_{2} (E u) = \min_{S \in S_{1}} \max_{u \in S ∖ {0}} Q_{1} (u) = λ_{k} (Ω_{1}),$ the inequality holding because the minimum over the larger family $S_{2}$ is at most the minimum over the restricted family $E (S_{1})$ . This proves the monotonicity $λ_{k} (Ω_{2}) \leq λ_{k} (Ω_{1})$ for every $k$ ; the case $k = 1$ is the statement about the first Dirichlet eigenvalue.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

57 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

Leon Simon, Lectures on Partial Differential Equations (Stanford, complete 223-page author scan) (standard reference, not scraped)
Richard S. Laugesen, Spectral Theory of Partial Differential Equations (University of Illinois lecture notes, arXiv:1203.2344, complete 120 pages) (standard reference, not scraped)
John K. Hunter, Notes on Partial Differential Equations (UC Davis, revised 18 June 2014, complete 242-page notes) (standard reference, not scraped)