Positivity and orthogonality of Dirichlet eigenpairs

import PDETextbook.Base

open MeasureTheory
open scoped BigOperators ENNReal

noncomputable section

namespace PDETextbook.LarssonThomee.Thm61

/-- `Ω` is a bounded domain (open, connected, bounded) in `ℝ^d` with smooth boundary `Γ = ∂Ω`.
Smoothness of `Γ` is expressed by local `C^∞` defining functions with nonvanishing differential:
near each boundary point `x` there are an open `U ∋ x` and a smooth `ρ` with `dρ ≠ 0` on `U`
and `Ω ∩ U = {ρ < 0}`. -/
def IsBoundedSmoothDomain {d : ℕ} (Ω : Set (Euclidean d)) : Prop :=
  IsOpen Ω ∧ IsConnected Ω ∧ Bornology.IsBounded Ω ∧
  ∀ x ∈ frontier Ω, ∃ U : Set (Euclidean d), IsOpen U ∧ x ∈ U ∧
    ∃ ρ : Euclidean d → ℝ, (∀ n : ℕ, ContDiff ℝ n ρ) ∧
      (∀ y ∈ U, fderiv ℝ ρ y ≠ 0) ∧
      Ω ∩ U = {y ∈ U | ρ y < 0}

/-- The `L₂(Ω)` scalar product `(u,v) = ∫_Ω u v̄ dx` of (6.7), linear in the first argument
(for real-valued functions it is `∫_Ω u v dx`). -/
def l2Form {d : ℕ} (Ω : Set (Euclidean d)) (u v : Euclidean d → ℂ) : ℂ :=
  ∫ x in Ω, u x * (starRingEnd ℂ) (v x)

/-- The form `a(u,v) = ∫_Ω ∇u · ∇v̄ dx = (∇u, ∇v)` of (6.7), written in terms of
(weak) gradients `G = ∇u`, `H = ∇v`. -/
def dirichletForm {d : ℕ} (Ω : Set (Euclidean d)) (G H : Fin d → Euclidean d → ℂ) : ℂ :=
  ∑ i, ∫ x in Ω, G i x * (starRingEnd ℂ) (H i x)

/-- Variational form of the Dirichlet eigenvalue problem (6.5):
`φ ∈ H₀¹(Ω)`, `φ ≠ 0`, and `a(φ,v) = λ (φ,v)` for all `v ∈ H₀¹(Ω)`. -/
def IsDirichletEigenpair {d : ℕ} (Ω : Set (Euclidean d)) (lam : ℂ)
    (φ : Euclidean d → ℂ) : Prop :=
  InH10Closure Ω φ ∧ ¬ (φ =ᵐ[domainMeasure Ω] (0 : Euclidean d → ℂ)) ∧
  ∀ G : Fin d → Euclidean d → ℂ, HasH1Gradient Ω φ G →
    ∀ (v : Euclidean d → ℂ) (H : Fin d → Euclidean d → ℂ),
      InH10Closure Ω v → HasH1Gradient Ω v H →
        dirichletForm Ω G H = lam * l2Form Ω φ v

/-- `λ` is an eigenvalue of (6.5). -/
def IsDirichletEigenvalue {d : ℕ} (Ω : Set (Euclidean d)) (lam : ℂ) : Prop :=
  ∃ φ : Euclidean d → ℂ, IsDirichletEigenpair Ω lam φ

/-- Theorem 6.1 (Larsson–Thomée). The eigenvalues of (6.5) are real and positive. Two
eigenfunctions corresponding to different eigenvalues are orthogonal in `L₂` and `H₀¹`
(orthogonality in `H₀¹` is stated as `a(φ,ψ) = 0`; together with `(φ,ψ) = 0` this also gives
orthogonality for the full `H¹` scalar product). -/
theorem thm_6_1 {d : ℕ} (hd : 0 < d) (Ω : Set (Euclidean d))
    (hΩ : IsBoundedSmoothDomain Ω) :
    (∀ lam : ℂ, IsDirichletEigenvalue Ω lam → lam.im = 0 ∧ 0 < lam.re) ∧
    (∀ (lam mu : ℂ) (φ ψ : Euclidean d → ℂ),
      IsDirichletEigenpair Ω lam φ → IsDirichletEigenpair Ω mu ψ → lam ≠ mu →
        l2Form Ω φ ψ = 0 ∧
        ∀ G H : Fin d → Euclidean d → ℂ,
          HasH1Gradient Ω φ G → HasH1Gradient Ω ψ H → dirichletForm Ω G H = 0) := by
  sorry

end PDETextbook.LarssonThomee.Thm61