Min–max characterization of Dirichlet eigenvalues

import PDETextbook.Base

open MeasureTheory
open scoped BigOperators ENNReal

noncomputable section

namespace PDETextbook.LarssonThomee.Thm65

/-- Smooth (C^∞) boundary of a bounded open set, realized by a smooth defining function
`ρ` with `Ω = {ρ < 0}` and nonvanishing differential on the boundary `Γ = frontier Ω`. -/
def HasSmoothBoundary {d : ℕ} (Ω : Set (Euclidean d)) : Prop :=
  ∃ ρ : Euclidean d → ℝ, ContDiff ℝ (⊤ : ℕ∞) ρ ∧ Ω = {x | ρ x < 0} ∧
    ∀ x ∈ frontier Ω, fderiv ℝ ρ x ≠ 0

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

open Classical in
/-- The bilinear form `a(u,v) = ∫_Ω ∇u · ∇v dx` of (6.7), using (weak) H¹ gradients. -/
def dirichletForm {d : ℕ} (Ω : Set (Euclidean d)) (u v : Euclidean d → ℝ) : ℝ :=
  if hu : InH1 Ω u then
    if hv : InH1 Ω v then ∫ x in Ω, ∑ i, hu.choose i x * hv.choose i x else 0
  else 0

/-- Rayleigh quotient `a(v,v)/‖v‖²`. -/
def rayleigh {d : ℕ} (Ω : Set (Euclidean d)) (v : Euclidean d → ℝ) : ℝ :=
  dirichletForm Ω v v / l2Prod Ω v v

/-- The Dirichlet eigenvalues `λ_n` (indices `n ≥ 1`) with orthonormal eigenfunctions `φ_n`:
weak eigen-equation (6.4) in `H_0^1`, and the characterization (6.13)
`λ_n = a(φ_n,φ_n) = inf {a(v,v) : v ∈ H_0^1, ‖v‖ = 1, (v,φ_j) = 0, j = 1,…,n-1}`. -/
def IsDirichletEigenSequence {d : ℕ} (Ω : Set (Euclidean d))
    (lam : ℕ → ℝ) (φ : ℕ → Euclidean d → ℝ) : Prop :=
  ∀ n : ℕ, 1 ≤ n →
    InH10Closure Ω (φ n) ∧
    (∀ m : ℕ, 1 ≤ m → l2Prod Ω (φ n) (φ m) = if n = m then 1 else 0) ∧
    (∀ v : Euclidean d → ℝ, InH10Closure Ω v →
      dirichletForm Ω (φ n) v = lam n * l2Prod Ω (φ n) v) ∧
    lam n = dirichletForm Ω (φ n) (φ n) ∧
    IsGLB {r : ℝ | ∃ v : Euclidean d → ℝ, InH10Closure Ω v ∧ l2Prod Ω v v = 1 ∧
        (∀ j : ℕ, 1 ≤ j → j < n → l2Prod Ω v (φ j) = 0) ∧ r = dirichletForm Ω v v}
      (lam n)

/-- An `n`-dimensional subspace of `H_0^1`, represented by a space of representatives on
which the L² norm is definite (so it is `n`-dimensional as a space of a.e. classes). -/
def IsH10Subspace {d : ℕ} (Ω : Set (Euclidean d)) (n : ℕ)
    (V : Submodule ℝ (Euclidean d → ℝ)) : Prop :=
  Module.finrank ℝ V = n ∧ (∀ v ∈ V, InH10Closure Ω v) ∧
    (∀ v ∈ V, l2Prod Ω v v = 0 → v = 0)

/-- The set of Rayleigh quotients over the nonzero elements of `V`. -/
def rayleighSet {d : ℕ} (Ω : Set (Euclidean d)) (V : Submodule ℝ (Euclidean d → ℝ)) :
    Set ℝ :=
  {r : ℝ | ∃ v ∈ V, v ≠ 0 ∧ r = rayleigh Ω v}

/-- Theorem 6.5 (min–max, (6.18)): `λ_n = min_{V_n} max_{v ∈ V_n} a(v,v)/‖v‖²`, where `V_n`
ranges over all `n`-dimensional subspaces of `H_0^1(Ω)`, for the Dirichlet eigenvalue
problem (6.5) on a bounded domain `Ω ⊂ ℝ^d` with smooth boundary. The max is attained for
every `V_n`, and the min over `V_n` is attained and equals `λ_n`. -/
theorem minmax_dirichlet_eigenvalue {d : ℕ} (Ω : Set (Euclidean d))
    (hΩopen : IsOpen Ω) (hΩconn : IsConnected Ω) (hΩbdd : Bornology.IsBounded Ω)
    (hΩsmooth : HasSmoothBoundary Ω)
    (lam : ℕ → ℝ) (φ : ℕ → Euclidean d → ℝ) (hEig : IsDirichletEigenSequence Ω lam φ)
    (n : ℕ) (hn : 1 ≤ n) :
    (∀ V : Submodule ℝ (Euclidean d → ℝ), IsH10Subspace Ω n V →
        ∃ M : ℝ, IsGreatest (rayleighSet Ω V) M ∧ lam n ≤ M) ∧
    (∃ V : Submodule ℝ (Euclidean d → ℝ), IsH10Subspace Ω n V ∧
        IsGreatest (rayleighSet Ω V) (lam n)) := by sorry

end PDETextbook.LarssonThomee.Thm65