Wave energy inside a backward cone

import PDETextbook.Base

open MeasureTheory
open scoped BigOperators ENNReal

noncomputable section

namespace PDETextbook.LarssonThomee.Thm11_3

/-- The closed space-time half space `R^d × [0, ∞)` on which the solution of (11.8) lives
(PDE in `t > 0`, initial data at `t = 0`). -/
def halfSpace (d : ℕ) : Set (Euclidean d × ℝ) := Set.univ ×ˢ Set.Ici (0 : ℝ)

/-- `u_t(x,t)`, the time derivative, taken within the half space so it is meaningful at `t = 0`. -/
def timeDeriv {d : ℕ} (U : Euclidean d × ℝ → ℝ) (x : Euclidean d) (t : ℝ) : ℝ :=
  fderivWithin ℝ U (halfSpace d) (x, t) ((0 : Euclidean d), (1 : ℝ))

/-- `∂u/∂x_i (x,t)`, taken within the half space. -/
def spaceDeriv {d : ℕ} (U : Euclidean d × ℝ → ℝ) (i : Fin d) (x : Euclidean d) (t : ℝ) : ℝ :=
  fderivWithin ℝ U (halfSpace d) (x, t) (EuclideanSpace.single i (1 : ℝ), (0 : ℝ))

/-- `u` is a (classical) solution of the pure initial value problem (11.8):
`u_tt - Δu = 0` in `R^d × R_+`, `u(·,0) = v`, `u_t(·,0) = w` in `R^d`. -/
def IsWaveSolution {d : ℕ} (U : Euclidean d × ℝ → ℝ) (v w : Euclidean d → ℝ) : Prop :=
  ContDiffOn ℝ 2 U (halfSpace d) ∧
  (∀ (x : Euclidean d) (t : ℝ), 0 < t →
    iteratedFDeriv ℝ 2 U (x, t)
        ![((0 : Euclidean d), (1 : ℝ)), ((0 : Euclidean d), (1 : ℝ))]
      - ∑ i : Fin d, iteratedFDeriv ℝ 2 U (x, t)
        ![(EuclideanSpace.single i (1 : ℝ), (0 : ℝ)), (EuclideanSpace.single i (1 : ℝ), (0 : ℝ))]
      = 0) ∧
  (∀ x : Euclidean d, U (x, 0) = v x) ∧
  (∀ x : Euclidean d, timeDeriv U x 0 = w x)

/-- The circular cone (11.9): `K = {(x,t) ∈ R^d × R_+ : |x - x̄| ≤ t̄ - t, t ≤ t̄}`. -/
def coneK {d : ℕ} (xbar : Euclidean d) (tbar : ℝ) : Set (Euclidean d × ℝ) :=
  {p | 0 ≤ p.2 ∧ ‖p.1 - xbar‖ ≤ tbar - p.2 ∧ p.2 ≤ tbar}

/-- `B_t = {x ∈ R^d : (x,t) ∈ K}`. -/
def ballSection {d : ℕ} (K : Set (Euclidean d × ℝ)) (t : ℝ) : Set (Euclidean d) :=
  {x | (x, t) ∈ K}

/-- `𝓔_K(t) = ½ ∫_{B_t} (u_t(x,t)² + |∇u(x,t)|²) dx`. -/
def energyK {d : ℕ} (U : Euclidean d × ℝ → ℝ) (xbar : Euclidean d) (tbar t : ℝ) : ℝ :=
  (1 / 2 : ℝ) * ∫ x in ballSection (coneK xbar tbar) t,
    (timeDeriv U x t ^ 2 + ∑ i : Fin d, spaceDeriv U i x t ^ 2)

/-- Theorem 11.3 (Larsson–Thomée): for a solution `u` of the wave equation (11.8) and a point
`(x̄, t̄) ∈ R^d × R_+`, the local energy over the sections of the backward cone `K` is
nonincreasing: `𝓔_K(t) ≤ 𝓔_K(0)` for `0 ≤ t ≤ t̄`. -/
theorem thm_11_3 {d : ℕ} (U : Euclidean d × ℝ → ℝ) (v w : Euclidean d → ℝ)
    (hU : IsWaveSolution U v w) (xbar : Euclidean d) (tbar : ℝ) (htbar : 0 < tbar) :
    ∀ t : ℝ, 0 ≤ t → t ≤ tbar → energyK U xbar tbar t ≤ energyK U xbar tbar 0 := by
  sorry

end PDETextbook.LarssonThomee.Thm11_3