Attainment of the first Dirichlet Rayleigh quotient

import PDETextbook.Base

open MeasureTheory
open scoped BigOperators ENNReal

noncomputable section

namespace PDETextbook.LarssonThomee.Thm62

/-- Smooth (C^∞) boundary of `Ω`, realized by a global smooth defining function:
`Ω = {ρ < 0}` and `dρ ≠ 0` on `{ρ = 0}`. This zero set is then exactly `Γ = ∂Ω`. -/
def HasSmoothBoundary {d : ℕ} (Ω : Set (Euclidean d)) : Prop :=
  ∃ ρ : Euclidean d → ℝ, ContDiff ℝ ((⊤ : ℕ∞)) ρ ∧ Ω = {x | ρ x < 0} ∧
    ∀ x, ρ x = 0 → fderiv ℝ ρ x ≠ 0

/-- The book's `(u, v) = ∫_Ω u v dx` (real-valued functions). -/
def l2Prod {d : ℕ} (Ω : Set (Euclidean d)) (u v : Euclidean d → ℝ) : ℝ :=
  ∫ x in Ω, u x * v x

/-- The book's `a(u, v) = (∇u, ∇v) = ∫_Ω ∇u · ∇v dx`, evaluated on weak gradients `G`, `H`. -/
def dirForm {d : ℕ} (Ω : Set (Euclidean d)) (G H : Fin d → Euclidean d → ℝ) : ℝ :=
  ∑ i, ∫ x in Ω, G i x * H i x

/-- The admissible values `a(v, v) = ‖∇v‖²` with `v ∈ H₀¹`, `‖v‖ = 1`, appearing in (6.10). -/
def rayleighSet {d : ℕ} (Ω : Set (Euclidean d)) : Set ℝ :=
  {r | ∃ (v : Euclidean d → ℝ) (G : Fin d → Euclidean d → ℝ),
    InH10Closure Ω v ∧ HasH1Gradient Ω v G ∧ l2Prod Ω v v = 1 ∧ r = dirForm Ω G G}

/-- (6.10): `λ₁ = inf { a(v,v) : v ∈ H₀¹, ‖v‖ = 1 }`. -/
def lambda1 {d : ℕ} (Ω : Set (Euclidean d)) : ℝ := sInf (rayleighSet Ω)

/-- Variational (weak) 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) ∧
    ∃ Gφ : Fin d → Euclidean d → ℝ, HasH1Gradient Ω φ Gφ ∧
      ∀ (v : Euclidean d → ℝ) (Gv : Fin d → Euclidean d → ℝ),
        InH10Closure Ω v → HasH1Gradient Ω v Gv →
          dirForm Ω Gφ Gv = lam * l2Prod Ω φ v

/-- Theorem 6.2 (Larsson–Thomée). For a bounded domain `Ω ⊂ ℝ^d` with smooth boundary,
the infimum in (6.10) is attained by some `φ₁ ∈ H₀¹` with `‖φ₁‖ = 1`, and `φ₁` is an
eigenfunction of (6.5) with eigenvalue `λ₁`. -/
theorem thm_6_2 {d : ℕ} (Ω : Set (Euclidean d))
    (hOpen : IsOpen Ω) (hConn : IsConnected Ω) (hBdd : Bornology.IsBounded Ω)
    (hSmooth : HasSmoothBoundary Ω) :
    ∃ (φ₁ : Euclidean d → ℝ) (G₁ : Fin d → Euclidean d → ℝ),
      InH10Closure Ω φ₁ ∧ HasH1Gradient Ω φ₁ G₁ ∧ l2Prod Ω φ₁ φ₁ = 1 ∧
      dirForm Ω G₁ G₁ = lambda1 Ω ∧
      IsDirichletEigenpair Ω (lambda1 Ω) φ₁ := by
  sorry

end PDETextbook.LarssonThomee.Thm62