Maximum principles on bounded domains

import PDETextbook.Base

open MeasureTheory
open scoped BigOperators ENNReal

noncomputable section

namespace PDETextbook
namespace LarssonThomee.Thm31

/-- Smooth (C^∞) boundary: near each boundary point, Ω is the sublevel set `{ψ < 0}` of a local
C^∞ defining function `ψ` whose differential does not vanish on `Γ = ∂Ω`. -/
def HasSmoothBoundary {d : ℕ} (Ω : Set (Euclidean d)) : Prop :=
  ∀ p ∈ frontier Ω, ∃ U : Set (Euclidean d), IsOpen U ∧ p ∈ U ∧
    ∃ ψ : Euclidean d → ℝ, ContDiffOn ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) ψ U ∧
      (∀ x ∈ U ∩ frontier Ω, fderiv ℝ ψ x ≠ 0) ∧
      Ω ∩ U = {x | x ∈ U ∧ ψ x < 0}

/-- The book's `𝒞²(Ω̄)`: `v ∈ 𝒞²(Ω)` and `D^α v ∈ 𝒞(Ω̄)` for all `|α| ≤ 2`.
For `|α| = 0` this means `v` itself is continuous on `Ω̄`; for `|α| = 1, 2` the classical
partial derivatives on `Ω` extend continuously to `Ω̄`. -/
def InC2Closure {d : ℕ} (Ω : Set (Euclidean d)) (v : Euclidean d → ℝ) : Prop :=
  ContDiffOn ℝ 2 v Ω ∧
  ContinuousOn v (closure Ω) ∧
  (∀ i : Fin d, ∃ G : Euclidean d → ℝ, ContinuousOn G (closure Ω) ∧
      Set.EqOn G (partialDeriv v i) Ω) ∧
  (∀ i j : Fin d, ∃ H : Euclidean d → ℝ, ContinuousOn H (closure Ω) ∧
      Set.EqOn H (partialDeriv (partialDeriv v j) i) Ω)

/-- The operator (3.1): `𝒜u = -∇·(a∇u) + b·∇u + cu`, evaluated classically at `x`. -/
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

/-- Theorem 3.1 (maximum principle). Ω ⊂ ℝ^d (d = 1,2,3) is a bounded domain with smooth
boundary Γ = ∂Ω; the coefficients a, b, c are smooth in Ω with a ≥ a₀ > 0 and c ≥ 0 in Ω (3.2);
u ∈ 𝒞²(Ω̄). If 𝒜u ≤ 0 in Ω then (i) c = 0 gives max_Ω̄ u = max_Γ u and (ii) c ≥ 0 gives
max_Ω̄ u ≤ max{max_Γ u, 0}; if 𝒜u ≥ 0 the corresponding minimum statements hold. -/
theorem maximum_principle {d : ℕ} (hd : 1 ≤ d ∧ d ≤ 3)
    (Ω : Set (Euclidean d)) (hΩopen : IsOpen Ω) (hΩconn : IsConnected Ω)
    (hΩbdd : Bornology.IsBounded Ω) (hΓ : HasSmoothBoundary Ω)
    (a : Euclidean d → ℝ) (b : Euclidean d → Euclidean d) (c : Euclidean d → ℝ)
    (ha : ContDiffOn ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) a Ω)
    (hb : ContDiffOn ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) b Ω)
    (hc : ContDiffOn ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) c Ω)
    (a₀ : ℝ) (ha₀ : 0 < a₀) (ha_ge : ∀ x ∈ Ω, a₀ ≤ a x)
    (hc_nonneg : ∀ x ∈ Ω, 0 ≤ c x)
    (u : Euclidean d → ℝ) (hu : InC2Closure Ω u) :
    ((∀ x ∈ Ω, opA a b c u x ≤ 0) →
      ((∀ x ∈ Ω, c x = 0) →
          sSup (u '' closure Ω) = sSup (u '' frontier Ω)) ∧
      ((∀ x ∈ Ω, 0 ≤ c x) →
          sSup (u '' closure Ω) ≤ max (sSup (u '' frontier Ω)) 0)) ∧
    ((∀ x ∈ Ω, 0 ≤ opA a b c u x) →
      ((∀ x ∈ Ω, c x = 0) →
          sInf (u '' closure Ω) = sInf (u '' frontier Ω)) ∧
      ((∀ x ∈ Ω, 0 ≤ c x) →
          min (sInf (u '' frontier Ω)) 0 ≤ sInf (u '' closure Ω))) := by
  sorry

end LarssonThomee.Thm31
end PDETextbook