Supremum-norm contraction of the heat flow

import PDETextbook.Base

open MeasureTheory
open scoped BigOperators ENNReal

noncomputable section

namespace PDETextbook.LarssonThomee.Thm82

/-- The solution operator `E(t)` of the heat equation (8.1) on `ℝ^d`.
For `t > 0` it is the formula (8.6):
`(E(t)v)(x) = (4πt)^{-d/2} ∫_{ℝ^d} v(y) e^{-|x-y|²/4t} dy`.
At `t = 0` the initial condition `u(·,0) = v` of (8.1) gives `E(0)v = v`.
Values for `t < 0` are never used. -/
def heatSolutionOp (d : ℕ) (t : ℝ) (v : Euclidean d → ℝ) (x : Euclidean d) : ℝ :=
  if t = 0 then v x
  else (4 * Real.pi * t) ^ (-(d : ℝ) / 2) *
    ∫ y : Euclidean d, v y * Real.exp (-(‖x - y‖ ^ 2) / (4 * t))

/-- Theorem 8.2. Here `𝒞` is the space of bounded continuous functions on `ℝ^d` with the
supremum norm, realized as Mathlib's `BoundedContinuousFunction (Euclidean d) ℝ`.

(8.7): for every `v ∈ 𝒞` and `t ≥ 0`, `E(t)v` is again in `𝒞` and `‖E(t)v‖_𝒞 ≤ ‖v‖_𝒞`.

(8.8): for bounded continuous `v₁, v₂`, the corresponding solutions `u_i(t) = E(t)v_i`
of (8.1) satisfy `‖u₁(t) - u₂(t)‖_𝒞 ≤ ‖v₁ - v₂‖_𝒞` for `t ≥ 0`. -/
theorem thm_8_2 (d : ℕ) :
    (∀ (v : BoundedContinuousFunction (Euclidean d) ℝ) (t : ℝ), 0 ≤ t →
      ∃ w : BoundedContinuousFunction (Euclidean d) ℝ,
        (⇑w = heatSolutionOp d t v) ∧ ‖w‖ ≤ ‖v‖) ∧
    (∀ (v₁ v₂ : BoundedContinuousFunction (Euclidean d) ℝ) (t : ℝ), 0 ≤ t →
      ∃ w : BoundedContinuousFunction (Euclidean d) ℝ,
        (⇑w = fun x => heatSolutionOp d t v₁ x - heatSolutionOp d t v₂ x) ∧
        ‖w‖ ≤ ‖v₁ - v₂‖) := by
  sorry

end PDETextbook.LarssonThomee.Thm82