TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck pass

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.

Spectral series solution of an invertible symmetric elliptic problem

Statement

Assume the Axiom of Choice and Countable Choice. In the symmetric case of The $L^{2}$ operator associated with a symmetric elliptic form with $Ω$ nonempty bounded open, suppose $0$ is not an eigenvalue of $L$ (equivalently, by Discrete spectrum of a symmetric elliptic Dirichlet operator, no nonzero $u \in H_{0}^{1} (Ω)$ satisfies $a (u, v) = 0$ for all $v$ ; this holds in particular when $a$ is coercive on $H_{0}^{1} (Ω)$ ). Then $L : D (L) \to L^{2} (Ω)$ is bijective, and for every $f \in L^{2} (Ω)$ the unique weak solution $u \in H_{0}^{1} (Ω)$ of $a (u, v) = (f, v)_{L^{2}}$ for all $v$ is $u = L^{- 1} f = \sum_{j \geq 1} \frac{(f, e_{j})_{L^{2}}}{λ_{j}} e_{j},$ the series converging in $L^{2} (Ω)$ and in $H_{0}^{1} (Ω)$ ; moreover $u \in D (L)$ with $L u = f$ and $∥ u ∥_{L^{2}} \leq (\min_{j} ∣ λ_{j} ∣)^{- 1} ∥ f ∥_{L^{2}}$ (and $∥ u ∥_{L^{2}} \leq λ_{1}^{- 1} ∥ f ∥_{L^{2}}$ when $λ_{1} > 0$ , in particular under coercivity of $a$ ).

Facts & Assumptions

Given: the Axiom of Choice and Countable Choice; a nonempty bounded open set $Ω \subseteq R^{n}$ ; the symmetric divergence-form case with form $a$ and operator $L$ ; the eigenbasis ${e_{j}}$ and eigenvalue list $λ_{j} \to + \infty$ of the discrete spectral theorem; the hypothesis that $0$ is not an eigenvalue; and $f \in L^{2} (Ω)$ .

[F1]

Spectral series for the inverse at $λ = 0$ : the complex spectrum of the relevant complex realization is $σ (\tilde{L}) = {λ_{j}}$ , and the corollary gives the base-field inverse series for every real parameter outside this list. Since $0$ is not an eigenvalue, $L$ is bijective with bounded inverse $L^{- 1}$ , and $L^{- 1} f = \sum_{j} (f, e_{j})_{L^{2}} λ_{j}^{- 1} e_{j}$ with convergence in $L^{2} (Ω)$ and in $H_{0}^{1} (Ω)$ (Non-invertible elliptic shifts form a discrete set in the self-adjoint case, Discrete spectrum of a symmetric elliptic Dirichlet operator).

[F2]

Weak solutions: $u \in H_{0}^{1} (Ω)$ is a weak solution of the Dirichlet problem with datum $f \in L^{2} (Ω)$ exactly when $u \in D (L)$ and $L u = f$ (The $L^{2}$ operator associated with a symmetric elliptic form, Weak Dirichlet solutions for a divergence-form operator).

[F3]

Parseval: $∥ f ∥_{L^{2}}^{2} = \sum_{j} ∣ (f, e_{j})_{L^{2}} ∣^{2}$ for every $f \in L^{2} (Ω)$ , and the eigenbasis is orthonormal (Eigenbasis expansion in the form norm, Discrete spectrum of a symmetric elliptic Dirichlet operator).

[F4]

Rayleigh: if $λ_{1} > 0$ then all $λ_{j} \geq λ_{1}$ , and coercivity of $a$ with constant $α^{'} > 0$ implies $λ_{1} \geq α^{'} > 0$ and hence that $0$ is not an eigenvalue (The Rayleigh principle for the first Dirichlet eigenvalue, The $L^{2}$ operator associated with a symmetric elliptic form).

Proof

technique · direct

1.1F1given

Bijectivity and the series. The hypothesis says $0$ is not a weak eigenvalue, so $L$ is injective; since the eigenvalues of $L$ are exactly the list ${λ_{j}}$ , the resolvent corollary [F1] applies with $λ = 0$ and gives that $L$ is bijective with bounded inverse and that the inverse is the displayed series, converging in $L^{2} (Ω)$ and in $H_{0}^{1} (Ω)$ .

2.1F1F2step 1.1given

The weak solution. For $f \in L^{2} (Ω)$ put $u : = L^{- 1} f$ , which lies in $D (L)$ with $L u = f$ ; by [F2] $u$ is the unique weak solution of $a (u, v) = (f, v)_{L^{2}}$ for all $v$ , and by step 1.1 it is the series of the statement. Since $L$ is injective with range $L^{2} (Ω)$ , the weak solution is unique, so this identifies the solution set with the single class $u$ .

2.2F3step 1.1givenalgebra

The norm bound. Put $δ : = \inf_{j} ∣ λ_{j} ∣ > 0$ (positive because $λ_{j} \to + \infty$ and no $λ_{j} = 0$ ). The series of step 1.1 and Parseval [F3] give $∥ u ∥_{L^{2}}^{2} = \sum_{j} \frac{∣ (f, e_{j})_{L^{2}} ∣^{2}}{λ_{j}^{2}} \leq δ^{- 2} \sum_{j} ∣ (f, e_{j})_{L^{2}} ∣^{2} = δ^{- 2} ∥ f ∥_{L^{2}}^{2},$ that is $∥ u ∥_{L^{2}} \leq (\min_{j} ∣ λ_{j} ∣)^{- 1} ∥ f ∥_{L^{2}}$ . If $λ_{1} > 0$ all $λ_{j} \geq λ_{1} > 0$ , so $\min_{j} ∣ λ_{j} ∣ = λ_{1}$ and the sharper bound $∥ u ∥_{L^{2}} \leq λ_{1}^{- 1} ∥ f ∥_{L^{2}}$ holds.

3.1F4step 1.1step 2.1step 2.2given∎

Coercivity gives the hypothesis. If $a$ is coercive with constant $α^{'} > 0$ then $a (u, u) \geq α^{'} ∥ u ∥_{L^{2}}^{2} > 0$ for every nonzero $u$ , so $0$ cannot be a weak eigenvalue and the previous conclusions apply; by [F4] one also has $λ_{1} \geq α^{'} > 0$ , so the sharper bound of step 2.2 is available.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

61 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)
Richard S. Laugesen, Spectral Theory of Partial Differential Equations (University of Illinois lecture notes, arXiv:1203.2344, complete 120 pages) (standard reference, not scraped)
Richard S. Laugesen, Linear Analysis and Partial Differential Equations (University of Illinois, 2020, complete 158-page graduate notes) (standard reference, not scraped)