Eigenvalue theory for the symmetric elliptic Dirichlet problem #
Evans §6.5.1, Theorem 1.
For a symmetric coercive bilinear form B on H₀¹(Ω) we build the solution operator on
L²(Ω) and apply Mathlib's spectral theorem for compact self-adjoint operators to obtain a
complete orthogonal family of eigenfunctions.
solOp B hco := ι ∘ (B♯)⁻¹ ∘ ι† : L²(Ω) →L[ℝ] L²(Ω), whereι = embL2 Ωis the Rellich embedding andB♯⁻¹is the Lax-Milgram inverse of the coercive formB.solOp_isCompact:solOpis compact, becauseιis compact (Rellich) and the rest is bounded.solOp_inner_symm:solOpis symmetric, becauseBis symmetric (soB♯andB♯⁻¹are).solOp_inner_self_nonneg:solOpis positive, from coercivity.solOp_spectral: the spectral theorem: the eigenspaces ofsolOpspanL²(Ω)(their orthogonal complement is trivial). The eigenvalues are of finite multiplicity (ContinuousLinearMap.finite_dimensional_eigenspace) and, bysolOp_eigenvalue_nonneg, nonnegative.solOp_weak_eigen: each eigenpairsolOp φ = μ φlifts to a weak eigenfunctionu ∈ H₀¹(Ω)of the elliptic operator:⟪u, v⟫_{L²} = μ B[u, v]for allv, i.e.B[u, v] = λ ⟪u, v⟫_{L²}with the elliptic eigenvalueλ = μ⁻¹. Lettingμ → 0⁺gives the Dirichlet eigenvaluesλ → +∞.
Instantiated on the Dirichlet (Poisson) form laplaceBilin, giving the eigenvalue theory of
-Δ with Dirichlet boundary data (dirichlet_spectral). The compact embedding for bounded Ω
is the single analytic input, threaded as the hypothesis IsCompactOperator (embL2 Ω)
(Rellich-Kondrachov) exactly as in Compactness.lean.
The solution operator on L²(Ω) of a coercive form B: G = ι ∘ (B♯)⁻¹ ∘ ι†, with
ι = embL2 Ω the Rellich embedding and (B♯)⁻¹ the Lax-Milgram inverse of B.
Equations
Instances For
Evaluation: solOp B hco f = embL2 Ω ((B♯)⁻¹ ((embL2 Ω)† f)).
The Riesz representative B♯ of a symmetric form is symmetric: ⟪B♯ u, v⟫ = ⟪u, B♯ v⟫.
The Lax-Milgram inverse (B♯)⁻¹ of a symmetric coercive form is symmetric.
Compactness, symmetry, positivity of the solution operator #
The solution operator is compact: it is the compact embedding ι postcomposed with the
bounded operator (B♯)⁻¹ ∘ ι†.
The solution operator is symmetric: ⟪G f, g⟫ = ⟪f, G g⟫, because (B♯)⁻¹ is symmetric
and ι, ι† are mutual adjoints.
Spectral theorem and eigenfunction correspondence #
Spectral theorem for the symmetric elliptic Dirichlet problem (Evans §6.5). Given the
Rellich compact embedding, the eigenspaces of the solution operator span L²(Ω): their
orthogonal complement is trivial. Equivalently, L²(Ω) has an orthonormal basis of
eigenfunctions of the solution operator.
Eigenfunction correspondence. Each eigenpair solOp φ = μ φ lifts to a weak eigenfunction
u ∈ H₀¹(Ω) of the elliptic operator: ι u = μ φ and ⟪u, v⟫_{L²} = μ B[u, v] for every
v ∈ H₀¹(Ω). For μ ≠ 0 this is the weak Dirichlet eigenvalue problem B[u, v] = λ ⟪u, v⟫_{L²}
with elliptic eigenvalue λ = μ⁻¹.
The eigenvalues of the solution operator are nonnegative (so the elliptic eigenvalues
λ = μ⁻¹ are positive): positivity of G forces 0 ≤ μ on any nonzero eigenvector.
Instantiation at the Dirichlet (Poisson) form -Δ #
The bilinear form of the Laplacian is symmetric.
Spectral theorem for the Dirichlet Laplacian (-Δ with Dirichlet data, Evans §6.5).
Given the test-function Poincaré bound (coercivity) and the Rellich compact embedding, the
eigenfunctions of the Dirichlet solution operator form a complete orthogonal family in L²(Ω).
Instantiation at the general symmetric divergence-form operator -Dⱼ(aᵢⱼ Dᵢ·) + c #
The principal-part form B_A is symmetric when the coefficient matrix is symmetric
(aᵢⱼ = aⱼᵢ a.e. on Ω): swap the summation order and use a symmetry plus
commutativity of the product.
Spectral theorem for the general symmetric divergence-form operator Lu = -Dⱼ(aᵢⱼ Dᵢu) + cu
with symmetric matrix A, no transport (b ≡ 0), and c ≥ 0 (Evans §6.5). Given the
test-function Poincaré bound and the Rellich compact embedding, the eigenfunctions of the
solution operator form a complete orthogonal family in L²(Ω).