Eigenvalue sequence by iterated constrained minimisation

EllipticPdes.Sobolev.exists_higher_eigenpair produces one eigenpair orthogonal to a given finite family. Iterating it produces, for every n, an L²-orthonormal family of n weak eigenfunctions whose eigenvalues increase. That is the variational construction of the Dirichlet spectrum, and it names every eigenvalue by a Rayleigh quotient rather than one at a time through the spectral theorem, which is what EllipticPdes.Sobolev.solOp_spectral does.

The induction records one thing beyond the conclusion: every eigenvalue produced so far is at most the infimum over the current constraint submodule. That is what makes the next eigenvalue the largest, since the next one is exactly that infimum, and the constraint submodule shrinks at each step, so the infima increase.

The recursion needs a vector orthogonal to the family at every stage, which is infinite dimensionality of the L² image of H₀¹(Ω). It is a hypothesis here, stated as the existence of a single vector at each stage rather than as a dimension count.

Main declarations

• EllipticPdes.Sobolev.eigenvalueOn_mono: tightening the constraint raises the infimum.
• EllipticPdes.Sobolev.orthSubmodule_snoc_subset: appending shrinks the constraint.
• EllipticPdes.Sobolev.exists_eigen_family: the orthonormal family and its increasing eigenvalues.
• EllipticPdes.Sobolev.principalEigenvalue_le_of_eigen_family: every eigenvalue of such a family is at least the principal one.
• EllipticPdes.Sobolev.dirichlet_eigen_family_of_bounded: the instance at -Δ on a bounded measurable domain, reading 0 < λ₁ ≤ ⋯ ≤ λₙ.

References

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

Monotonicity of the constrained infimum

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

Tightening the constraint raises the infimum.

theorem EllipticPdes.Sobolev.rayleighSphere_inter_nonempty {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} {K : Submodule ℝ ↥(H01 Ω)} (h : ∃ U ∈ K, (embL2 Ω) U ≠ 0) : (rayleighSphere Ω ∩ ↑K).Nonempty

A submodule with a vector of nonzero L² class meets the unit L² sphere: rescale.

theorem EllipticPdes.Sobolev.orthSubmodule_snoc_subset {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} {n : ℕ} (w : Fin n → ↥(H01 Ω)) (U : ↥(H01 Ω)) : ↑(orthSubmodule (Fin.snoc w U)) ⊆ ↑(orthSubmodule w)

Appending a vector shrinks the constraint submodule.

The family

theorem EllipticPdes.Sobolev.exists_eigen_family {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 Ω)) (hdim : ∀ (m : ℕ) (v : Fin m → ↥(H01 Ω)), ∃ U ∈ orthSubmodule v, (embL2 Ω) U ≠ 0) (n : ℕ) : ∃ (w : Fin n → ↥(H01 Ω)) (lam : Fin n → ℝ), (∀ (i : Fin n), ‖(embL2 Ω) (w i)‖ = 1) ∧ (∀ (i j : Fin n), i ≠ j → inner ℝ ((embL2 Ω) (w i)) ((embL2 Ω) (w j)) = 0) ∧ (∀ (i : Fin n) (V : ↥(H01 Ω)), (B (w i)) V = lam i * inner ℝ ((embL2 Ω) (w i)) ((embL2 Ω) V)) ∧ (∀ (i j : Fin n), i ≤ j → lam i ≤ lam j) ∧ ∀ (i : Fin n), lam i ≤ eigenvalueOn B ↑(orthSubmodule w)

Eigenvalue sequence. For every n there is an L²-orthonormal family of n weak eigenfunctions of B whose eigenvalues increase with the index. The hypothesis hdim supplies, at each stage, a vector of nonzero L² class orthogonal to the family built so far; on a bounded domain it is the infinite dimensionality of H₀¹(Ω).

The fifth conclusion is the induction's own invariant: every eigenvalue produced so far is at most the infimum over the current constraint submodule, which is what the next step returns.

theorem EllipticPdes.Sobolev.principalEigenvalue_le_of_eigen_family {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} {B : ↥(H01 Ω) →L[ℝ] ↥(H01 Ω) →L[ℝ] ℝ} (hco : IsCoercive B) {n : ℕ} {w : Fin n → ↥(H01 Ω)} {lam : Fin n → ℝ} (hwnorm : ∀ (i : Fin n), ‖(embL2 Ω) (w i)‖ = 1) (hweig : ∀ (i : Fin n) (V : ↥(H01 Ω)), (B (w i)) V = lam i * inner ℝ ((embL2 Ω) (w i)) ((embL2 Ω) V)) (i : Fin n) : principalEigenvalue B ≤ lam i

Every eigenvalue of an orthonormal family is at least the principal one. A member of the family has unit L² norm and so is nonzero, which is what principalEigenvalue_le_of_weak_eigen asks for.

theorem EllipticPdes.Sobolev.dirichlet_eigen_family_of_bounded {m : ℕ} (Ω : Set (EuclideanSpace ℝ (Fin (m + 1)))) (hΩm : MeasurableSet Ω) (hΩb : Bornology.IsBounded Ω) (hdim : ∀ (k : ℕ) (v : Fin k → ↥(H01 Ω)), ∃ U ∈ orthSubmodule v, (embL2 Ω) U ≠ 0) (n : ℕ) : ∃ (w : Fin n → ↥(H01 Ω)) (lam : Fin n → ℝ), (∀ (i : Fin n), ‖(embL2 Ω) (w i)‖ = 1) ∧ (∀ (i j : Fin n), i ≠ j → inner ℝ ((embL2 Ω) (w i)) ((embL2 Ω) (w j)) = 0) ∧ (∀ (i : Fin n), 0 < lam i) ∧ (∀ (i j : Fin n), i ≤ j → lam i ≤ lam j) ∧ ∀ (i : Fin n) (V : ↥(H01 Ω)), ((laplaceBilin Ω) (w i)) V = lam i * inner ℝ ((embL2 Ω) (w i)) ((embL2 Ω) V)

Dirichlet eigenvalue sequence on a bounded domain. For every n there is an L²-orthonormal family of n weak solutions of -Δw = λw with 0 < λ₁ ≤ ⋯ ≤ λₙ. Boundedness and measurability of Ω discharge coercivity and the compact embedding; hdim is the infinite dimensionality of H₀¹(Ω), stated as a vector at each stage.