Positivity and finite multiplicity of the Dirichlet eigenvalues

The spectral theorem EllipticPdes.Sobolev.solOp_spectral produces the eigenspaces and says nothing about where the eigenvalues sit or how large the eigenspaces are. Both follow from what is already at hand.

Positivity is the Rayleigh bound: principalEigenvalue_le_of_weak_eigen places every weak eigenvalue above λ₁, and principalEigenvalue_pos places λ₁ above the coercivity constant. Finite multiplicity is the compactness of the solution operator, through Mathlib's ContinuousLinearMap.finite_dimensional_eigenspace, which the Rellich embedding supplies.

Main declarations

• EllipticPdes.Sobolev.weak_eigenvalue_pos: every weak Dirichlet eigenvalue is positive.
• EllipticPdes.Sobolev.solOp_finiteDimensional_eigenspace: each eigenspace at a nonzero eigenvalue of the solution operator is finite dimensional.
• EllipticPdes.Sobolev.dirichlet_eigenvalue_pos_of_bounded and EllipticPdes.Sobolev.dirichlet_finiteDimensional_eigenspace_of_bounded: the two at -Δ on a bounded domain, with boundedness the only hypothesis beyond the eigenpair.

References

L. C. Evans, Partial Differential Equations (2nd ed.), §6.5.1, Theorem 1.

theorem EllipticPdes.Sobolev.weak_eigenvalue_pos {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} {B : ↥(H01 Ω) →L[ℝ] ↥(H01 Ω) →L[ℝ] ℝ} (hco : IsCoercive B) (hne : ∃ (V : ↥(H01 Ω)), (embL2 Ω) V ≠ 0) {lam : ℝ} {U : ↥(H01 Ω)} (hU : U ≠ 0) (heig : ∀ (V : ↥(H01 Ω)), (B U) V = lam * inner ℝ ((embL2 Ω) U) ((embL2 Ω) V)) : 0 < lam

Every weak Dirichlet eigenvalue is positive. A nonzero weak eigenfunction has eigenvalue at least λ₁, and λ₁ exceeds the coercivity constant.

theorem EllipticPdes.Sobolev.solOp_finiteDimensional_eigenspace {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} {B : ↥(H01 Ω) →L[ℝ] ↥(H01 Ω) →L[ℝ] ℝ} (hco : IsCoercive B) (hRellich : IsCompactOperator ⇑(embL2 Ω)) {μ : ℝ} (hμ : μ ≠ 0) : FiniteDimensional ℝ ↥(Module.End.eigenspace (↑(solOp B hco)) μ)

Finite multiplicity of the eigenvalues. The eigenspace of the solution operator at a nonzero eigenvalue is finite dimensional, the operator being compact.

theorem EllipticPdes.Sobolev.dirichlet_eigenvalue_pos_of_bounded {n : ℕ} (Ω : Set (EuclideanSpace ℝ (Fin (n + 1)))) (hΩb : Bornology.IsBounded Ω) (hne : ∃ (V : ↥(H01 Ω)), (embL2 Ω) V ≠ 0) {lam : ℝ} {U : ↥(H01 Ω)} (hU : U ≠ 0) (heig : ∀ (V : ↥(H01 Ω)), ((laplaceBilin Ω) U) V = lam * inner ℝ ((embL2 Ω) U) ((embL2 Ω) V)) : 0 < lam

Positivity at -Δ on a bounded domain, with the Poincaré inequality supplying coercivity.

theorem EllipticPdes.Sobolev.dirichlet_finiteDimensional_eigenspace_of_bounded {n : ℕ} (Ω : Set (EuclideanSpace ℝ (Fin (n + 1)))) (hΩm : MeasurableSet Ω) (hΩb : Bornology.IsBounded Ω) {μ : ℝ} (hμ : μ ≠ 0) : FiniteDimensional ℝ ↥(Module.End.eigenspace (↑(solOp (laplaceBilin Ω) ⋯)) μ)

Finite multiplicity at -Δ on a bounded measurable domain.