Uniqueness of bounded whole-space heat solutions

import PDETextbook.Base

open MeasureTheory
open scoped BigOperators ENNReal

noncomputable section

namespace PDETextbook.LarssonThomee.Thm88

/-- Spatial Laplacian `Δw(x) = ∑ᵢ ∂²w/∂xᵢ²(x)`, built from classical partial derivatives.
It is used only on functions assumed to be C² in space. -/
def spatialLaplacian {d : ℕ} (w : Euclidean d → ℝ) (x : Euclidean d) : ℝ :=
  ∑ i : Fin d, partialDeriv (fun y => partialDeriv w i y) i x

/-- A (classical) solution of the pure initial value problem (8.1):
`∂u/∂t - Δu = 0` in `ℝ^d × ℝ_+`, `u(·,0) = v` in `ℝ^d`.
Here `u x t` is the value at `(x,t)`. Regularity: `u` is continuous on `ℝ^d × [0,∞)`.
For each `t > 0` it is C² in `x`, and it is differentiable in `t` there. -/
structure IsHeatIVPSolution {d : ℕ} (v : Euclidean d → ℝ) (u : Euclidean d → ℝ → ℝ) : Prop where
  cont : ContinuousOn (fun p : Euclidean d × ℝ => u p.1 p.2) (Set.univ ×ˢ Set.Ici (0 : ℝ))
  space_C2 : ∀ t : ℝ, 0 < t → ContDiff ℝ 2 (fun x => u x t)
  time_diff : ∀ x : Euclidean d, ∀ t : ℝ, 0 < t → DifferentiableAt ℝ (fun s => u x s) t
  pde : ∀ x : Euclidean d, ∀ t : ℝ, 0 < t →
    deriv (fun s => u x s) t - spatialLaplacian (fun y => u y t) x = 0
  init : ∀ x : Euclidean d, u x 0 = v x

/-- Boundedness of `u` in the strip `ℝ^d × [0,T]`. -/
def BoundedInStrip {d : ℕ} (u : Euclidean d → ℝ → ℝ) (T : ℝ) : Prop :=
  ∃ M : ℝ, ∀ x : Euclidean d, ∀ t ∈ Set.Icc (0 : ℝ) T, |u x t| ≤ M

/-- Theorem 8.8: the initial value problem (8.1) has at most one solution which is
bounded in `ℝ^d × [0,T]`, with `T` arbitrary. Two solutions with the same initial data `v`
that are both bounded in the strip coincide on the strip. -/
theorem thm_8_8 {d : ℕ} (v : Euclidean d → ℝ) (T : ℝ) (hT : 0 < T)
    (u₁ u₂ : Euclidean d → ℝ → ℝ)
    (h₁ : IsHeatIVPSolution v u₁) (h₂ : IsHeatIVPSolution v u₂)
    (hb₁ : BoundedInStrip u₁ T) (hb₂ : BoundedInStrip u₂ T) :
    ∀ x : Euclidean d, ∀ t ∈ Set.Icc (0 : ℝ) T, u₁ x t = u₂ x t := by
  sorry

end PDETextbook.LarssonThomee.Thm88