AcceptedTheorem · Statement with omitted proof

Spectral characterization of the zero-boundary Sobolev space

Dirichlet eigenfunctions form a complete orthonormal basis, and their weighted coefficients characterize first-order zero-boundary regularity.

Larsson & Thomée ↗
Theorem 6.4 · printed p. 83

Download Lean file ↓

Formal statement. The assumptions and conclusion are explicit; the theorem proof is omitted (sorry).

01 / MATHEMATICAL STATEMENT

Meaning & conditions

Mathematical summary

Dirichlet eigenfunctions form a complete orthonormal basis, and their weighted coefficients characterize first-order zero-boundary regularity.

v\in H_0^1(\Omega)\ \Longleftrightarrow\ \sum_j\lambda_j|(v,\varphi_j)|^2<\infty,\qquad |v|_1^2=\sum_j\lambda_j|(v,\varphi_j)|^2.

Assumptions & context

The stated Dirichlet eigensystem assumptions on a bounded smooth domain, including completeness of the eigenspaces.

Source

Larsson & Thomée. Partial differential equations with numerical methods.

Theorem 6.4 · printed p. 83

02 / LEAN REPRESENTATION

Formal statement

Statement with omitted proof. Expand the complete file below to read imports, local definitions and surrounding context.

theorem thm_6_4 {d : ℕ} (Ω : Set (Euclidean d)) (hΩ : IsBoundedSmoothDomain Ω)
    (lam : ℕ → ℝ) (φ : ℕ → Euclidean d → ℝ)
    (hEig : ∀ j, IsDirichletEigenpair Ω (lam j) (φ j))
    (hOrth : ∀ i j, l2Prod Ω (φ i) (φ j) = if i = j then 1 else 0)
    (hAll : ∀ (μ : ℝ) (ψ : Euclidean d → ℝ), IsDirichletEigenpair Ω μ ψ →
      ∃ s : Finset ℕ, ∃ c : ℕ → ℝ, (∀ j ∈ s, lam j = μ) ∧
        ψ =ᵐ[domainMeasure Ω] fun x => ∑ j ∈ s, c j * φ j x) :
    (∃ b : HilbertBasis ℕ ℝ (L2 ℝ Ω),
        ∀ j, b j = MemLp.toLp (φ j) (hEig j).1.inH1.inL2) ∧
    (∀ v : Euclidean d → ℝ, InL2 Ω v →
        ((∃ S : ℝ, Tendsto
            (fun n => ∑ j ∈ Finset.range n, lam j * (l2Prod Ω v (φ j)) ^ 2)
            atTop (𝓝 S)) ↔ InH10Closure Ω v)) ∧
    (∀ (v : Euclidean d → ℝ) (G : Fin d → Euclidean d → ℝ),
        InH10Closure Ω v → HasH1Gradient Ω v G →
          gradNormSq Ω G = aForm Ω G G ∧
          Tendsto
            (fun n => ∑ j ∈ Finset.range n, lam j * (l2Prod Ω v (φ j)) ^ 2)
            atTop (𝓝 (aForm Ω G G))) := by
  sorry

Complete Lean file and local definitions

import PDETextbook.Base

open MeasureTheory
open scoped BigOperators ENNReal

noncomputable section

namespace PDETextbook.LarssonThomee.Thm64

open Filter Topology

/-- `Ω` is a bounded domain (open, connected, bounded) in `R^d` with smooth boundary `Γ`.
The smooth boundary is realized by a global C^∞ defining function `ρ` with `Ω = {ρ < 0}`
and nonvanishing differential on `{ρ = 0}`, which is then the boundary `Γ`. -/
def IsBoundedSmoothDomain {d : ℕ} (Ω : Set (Euclidean d)) : Prop :=
  IsOpen Ω ∧ IsConnected Ω ∧ Bornology.IsBounded Ω ∧
    ∃ ρ : Euclidean d → ℝ, (∀ n : ℕ, ContDiff ℝ n ρ) ∧ Ω = {x | ρ x < 0} ∧
      ∀ x, ρ x = 0 → fderiv ℝ ρ x ≠ 0

