theorem CM6.heat_translation_invariance {n : ℕ} (D A t₀ : ℝ) (x₀ : Fin n → ℝ) (u_t Δu : ℝ → (Fin n → ℝ) → ℝ) (hpde : ∀ (t : ℝ) (x : Fin n → ℝ), u_t t x - D * Δu t x = 0) (t : ℝ) (x : Fin n → ℝ) : A * u_t (t - t₀) (x - x₀) - D * (A * Δu (t - t₀) (x - x₀)) = 0

Translation invariance of the heat equation expressed at the level of the pointwise PDE relation: if $u_t - D \Delta u = 0$ everywhere, then for any constants $A, t_0 \in \mathbb{R}$ and $x_0 \in \mathbb{R}^n$, the analogous identity holds with $u_t, \Delta u$ evaluated at $(t - t_0, x - x_0)$ and multiplied by $A$.

noncomputable def CM6.totalThermalEnergy {n : ℕ} (u : ℝ → (Fin n → ℝ) → ℝ) (t : ℝ) : ℝ

The total thermal energy of $u$ at time $t$ (Definition 2.0.2): $\mathcal{T}(t) = \int_{\mathbb{R}^n} u(t, x)\, d^n x$.