Energy estimates for the forced heat equation

import PDETextbook.Base

open MeasureTheory
open scoped BigOperators ENNReal

noncomputable section

namespace PDETextbook.LarssonThomee.Thm85

/-- `‖w‖² = ∫_Ω w² dx` (real L² norm squared), valued in ℝ≥0∞. -/
def l2NormSq {d : ℕ} (Ω : Set (Euclidean d)) (w : Euclidean d → ℝ) : ℝ≥0∞ :=
  ∫⁻ x in Ω, ENNReal.ofReal (w x ^ 2)

/-- `|∇w(x)|² = Σᵢ (∂ᵢ w(x))²`, i.e. `Σ_{|α|=1} (D^α w(x))²`. -/
def gradNormSq {d : ℕ} (w : Euclidean d → ℝ) (x : Euclidean d) : ℝ :=
  ∑ i, (partialDeriv w i x) ^ 2

/-- `|w|₁² = Σ_{|α|=1} ‖D^α w‖² = ∫_Ω |∇w|² dx`. -/
def h1SeminormSq {d : ℕ} (Ω : Set (Euclidean d)) (w : Euclidean d → ℝ) : ℝ≥0∞ :=
  ∫⁻ x in Ω, ENNReal.ofReal (gradNormSq w x)

/-- Time derivative `u_t(x,t)`. -/
def timeDeriv {d : ℕ} (u : ℝ → Euclidean d → ℝ) (t : ℝ) (x : Euclidean d) : ℝ :=
  deriv (fun s => u s x) t

/-- `(v,w) = ∫_Ω v w dx`. -/
def l2Pair {d : ℕ} (Ω : Set (Euclidean d)) (v w : Euclidean d → ℝ) : ℝ :=
  ∫ x in Ω, v x * w x

/-- `a(w,φ) = ∫_Ω ∇w · ∇φ dx`, with `Gφ` the weak gradient of `φ`. -/
def bilinA {d : ℕ} (Ω : Set (Euclidean d)) (w : Euclidean d → ℝ)
    (Gφ : Fin d → Euclidean d → ℝ) : ℝ :=
  ∫ x in Ω, ∑ i, partialDeriv w i x * Gφ i x

/-- Smooth (C^∞) boundary, via local defining functions. Every boundary point `p` has an
open neighbourhood `U` and a C^∞ function `ψ` with nonvanishing differential at `p`
such that `Ω ∩ U = {x ∈ U | ψ x < 0}`. This is the standard level-set form of the
local-graph definition of a smooth boundary. -/
def HasSmoothBoundary {d : ℕ} (Ω : Set (Euclidean d)) : Prop :=
  ∀ p ∈ frontier Ω, ∃ U : Set (Euclidean d), IsOpen U ∧ p ∈ U ∧
    ∃ ψ : Euclidean d → ℝ, ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) ψ ∧
      fderiv ℝ ψ p ≠ 0 ∧ Ω ∩ U = {x | x ∈ U ∧ ψ x < 0}

/-- (8.29): `(u_t, φ) + a(u, φ) = (f, φ)` for all `φ ∈ H₀¹`, `t ∈ ℝ₊`. -/
def SatisfiesEq829 {d : ℕ} (Ω : Set (Euclidean d)) (u f : ℝ → Euclidean d → ℝ) : Prop :=
  ∀ t : ℝ, 0 < t → ∀ (φ : Euclidean d → ℝ) (Gφ : Fin d → Euclidean d → ℝ),
    InH10Closure Ω φ → HasH1Gradient Ω φ Gφ →
      l2Pair Ω (timeDeriv u t) φ + bilinA Ω (u t) Gφ = l2Pair Ω (f t) φ

/-- (8.30): `u(·,0) = v` in `Ω`. -/
def SatisfiesEq830 {d : ℕ} (Ω : Set (Euclidean d)) (u : ℝ → Euclidean d → ℝ)
    (v : Euclidean d → ℝ) : Prop :=
  ∀ x ∈ Ω, u 0 x = v x

/-- Theorem 8.5, estimates (8.31) and (8.32).

Setting (Chapter 8): `Ω` is a bounded domain (open and connected) in `ℝ^d`, `d ≥ 1`,
with smooth boundary `Γ = frontier Ω`.

"Appropriately smooth for t ≥ 0" is realized as joint `C^∞` in `(t,x)` on
`[0,∞) × closure Ω`.

Following the source's literal order ("Let u(t) satisfy ... Then there is a constant C
such that, for t ≥ 0"), `C` is chosen after `u`, `f`, `v` and before `t`.

`C` enters through `ENNReal.ofReal C`, so requiring `0 ≤ C` loses nothing. -/
theorem thm_8_5 {d : ℕ} (hd : 0 < d) (Ω : Set (Euclidean d)) (hΩopen : IsOpen Ω)
    (hΩconn : IsConnected Ω) (hΩbdd : Bornology.IsBounded Ω)
    (hΓ : HasSmoothBoundary Ω)
    (u f : ℝ → Euclidean d → ℝ) (v : Euclidean d → ℝ)
    (hsmooth : ContDiffOn ℝ ((⊤ : ℕ∞) : WithTop ℕ∞)
      (fun p : ℝ × Euclidean d => u p.1 p.2) (Set.Ici (0 : ℝ) ×ˢ closure Ω))
    (hbdry : ∀ t : ℝ, 0 ≤ t → ∀ x ∈ frontier Ω, u t x = 0)
    (hf : ∀ t : ℝ, 0 < t → InL2 Ω (f t))
    (h829 : SatisfiesEq829 Ω u f)
    (h830 : SatisfiesEq830 Ω u v) :
    ∃ C : ℝ, 0 ≤ C ∧
      ∀ t : ℝ, 0 ≤ t →
        (l2NormSq Ω (u t) + ∫⁻ s in Set.Ioc 0 t, h1SeminormSq Ω (u s)
            ≤ l2NormSq Ω v + ENNReal.ofReal C * ∫⁻ s in Set.Ioc 0 t, l2NormSq Ω (f s)) ∧
        (h1SeminormSq Ω (u t) + ∫⁻ s in Set.Ioc 0 t, l2NormSq Ω (timeDeriv u s)
            ≤ h1SeminormSq Ω v + ∫⁻ s in Set.Ioc 0 t, l2NormSq Ω (f s)) := by
  sorry

end PDETextbook.LarssonThomee.Thm85