theorem CM9.Wave.hasDerivAt_comp_add_right {f : ℝ → ℝ} {x t : ℝ} (hF : DifferentiableAt ℝ f (x + t)) : HasDerivAt (fun (s : ℝ) => f (x + s)) (deriv f (x + t)) t

Chain rule helper: if $f$ is differentiable at $x + t$, then the map $s \mapsto f(x + s)$ has derivative $f'(x + t)$ at $t$.

theorem CM9.Wave.hasDerivAt_comp_sub_right {f : ℝ → ℝ} {x t : ℝ} (hF : DifferentiableAt ℝ f (x - t)) : HasDerivAt (fun (s : ℝ) => f (x - s)) (-deriv f (x - t)) t

Chain rule helper: if $f$ is differentiable at $x - t$, then the map $s \mapsto f(x - s)$ has derivative $-f'(x - t)$ at $t$.

theorem CM9.Wave.hasDerivAt_comp_add_left {f : ℝ → ℝ} {x t : ℝ} (hF : DifferentiableAt ℝ f (t + x)) : HasDerivAt (fun (s : ℝ) => f (s + x)) (deriv f (t + x)) t

Chain rule helper: if $f$ is differentiable at $t + x$, then $s \mapsto f(s + x)$ has derivative $f'(t + x)$ at $t$.

theorem CM9.Wave.hasDerivAt_comp_sub_left {f : ℝ → ℝ} {x t : ℝ} (hF : DifferentiableAt ℝ f (t - x)) : HasDerivAt (fun (s : ℝ) => f (s - x)) (deriv f (t - x)) t

Chain rule helper: if $f$ is differentiable at $t - x$, then $s \mapsto f(s - x)$ has derivative $f'(t - x)$ at $t$.

theorem CM9.Wave.differentiable_of_contDiff2 {f : ℝ → ℝ} (hf : ContDiff ℝ 2 f) : Differentiable ℝ f

A $C^2$ function is differentiable.

theorem CM9.Wave.differentiable_deriv_of_contDiff2 {f : ℝ → ℝ} (hf : ContDiff ℝ 2 f) : Differentiable ℝ (deriv f)

For a $C^2$ function $f$ on $\mathbb{R}$, the derivative $f'$ is also differentiable.

theorem CM9.Wave.contDiff_antideriv (g : ℝ → ℝ) (hg : ContDiff ℝ 1 g) : ContDiff ℝ 2 fun (z : ℝ) => ∫ (y : ℝ) in 0..z, g y

The antiderivative $z \mapsto \int_0^z g(y) \, dy$ of a $C^1$ function $g$ is $C^2$ (one extra degree of smoothness from integration).

