Second-order L2 error on convex polygonal domains

import PDETextbook.Base

open MeasureTheory
open scoped BigOperators ENNReal

noncomputable section

namespace PDETextbook.LarssonThomee.Thm54

/-- Sect. 5.2: a polygonal domain in R^2 (open, connected), whose boundary Γ is a polygon. -/
def IsPolygonalDomain (Ω : Set (Euclidean 2)) : Prop :=
  IsOpen Ω ∧ IsConnected Ω ∧
    ∃ (n : ℕ) (P : Fin (n + 3) → Euclidean 2),
      frontier Ω = ⋃ i : Fin (n + 3), segment ℝ (P i) (P (i + 1))

/-- Closed triangle with vertices K 0, K 1, K 2. -/
def tri (K : Fin 3 → Euclidean 2) : Set (Euclidean 2) := convexHull ℝ (Set.range K)

/-- Sect. 5.2 triangulation T_h of Ω. -/
structure Triangulation (Ω : Set (Euclidean 2)) where
  tris : Finset (Fin 3 → Euclidean 2)
  affineIndep : ∀ K ∈ tris, AffineIndependent ℝ K
  covers : closure Ω = ⋃ K ∈ tris, tri K
  conforming : ∀ K ∈ tris, ∀ K' ∈ tris, tri K ≠ tri K' →
    (tri K ∩ tri K' = ∅) ∨
    (∃ i j, K i = K' j ∧ tri K ∩ tri K' = {K i}) ∨
    (∃ i₁ i₂ j₁ j₂, i₁ ≠ i₂ ∧ K i₁ = K' j₁ ∧ K i₂ = K' j₂ ∧
      tri K ∩ tri K' = segment ℝ (K i₁) (K i₂))
  noHangingNode : ∀ K ∈ tris, ∀ K' ∈ tris, ∀ i j k : Fin 3, i ≠ j →
    K' k ∉ openSegment ℝ (K i) (K j)

/-- h = max_K diam K. -/
def meshSize {Ω : Set (Euclidean 2)} (T : Triangulation Ω) : ℝ :=
  ⨆ K ∈ T.tris, Metric.diam (tri K)

/-- S_h: continuous on the closure of Ω, linear in each K, vanishing on Γ. -/
def Sh {Ω : Set (Euclidean 2)} (T : Triangulation Ω) : Set (Euclidean 2 → ℝ) :=
  {v | ContinuousOn v (closure Ω) ∧
    (∀ K ∈ T.tris, ∃ L : Euclidean 2 →ᵃ[ℝ] ℝ, ∀ x ∈ tri K, v x = L x) ∧
    ∀ x ∈ frontier Ω, v x = 0}

/-- a(v,w) = ∫_Ω a ∇v·∇w via weak gradients. -/
def aForm (Ω : Set (Euclidean 2)) (a : Euclidean 2 → ℝ)
    (Gv Gw : Fin 2 → Euclidean 2 → ℝ) : ℝ :=
  ∫ x in Ω, a x * ∑ i, Gv i x * Gw i x

/-- (5.24). -/
def IsVariationalSolution (Ω : Set (Euclidean 2)) (a f u : Euclidean 2 → ℝ) : Prop :=
  InH10Closure Ω u ∧
    ∀ Gu, HasH1Gradient Ω u Gu → ∀ v : Euclidean 2 → ℝ, ∀ Gv, InH10Closure Ω v →
      HasH1Gradient Ω v Gv → aForm Ω a Gu Gv = ∫ x in Ω, f x * v x

/-- (5.26). -/
def IsFESolution {Ω : Set (Euclidean 2)} (a f : Euclidean 2 → ℝ) (T : Triangulation Ω)
    (uh : Euclidean 2 → ℝ) : Prop :=
  uh ∈ Sh T ∧
    ∀ Gu, HasH1Gradient Ω uh Gu → ∀ χ ∈ Sh T, ∀ Gχ, HasH1Gradient Ω χ Gχ →
      aForm Ω a Gu Gχ = ∫ x in Ω, f x * χ x

/-- L2 norm on Ω. -/
def l2Norm (Ω : Set (Euclidean 2)) (v : Euclidean 2 → ℝ) : ℝ :=
  Real.sqrt (∫ x in Ω, v x ^ 2)

/-- ‖u‖_2 over |α| ≤ 2; H i j = ∂_j ∂_i u, each multi-index counted once (i ≤ j). -/
def H2Norm (Ω : Set (Euclidean 2)) (u : Euclidean 2 → ℝ)
    (G : Fin 2 → Euclidean 2 → ℝ) (H : Fin 2 → Fin 2 → Euclidean 2 → ℝ) : ℝ :=
  Real.sqrt ((∫ x in Ω, u x ^ 2) + ∑ i, (∫ x in Ω, G i x ^ 2) +
    ∑ i, ∑ j, if i ≤ j then (∫ x in Ω, H i j x ^ 2) else 0)

/-- Theorem 5.4: ‖u_h − u‖ ≤ C h² ‖u‖_2 for convex polygonal Ω.
The family {T_h} is indexed by an arbitrary set `Hs ⊆ (0,1)` of mesh sizes, with
`meshSize (T h) = h` for `h ∈ Hs`. All triangle angles in the family are bounded below
by a common θ₀ > 0 (Sect. 5.3). C may depend on the family, Ω and a, but not on h, f, u or u_h. -/
theorem thm_5_4 (Ω : Set (Euclidean 2)) (hpoly : IsPolygonalDomain Ω) (hconv : Convex ℝ Ω)
    (a : Euclidean 2 → ℝ) (a₀ : ℝ) (ha₀ : 0 < a₀)
    (ha_smooth : ContDiffOn ℝ (⊤ : ℕ∞) a (closure Ω))
    (ha_lower : ∀ x ∈ closure Ω, a₀ ≤ a x)
    (Hs : Set ℝ) (hHs : Hs ⊆ Set.Ioo (0 : ℝ) 1)
    (T : ℝ → Triangulation Ω)
    (hT_mesh : ∀ h ∈ Hs, meshSize (T h) = h)
    (hT_angle : ∃ θ₀ > (0 : ℝ), ∀ h ∈ Hs, ∀ K ∈ (T h).tris,
      ∀ i j k : Fin 3, i ≠ j → i ≠ k → j ≠ k →
        θ₀ ≤ EuclideanGeometry.angle (K j) (K i) (K k)) :
    ∃ C : ℝ, ∀ f : Euclidean 2 → ℝ, InL2 Ω f →
      ∀ u : Euclidean 2 → ℝ, IsVariationalSolution Ω a f u →
      ∀ h ∈ Hs, ∀ uh : Euclidean 2 → ℝ, IsFESolution a f (T h) uh →
        ∃ (G : Fin 2 → Euclidean 2 → ℝ) (H : Fin 2 → Fin 2 → Euclidean 2 → ℝ),
          HasH1Gradient Ω u G ∧ (∀ i, HasH1Gradient Ω (G i) (H i)) ∧
          l2Norm Ω (fun x => uh x - u x) ≤ C * h ^ 2 * H2Norm Ω u G H := by
  sorry

end PDETextbook.LarssonThomee.Thm54