/-- The `L_2` scalar product `(u, v) = ∫_Ω u v dx` of (6.7). -/
def l2Prod {d : ℕ} (Ω : Set (Euclidean d)) (u v : Euclidean d → ℝ) : ℝ :=
  ∫ x in Ω, u x * v x

/-- `a(u, v) = ∫_Ω ∇u · ∇v dx` of (6.7), in terms of weak gradients `Gu`, `Gv`. -/
def aForm {d : ℕ} (Ω : Set (Euclidean d)) (Gu Gv : Fin d → Euclidean d → ℝ) : ℝ :=
  ∫ x in Ω, ∑ i, Gu i x * Gv i x

/-- `‖∇v‖² = ∫_Ω |∇v|² dx` for the weak gradient `G` of `v`. -/
def gradNormSq {d : ℕ} (Ω : Set (Euclidean d)) (G : Fin d → Euclidean d → ℝ) : ℝ :=
  ∫ x in Ω, ∑ i, (G i x) ^ 2

/-- Variational Dirichlet eigenvalue problem (6.5)/(6.4): `φ ∈ H_0^1`, `φ ≠ 0`, and
`a(φ, v) = λ (φ, v)` for all `v ∈ H_0^1`. -/
def IsDirichletEigenpair {d : ℕ} (Ω : Set (Euclidean d)) (lam : ℝ)
    (φ : Euclidean d → ℝ) : Prop :=
  InH10Closure Ω φ ∧ ¬ (φ =ᵐ[domainMeasure Ω] 0) ∧
    ∀ Gφ : Fin d → Euclidean d → ℝ, HasH1Gradient Ω φ Gφ →
      ∀ (v : Euclidean d → ℝ) (Gv : Fin d → Euclidean d → ℝ),
        InH10Closure Ω v → HasH1Gradient Ω v Gv →
          aForm Ω Gφ Gv = lam * l2Prod Ω φ v

/-- Theorem 6.4 (Larsson–Thomée). `φ j`, `lam j` (j : ℕ) stand for `φ_{j+1}`, `λ_{j+1}`.
The system `{φ_j}` of eigenfunctions of (6.5) is given as an L_2-orthonormal sequence of
eigenfunctions which spans every eigenspace (each eigenvalue counted with multiplicity). -/
theorem thm_6_4 {d : ℕ} (Ω : Set (Euclidean d)) (hΩ : IsBoundedSmoothDomain Ω)
    (lam : ℕ → ℝ) (φ : ℕ → Euclidean d → ℝ)
    (hEig : ∀ j, IsDirichletEigenpair Ω (lam j) (φ j))
    (hOrth : ∀ i j, l2Prod Ω (φ i) (φ j) = if i = j then 1 else 0)
    (hAll : ∀ (μ : ℝ) (ψ : Euclidean d → ℝ), IsDirichletEigenpair Ω μ ψ →
      ∃ s : Finset ℕ, ∃ c : ℕ → ℝ, (∀ j ∈ s, lam j = μ) ∧
        ψ =ᵐ[domainMeasure Ω] fun x => ∑ j ∈ s, c j * φ j x) :
    (∃ b : HilbertBasis ℕ ℝ (L2 ℝ Ω),
        ∀ j, b j = MemLp.toLp (φ j) (hEig j).1.inH1.inL2) ∧
    (∀ v : Euclidean d → ℝ, InL2 Ω v →
        ((∃ S : ℝ, Tendsto
            (fun n => ∑ j ∈ Finset.range n, lam j * (l2Prod Ω v (φ j)) ^ 2)
            atTop (𝓝 S)) ↔ InH10Closure Ω v)) ∧
    (∀ (v : Euclidean d → ℝ) (G : Fin d → Euclidean d → ℝ),
        InH10Closure Ω v → HasH1Gradient Ω v G →
          gradNormSq Ω G = aForm Ω G G ∧
          Tendsto
            (fun n => ∑ j ∈ Finset.range n, lam j * (l2Prod Ω v (φ j)) ^ 2)
            atTop (𝓝 (aForm Ω G G))) := by
  sorry

end PDETextbook.LarssonThomee.Thm64

How to read the formalization

For a function in the Sobolev space, the weighted coefficient sum equals the squared gradient norm.

← Back to all statements