The Dirichlet spectrum of a divergence-form elliptic operator #
For a divergence-form operator L u = -∂ⱼ(aⁱʲ ∂ᵢu) + bⁱ ∂ᵢu + c u on an open set
Ω ⊆ ℝⁿ, a real number κ is a Dirichlet eigenvalue when the homogeneous Dirichlet
problem L u = κ u in Ω, u = 0 on ∂Ω, has a nonzero weak solution: some
u ∈ H¹₀(Ω), u ≠ 0, with
a(u, v) = κ ∫_Ω u v for every v ∈ H¹₀(Ω),
where a is the energy form of L. This file develops that eigenvalue problem through the
solution operator S : L²(Ω) → L²(Ω), which sends f to the value of the weak solution of
L u = f.
S is the inverse of L under the homogeneous boundary condition, and it is the object that
carries the spectral theory: it is compact for a bounded Ω because the inclusion
H¹₀(Ω) → L²(Ω) is (Rellich--Kondrachov), it is symmetric when the energy form is, and its
nonzero eigenvalues are exactly the reciprocals of the Dirichlet eigenvalues. Mathlib's
spectral theorem for compact self-adjoint operators then applies, giving eigenvectors with dense
span in L²(Ω) and finite-dimensional eigenspaces at the nonzero eigenvalues; the eigenvalue 0
is absent because the value map H¹₀(Ω) → L²(Ω) has dense range. Assembling Hilbert bases of
the eigenspaces turns that density into an orthonormal basis of L²(Ω) of Dirichlet
eigenfunctions, in which the solution operator is diagonal.
Hypotheses, and what each result needs #
No regularity of ∂Ω is used anywhere: the boundary condition is membership in H¹₀(Ω), the
closure of C_c^∞(Ω). The hypotheses are carried separately and named at each statement.
- Coercivity of the energy form on
H¹₀(Ω)is what makes the solution operator exist at all. It also forces every Dirichlet eigenvalue to be positive, and quantitatively to be at least the coercivity constant, because theL²norm of a Sobolev jet is dominated by its graph norm. For a domain inside a ball this is the explicit Poincaré constant ofTauCeti.PDE.UniformlyEllipticOn.mul_norm_sq_le_energyFormH1_self_of_subset_ball, so the first Dirichlet eigenvalue is bounded below by the constant in the Poincaré inequality. - Boundedness of
Ωis what makes the solution operator compact, hence what gives finite-dimensional eigenspaces and the spectral theorem. It is not needed for the eigenvalue bounds. - Symmetry of the energy form is what makes the solution operator self-adjoint. It is not
an assumption on
Ωeither: with no drift and an almost everywhere symmetric principal coefficient it holds outright, byTauCeti.PDE.energyFormH1_comm_of_isSymm_ae. - Dense range of the value map
H¹₀(Ω) → L²(Ω)rules out the eigenvalue0of the solution operator: the kernel of the solution operator is exactly the orthogonal complement of its range. The density follows because the range contains all test functions and test functions are dense inL²(Ω).
The Fredholm alternative in eigenvalue language #
Reading the Fredholm alternative for a scalar mass shift through this vocabulary gives the
familiar statement: if κ is not a Dirichlet eigenvalue, then L u - κ u = f has exactly one
weak solution for every f ∈ L²(Ω), with mass coefficient written explicitly as c - κ in
TauCeti.PDE.existsUnique_isWeakSolutionDirichlet_sub_const_of_not_isDirichletEigenvalue.
The variational characterization #
The first Dirichlet eigenvalue is not only the least one: it is the minimum of the Rayleigh
quotient a(u, u) / ‖u‖²_{L²(Ω)} over H¹₀(Ω), equivalently the largest constant C for which
the Poincaré-type inequality C‖u‖²_{L²(Ω)} ≤ a(u, u) holds. The inequality itself needs
neither boundedness nor nonemptiness of Ω; boundedness together with nonemptiness makes the
minimum attained, through compactness of the solution operator and nonvanishing of the value
map.
Main declarations #
TauCeti.PDE.dirichletSolutionOperator: the solution operator onL²(Ω), withTauCeti.PDE.dirichletSolutionOperator_applyidentifying it as the value of the weak solution, andTauCeti.PDE.isCompactOperator_dirichletSolutionOperator,TauCeti.PDE.isSymmetric_dirichletSolutionOperatorandTauCeti.PDE.inner_dirichletSolutionOperator_self_nonneg.TauCeti.PDE.IsDirichletEigenvalue: the Dirichlet eigenvalue problem, withTauCeti.PDE.isDirichletEigenvalue_iff_setIntegralwriting it as an integral identity andTauCeti.PDE.isDirichletEigenvalue_iff_exists_isWeakSolutionDirichlet_sub_constmatching it with a homogeneous weak equation for the mass coefficientc - κ.TauCeti.PDE.firstDirichletEigenvalueandTauCeti.PDE.isDirichletEigenvalue_first: the least Dirichlet eigenvalue and its attainment on a nonempty bounded domain.TauCeti.PDE.pos_of_isDirichletEigenvalueandTauCeti.PDE.le_of_isDirichletEigenvalue: every Dirichlet eigenvalue is positive, and at least the coercivity constant.TauCeti.PDE.isLeast_rayleighQuotient_firstDirichletEigenvalue: the Rayleigh principle, that the first Dirichlet eigenvalue is the minimum ofa(u, u) / ‖u‖²_{L²(Ω)}, with its inequality halfTauCeti.PDE.firstDirichletEigenvalue_mul_norm_value_sq_leand its reading as the optimal Poincaré constantTauCeti.PDE.isGreatest_firstDirichletEigenvalue.TauCeti.PDE.isDirichletEigenvalue_iff_hasEigenvalue: the reciprocal correspondence with the nonzero eigenvalues of the solution operator.TauCeti.PDE.finiteDimensional_eigenspace_dirichletSolutionOperatorandTauCeti.PDE.orthogonalComplement_iSup_eigenspaces_dirichletSolutionOperator_eq_bot: the eigenspaces are finite dimensional and the eigenfunctions span a dense subspace ofL²(Ω).TauCeti.PDE.exists_hilbertBasis_forall_isDirichletEigenvalue: the Dirichlet eigenfunctions form an orthonormal basis ofL²(Ω), and the Dirichlet problem is solved in it by the eigenfunction expansion.TauCeti.PDE.UniformlyEllipticOn.le_of_isDirichletEigenvalue_of_subset_ballandTauCeti.PDE.le_of_isDirichletEigenvalue_laplacian_of_subset_ball: the explicit lower bound on the Dirichlet spectrum of a domain inside a ball, and its-Δcase1/(2(4R² + 1)) ≤ κ.
References #
L. C. Evans, Partial Differential Equations, Section 6.5 (eigenvalues and eigenfunctions); D. Gilbarg and N. Trudinger, Elliptic Partial Differential Equations of Second Order, Chapter 8, Section 8.12; H. Brezis, Functional Analysis, Sobolev Spaces and Partial Differential Equations, Section 9.8.
Shortcut normed group instance on H¹₀(Ω), needed by the inherited Hilbert structure.
Instances For
Shortcut inner-product instance on H¹₀(Ω).
Instances For
The solution operator on L²(Ω) #
The solution operator of the Dirichlet problem: the map sending f ∈ L²(Ω) to the
value of the unique weak solution of L u = f in Ω, u = 0 on ∂Ω. It inverts the
Dirichlet problem, and it is the operator whose spectrum carries the Dirichlet eigenvalue
problem; TauCeti.PDE.dirichletSolutionOperator_apply identifies its value with the
Lax--Milgram solution.
Equations
- TauCeti.PDE.dirichletSolutionOperator hcoeff hcoercive = hcoercive.formSolutionOperator TauCeti.W1p0.valueL
Instances For
The abstract solution map of the energy form along the value inclusion is the weak solution of the Dirichlet problem.
The solution operator returns the value component of the weak solution.
The solution operator is compact on a bounded domain, by Rellich--Kondrachov.
The solution operator is self-adjoint for a symmetric energy form. With no drift and an
almost everywhere symmetric principal coefficient the symmetry hypothesis is supplied by
TauCeti.PDE.energyFormH1_comm_of_isSymm_ae.
The solution operator is positive semidefinite: its quadratic form is the energy of the solution it produces.
Dirichlet eigenvalues #
A Dirichlet eigenvalue of the divergence-form operator
L u = -∂ⱼ(aⁱʲ ∂ᵢu) + bⁱ ∂ᵢu + c u on Ω: a real number κ for which the homogeneous
Dirichlet problem L u = κ u has a nonzero weak solution u ∈ H¹₀(Ω), that is
a(u, v) = κ ∫_Ω u v for every v ∈ H¹₀(Ω).
The boundary condition is membership in H¹₀(Ω), so no regularity of ∂Ω enters, and nothing
is assumed about the coefficients here; each theorem below names the hypotheses it uses.
TauCeti.PDE.isDirichletEigenvalue_iff_setIntegral writes the condition out as an integral
identity.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Being a Dirichlet eigenvalue, written out as the integral identity
a(u, v) = κ ∫_Ω u v.
A Dirichlet eigenvalue is exactly a scalar mass shift with a nonzero homogeneous weak solution.
A Dirichlet eigenvalue is exactly a constant shift of the mass coefficient for which the homogeneous Dirichlet equation has a nonzero weak solution.
Every Dirichlet eigenvalue of a coercive form is positive. Coercivity of the energy
form on H¹₀(Ω) is the only hypothesis: neither boundedness nor any regularity of Ω is
needed.
The Dirichlet spectrum lies above the coercivity constant. Any diagonal lower bound
C‖w‖²_{H¹} ≤ a(w, w) on H¹₀(Ω) bounds every Dirichlet eigenvalue below by C. The C
available on a bounded domain is a Poincaré constant, so this says that the first Dirichlet
eigenvalue is at least the Poincaré constant.
The first Dirichlet eigenvalue is the reciprocal of the norm of the Dirichlet solution
operator. On a nonempty bounded domain with symmetric energy form this value is attained and is
the least Dirichlet eigenvalue; see TauCeti.PDE.isDirichletEigenvalue_first and
TauCeti.PDE.firstDirichletEigenvalue_le.
Equations
- TauCeti.PDE.firstDirichletEigenvalue hcoeff hcoercive = ‖TauCeti.PDE.dirichletSolutionOperator hcoeff hcoercive‖⁻¹
Instances For
The first Dirichlet eigenvalue is the reciprocal of the operator norm of the Dirichlet solution operator.
Existence of a Dirichlet eigenvalue. On a nonempty bounded domain with a symmetric energy form, the Dirichlet eigenvalue problem has a nonzero weak solution.
The Dirichlet eigenvalues are the reciprocals of the nonzero eigenvalues of the solution
operator. This is the passage that turns the eigenvalue problem for the unbounded operator
L into one for a bounded — and, on a bounded domain, compact — operator on L²(Ω).
The first Dirichlet eigenvalue is attained on a nonempty bounded domain with symmetric energy form.
The first Dirichlet eigenvalue is positive.
The first Dirichlet eigenvalue is no greater than any Dirichlet eigenvalue.
A diagonal lower bound for the energy form bounds the first Dirichlet eigenvalue below.
The Rayleigh principle #
The quantity firstDirichletEigenvalue is a Poincaré constant for the energy form:
κ₁ ‖u‖²_{L²(Ω)} ≤ a(u, u) for every u ∈ H¹₀(Ω),
and by TauCeti.PDE.isGreatest_firstDirichletEigenvalue it is the largest constant for
which this holds. Neither boundedness nor nonemptiness of Ω is needed here: only coercivity,
which makes the solution operator exist, and symmetry, which gives the energy form its
Cauchy--Schwarz inequality.
The Rayleigh principle for the Dirichlet problem. On a nonempty bounded domain with a symmetric energy form, the first Dirichlet eigenvalue is the minimum of the Rayleigh quotient
a(u, u) / ‖u‖²_{L²(Ω)}
over the u ∈ H¹₀(Ω) with nonzero L² value; the minimum is attained at an eigenfunction.
Boundedness of Ω enters only through the attainment, by way of Rellich--Kondrachov: the
inequality alone is TauCeti.PDE.firstDirichletEigenvalue_mul_norm_value_sq_le.
The quantity firstDirichletEigenvalue is the optimal Poincaré constant of the energy
form: it is the greatest C with C ‖u‖²_{L²(Ω)} ≤ a(u, u) for all u ∈ H¹₀(Ω). This is the
Rayleigh principle read as an inequality, and it shows that the bound
TauCeti.PDE.firstDirichletEigenvalue_mul_norm_value_sq_le is optimal. Boundedness of Ω is
not needed because this optimal-constant characterization does not assert attainment.
The eigenspaces of the Dirichlet problem are finite dimensional on a bounded domain.
The spectral theorem for the Dirichlet problem: on a bounded domain and for a symmetric
energy form, the eigenvectors of the solution operator span a dense subspace of L²(Ω).
The Dirichlet eigenfunctions span a dense subspace of L²(Ω). The value map
H¹₀(Ω) → L²(Ω) has dense range, so the eigenvalue 0 of the solution operator is absent and
the eigenspaces at nonzero eigenvalues already have trivial orthogonal complement.
The Dirichlet eigenfunctions form an orthonormal basis of L²(Ω). On a bounded domain
and for a symmetric energy form, L²(Ω) has an orthonormal basis whose vectors are the values of
weak solutions u ∈ H¹₀(Ω) of L u = κ u at positive Dirichlet eigenvalues κ, and the
L²(Ω) value of the weak solution to the Dirichlet problem has the eigenfunction expansion
W1p.value u = ∑ κ⁻¹ ⟪eₖ, f⟫ eₖ. No regularity of ∂Ω enters, and L²(Ω) is not assumed
separable, so the basis is indexed by a set of functions as in exists_hilbertBasis.
The Fredholm alternative in eigenvalue language. On a bounded domain, if κ is not a
Dirichlet eigenvalue then L u - κ u = f in Ω, u = 0 on ∂Ω, has exactly one weak solution
for every f ∈ L²(Ω).
The Dirichlet spectrum of a domain inside a ball #
A lower bound for the Dirichlet spectrum of a domain inside a ball. For
Ω ⊆ B(z, R) ⊆ ℝ^{n+1} with a uniformly elliptic principal part, a drift bounded by β, a
bounded nonnegative mass coefficient and the smallness condition 2βR < λ, every Dirichlet
eigenvalue satisfies
(λ² - 4β²R²)/(2λ(4R² + 1)) ≤ κ.
The constant is the Poincaré constant of the ball, which is positive under the smallness
condition, so in particular the Dirichlet spectrum is bounded away from 0.
The Dirichlet spectrum of -Δ on a domain inside a ball. For
Ω ⊆ B(z, R) ⊆ ℝ^{n+1}, every κ for which -Δu = κu in Ω, u = 0 on ∂Ω, has a nonzero
weak solution satisfies 1/(2(4R² + 1)) ≤ κ; in particular the first Dirichlet eigenvalue of
-Δ is positive. The bound is the Poincaré constant of the ball, not the sharp eigenvalue.
Every Dirichlet eigenvalue of -Δ is positive on a domain inside a ball.