Dirichlet spectrum of the unit ball

Every eigenvalue statement of the chapter asks that H₀¹(Ω) have an element of nonzero L² class, which is false for a domain of measure zero and so cannot be dropped in general. On the unit ball it is discharged: EllipticPdes.Embedding.exists_norm_rellichEmbL_eq_one at q = 2 produces an element whose L² norm is one, and EllipticPdes.Embedding.coeFn_sobolevEmbL identifies that norm with the norm of the function coordinate.

dirichlet_principal_eigenpair_ball is then the principal eigenvalue theorem with no hypotheses beyond 2 < d.

Main declarations

• EllipticPdes.Sobolev.exists_embL2_ne_zero_ball: the unit ball supports a function of nonzero L² class in H₀¹.
• EllipticPdes.Sobolev.dirichlet_principal_eigenpair_ball: the principal Dirichlet eigenvalue of the unit ball, attained and positive.

References

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

theorem EllipticPdes.Sobolev.exists_embL2_ne_zero_ball {d : ℕ} (hd : 2 < d) : ∃ (V : ↥(H01 (Metric.ball 0 1))), (embL2 (Metric.ball 0 1)) V ≠ 0

Function of nonzero L² class on the unit ball. A renormalised bump has unit L² norm, and the L² class of its graph is the function it represents.

theorem EllipticPdes.Sobolev.dirichlet_principal_eigenpair_ball {d : ℕ} (hd : 2 < d) : ∃ (U : ↥(H01 (Metric.ball 0 1))), ‖(embL2 (Metric.ball 0 1)) U‖ = 1 ∧ ((laplaceBilin (Metric.ball 0 1)) U) U = principalEigenvalue (laplaceBilin (Metric.ball 0 1)) ∧ 0 < principalEigenvalue (laplaceBilin (Metric.ball 0 1)) ∧ ∀ (V : ↥(H01 (Metric.ball 0 1))), ((laplaceBilin (Metric.ball 0 1)) U) V = principalEigenvalue (laplaceBilin (Metric.ball 0 1)) * inner ℝ ((embL2 (Metric.ball 0 1)) U) ((embL2 (Metric.ball 0 1)) V)

Principal Dirichlet eigenvalue of the unit ball, with 2 < d the only hypothesis: there is a U of unit L² norm attaining the infimum of the Rayleigh quotient, the infimum is positive, and U solves the weak eigenvalue problem.