Supremum-norm stability on a bounded domain

import PDETextbook.Base

open MeasureTheory
open scoped BigOperators ENNReal

open scoped ContDiff

noncomputable section

namespace PDETextbook.LarssonThomee.Thm32

open PDETextbook

/-- Standing assumption (book §0): `Γ = ∂Ω` is smooth. Realized as a C^∞ local graph:
near each boundary point `Ω` is, after a rotation, the region below the graph of a smooth
function of the remaining coordinates. -/
def SmoothBoundary {d : ℕ} (Ω : Set (Euclidean d)) : Prop :=
  ∀ p ∈ frontier Ω, ∃ r : ℝ, 0 < r ∧
    ∃ e : Euclidean d ≃ₗᵢ[ℝ] Euclidean d, ∃ k : Fin d, ∃ h : Euclidean d → ℝ,
      ContDiff ℝ ∞ h ∧
      (∀ (y : Euclidean d) (t : ℝ), h (y + t • EuclideanSpace.single k (1 : ℝ)) = h y) ∧
      ∀ x ∈ Metric.ball p r, (x ∈ Ω ↔ e x k < h (e x))

/-- Standing assumption (book §0): `Γ` is a polygon (`d = 2`) or polyhedron (`d = 3`):
the boundary lies in finitely many affine lines/planes and `Ω` has no slits. -/
def PolygonalBoundary {d : ℕ} (Ω : Set (Euclidean d)) : Prop :=
  (d = 2 ∨ d = 3) ∧ interior (closure Ω) = Ω ∧
  ∃ H : Finset (Euclidean d × ℝ), (∀ q ∈ H, q.1 ≠ 0) ∧
    frontier Ω ⊆ ⋃ q ∈ H, {x : Euclidean d | inner ℝ q.1 x = q.2}

/-- The operator of (3.1): `𝒜u = -∇·(a∇u) + b·∇u + cu`, with scalar `a`, vector `b`,
scalar `c` (classical derivatives, used on the open set Ω). -/
def opA {d : ℕ} (a : Euclidean d → ℝ) (b : Euclidean d → Euclidean d)
    (c : Euclidean d → ℝ) (u : Euclidean d → ℝ) (x : Euclidean d) : ℝ :=
  -(∑ i : Fin d, partialDeriv (fun y => a y * partialDeriv u i y) i x)
    + (∑ i : Fin d, b x i * partialDeriv u i x) + c x * u x

/-- Maximum norm `‖f‖_{𝒞(S)} = sup_{x ∈ S} |f x|`. -/
def supNormOn {d : ℕ} (S : Set (Euclidean d)) (f : Euclidean d → ℝ) : ℝ :=
  ⨆ x : S, |f x|

/-- Theorem 3.2 (Larsson–Thomée). Under the standing assumptions on `Ω` (bounded domain
in `ℝ^d`, `d ∈ {1,2,3}`, `Γ` smooth or polygonal/polyhedral) and on the coefficients of
(3.1)–(3.2) (smooth, `a ≥ a₀ > 0`, `c ≥ 0` in Ω), there is a constant `C`, independent of
`u`, such that for every `u ∈ 𝒞²(Ω̄)`:
`‖u‖_{𝒞(Ω̄)} ≤ ‖u‖_{𝒞(Γ)} + C ‖𝒜u‖_{𝒞(Ω̄)}`.
The sup of the continuous extension of `𝒜u` over `Ω̄` equals its sup over the dense open `Ω`. -/
theorem thm_3_2 {d : ℕ} (hd : d = 1 ∨ d = 2 ∨ d = 3)
    (Ω : Set (Euclidean d)) (hΩopen : IsOpen Ω) (hΩconn : IsConnected Ω)
    (hΩbdd : Bornology.IsBounded Ω)
    (hΓ : SmoothBoundary Ω ∨ PolygonalBoundary Ω)
    (a : Euclidean d → ℝ) (b : Euclidean d → Euclidean d) (c : Euclidean d → ℝ)
    (ha : ContDiffOn ℝ ∞ a (closure Ω)) (hb : ContDiffOn ℝ ∞ b (closure Ω))
    (hc : ContDiffOn ℝ ∞ c (closure Ω))
    (a₀ : ℝ) (ha₀ : 0 < a₀) (ha_lower : ∀ x ∈ Ω, a₀ ≤ a x)
    (hc_nonneg : ∀ x ∈ Ω, 0 ≤ c x) :
    ∃ C : ℝ, ∀ u : Euclidean d → ℝ, ContDiffOn ℝ 2 u (closure Ω) →
      supNormOn (closure Ω) u ≤
        supNormOn (frontier Ω) u + C * supNormOn Ω (opA a b c u) := by
  sorry

end PDETextbook.LarssonThomee.Thm32