Variational characterisation of the principal eigenvalue

EllipticPdes.Sobolev.solOp_spectral produces the Dirichlet eigenvalues from the spectral theorem for the compact self-adjoint solution operator, one eigenvalue at a time and with no formula for any of them. This file gives the first eigenvalue a formula: it is the infimum of the Rayleigh quotient

λ₁ = inf { B[U, U] : U ∈ H₀¹(Ω), ‖U‖_{L²(Ω)} = 1 },

the infimum is attained, and a minimiser is a weak eigenfunction at that eigenvalue. Every weak eigenvalue of B is at least λ₁, so the name is the theorem.

The proof is the direct method in the abstract setting. Coercivity bounds a minimising sequence in H₀¹(Ω), EllipticPdes.Analysis.exists_weakLimit extracts a weak limit, and the Rellich compact embedding embL2 Ω takes the constraint to that limit along a further subsequence. Weak lower semicontinuity of the form is the expansion of 0 ≤ B[Uₖ - w, Uₖ - w] together with B[Uₖ, w] → B[w, w], which needs symmetry and nothing else. The Euler-Lagrange step is a one-variable argument: t ↦ B[U + tV, U + tV] - λ₁‖U + tV‖²_{L²} is a quadratic that vanishes at t = 0 and is nonnegative everywhere, so its linear coefficient vanishes.

EllipticPdes.Embedding.exists_minimiser_of_lt runs the same method at a subcritical L^q constraint, where the compactness comes from rellichEmbL_isCompact_of_lt. The two files differ in which compact embedding does the work and in whether the constraint is quadratic; at q = 2 the constraint is quadratic and the minimiser satisfies a linear equation, which is this file.

Main declarations

• EllipticPdes.Sobolev.principalEigenvalue: the infimum of the Rayleigh quotient.
• EllipticPdes.Sobolev.principalEigenvalue_mul_norm_sq_le: λ₁‖U‖²_{L²} ≤ B[U, U] for every U, the Rayleigh quotient bound off the constraint set.
• EllipticPdes.Sobolev.exists_rayleigh_minimiser: the infimum is attained.
• EllipticPdes.Sobolev.rayleigh_euler_lagrange: a minimiser is a weak eigenfunction.
• EllipticPdes.Sobolev.exists_principal_eigenpair: the two previous statements combined.
• EllipticPdes.Sobolev.principalEigenvalue_le_of_weak_eigen: no weak eigenvalue is smaller.
• EllipticPdes.Sobolev.dirichlet_principal_eigenpair: the instance at -Δ on a bounded measurable domain, with the compact embedding discharged by embL2_isCompact.

References

L. C. Evans, Partial Differential Equations (2nd ed.), §6.5.1, Theorem 2; James Guo, Partial Differential Equations, Section IX.1.

The Rayleigh quotient and its infimum

def EllipticPdes.Sobolev.rayleighSphere {d : ℕ} (Ω : Set (EuclideanSpace ℝ (Fin d))) : Set ↥(H01 Ω)

The unit L² sphere of H₀¹(Ω), the constraint set of the Rayleigh problem.

Equations

• EllipticPdes.Sobolev.rayleighSphere Ω = {U : ↥(EllipticPdes.Sobolev.H01 Ω) | ‖(EllipticPdes.Sobolev.embL2 Ω) U‖ = 1}

