Decay of the Dirichlet heat energy seminorm

import PDETextbook.Base

open MeasureTheory
open scoped BigOperators ENNReal

noncomputable section

namespace PDETextbook.LarssonThomee.Thm84

open Filter Topology

/-- `Ω` has smooth boundary `Γ = ∂Ω`: near every boundary point, `Ω` is the sublevel set
`{ρ < 0}` of a C^∞ function `ρ` with nonvanishing differential. -/
def SmoothBoundary {d : ℕ} (Ω : Set (Euclidean d)) : Prop :=
  ∀ p ∈ frontier Ω, ∃ U ∈ 𝓝 p, ∃ ρ : Euclidean d → ℝ,
    (∀ n : ℕ, ContDiff ℝ n ρ) ∧ (∀ x ∈ U, fderiv ℝ ρ x ≠ 0) ∧
    Ω ∩ U = {x | ρ x < 0} ∩ U

/-- Classical Laplacian `Δw = Σ_i ∂²w/∂x_i²`. -/
def laplacian {d : ℕ} (w : Euclidean d → ℝ) (x : Euclidean d) : ℝ :=
  ∑ i : Fin d, partialDeriv (fun y => partialDeriv w i y) i x

/-- `{φ_j}` is an orthonormal basis of `L₂(Ω)` of classical Dirichlet eigenfunctions:
`-Δφ_j = λ_j φ_j` in `Ω`, `φ_j = 0` on `Γ`. -/
def IsDirichletEigenbasis {d : ℕ} (Ω : Set (Euclidean d))
    (lam : ℕ → ℝ) (φ : ℕ → Euclidean d → ℝ) : Prop :=
  (∀ j, (∀ n : ℕ, ContDiffOn ℝ n (φ j) Ω) ∧ ContinuousOn (φ j) (closure Ω) ∧
      (∀ x ∈ frontier Ω, φ j x = 0) ∧
      (∀ x ∈ Ω, -laplacian (φ j) x = lam j * φ j x)) ∧
  (∀ i j, (∫ x in Ω, φ i x * φ j x) = if i = j then 1 else 0) ∧
  (∀ w : Euclidean d → ℝ, InL2 Ω w → (∀ j, (∫ x in Ω, w x * φ j x) = 0) →
      w =ᵐ[domainMeasure Ω] 0)

/-- `u(·,t)` is given by the eigenfunction expansion (8.13),
`u(t) = Σ_j e^{-λ_j t} (v, φ_j) φ_j`, convergent in `L₂(Ω)`. -/
def IsEigenExpansionSolution {d : ℕ} (Ω : Set (Euclidean d))
    (lam : ℕ → ℝ) (φ : ℕ → Euclidean d → ℝ) (v : Euclidean d → ℝ)
    (u : Euclidean d → ℝ → ℝ) : Prop :=
  ∀ t : ℝ, 0 ≤ t → InL2 Ω (fun x => u x t) ∧
    Tendsto (fun N : ℕ => eLpNorm (fun x =>
        (∑ j ∈ Finset.range N,
          Real.exp (-lam j * t) * (∫ y in Ω, v y * φ j y) * φ j x) - u x t)
        2 (domainMeasure Ω)) atTop (𝓝 0)

/-- The H¹ seminorm `|w|_1 = ‖∇w‖ = (Σ_i ∫_Ω (∂w/∂x_i)²)^{1/2}`, in terms of a weak gradient `G`. -/
def h1Seminorm {d : ℕ} (Ω : Set (Euclidean d)) (G : Fin d → Euclidean d → ℝ) : ℝ :=
  Real.sqrt (∑ i : Fin d, ∫ x in Ω, (G i x) ^ 2)

/-- Theorem 8.4 (Larsson–Thomée). For `v ∈ H₀¹`, the solution of (8.10) given by the
eigenfunction expansion (8.13) of Theorem 8.3 satisfies `|u(·,t)|_1 ≤ |v|_1` for `t ≥ 0`.
The conclusion includes `u(·,t) ∈ H¹`, so that `|u(·,t)|_1` is defined. -/
theorem thm_8_4 {d : ℕ} (Ω : Set (Euclidean d))
    (hΩopen : IsOpen Ω) (hΩconn : IsConnected Ω) (hΩbdd : Bornology.IsBounded Ω)
    (hΓ : SmoothBoundary Ω)
    (lam : ℕ → ℝ) (φ : ℕ → Euclidean d → ℝ) (hφ : IsDirichletEigenbasis Ω lam φ)
    (v : Euclidean d → ℝ) (hv : InH10Closure Ω v)
    (u : Euclidean d → ℝ → ℝ) (hu : IsEigenExpansionSolution Ω lam φ v u) :
    ∀ t : ℝ, 0 ≤ t →
      InH1 Ω (fun x => u x t) ∧
      ∀ Gu Gv : Fin d → Euclidean d → ℝ,
        HasH1Gradient Ω (fun x => u x t) Gu → HasH1Gradient Ω v Gv →
          h1Seminorm Ω Gu ≤ h1Seminorm Ω Gv := by
  sorry

end PDETextbook.LarssonThomee.Thm84