Documentation

LeanPool.EllipticPDE.Spectrum.HigherEigenvalues

Later eigenvalues by constrained minimisation #

EllipticPdes.Sobolev.exists_principal_eigenpair names the first Dirichlet eigenvalue as the infimum of the Rayleigh quotient over the unit L² sphere. Minimising over the part of that sphere L²-orthogonal to a finite family of eigenfunctions names the next one, and repeating the step names them all. This file supplies the step.

Two things have to be checked. The constraint is weakly closed, so EllipticPdes.Sobolev.exists_rayleigh_minimiser_on applies to it and the minimum is attained; and the minimiser is a weak eigenfunction of the whole space rather than only of the constrained subspace. The second is where the multipliers drop out: a test vector splits as an admissible part plus a combination of the wᵢ, and both B[U, wᵢ] and ⟪U, wᵢ⟫_{L²} vanish, the first because wᵢ is an eigenfunction and U is orthogonal to it, the second by the constraint itself.

Main declarations #

References #

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

The orthogonality constraint #

source
def EllipticPdes.Sobolev.orthSubmodule {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} {n : ℕ} (w : Fin n → ↥(H01 Ω)) :
Submodule ℝ ↥(H01 Ω)

The vectors of H₀¹(Ω) whose L² classes are orthogonal to those of a finite family.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem EllipticPdes.Sobolev.mem_orthSubmodule {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} {n : ℕ} {w : Fin n → ↥(H01 Ω)} {U : ↥(H01 Ω)} :
    U ∈ orthSubmodule w ↔ ∀ (i : Fin n), inner ℝ ((embL2 Ω) U) ((embL2 Ω) (w i)) = 0
    source
    theorem EllipticPdes.Sobolev.orthSubmodule_weaklyClosed {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} {n : ℕ} (w : Fin n → ↥(H01 Ω)) (u : ℕ → ↥(H01 Ω)) (z : ↥(H01 Ω)) (hu : ∀ (k : ℕ), u k ∈ orthSubmodule w) (hz : ∀ (v : ↥(H01 Ω)), Filter.Tendsto (fun (k : ℕ) => inner ℝ (u k) v) Filter.atTop (nhds (inner ℝ z v))) :
    z ∈ orthSubmodule w

    Passage of the orthogonality constraint to weak limits. Testing the weak convergence against the adjoint image of each wᵢ turns it into convergence of the L² inner products.

    The Rayleigh bound and the equation inside a submodule #

    source
    theorem EllipticPdes.Sobolev.eigenvalueOn_mul_norm_sq_le {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} {B : ↥(H01 Ω) →L[ℝ] ↥(H01 Ω) →L[ℝ] ℝ} (hco : IsCoercive B) (K : Submodule ℝ ↥(H01 Ω)) {U : ↥(H01 Ω)} (hUK : U ∈ K) :
    eigenvalueOn B ↑K * ‖(embL2 Ω) U‖ ^ 2 ≤ (B U) U

    Rayleigh bound inside a submodule. Rescaling stays in the submodule, so the bound of principalEigenvalue_mul_norm_sq_le runs there unchanged.

    source
    theorem EllipticPdes.Sobolev.rayleigh_euler_lagrange_on {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} {B : ↥(H01 Ω) →L[ℝ] ↥(H01 Ω) →L[ℝ] ℝ} (hco : IsCoercive B) (hsymm : ∀ (U V : ↥(H01 Ω)), (B U) V = (B V) U) (K : Submodule ℝ ↥(H01 Ω)) {U : ↥(H01 Ω)} (hU : ‖(embL2 Ω) U‖ = 1) (hUK : U ∈ K) (hmin : (B U) U = eigenvalueOn B ↑K) {V : ↥(H01 Ω)} (hVK : V ∈ K) :
    (B U) V = eigenvalueOn B ↑K * inner ℝ ((embL2 Ω) U) ((embL2 Ω) V)

    Euler-Lagrange equation inside a submodule. A minimiser over the unit L² sphere of K satisfies the eigenvalue identity against every test vector of K.

    The equation on the whole space #

    source
    theorem EllipticPdes.Sobolev.euler_lagrange_of_orthogonal_eigen {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} {B : ↥(H01 Ω) →L[ℝ] ↥(H01 Ω) →L[ℝ] ℝ} (hco : IsCoercive B) (hsymm : ∀ (U V : ↥(H01 Ω)), (B U) V = (B V) U) {n : ℕ} {w : Fin n → ↥(H01 Ω)} {lam : Fin n → ℝ} (hwnorm : ∀ (i : Fin n), ‖(embL2 Ω) (w i)‖ = 1) (hworth : ∀ (i j : Fin n), i ≠ j → inner ℝ ((embL2 Ω) (w i)) ((embL2 Ω) (w j)) = 0) (hweig : ∀ (i : Fin n) (V : ↥(H01 Ω)), (B (w i)) V = lam i * inner ℝ ((embL2 Ω) (w i)) ((embL2 Ω) V)) {U : ↥(H01 Ω)} (hU : ‖(embL2 Ω) U‖ = 1) (hUK : U ∈ orthSubmodule w) (hmin : (B U) U = eigenvalueOn B ↑(orthSubmodule w)) (V : ↥(H01 Ω)) :
    (B U) V = eigenvalueOn B ↑(orthSubmodule w) * inner ℝ ((embL2 Ω) U) ((embL2 Ω) V)

    Constrained minimiser as a weak eigenfunction of the whole space. Split a test vector into its admissible part and a combination of the wᵢ; the second half contributes nothing to either side. B[U, wᵢ] vanishes because wᵢ is an eigenfunction and U is orthogonal to it, and ⟪U, wᵢ⟫_{L²} vanishes by the constraint.

    The constrained eigenpair #

    source
    theorem EllipticPdes.Sobolev.exists_higher_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 Ω)) {n : ℕ} {w : Fin n → ↥(H01 Ω)} {lam : Fin n → ℝ} (hwnorm : ∀ (i : Fin n), ‖(embL2 Ω) (w i)‖ = 1) (hworth : ∀ (i j : Fin n), i ≠ j → inner ℝ ((embL2 Ω) (w i)) ((embL2 Ω) (w j)) = 0) (hweig : ∀ (i : Fin n) (V : ↥(H01 Ω)), (B (w i)) V = lam i * inner ℝ ((embL2 Ω) (w i)) ((embL2 Ω) V)) (hne : (rayleighSphere Ω ∩ ↑(orthSubmodule w)).Nonempty) :
    ∃ (U : ↥(H01 Ω)) (μ : ℝ), ‖(embL2 Ω) U‖ = 1 ∧ U ∈ orthSubmodule w ∧ (B U) U = μ ∧ principalEigenvalue B ≤ μ ∧ ∀ (V : ↥(H01 Ω)), (B U) V = μ * inner ℝ ((embL2 Ω) U) ((embL2 Ω) V)

    Later eigenpair. Minimising over the part of the unit L² sphere orthogonal to a finite orthonormal family of eigenfunctions produces another eigenpair, whose eigenvalue is at least the principal one. Iterating the step produces the whole sequence.