theorem CM9.Wave.general_solution_satisfies_wave_eq (F G : ℝ → ℝ) (hF : ContDiff ℝ 2 F) (hG : ContDiff ℝ 2 G) (t x : ℝ) : deriv (fun (t' : ℝ) => deriv (fun (t'' : ℝ) => F (x + t'') + G (x - t'')) t') t = deriv (fun (x' : ℝ) => deriv (fun (x'' : ℝ) => F (x'' + t) + G (x'' - t)) x') x

Any function of the form $u(t, x) = F(x + t) + G(x - t)$ with $F, G \in C^2$ solves the $1{+}1$ dimensional wave equation $u_{tt} = u_{xx}$. (Null decomposition / d'Alembert form.)

noncomputable def CM9.Wave.dAlembertFormula (f g : ℝ → ℝ) (t x : ℝ) : ℝ

d'Alembert's formula for the $1{+}1$ wave equation with initial data $u(0, x) = f(x)$, $u_t(0, x) = g(x)$: $$u(t, x) = \tfrac{1}{2} (f(x + t) + f(x - t)) + \tfrac{1}{2} \int_{x - t}^{x + t} g(z) \, dz.$$

theorem CM9.Wave.dAlembert_regularity (f g : ℝ → ℝ) (hf : ContDiff ℝ 2 f) (hg : ContDiff ℝ 1 g) : ContDiff ℝ 2 fun (p : ℝ × ℝ) => dAlembertFormula f g p.1 p.2

Regularity for d'Alembert. If $f \in C^2(\mathbb{R})$ and $g \in C^1(\mathbb{R})$, then the function $(t, x) \mapsto u(t, x)$ defined by d'Alembert's formula is jointly $C^2$ on $\mathbb{R}^2$.

theorem CM9.Wave.wave_uniqueness (u₁ u₂ : ℝ → ℝ → ℝ) (h₁_reg : ContDiff ℝ 2 fun (p : ℝ × ℝ) => u₁ p.1 p.2) (h₁_wave : ∀ (t x : ℝ), deriv (fun (t' : ℝ) => deriv (fun (t'' : ℝ) => u₁ t'' x) t') t = deriv (fun (x' : ℝ) => deriv (fun (x'' : ℝ) => u₁ t x'') x') x) (h₂_reg : ContDiff ℝ 2 fun (p : ℝ × ℝ) => u₂ p.1 p.2) (h₂_wave : ∀ (t x : ℝ), deriv (fun (t' : ℝ) => deriv (fun (t'' : ℝ) => u₂ t'' x) t') t = deriv (fun (x' : ℝ) => deriv (fun (x'' : ℝ) => u₂ t x'') x') x) (h_pos : ∀ (x : ℝ), u₁ 0 x = u₂ 0 x) (h_vel : ∀ (x : ℝ), deriv (fun (t : ℝ) => u₁ t x) 0 = deriv (fun (t : ℝ) => u₂ t x) 0) (t x : ℝ) : u₁ t x = u₂ t x

Uniqueness for the $1{+}1$ wave equation. Two $C^2$ solutions of $u_{tt} = u_{xx}$ with the same initial position $u(0, \cdot)$ and initial velocity $u_t(0, \cdot)$ are identical on $\mathbb{R}^2$.

theorem CM9.Wave.wave_null_decomposition (u : ℝ → ℝ → ℝ) (hu_reg : ContDiff ℝ 2 fun (p : ℝ × ℝ) => u p.1 p.2) (hu_wave : ∀ (t x : ℝ), deriv (fun (t' : ℝ) => deriv (fun (t'' : ℝ) => u t'' x) t') t = deriv (fun (x' : ℝ) => deriv (fun (x'' : ℝ) => u t x'') x') x) : ∃ (F : ℝ → ℝ) (G : ℝ → ℝ), ContDiff ℝ 2 F ∧ ContDiff ℝ 2 G ∧ ∀ (t x : ℝ), u t x = F (x + t) + G (x - t)

Null decomposition of any $C^2$ solution of the wave equation: there exist $C^2$ functions $F, G : \mathbb{R} \to \mathbb{R}$ such that $u(t, x) = F(x + t) + G(x - t)$.

theorem CM9.Wave.hasDerivAt_F_of_null_decomp (f g F G : ℝ → ℝ) (hf : ContDiff ℝ 2 f) (_hg : ContDiff ℝ 1 g) (hFd : Differentiable ℝ F) (hFG_init_pos : ∀ (x : ℝ), F x + G x = f x) (hFG_init_vel : ∀ (x : ℝ), HasDerivAt (fun (t : ℝ) => F (x + t) + G (x - t)) (g x) 0) (x : ℝ) : HasDerivAt F ((deriv f x + g x) / 2) x

Given a null decomposition $u(t, x) = F(x + t) + G(x - t)$ matching initial data $u(0, \cdot) = f$ and $u_t(0, \cdot) = g$, one obtains the explicit formula $F'(x) = \tfrac{1}{2}(f'(x) + g(x))$.

theorem CM9.Wave.null_decomposition_determines_dAlembert (f g F G : ℝ → ℝ) (hf : ContDiff ℝ 2 f) (hg : ContDiff ℝ 1 g) (hFd : Differentiable ℝ F) (hFG_init_pos : ∀ (x : ℝ), F x + G x = f x) (hFG_init_vel : ∀ (x : ℝ), HasDerivAt (fun (t : ℝ) => F (x + t) + G (x - t)) (g x) 0) (t x : ℝ) : F (x + t) + G (x - t) = dAlembertFormula f g t x

Any null decomposition $F(x + t) + G(x - t)$ matching the initial data $(f, g)$ coincides pointwise with d'Alembert's formula. Combined with the existence of such a decomposition (wave_null_decomposition), this gives the explicit formula for any wave-equation solution.

theorem CM9.Wave.dAlembert_uniqueness (f g : ℝ → ℝ) (u : ℝ → ℝ → ℝ) (hf : ContDiff ℝ 2 f) (hg : ContDiff ℝ 1 g) (hu_reg : ContDiff ℝ 2 fun (p : ℝ × ℝ) => u p.1 p.2) (hu_wave : ∀ (t x : ℝ), deriv (fun (t' : ℝ) => deriv (fun (t'' : ℝ) => u t'' x) t') t = deriv (fun (x' : ℝ) => deriv (fun (x'' : ℝ) => u t x'') x') x) (hu_init_pos : ∀ (x : ℝ), u 0 x = f x) (hu_init_vel : ∀ (x : ℝ), HasDerivAt (fun (t : ℝ) => u t x) (g x) 0) (t x : ℝ) : u t x = dAlembertFormula f g t x

Theorem 4.1 (d'Alembert's formula). Let $f \in C^2(\mathbb{R})$ and $g \in C^1(\mathbb{R})$. Any $C^2$ solution $u(t, x)$ of the $1{+}1$ dimensional wave equation $u_{tt} = u_{xx}$ with initial data $u(0, x) = f(x)$ and $u_t(0, x) = g(x)$ is given by d'Alembert's formula: $$u(t, x) = \tfrac{1}{2}(f(x + t) + f(x - t)) + \tfrac{1}{2} \int_{x - t}^{x + t} g(z) \, dz.$$