def EllipticPdes.Sobolev.rayleighValues {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (B : ↥(H01 Ω) →L[ℝ] ↥(H01 Ω) →L[ℝ] ℝ) : Set ℝ

The values a bilinear form takes on the unit L² sphere.

Equations

• EllipticPdes.Sobolev.rayleighValues B = (fun (U : ↥(EllipticPdes.Sobolev.H01 Ω)) => (B U) U) '' EllipticPdes.Sobolev.rayleighSphere Ω

noncomputable def EllipticPdes.Sobolev.principalEigenvalue {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (B : ↥(H01 Ω) →L[ℝ] ↥(H01 Ω) →L[ℝ] ℝ) : ℝ

Principal eigenvalue of a symmetric coercive form on H₀¹(Ω): the infimum of the Rayleigh quotient B[U, U] over the functions of unit L² norm.

Equations

• EllipticPdes.Sobolev.principalEigenvalue B = sInf (EllipticPdes.Sobolev.rayleighValues B)

theorem EllipticPdes.Sobolev.nonneg_of_isCoercive {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} {B : ↥(H01 Ω) →L[ℝ] ↥(H01 Ω) →L[ℝ] ℝ} (hco : IsCoercive B) (U : ↥(H01 Ω)) : 0 ≤ (B U) U

A coercive form is positive semidefinite.

theorem EllipticPdes.Sobolev.rayleighSphere_nonempty {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (hne : ∃ (V : ↥(H01 Ω)), (embL2 Ω) V ≠ 0) : (rayleighSphere Ω).Nonempty

The constraint set is inhabited as soon as some element has a nonzero L² class: rescale.

theorem EllipticPdes.Sobolev.rayleighValues_bddBelow {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} {B : ↥(H01 Ω) →L[ℝ] ↥(H01 Ω) →L[ℝ] ℝ} (hco : IsCoercive B) : BddBelow (rayleighValues B)

Positive semidefiniteness bounds the Rayleigh values below by zero.

theorem EllipticPdes.Sobolev.principalEigenvalue_le {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} {B : ↥(H01 Ω) →L[ℝ] ↥(H01 Ω) →L[ℝ] ℝ} (hco : IsCoercive B) {U : ↥(H01 Ω)} (hU : ‖(embL2 Ω) U‖ = 1) : principalEigenvalue B ≤ (B U) U

The infimum is a lower bound on the constraint set.

theorem EllipticPdes.Sobolev.principalEigenvalue_mul_norm_sq_le {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} {B : ↥(H01 Ω) →L[ℝ] ↥(H01 Ω) →L[ℝ] ℝ} (hco : IsCoercive B) (U : ↥(H01 Ω)) : principalEigenvalue B * ‖(embL2 Ω) U‖ ^ 2 ≤ (B U) U

Rayleigh bound off the constraint set: λ₁‖U‖²_{L²} ≤ B[U, U] for every U. On the constraint set this is the definition of the infimum, and elsewhere it follows by rescaling.

theorem EllipticPdes.Sobolev.le_principalEigenvalue_of_coercive {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} {B : ↥(H01 Ω) →L[ℝ] ↥(H01 Ω) →L[ℝ] ℝ} (hne : ∃ (V : ↥(H01 Ω)), (embL2 Ω) V ≠ 0) {C : ℝ} (hC : 0 < C) (hcoer : ∀ (U : ↥(H01 Ω)), C * ‖U‖ * ‖U‖ ≤ (B U) U) : C ≤ principalEigenvalue B

Coercivity bounds the principal eigenvalue below by the coercivity constant: on the constraint set 1 = ‖U‖_{L²} ≤ ‖U‖_{H₀¹}, so C ≤ C‖U‖² ≤ B[U, U].

theorem EllipticPdes.Sobolev.principalEigenvalue_pos {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} {B : ↥(H01 Ω) →L[ℝ] ↥(H01 Ω) →L[ℝ] ℝ} (hco : IsCoercive B) (hne : ∃ (V : ↥(H01 Ω)), (embL2 Ω) V ≠ 0) : 0 < principalEigenvalue B

The principal eigenvalue of a coercive form is positive.

The Euler-Lagrange equation

theorem EllipticPdes.Sobolev.eq_zero_of_quadratic_nonneg {a b : ℝ} (h : ∀ (t : ℝ), 0 ≤ 2 * t * b + t ^ 2 * a) : b = 0

A quadratic in t that vanishes at t = 0 and is nonnegative everywhere has no linear term.

theorem EllipticPdes.Sobolev.rayleigh_euler_lagrange {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} {B : ↥(H01 Ω) →L[ℝ] ↥(H01 Ω) →L[ℝ] ℝ} (hco : IsCoercive B) (hsymm : ∀ (U V : ↥(H01 Ω)), (B U) V = (B V) U) {U : ↥(H01 Ω)} (hU : ‖(embL2 Ω) U‖ = 1) (hmin : (B U) U = principalEigenvalue B) (V : ↥(H01 Ω)) : (B U) V = principalEigenvalue B * inner ℝ ((embL2 Ω) U) ((embL2 Ω) V)

Euler-Lagrange equation of the Rayleigh problem. A minimiser on the unit L² sphere is a weak eigenfunction at the principal eigenvalue: B[U, V] = λ₁⟪U, V⟫_{L²} for every V.

The Rayleigh problem under a further constraint

def EllipticPdes.Sobolev.rayleighValuesOn {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (B : ↥(H01 Ω) →L[ℝ] ↥(H01 Ω) →L[ℝ] ℝ) (S : Set ↥(H01 Ω)) : Set ℝ

The values a form takes on the unit L² sphere inside a set S.

Equations

• EllipticPdes.Sobolev.rayleighValuesOn B S = (fun (U : ↥(EllipticPdes.Sobolev.H01 Ω)) => (B U) U) '' (EllipticPdes.Sobolev.rayleighSphere Ω ∩ S)

noncomputable def EllipticPdes.Sobolev.eigenvalueOn {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (B : ↥(H01 Ω) →L[ℝ] ↥(H01 Ω) →L[ℝ] ℝ) (S : Set ↥(H01 Ω)) : ℝ

The infimum of the Rayleigh quotient over the unit L² sphere inside S. Taking S to be the vectors L²-orthogonal to the earlier eigenfunctions gives the later eigenvalues.

Equations

• EllipticPdes.Sobolev.eigenvalueOn B S = sInf (EllipticPdes.Sobolev.rayleighValuesOn B S)

theorem EllipticPdes.Sobolev.rayleighValuesOn_univ {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} {B : ↥(H01 Ω) →L[ℝ] ↥(H01 Ω) →L[ℝ] ℝ} : rayleighValuesOn B Set.univ = rayleighValues B

With no constraint the values are those of the whole sphere.

theorem EllipticPdes.Sobolev.eigenvalueOn_univ {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} {B : ↥(H01 Ω) →L[ℝ] ↥(H01 Ω) →L[ℝ] ℝ} : eigenvalueOn B Set.univ = principalEigenvalue B

With no constraint the infimum is the principal eigenvalue.

theorem EllipticPdes.Sobolev.rayleighValuesOn_bddBelow {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} {B : ↥(H01 Ω) →L[ℝ] ↥(H01 Ω) →L[ℝ] ℝ} (hco : IsCoercive B) (S : Set ↥(H01 Ω)) : BddBelow (rayleighValuesOn B S)

Positive semidefiniteness bounds the constrained values below by zero.

theorem EllipticPdes.Sobolev.eigenvalueOn_le {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} {B : ↥(H01 Ω) →L[ℝ] ↥(H01 Ω) →L[ℝ] ℝ} (hco : IsCoercive B) {S : Set ↥(H01 Ω)} {U : ↥(H01 Ω)} (hU : ‖(embL2 Ω) U‖ = 1) (hUS : U ∈ S) : eigenvalueOn B S ≤ (B U) U

The constrained infimum is a lower bound on the constrained sphere.

theorem EllipticPdes.Sobolev.principalEigenvalue_le_eigenvalueOn {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} {B : ↥(H01 Ω) →L[ℝ] ↥(H01 Ω) →L[ℝ] ℝ} (hco : IsCoercive B) {S : Set ↥(H01 Ω)} (hne : (rayleighSphere Ω ∩ S).Nonempty) : principalEigenvalue B ≤ eigenvalueOn B S

Tightening the constraint raises the infimum.

Existence of a minimiser

theorem EllipticPdes.Sobolev.exists_rayleigh_minimiser_on {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} {B : ↥(H01 Ω) →L[ℝ] ↥(H01 Ω) →L[ℝ] ℝ} (hco : IsCoercive B) (hsymm : ∀ (U V : ↥(H01 Ω)), (B U) V = (B V) U) (hRellich : IsCompactOperator ⇑(embL2 Ω)) {S : Set ↥(H01 Ω)} (hSclosed : ∀ (u : ℕ → ↥(H01 Ω)) (w : ↥(H01 Ω)), (∀ (k : ℕ), u k ∈ S) → (∀ (v : ↥(H01 Ω)), Filter.Tendsto (fun (k : ℕ) => inner ℝ (u k) v) Filter.atTop (nhds (inner ℝ w v))) → w ∈ S) (hne : (rayleighSphere Ω ∩ S).Nonempty) : ∃ (U : ↥(H01 Ω)), ‖(embL2 Ω) U‖ = 1 ∧ U ∈ S ∧ (B U) U = eigenvalueOn B S

Attainment of the infimum of the Rayleigh quotient over a weakly closed set. Coercivity bounds a minimising sequence, weak compactness supplies a limit, the constraint S passes to that limit by hypothesis, and the Rellich compact embedding takes the unit L² norm to it.

theorem EllipticPdes.Sobolev.exists_rayleigh_minimiser {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} {B : ↥(H01 Ω) →L[ℝ] ↥(H01 Ω) →L[ℝ] ℝ} (hco : IsCoercive B) (hsymm : ∀ (U V : ↥(H01 Ω)), (B U) V = (B V) U) (hRellich : IsCompactOperator ⇑(embL2 Ω)) (hne : ∃ (V : ↥(H01 Ω)), (embL2 Ω) V ≠ 0) : ∃ (U : ↥(H01 Ω)), ‖(embL2 Ω) U‖ = 1 ∧ (B U) U = principalEigenvalue B

Attainment of the infimum of the Rayleigh quotient. The unconstrained case.

theorem EllipticPdes.Sobolev.exists_principal_eigenpair {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} {B : ↥(H01 Ω) →L[ℝ] ↥(H01 Ω) →L[ℝ] ℝ} (hco : IsCoercive B) (hsymm : ∀ (U V : ↥(H01 Ω)), (B U) V = (B V) U) (hRellich : IsCompactOperator ⇑(embL2 Ω)) (hne : ∃ (V : ↥(H01 Ω)), (embL2 Ω) V ≠ 0) : ∃ (U : ↥(H01 Ω)), ‖(embL2 Ω) U‖ = 1 ∧ (B U) U = principalEigenvalue B ∧ ∀ (V : ↥(H01 Ω)), (B U) V = principalEigenvalue B * inner ℝ ((embL2 Ω) U) ((embL2 Ω) V)

Principal eigenpair. For a symmetric coercive form with the Rellich compact embedding there is a U of unit L² norm attaining the infimum of the Rayleigh quotient, and it solves the weak eigenvalue problem at that value.

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

Minimality of the principal eigenvalue. Any nonzero weak eigenfunction has eigenvalue at least λ₁. Coercivity rules out a nonzero element with vanishing L² class, so the Rayleigh bound applies.

The Dirichlet Laplacian on a bounded measurable domain

theorem EllipticPdes.Sobolev.dirichlet_principal_eigenpair {d : ℕ} (Ω : Set (EuclideanSpace ℝ (Fin d))) (hΩm : MeasurableSet Ω) (hΩb : Bornology.IsBounded Ω) (CP : ℝ) (hCP : 0 ≤ CP) (hbase : ∀ {φ : EuclideanSpace ℝ (Fin d) → ℝ} (h : IsTestFn Ω φ), ‖h.testGraph.ofLp 0‖ ^ 2 ≤ CP * ∑ i : Fin d, ‖h.testGraph.ofLp i.succ‖ ^ 2) (hne : ∃ (V : ↥(H01 Ω)), (embL2 Ω) V ≠ 0) : ∃ (U : ↥(H01 Ω)), ‖(embL2 Ω) U‖ = 1 ∧ ((laplaceBilin Ω) U) U = principalEigenvalue (laplaceBilin Ω) ∧ ∀ (V : ↥(H01 Ω)), ((laplaceBilin Ω) U) V = principalEigenvalue (laplaceBilin Ω) * inner ℝ ((embL2 Ω) U) ((embL2 Ω) V)

Principal Dirichlet eigenvalue of -Δ on a bounded measurable domain, with the compact embedding discharged by embL2_isCompact. The eigenvalue of -Δ itself is λ₁ - 1, since the graph norm on H₀¹(Ω) includes the function coordinate: the identity below reads ∫ ∇u · ∇v = (λ₁ - 1) ∫ u v once ⟪U, V⟫_{H₀¹} is split off.

theorem EllipticPdes.Sobolev.dirichlet_poincare_sharp {d : ℕ} (Ω : Set (EuclideanSpace ℝ (Fin d))) (CP : ℝ) (hCP : 0 ≤ CP) (hbase : ∀ {φ : EuclideanSpace ℝ (Fin d) → ℝ} (h : IsTestFn Ω φ), ‖h.testGraph.ofLp 0‖ ^ 2 ≤ CP * ∑ i : Fin d, ‖h.testGraph.ofLp i.succ‖ ^ 2) (U : ↥(H01 Ω)) : principalEigenvalue (laplaceBilin Ω) * ‖(↑U).ofLp 0‖ ^ 2 ≤ ∑ i : Fin d, ‖(↑U).ofLp i.succ‖ ^ 2

Poincaré inequality with its optimal constant. The principal Dirichlet eigenvalue is the largest constant for which λ‖u‖²_{L²} ≤ ∫ |∇u|² on all of H₀¹(Ω), since dirichlet_poincare_attained produces an equality case.

theorem EllipticPdes.Sobolev.dirichlet_poincare_attained {d : ℕ} (Ω : Set (EuclideanSpace ℝ (Fin d))) (hΩm : MeasurableSet Ω) (hΩb : Bornology.IsBounded Ω) (CP : ℝ) (hCP : 0 ≤ CP) (hbase : ∀ {φ : EuclideanSpace ℝ (Fin d) → ℝ} (h : IsTestFn Ω φ), ‖h.testGraph.ofLp 0‖ ^ 2 ≤ CP * ∑ i : Fin d, ‖h.testGraph.ofLp i.succ‖ ^ 2) (hne : ∃ (V : ↥(H01 Ω)), (embL2 Ω) V ≠ 0) : ∃ (U : ↥(H01 Ω)), ‖(↑U).ofLp 0‖ = 1 ∧ ∑ i : Fin d, ‖(↑U).ofLp i.succ‖ ^ 2 = principalEigenvalue (laplaceBilin Ω)

The optimal Poincaré constant is attained: some u of unit L² norm has Dirichlet energy exactly λ₁.

theorem EllipticPdes.Sobolev.dirichlet_principalEigenvalue_pos {d : ℕ} (Ω : Set (EuclideanSpace ℝ (Fin d))) (CP : ℝ) (hCP : 0 ≤ CP) (hbase : ∀ {φ : EuclideanSpace ℝ (Fin d) → ℝ} (h : IsTestFn Ω φ), ‖h.testGraph.ofLp 0‖ ^ 2 ≤ CP * ∑ i : Fin d, ‖h.testGraph.ofLp i.succ‖ ^ 2) (hne : ∃ (V : ↥(H01 Ω)), (embL2 Ω) V ≠ 0) : 0 < principalEigenvalue (laplaceBilin Ω)

The principal Dirichlet eigenvalue is positive.

theorem EllipticPdes.Sobolev.dirichlet_principal_eigenpair_of_bounded {n : ℕ} (Ω : Set (EuclideanSpace ℝ (Fin (n + 1)))) (hΩm : MeasurableSet Ω) (hΩb : Bornology.IsBounded Ω) (hne : ∃ (V : ↥(H01 Ω)), (embL2 Ω) V ≠ 0) : ∃ (U : ↥(H01 Ω)), ‖(embL2 Ω) U‖ = 1 ∧ ((laplaceBilin Ω) U) U = principalEigenvalue (laplaceBilin Ω) ∧ 0 < principalEigenvalue (laplaceBilin Ω) ∧ ∀ (V : ↥(H01 Ω)), ((laplaceBilin Ω) U) V = principalEigenvalue (laplaceBilin Ω) * inner ℝ ((embL2 Ω) U) ((embL2 Ω) V)

Principal Dirichlet eigenpair on a bounded domain, with no abstract Poincaré hypothesis: EllipticPdes.Poincare.laplaceBilin_coercive_of_bounded names the constant, so boundedness and measurability of Ω are the whole input. This is the statement Evans makes, and it includes the positivity of λ₁.