FARMSAcceptedTheorem · Statement with omitted proof
Energy conservation for the Dirichlet wave equation
The total kinetic and gradient energy of a smooth unforced Dirichlet wave solution is constant.
Larsson & Thomée ↗
Theorem 11.2 · printed p. 167
Formal statement. The assumptions and conclusion are explicit; the theorem proof is omitted (sorry).
01 / MATHEMATICAL STATEMENT
Meaning & conditions
Mathematical summary
The total kinetic and gradient energy of a smooth unforced Dirichlet wave solution is constant.
Assumptions & context
- A bounded spatial domain, a twice continuously differentiable space–time solution, homogeneous Dirichlet boundary conditions, and the stated initial displacement and velocity.
Source
Larsson & Thomée. Partial differential equations with numerical methods.
Theorem 11.2 · printed p. 167
02 / LEAN REPRESENTATION
Formal statement
Statement with omitted proof. Expand the complete file below to read imports, local definitions and surrounding context.
theorem energy_conservation {d : ℕ} (Ω : Set (Euclidean d)) (hΩ : IsBoundedDomain Ω)
(v w : Euclidean d → ℝ) (u : Euclidean d → ℝ → ℝ)
(hsmooth : ContDiff ℝ 2 (fun p : Euclidean d × ℝ => u p.1 p.2))
(hsol : IsWaveIBVPSolution Ω v w u) :
∀ t : ℝ, 0 ≤ t → totalEnergy Ω u t = totalEnergy Ω u 0 := by
sorry
Complete Lean file and local definitions
import PDETextbook.Base
open MeasureTheory
open scoped BigOperators ENNReal
noncomputable section
namespace PDETextbook.LarssonThomee.Thm11_2
/-- First time derivative `u_t(x,t)` of a space-time function `u(x,t)`. -/
def timeDeriv {d : ℕ} (u : Euclidean d → ℝ → ℝ) (x : Euclidean d) (t : ℝ) : ℝ :=
deriv (fun s => u x s) t
/-- Second time derivative `u_tt(x,t)`. -/
def timeDeriv2 {d : ℕ} (u : Euclidean d → ℝ → ℝ) (x : Euclidean d) (t : ℝ) : ℝ :=
deriv (fun s => timeDeriv u x s) t
/-- Spatial Laplacian `Δu(x,t) = ∑ᵢ ∂²u/∂xᵢ²` (positive-sign convention, as in `u_tt - Δu = 0`). -/
def spatialLaplacian {d : ℕ} (u : Euclidean d → ℝ → ℝ) (x : Euclidean d) (t : ℝ) : ℝ :=
∑ i : Fin d, partialDeriv (fun y => partialDeriv (fun z => u z t) i y) i x
/-- `|∇u(x,t)|²`, the squared Euclidean norm of the spatial gradient. -/
def gradSq {d : ℕ} (u : Euclidean d → ℝ → ℝ) (x : Euclidean d) (t : ℝ) : ℝ :=
∑ i : Fin d, (partialDeriv (fun y => u y t) i x) ^ 2
/-- `Ω` is a bounded domain in `ℝ^d` (open, connected, bounded). -/
def IsBoundedDomain {d : ℕ} (Ω : Set (Euclidean d)) : Prop :=
IsOpen Ω ∧ IsConnected Ω ∧ Bornology.IsBounded Ω
/-- `u` solves the initial-boundary value problem (11.5) for the wave equation:
`u_tt - Δu = 0` in `Ω × ℝ₊`, `u = 0` on `Γ × ℝ₊` (`Γ = ∂Ω`),
`u(·,0) = v`, `u_t(·,0) = w` in `Ω`. -/
def IsWaveIBVPSolution {d : ℕ} (Ω : Set (Euclidean d)) (v w : Euclidean d → ℝ)
(u : Euclidean d → ℝ → ℝ) : Prop :=
(∀ x ∈ Ω, ∀ t : ℝ, 0 < t → timeDeriv2 u x t - spatialLaplacian u x t = 0) ∧
(∀ x ∈ frontier Ω, ∀ t : ℝ, 0 < t → u x t = 0) ∧
(∀ x ∈ Ω, u x 0 = v x) ∧
(∀ x ∈ Ω, timeDeriv u x 0 = w x)
/-- Total energy `𝓔(t) = ½ ∫_Ω (u_t² + |∇u|²) dx`, eq. (11.7). -/
def totalEnergy {d : ℕ} (Ω : Set (Euclidean d)) (u : Euclidean d → ℝ → ℝ) (t : ℝ) : ℝ :=
(1 / 2 : ℝ) * ∫ x in Ω, ((timeDeriv u x t) ^ 2 + gradSq u x t)
/-- Theorem 11.2 (Larsson–Thomée). If `u` is a sufficiently smooth solution of (11.5)
(realized as: the space-time function `(x,t) ↦ u(x,t)` is `C²`), then the total energy
is conserved: `𝓔(t) = 𝓔(0)` for all `t ≥ 0`. -/
theorem energy_conservation {d : ℕ} (Ω : Set (Euclidean d)) (hΩ : IsBoundedDomain Ω)
(v w : Euclidean d → ℝ) (u : Euclidean d → ℝ → ℝ)
(hsmooth : ContDiff ℝ 2 (fun p : Euclidean d × ℝ => u p.1 p.2))
(hsol : IsWaveIBVPSolution Ω v w u) :
∀ t : ℝ, 0 ≤ t → totalEnergy Ω u t = totalEnergy Ω u 0 := by
sorry
end PDETextbook.LarssonThomee.Thm11_2
How to read the formalization
- The statement concerns the continuous PDE. The linked application uses an explicit implication from these premises to a computational energy certificate.
Computational use
In the wave-response application, energy conservation is an explicit source premise. Together with a matrix residual bound, it controls response error for a prescribed excitation family.
Explore the application →