Approximation of the principal eigenfunction

import PDETextbook.Base

open MeasureTheory
open scoped BigOperators ENNReal

noncomputable section

namespace PDETextbook.LarssonThomee.Thm68

abbrev E2 := Euclidean 2

/-- A closed nondegenerate triangle `K` in `ℝ²`. -/
structure Tri where
  v : Fin 3 → E2
  indep : AffineIndependent ℝ v

def Tri.set (K : Tri) : Set E2 := convexHull ℝ (Set.range K.v)

/-- Interior angle of `K` at vertex `i`. -/
def Tri.angle (K : Tri) (i : Fin 3) : ℝ :=
  InnerProductGeometry.angle (K.v (i + 1) - K.v i) (K.v (i + 2) - K.v i)

/-- A triangulation `𝒯_h = {K}`: finitely many closed triangles with disjoint interiors,
any two meeting in the hull of their common vertices (empty, a vertex or an edge). -/
structure Triangulation where
  n : ℕ
  K : Fin n → Tri
  disjointInt : ∀ i j, i ≠ j → interior (K i).set ∩ interior (K j).set = ∅
  conforming : ∀ i j, i ≠ j →
    (K i).set ∩ (K j).set = convexHull ℝ (Set.range (K i).v ∩ Set.range (K j).v)

/-- `Ω_h`, the union of the triangles. -/
def Triangulation.region (T : Triangulation) : Set E2 := ⋃ i, (T.K i).set

/-- `h = max_K diam(K)`. -/
def Triangulation.meshsize (T : Triangulation) : ℝ := ⨆ i, Metric.diam (T.K i).set

/-- `Ω ⊂ ℝ²` a convex domain with smooth boundary `Γ` (smooth defining function). -/
def SmoothConvexDomain (Ω : Set E2) : Prop :=
  Ω.Nonempty ∧ Convex ℝ Ω ∧
  ∃ ρ : E2 → ℝ, ContDiff ℝ (⊤ : ℕ∞) ρ ∧ Ω = {x | ρ x < 0} ∧
    ∀ x, ρ x = 0 → fderiv ℝ ρ x ≠ 0

/-- Regular family `{𝒯_h}_{0<h<1}` for smooth convex `Ω` (Sect. 5.2): `Ω_h ⊆ Ω̄`, boundary
vertices of `Ω_h` on `Γ`, `Ω \ Ω_h` of width `O(h²)`, angles bounded below uniformly. -/
structure RegularFamily (Ω : Set E2) where
  T : ℝ → Triangulation
  mesh : ∀ h ∈ Set.Ioo (0 : ℝ) 1, (T h).meshsize = h
  inside : ∀ h ∈ Set.Ioo (0 : ℝ) 1, (T h).region ⊆ closure Ω
  bdryVertices : ∀ h ∈ Set.Ioo (0 : ℝ) 1, ∀ i a,
    ((T h).K i).v a ∈ frontier (T h).region → ((T h).K i).v a ∈ frontier Ω
  width : ∃ c : ℝ, ∀ h ∈ Set.Ioo (0 : ℝ) 1, ∀ x ∈ Ω \ (T h).region,
    Metric.infDist x (frontier Ω) ≤ c * h ^ 2
  regular : ∃ α : ℝ, 0 < α ∧ ∀ h ∈ Set.Ioo (0 : ℝ) 1, ∀ i a, α ≤ ((T h).K i).angle a

/-- `S_h`: continuous on `Ω̄`, linear on each `K`, vanishing on `Γ` and on `Ω̄ \ Ω_h`. -/
def InSh (Ω : Set E2) (T : Triangulation) (v : E2 → ℝ) : Prop :=
  ContinuousOn v (closure Ω) ∧
  (∀ i, ∃ f : E2 →ᵃ[ℝ] ℝ, ∀ x ∈ (T.K i).set, v x = f x) ∧
  (∀ x ∈ closure Ω \ T.region, v x = 0) ∧ (∀ x ∈ frontier Ω, v x = 0)

