Finite-element eigenvalue bounds

import PDETextbook.Base

open MeasureTheory
open scoped BigOperators ENNReal

noncomputable section

namespace PDETextbook.LarssonThomee.Thm67

/-- Gamma = frontier of Omega is a smooth closed (Jordan) curve. -/
def SmoothBoundary (Ω : Set (Euclidean 2)) : Prop :=
  ∃ γ : ℝ → Euclidean 2, (∀ k : ℕ, ContDiff ℝ k γ) ∧ Function.Periodic γ 1 ∧
    Set.InjOn γ (Set.Ico 0 1) ∧ (∀ t, deriv γ t ≠ 0) ∧ frontier Ω = Set.range γ

/-- Closed triangle K with vertex triple p. -/
def tri (p : Fin 3 → Euclidean 2) : Set (Euclidean 2) := convexHull ℝ (Set.range p)

/-- Omega_h: the union of the triangles of T_h. -/
def Ωh (T : Finset (Fin 3 → Euclidean 2)) : Set (Euclidean 2) := ⋃ p ∈ T, tri p

/-- Triangulation T_h of the convex smooth domain Omega (Sect. 5.2).
T_h is a set of closed triangles. They are nondegenerate and conforming: two distinct
triangles meet in a common vertex, a common edge, or not at all, as needed for the
pyramid basis used in (6.32). Their union Omega_h lies in closure Omega, and the boundary
vertices of Omega_h are chosen on Gamma. No convexity of Omega_h is assumed. -/
def IsTriangulation (Ω : Set (Euclidean 2)) (T : Finset (Fin 3 → Euclidean 2)) : Prop :=
  (∀ p ∈ T, AffineIndependent ℝ p) ∧
  (∀ p ∈ T, ∀ q ∈ T, tri p ≠ tri q →
      tri p ∩ tri q = convexHull ℝ (Set.range p ∩ Set.range q)) ∧
  Ωh T ⊆ closure Ω ∧
  (∀ p ∈ T, ∀ i, p i ∈ frontier (Ωh T) → p i ∈ frontier Ω)

/-- h = max_K diam(K). -/
def HasMeshSize (T : Finset (Fin 3 → Euclidean 2)) (h : ℝ) : Prop :=
  (∀ p ∈ T, Metric.diam (tri p) ≤ h) ∧ ∃ p ∈ T, Metric.diam (tri p) = h

/-- Regular family {T_h}, with h ranging over an index set H ⊆ (0,1) of mesh parameters.
For each h ∈ H, T_h is a triangulation with mesh size h = max_K diam K.
All angles of all triangles are bounded below independently of h.
The uncovered set Omega minus Omega_h has width O(h^2), uniformly in h: every point of Omega
not covered by the triangulation lies within C h^2 of Gamma (Sect. 5.2, Fig. 5.5). -/
def IsRegularFamily (Ω : Set (Euclidean 2)) (H : Set ℝ)
    (T : ℝ → Finset (Fin 3 → Euclidean 2)) : Prop :=
  (∀ h ∈ H, IsTriangulation Ω (T h) ∧ HasMeshSize (T h) h) ∧
  (∃ θ₀ : ℝ, 0 < θ₀ ∧ ∀ h ∈ H, ∀ p ∈ T h, ∀ i j k : Fin 3,
    i ≠ j → j ≠ k → i ≠ k → θ₀ ≤ EuclideanGeometry.angle (p i) (p j) (p k)) ∧
  (∃ Cw : ℝ, ∀ h ∈ H, ∀ x : Euclidean 2, x ∈ Ω → x ∉ Ωh (T h) →
    Metric.infDist x (frontier Ω) ≤ Cw * h ^ 2)

/-- S_h: continuous on closure Omega, linear on each K, zero on Gamma, zero off Omega_h. -/
def InSh (Ω : Set (Euclidean 2)) (T : Finset (Fin 3 → Euclidean 2))
    (v : Euclidean 2 → ℝ) : Prop :=
  ContinuousOn v (closure Ω) ∧
  (∀ p ∈ T, ∃ f : Euclidean 2 →ᵃ[ℝ] ℝ, Set.EqOn v f (tri p)) ∧
  (∀ x ∈ frontier Ω, v x = 0) ∧ (∀ x, x ∉ Ωh T → v x = 0)

/-- Min-max (Rayleigh quotient) value for a(v,w) = (grad v, grad w).
The infimum is taken over n-dimensional subspaces of admissible functions, each given by an
L2-orthonormal basis. This is the n-th eigenvalue counted with multiplicity. -/
def minmaxValue (Ω : Set (Euclidean 2)) (Adm : (Euclidean 2 → ℝ) → Prop) (n : ℕ) : ℝ :=
  sInf {μ : ℝ | ∃ (v : Fin n → Euclidean 2 → ℝ) (G : Fin n → Fin 2 → Euclidean 2 → ℝ),
    (∀ i, Adm (v i) ∧ HasH1Gradient Ω (v i) (G i)) ∧
    (∀ i j, (∫ x in Ω, v i x * v j x) = if i = j then 1 else 0) ∧
    μ = ⨆ c : {c : Fin n → ℝ // ∑ i, c i ^ 2 = 1},
      ∫ x in Ω, ∑ k : Fin 2, (∑ i, c.1 i * G i k x) ^ 2}

/-- lambda_n: n-th eigenvalue of (6.31), -Δu = λu in Ω, u = 0 on Γ (weak H¹₀ form). -/
def dirichletEigenvalue (Ω : Set (Euclidean 2)) (n : ℕ) : ℝ :=
  minmaxValue Ω (InH10Closure Ω) n

/-- lambda_{n,h}: n-th eigenvalue of (6.32), a(u_h,χ) = λ(u_h,χ) for all χ in S_h. -/
def discreteEigenvalue (Ω : Set (Euclidean 2)) (T : Finset (Fin 3 → Euclidean 2))
    (n : ℕ) : ℝ :=
  minmaxValue Ω (InSh Ω T) n

/-- Theorem 6.7 (6.34).
The family {T_h} is indexed by the set H ⊆ (0,1) of its mesh parameters. The bound holds for
every h ∈ H with h ≤ h₀. The constants C and h₀ are chosen after Ω, the family and n are
fixed. -/
theorem thm_6_7 (Ω : Set (Euclidean 2)) (hopen : IsOpen Ω) (hconn : IsConnected Ω)
    (hconv : Convex ℝ Ω) (hsmooth : SmoothBoundary Ω)
    (H : Set ℝ) (hH : H ⊆ Set.Ioo 0 1)
    (T : ℝ → Finset (Fin 3 → Euclidean 2)) (hT : IsRegularFamily Ω H T)
    (n : ℕ) (hn : 1 ≤ n) :
    ∃ C h₀ : ℝ, 0 < h₀ ∧ ∀ h ∈ H, h ≤ h₀ →
      dirichletEigenvalue Ω n ≤ discreteEigenvalue Ω (T h) n ∧
      discreteEigenvalue Ω (T h) n ≤ dirichletEigenvalue Ω n + C * h ^ 2 := by
  sorry

end PDETextbook.LarssonThomee.Thm67