Divergence of the Dirichlet eigenvalue sequence

import PDETextbook.Base

open MeasureTheory
open scoped BigOperators ENNReal

noncomputable section

namespace PDETextbook.LarssonThomee.Thm63

/-- `Ω` has smooth boundary `Γ = frontier Ω`: near each boundary point, `Ω` is the
sublevel set `{ρ < 0}` of a C^∞ defining function `ρ` whose differential does not
vanish on `{ρ = 0}`. -/
def HasSmoothBoundary {d : ℕ} (Ω : Set (Euclidean d)) : Prop :=
  ∀ x ∈ frontier Ω, ∃ U : Set (Euclidean d), IsOpen U ∧ x ∈ U ∧
    ∃ ρ : Euclidean d → ℝ, (∀ k : ℕ, ContDiff ℝ k ρ) ∧
      (∀ y ∈ U, ρ y = 0 → fderiv ℝ ρ y ≠ 0) ∧
      Ω ∩ U = {y ∈ U | ρ y < 0}

/-- Variational form of the Dirichlet eigenvalue problem (6.5) via (6.4)/(6.7):
`φ ∈ H₀¹`, `φ ≠ 0`, and `a(φ, v) = λ (φ, v)` for all `v ∈ H₀¹`, where
`a(u,v) = ∫_Ω ∇u·∇v dx` and `(u,v) = ∫_Ω u v dx`. -/
def IsDirichletEigenpair {d : ℕ} (Ω : Set (Euclidean d)) (lam : ℝ)
    (φ : Euclidean d → ℝ) : Prop :=
  InH10Closure Ω φ ∧ ¬ (φ =ᵐ[domainMeasure Ω] 0) ∧
  ∃ G : Fin d → Euclidean d → ℝ, HasH1Gradient Ω φ G ∧
    ∀ (v : Euclidean d → ℝ) (H : Fin d → Euclidean d → ℝ),
      InH10Closure Ω v → HasH1Gradient Ω v H →
        (∫ x in Ω, ∑ i, G i x * H i x) = lam * ∫ x in Ω, φ x * v x

/-- `lam n` is the `n`-th eigenvalue of (6.5): the eigenvalues listed in nondecreasing
order and repeated according to multiplicity, i.e. there are L²-orthonormal
eigenfunctions `φ n` with eigenvalue `lam n`, and every eigenfunction with eigenvalue
`μ` has a nonzero component along some `φ n` with `lam n = μ` (so the `φ n` with
`lam n = μ` exhaust the eigenspace of `μ`, and every eigenvalue occurs). -/
def IsDirichletEigenvalueSequence {d : ℕ} (Ω : Set (Euclidean d)) (lam : ℕ → ℝ) : Prop :=
  Monotone lam ∧ ∃ φ : ℕ → Euclidean d → ℝ,
    (∀ n, IsDirichletEigenpair Ω (lam n) (φ n)) ∧
    (∀ m n, (∫ x in Ω, φ m x * φ n x) = if m = n then (1 : ℝ) else 0) ∧
    (∀ (μ : ℝ) (ψ : Euclidean d → ℝ), IsDirichletEigenpair Ω μ ψ →
      ∃ n, lam n = μ ∧ (∫ x in Ω, ψ x * φ n x) ≠ 0)

/-- Theorem 6.3 (Larsson–Thomée): with `λ_n` the `n`-th eigenvalue of the Dirichlet
eigenvalue problem (6.5) on a bounded domain `Ω ⊂ ℝ^d` with smooth boundary,
`λ_n → ∞` as `n → ∞`. -/
theorem dirichlet_eigenvalues_tendsto_atTop {d : ℕ} (Ω : Set (Euclidean d))
    (hΩopen : IsOpen Ω) (hΩconn : IsConnected Ω) (hΩbdd : Bornology.IsBounded Ω)
    (hΓ : HasSmoothBoundary Ω)
    (lam : ℕ → ℝ) (hlam : IsDirichletEigenvalueSequence Ω lam) :
    Filter.Tendsto lam Filter.atTop Filter.atTop := by
  sorry

end PDETextbook.LarssonThomee.Thm63