/-- `(v, w)` on `Ω`. -/
def l2pair (Ω : Set E2) (u v : E2 → ℝ) : ℝ := ∫ x in Ω, u x * v x

/-- `(∇v, ∇w)` on `Ω`, via weak gradients. -/
def gradPair (Ω : Set E2) (G H : Fin 2 → E2 → ℝ) : ℝ := ∫ x in Ω, ∑ i, G i x * H i x

/-- (6.31) in weak form: `u ∈ H¹₀(Ω)`, `u ≠ 0`, `(∇u,∇v) = λ(u,v)` for all `v ∈ H¹₀(Ω)`. -/
def IsDirichletEigenpair (Ω : Set E2) (lam : ℝ) (u : E2 → ℝ) (G : Fin 2 → E2 → ℝ) : Prop :=
  HasH1Gradient Ω u G ∧ InH10Closure Ω u ∧ ¬ (u =ᵐ[domainMeasure Ω] 0) ∧
  ∀ v H, HasH1Gradient Ω v H → InH10Closure Ω v → gradPair Ω G H = lam * l2pair Ω u v

/-- Principal (least) eigenvalue `λ₁` of (6.31). -/
def IsPrincipalDirichletEigenvalue (Ω : Set E2) (lam : ℝ) : Prop :=
  (∃ u G, IsDirichletEigenpair Ω lam u G) ∧
  ∀ μ u G, IsDirichletEigenpair Ω μ u G → lam ≤ μ

/-- (6.32): `u_h ∈ S_h`, `u_h ≠ 0`, `a(u_h, χ) = λ(u_h, χ)` for all `χ ∈ S_h`. -/
def IsDiscreteEigenpair (Ω : Set E2) (T : Triangulation) (lam : ℝ) (u : E2 → ℝ)
    (G : Fin 2 → E2 → ℝ) : Prop :=
  InSh Ω T u ∧ HasH1Gradient Ω u G ∧ ¬ (u =ᵐ[domainMeasure Ω] 0) ∧
  ∀ χ H, InSh Ω T χ → HasH1Gradient Ω χ H → gradPair Ω G H = lam * l2pair Ω u χ

/-- Principal (least) eigenvalue `λ_{1,h}` of (6.32). -/
def IsPrincipalDiscreteEigenvalue (Ω : Set E2) (T : Triangulation) (lam : ℝ) : Prop :=
  (∃ u G, IsDiscreteEigenpair Ω T lam u G) ∧
  ∀ μ u G, IsDiscreteEigenpair Ω T μ u G → lam ≤ μ

/-- Theorem 6.8, (6.39)-(6.40). Normalized: `‖φ‖ = 1`, with the sign fixed by
`(φ_{1,h}, φ₁) ≥ 0` (eigenfunctions are otherwise only determined up to sign). -/
theorem thm_6_8 (Ω : Set E2) (hΩ : SmoothConvexDomain Ω) (F : RegularFamily Ω) :
    ∃ C : ℝ, ∀ h ∈ Set.Ioo (0 : ℝ) 1,
      ∀ lam1 φ1 G1, IsPrincipalDirichletEigenvalue Ω lam1 →
        IsDirichletEigenpair Ω lam1 φ1 G1 → l2pair Ω φ1 φ1 = 1 →
      ∀ lam1h φ1h G1h, IsPrincipalDiscreteEigenvalue Ω (F.T h) lam1h →
        IsDiscreteEigenpair Ω (F.T h) lam1h φ1h G1h → l2pair Ω φ1h φ1h = 1 →
        0 ≤ l2pair Ω φ1h φ1 →
        Real.sqrt (l2pair Ω (φ1h - φ1) (φ1h - φ1)) ≤ C * h ^ 2 ∧
        Real.sqrt (gradPair Ω (G1h - G1) (G1h - G1)) ≤ C * h := by
  sorry

end PDETextbook.LarssonThomee.Thm68