Dirichlet heat expansion and smoothing

import PDETextbook.Base

open MeasureTheory
open scoped BigOperators ENNReal

noncomputable section

namespace PDETextbook.LarssonThomee.Thm83

/-- Bounded domain with smooth (C^∞) boundary, realized by a global smooth defining
function `ρ` with `Ω = {ρ < 0}` and `∇ρ ≠ 0` on `Γ = ∂Ω`. -/
def IsBoundedSmoothDomain {d : ℕ} (Ω : Set (Euclidean d)) : Prop :=
  IsOpen Ω ∧ IsConnected Ω ∧ Bornology.IsBounded Ω ∧
  ∃ ρ : Euclidean d → ℝ, ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) ρ ∧
    Ω = {x | ρ x < 0} ∧ ∀ x ∈ frontier Ω, fderiv ℝ ρ x ≠ 0

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

/-- Dirichlet eigenpair `-Δφ = λφ` in `Ω`, `φ = 0` on `Γ`, in weak form:
`φ ∈ H₀¹` and `(∇φ, ∇w) = λ (φ, w)` for all compactly supported C¹ `w`. -/
def IsDirichletEigenpair {d : ℕ} (Ω : Set (Euclidean d)) (lam : ℝ)
    (φ : Euclidean d → ℝ) : Prop :=
  InH10Closure Ω φ ∧
  ∃ G : Fin d → Euclidean d → ℝ, HasH1Gradient Ω φ G ∧
    ∀ w : Euclidean d → ℝ, CompactC1 Ω w →
      (∫ x in Ω, ∑ j, G j x * partialDeriv w j x) = lam * ∫ x in Ω, φ x * w x

/-- The eigenfunctions `φ_i` (continuous representatives in `Ω`) with eigenvalues `λ_i`
form an orthonormal basis of `L₂(Ω)` (index shift `i ↦ i+1` relative to the book). -/
def IsDirichletEigensystem {d : ℕ} (Ω : Set (Euclidean d)) (lam : ℕ → ℝ)
    (φ : ℕ → Euclidean d → ℝ) : Prop :=
  (∀ i, IsDirichletEigenpair Ω (lam i) (φ i) ∧ ContinuousOn (φ i) Ω) ∧
  ∃ hL2 : ∀ i, InL2 Ω (φ i),
    Orthonormal ℝ (fun i => (hL2 i).toLp (φ i)) ∧
    (Submodule.span ℝ (Set.range fun i => (hL2 i).toLp (φ i))).topologicalClosure = ⊤

/-- The function (8.13): `u(x,t) = Σ_i v̂_i e^{-λ_i t} φ_i(x)`, `v̂_i = ∫_Ω v φ_i dx`. -/
def heatSeries {d : ℕ} (Ω : Set (Euclidean d)) (lam : ℕ → ℝ)
    (φ : ℕ → Euclidean d → ℝ) (v : Euclidean d → ℝ) (x : Euclidean d) (t : ℝ) : ℝ :=
  ∑' i, (∫ y in Ω, v y * φ i y) * Real.exp (-(lam i * t)) * φ i x

/-- Classical solution of `u_t - Δu = 0` in `Ω × ℝ₊`. -/
def IsClassicalHeatSolution {d : ℕ} (Ω : Set (Euclidean d))
    (u : Euclidean d → ℝ → ℝ) : Prop :=
  ContDiffOn ℝ 2 (fun p : Euclidean d × ℝ => u p.1 p.2) (Ω ×ˢ Set.Ioi 0) ∧
  ∀ x ∈ Ω, ∀ t : ℝ, 0 < t →
    HasDerivAt (fun s => u x s) (laplacian (fun y => u y t) x) t

/-- Mixed partial derivative `D^α w` for a multi-index `α`. -/
def mixedPartial {d : ℕ} (w : Euclidean d → ℝ) (α : Fin d → ℕ) : Euclidean d → ℝ :=
  (List.finRange d).foldr
    (fun j f => (fun g : Euclidean d → ℝ => fun x => partialDeriv g j x)^[α j] f) w

/-- Sobolev norm `‖w‖_s = (Σ_{|α| ≤ s} ‖D^α w‖²)^{1/2}` on `Ω` (ENNReal-valued). -/
def sobolevNorm {d : ℕ} (Ω : Set (Euclidean d)) (s : ℕ) (w : Euclidean d → ℝ) : ℝ≥0∞ :=
  (∑ α ∈ (Finset.univ.filter fun α : Fin d → Fin (s + 1) => ∑ j, (α j : ℕ) ≤ s),
      eLpNorm (mixedPartial w (fun j => (α j : ℕ))) 2 (domainMeasure Ω) ^ 2) ^ (1 / 2 : ℝ)

/-- Theorem 8.3 (Larsson–Thomée). For `v ∈ L₂`, the function (8.13) is a classical
solution of the heat equation in (8.10), vanishes on `Γ` for `t > 0`, satisfies (8.14),
and the smoothness estimate (8.17) holds. -/
theorem thm_8_3 {d : ℕ} (Ω : Set (Euclidean d)) (hΩ : IsBoundedSmoothDomain Ω)
    (lam : ℕ → ℝ) (φ : ℕ → Euclidean d → ℝ) (hφ : IsDirichletEigensystem Ω lam φ) :
    (∀ v : Euclidean d → ℝ, InL2 Ω v →
      IsClassicalHeatSolution Ω (heatSeries Ω lam φ v) ∧
      (∀ t : ℝ, 0 < t → ∀ z ∈ frontier Ω,
        Filter.Tendsto (fun x => heatSeries Ω lam φ v x t) (nhdsWithin z Ω) (nhds 0)) ∧
      Filter.Tendsto
        (fun t => eLpNorm (fun x => heatSeries Ω lam φ v x t - v x) 2 (domainMeasure Ω))
        (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)) ∧
    (∀ s m : ℕ, ∃ C : ℝ, ∀ v : Euclidean d → ℝ, InL2 Ω v → ∀ t : ℝ, 0 < t →
      sobolevNorm Ω s
          (fun x => iteratedDeriv m (fun τ => heatSeries Ω lam φ v x τ) t) ≤
        ENNReal.ofReal (C * t ^ (-(m : ℝ) - (s : ℝ) / 2)) * eLpNorm v 2 (domainMeasure Ω)) := by
  sorry

end PDETextbook.LarssonThomee.Thm83