WaveEquation1D
def
A scalar field u : ℝ × ℝ → ℝ satisfies the one-dimensional wave equation with wave speed c if for all (x, t), the second partial derivative of u with respect to time equals c^2 times the second partial derivative of u with respect to space.
Statement
def WaveEquation1D (c : ℝ) (u : ℝ × ℝ → ℝ) : Prop
- Source
- Jackson, Classical Electrodynamics, ch. 6
- Verified
- 11 Sep 2026
- Axioms
- none listed
- Used by 1
- klein_gordon_zero_mass_iff_wave_equationA scalar field φ : ℝ × ℝ → ℝ satisfies the one-dimensional Klein-Gordon equation with mass parameter 0 and speed c if and only if it…
Read back from the Lean
Given a real number $c$ and a function $u : \mathbb{R} \times \mathbb{R} \to \mathbb{R}$, WaveEquation1D c u asserts that for all $x, t \in \mathbb{R}$, the second derivative of $s \mapsto u(x, s)$ evaluated at $t$ equals $c^2$ times the second derivative of $y \mapsto u(y, t)$ evaluated at $x$.
Written by a model that saw only the Lean, never the English above. If the two disagree, that is worth a challenge.
Lean source view module on GitHub
/-- A scalar field u satisfies the 1D wave equation with speed c if d^2/dt^2 u = c^2 d^2/dx^2 u. -/ def WaveEquation1D (c : ℝ) (u : ℝ × ℝ → ℝ) : Prop := ∀ x t : ℝ, deriv (deriv (fun s => u (x, s))) t = c^2 * deriv (deriv (fun y => u (y, t))) x