Parabolic maximum principle

import PDETextbook.Base

open MeasureTheory
open scoped BigOperators ENNReal

noncomputable section

namespace PDETextbook

namespace LarssonThomee.Thm86

/-- Time derivative `u_t` of a function `u(x,t)` on `ℝ^d × ℝ`.
This is the classical partial derivative in the `t` direction. -/
def timeDeriv {d : ℕ} (u : Euclidean d × ℝ → ℝ) (p : Euclidean d × ℝ) : ℝ :=
  fderiv ℝ u p ((0 : Euclidean d), (1 : ℝ))

/-- Spatial Laplacian `Δu = ∑_i ∂²u/∂x_i²` of `u(x,t)`, using classical partial derivatives
in the space variables only. -/
def spaceLaplacian {d : ℕ} (u : Euclidean d × ℝ → ℝ) (p : Euclidean d × ℝ) : ℝ :=
  ∑ i : Fin d,
    fderiv ℝ (fun q => fderiv ℝ u q (EuclideanSpace.single i (1 : ℝ), (0 : ℝ))) p
      (EuclideanSpace.single i (1 : ℝ), (0 : ℝ))

/-- Theorem 8.6 (Larsson–Thomée). Let `Ω ⊂ ℝ^d` be a bounded domain and `I = (0,T)` a finite
time interval, `T > 0`. Let `u` be smooth on the closed cylinder `Ω̄ × Ī` and assume
`u_t - Δu ≤ 0` in `Ω × I`. Then `u` attains its maximum over `Ω̄ × Ī` on the parabolic boundary
`Γ_p = (Γ × Ī) ∪ (Ω × {t = 0})`, where `Γ = ∂Ω` (Mathlib `frontier Ω`).
The sets `Ω × I = Ω ×ˢ Set.Ioo 0 T`, `Ω̄ × Ī = closure Ω ×ˢ Set.Icc 0 T` and `Γ_p` are written
inline in the statement. -/
theorem max_principle_heat {d : ℕ} (Ω : Set (Euclidean d)) (T : ℝ)
    (hΩopen : IsOpen Ω) (hΩconn : IsConnected Ω) (hΩbdd : Bornology.IsBounded Ω)
    (hT : 0 < T)
    (u : Euclidean d × ℝ → ℝ)
    (hu : ContDiffOn ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) u (closure Ω ×ˢ Set.Icc 0 T))
    (hineq : ∀ p ∈ Ω ×ˢ Set.Ioo 0 T, timeDeriv u p - spaceLaplacian u p ≤ 0) :
    ∃ p ∈ (frontier Ω ×ˢ Set.Icc 0 T) ∪ (Ω ×ˢ ({0} : Set ℝ)),
      ∀ q ∈ closure Ω ×ˢ Set.Icc 0 T, u q ≤ u p := by
  sorry

end LarssonThomee.Thm86

end PDETextbook