noncomputable def HeatEquation.totalThermalEnergy (n : ℕ) (u : ℝ → (Fin n → ℝ) → ℝ) (t : ℝ) : ℝ

The total thermal energy at time $t$ associated to $u(t, x)$, defined by $\mathcal{T}(t) \stackrel{\text{def}}{=} \int_{\mathbb{R}^n} u(t, x) \, d^n x$. (Definition 2.0.2.)

theorem HeatEquation.divergence_theorem_ball_bound {n : ℕ} (laplacian_u grad_u_norm : ℝ → (Fin n → ℝ) → ℝ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (t R : ℝ), 0 < R → |∫ (x : Fin n → ℝ) in Metric.ball 0 R, laplacian_u t x| ≤ C * sSup ((fun (x : Fin n → ℝ) => R ^ (↑n - 1) * |grad_u_norm t x|) '' Metric.sphere 0 R)

Quantitative form of the divergence theorem: the integral of the Laplacian of $u$ over a ball of radius $R$ is controlled by an $R^{n-1}$-weighted supremum of the gradient on the sphere of radius $R$. Used as an abstract hypothesis to derive conservation of thermal energy.

theorem HeatEquation.integral_laplacian_eq_zero {n : ℕ} (laplacian_u grad_u_norm : ℝ → (Fin n → ℝ) → ℝ) (hdecay : ∀ (t : ℝ), Filter.Tendsto (fun (R : ℝ) => sSup ((fun (x : Fin n → ℝ) => R ^ (↑n - 1) * |grad_u_norm t x|) '' Metric.sphere 0 R)) Filter.atTop (nhds 0)) (hlapl_int : ∀ (t : ℝ), MeasureTheory.Integrable (laplacian_u t) MeasureTheory.volume) (hdiv_bound : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (t R : ℝ), 0 < R → |∫ (x : Fin n → ℝ) in Metric.ball 0 R, laplacian_u t x| ≤ C * sSup ((fun (x : Fin n → ℝ) => R ^ (↑n - 1) * |grad_u_norm t x|) '' Metric.sphere 0 R)) (t : ℝ) : ∫ (x : Fin n → ℝ), laplacian_u t x = 0

Under the decay assumption $\lim_{|x| \to \infty} |x|^{n-1} |\nabla_x u(t, x)| = 0$ together with integrability of the Laplacian and the divergence-theorem bound, the global integral of the Laplacian over $\mathbb{R}^n$ vanishes: $\int_{\mathbb{R}^n} \Delta u(t, x) \, d^n x = 0$.

theorem HeatEquation.deriv_totalThermalEnergy_eq_zero {n : ℕ} (u u_t laplacian_u grad_u_norm : ℝ → (Fin n → ℝ) → ℝ) (hpde : ∀ (t : ℝ) (x : Fin n → ℝ), u_t t x = laplacian_u t x) (hderiv : ∀ (x : Fin n → ℝ) (t : ℝ), HasDerivAt (fun (s : ℝ) => u s x) (u_t t x) t) (hdecay : ∀ (t : ℝ), Filter.Tendsto (fun (R : ℝ) => sSup ((fun (x : Fin n → ℝ) => R ^ (↑n - 1) * |grad_u_norm t x|) '' Metric.sphere 0 R)) Filter.atTop (nhds 0)) (f : (Fin n → ℝ) → ℝ) (_hf_nn : ∀ (x : Fin n → ℝ), 0 ≤ f x) (hf_int : MeasureTheory.Integrable f MeasureTheory.volume) (hdom : ∀ (t : ℝ) (x : Fin n → ℝ), |u_t t x| ≤ f x) (hu_meas : ∀ (t : ℝ), MeasureTheory.AEStronglyMeasurable (u t) MeasureTheory.volume) (hu_int : ∀ (t : ℝ), MeasureTheory.Integrable (u t) MeasureTheory.volume) (hut_meas : ∀ (t : ℝ), MeasureTheory.AEStronglyMeasurable (u_t t) MeasureTheory.volume) (t : ℝ) : HasDerivAt (totalThermalEnergy n u) 0 t

For a solution $u$ to the heat equation $\partial_t u = \Delta u$ on $\mathbb{R}^n$ with suitable decay and integrability hypotheses, the derivative of the total thermal energy with respect to time vanishes: $\mathcal{T}'(t) = 0$. This is the differential form of conservation of thermal energy (Lemma 2.0.3).

theorem HeatEquation.totalThermalEnergy_constant {n : ℕ} (u u_t laplacian_u grad_u_norm : ℝ → (Fin n → ℝ) → ℝ) (hpde : ∀ (t : ℝ) (x : Fin n → ℝ), u_t t x = laplacian_u t x) (hderiv : ∀ (x : Fin n → ℝ) (t : ℝ), HasDerivAt (fun (s : ℝ) => u s x) (u_t t x) t) (hdecay : ∀ (t : ℝ), Filter.Tendsto (fun (R : ℝ) => sSup ((fun (x : Fin n → ℝ) => R ^ (↑n - 1) * |grad_u_norm t x|) '' Metric.sphere 0 R)) Filter.atTop (nhds 0)) (f : (Fin n → ℝ) → ℝ) (hf_nn : ∀ (x : Fin n → ℝ), 0 ≤ f x) (hf_int : MeasureTheory.Integrable f MeasureTheory.volume) (hdom : ∀ (t : ℝ) (x : Fin n → ℝ), |u_t t x| ≤ f x) (hu_meas : ∀ (t : ℝ), MeasureTheory.AEStronglyMeasurable (u t) MeasureTheory.volume) (hu_int : ∀ (t : ℝ), MeasureTheory.Integrable (u t) MeasureTheory.volume) (hut_meas : ∀ (t : ℝ), MeasureTheory.AEStronglyMeasurable (u_t t) MeasureTheory.volume) (t : ℝ) : totalThermalEnergy n u t = totalThermalEnergy n u 0

Conservation of thermal energy (Lemma 2.0.3): for a solution $u$ to the heat equation $-\partial_t u + \Delta u = 0$ on $[0, \infty) \times \mathbb{R}^n$ satisfying the decay and integrability hypotheses, the total thermal energy is constant in time: $\mathcal{T}(t) = \mathcal{T}(0)$.