noncomputable def WaveEquation1D.dAlembertSolution (f g : ℝ → ℝ) (t x : ℝ) : ℝ

D'Alembert's formula for the $1+1$ dimensional wave equation: $u(t,x) = \frac{1}{2}(f(x+t) + f(x-t)) + \frac{1}{2}\int_{x-t}^{x+t} g(z)\,dz$.

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

If $g_0 \in C^1(\mathbb{R})$, then its antiderivative $z \mapsto \int_0^z g_0(y)\,dy$ is in $C^2(\mathbb{R})$.

theorem WaveEquation1D.hasDerivAt_comp_add_right' {h : ℝ → ℝ} {a b : ℝ} (hd : DifferentiableAt ℝ h (a + b)) : HasDerivAt (fun (s : ℝ) => h (a + s)) (deriv h (a + b)) b

Chain rule helper: if $h$ is differentiable at $a + b$, then the map $s \mapsto h(a + s)$ has derivative $h'(a + b)$ at $b$.

theorem WaveEquation1D.hasDerivAt_comp_sub_right' {h : ℝ → ℝ} {a b : ℝ} (hd : DifferentiableAt ℝ h (a - b)) : HasDerivAt (fun (s : ℝ) => h (a - s)) (-deriv h (a - b)) b

Chain rule helper: if $h$ is differentiable at $a - b$, then the map $s \mapsto h(a - s)$ has derivative $-h'(a - b)$ at $b$.

theorem WaveEquation1D.hasDerivAt_comp_add_left' {h : ℝ → ℝ} {a b : ℝ} (hd : DifferentiableAt ℝ h (b + a)) : HasDerivAt (fun (s : ℝ) => h (s + a)) (deriv h (b + a)) b

Chain rule helper: if $h$ is differentiable at $b + a$, then $s \mapsto h(s + a)$ has derivative $h'(b + a)$ at $b$.

theorem WaveEquation1D.hasDerivAt_comp_sub_left' {h : ℝ → ℝ} {a b : ℝ} (hd : DifferentiableAt ℝ h (b - a)) : HasDerivAt (fun (s : ℝ) => h (s - a)) (deriv h (b - a)) b

Chain rule helper: if $h$ is differentiable at $b - a$, then $s \mapsto h(s - a)$ has derivative $h'(b - a)$ at $b$.

theorem WaveEquation1D.dAlembert_regularity_proof (f g : ℝ → ℝ) (hf : ContDiff ℝ 2 f) (hg : ContDiff ℝ 1 g) : ContDiff ℝ 2 fun (p : ℝ × ℝ) => dAlembertSolution f g p.1 p.2

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

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

D'Alembert's solution is jointly $C^2$ in $(t, x)$ when $f \in C^2(\mathbb{R})$ and $g \in C^1(\mathbb{R})$.

theorem WaveEquation1D.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(\mathbb{R})$ satisfies the wave equation $\partial_t^2 u = \partial_x^2 u$.

theorem WaveEquation1D.zero_wave_is_zero (w : ℝ → ℝ → ℝ) (h_reg : ContDiff ℝ 2 fun (p : ℝ × ℝ) => w p.1 p.2) (h_wave : ∀ (t x : ℝ), deriv (fun (t' : ℝ) => deriv (fun (t'' : ℝ) => w t'' x) t') t = deriv (fun (x' : ℝ) => deriv (fun (x'' : ℝ) => w t x'') x') x) (h_pos : ∀ (x : ℝ), w 0 x = 0) (h_vel : ∀ (x : ℝ), deriv (fun (t : ℝ) => w t x) 0 = 0) (t x : ℝ) : w t x = 0

Uniqueness for the wave equation with zero initial data: if $w \in C^2(\mathbb{R}^2)$ satisfies $\partial_t^2 w = \partial_x^2 w$, $w(0, x) = 0$, and $\partial_t w(0, x) = 0$ for all $x$, then $w \equiv 0$.

theorem WaveEquation1D.wave_eq_of_sub (u₁ u₂ : ℝ → ℝ → ℝ) (h₁_reg : ContDiff ℝ 2 fun (p : ℝ × ℝ) => u₁ p.1 p.2) (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₂_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) (t x : ℝ) : deriv (fun (t' : ℝ) => deriv (fun (t'' : ℝ) => u₁ t'' x - u₂ t'' x) t') t = deriv (fun (x' : ℝ) => deriv (fun (x'' : ℝ) => u₁ t x'' - u₂ t x'') x') x

The difference of two solutions to the wave equation is itself a solution: if $u_1, u_2$ both satisfy $\partial_t^2 u = \partial_x^2 u$, then so does $u_1 - u_2$.

theorem WaveEquation1D.deriv_sub_zero (u₁ u₂ : ℝ → ℝ → ℝ) (h₁_reg : ContDiff ℝ 2 fun (p : ℝ × ℝ) => u₁ p.1 p.2) (h₂_reg : ContDiff ℝ 2 fun (p : ℝ × ℝ) => u₂ p.1 p.2) (h_vel : ∀ (x : ℝ), deriv (fun (t : ℝ) => u₁ t x) 0 = deriv (fun (t : ℝ) => u₂ t x) 0) (x : ℝ) : deriv (fun (t : ℝ) => u₁ t x - u₂ t x) 0 = 0

If two $C^2$ functions $u_1, u_2$ have equal initial $t$-derivatives at $t = 0$, then the $t$-derivative of their difference vanishes at $t = 0$.

theorem WaveEquation1D.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 wave equation: two $C^2$ solutions of the 1D wave equation that share the same initial position $u(0, x)$ and the same initial velocity $\partial_t u(0, x)$ must agree everywhere.

theorem WaveEquation1D.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 : ℝ → ℝ), (∀ (t x : ℝ), u t x = F (x + t) + G (x - t)) ∧ Differentiable ℝ F ∧ Differentiable ℝ G

Null decomposition for the wave equation: every $C^2$ solution $u$ of the 1D wave equation can be written as $u(t, x) = F(x + t) + G(x - t)$ for some differentiable $F, G : \mathbb{R} \to \mathbb{R}$ (travelling waves).

theorem WaveEquation1D.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

In a null decomposition $u(t, x) = F(x + t) + G(x - t)$ matching initial data $f$ and $g$, the right-moving wave $F$ satisfies $F'(x) = (f'(x) + g(x))/2$.

theorem WaveEquation1D.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) = dAlembertSolution f g t x

Any null decomposition $F(x + t) + G(x - t)$ that matches the initial position $f$ and initial velocity $g$ must coincide with d'Alembert's solution.

theorem WaveEquation1D.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 = dAlembertSolution f g t x

Theorem 4.1 (d'Alembert's formula, uniqueness part). The unique $C^2$ solution $u$ of the 1D wave equation $-\partial_t^2 u + \partial_x^2 u = 0$ with initial data $u(0, x) = f(x)$ and $\partial_t u(0, x) = g(x)$ is given by d'Alembert's formula.

noncomputable def WaveEquation1D.oddExtension (f : ℝ → ℝ) : ℝ → ℝ

The odd extension of a function $f : [0, \infty) \to \mathbb{R}$ to all of $\mathbb{R}$: $\tilde{f}(y) = f(y)$ for $y \ge 0$, and $\tilde{f}(y) = -f(-y)$ for $y < 0$.

theorem WaveEquation1D.oddExtension_neg (f : ℝ → ℝ) (hf0 : f 0 = 0) (y : ℝ) : oddExtension f (-y) = -oddExtension f y

If $f(0) = 0$, then the odd extension of $f$ is an odd function: $\tilde{f}(-y) = -\tilde{f}(y)$.

noncomputable def WaveEquation1D.dAlembertHalfLine (f g : ℝ → ℝ) (t x : ℝ) : ℝ

The d'Alembert formula for the half-line wave equation with Dirichlet boundary condition $u(t, 0) = 0$, obtained by applying d'Alembert's formula to the odd extensions of $f$ and $g$.

theorem WaveEquation1D.integral_odd_symmetric {h : ℝ → ℝ} (hodd : ∀ (y : ℝ), h (-y) = -h y) (hcont : Continuous h) (t : ℝ) : ∫ (y : ℝ) in -t..t, h y = 0

The integral of a continuous odd function over a symmetric interval vanishes: $\int_{-t}^{t} h(y)\,dy = 0$ when $h(-y) = -h(y)$.

theorem WaveEquation1D.oddExtension_continuous (g : ℝ → ℝ) (hg_cont : Continuous g) (hg0 : g 0 = 0) : Continuous (oddExtension g)

If $g : \mathbb{R} \to \mathbb{R}$ is continuous with $g(0) = 0$, then its odd extension is continuous.

theorem WaveEquation1D.oddExtension_continuous_of_continuousOn (g : ℝ → ℝ) (hg_cont : ContinuousOn g (Set.Ici 0)) (hg0 : g 0 = 0) : Continuous (oddExtension g)

If $g$ is continuous on $[0, \infty)$ with $g(0) = 0$, then its odd extension is continuous on all of $\mathbb{R}$.

theorem WaveEquation1D.oddExtension_hasDerivAt_of_contDiffOn (g : ℝ → ℝ) (hg : ContDiffOn ℝ 1 g (Set.Ici 0)) (hg0 : g 0 = 0) (x : ℝ) : HasDerivAt (oddExtension g) (derivWithin g (Set.Ici 0) |x|) x

Derivative of the odd extension (from $C^1$ on $[0, \infty)$): for $g \in C^1([0, \infty))$ with $g(0) = 0$, the odd extension is differentiable everywhere, with derivative $g'(\lvert x \rvert)$ at $x$.

theorem WaveEquation1D.oddExtension_contDiff_one_of_contDiffOn (g : ℝ → ℝ) (hg : ContDiffOn ℝ 1 g (Set.Ici 0)) (hg0 : g 0 = 0) : ContDiff ℝ 1 (oddExtension g)

If $g \in C^1([0, \infty))$ with $g(0) = 0$, then the odd extension of $g$ is in $C^1(\mathbb{R})$.

theorem WaveEquation1D.evenExtension_hasDerivAt_of_contDiffOn (h : ℝ → ℝ) (hh : ContDiffOn ℝ 1 h (Set.Ici 0)) (hh'0 : derivWithin h (Set.Ici 0) 0 = 0) (x : ℝ) : HasDerivAt (fun (y : ℝ) => h |y|) (oddExtension (derivWithin h (Set.Ici 0)) x) x

Derivative of an even extension: for $h \in C^1([0, \infty))$ with $h'(0) = 0$, the function $y \mapsto h(\lvert y \rvert)$ is differentiable everywhere with derivative given by the odd extension of $h'$.

theorem WaveEquation1D.oddExtension_contDiff_two_of_contDiffOn (f : ℝ → ℝ) (hf : ContDiffOn ℝ 2 f (Set.Ici 0)) (hf0 : f 0 = 0) (hf''0 : iteratedDerivWithin 2 f (Set.Ici 0) 0 = 0) : ContDiff ℝ 2 (oddExtension f)

If $f \in C^2([0, \infty))$ with $f(0) = 0$ and $f''(0) = 0$, then the odd extension of $f$ is in $C^2(\mathbb{R})$. The compatibility condition $f''(0) = 0$ is necessary for smoothness across the origin.

theorem WaveEquation1D.oddExtension_hasDerivAt (g : ℝ → ℝ) (hg : ContDiff ℝ 1 g) (hg0 : g 0 = 0) (x : ℝ) : HasDerivAt (oddExtension g) (deriv g |x|) x

Derivative of the odd extension (from $C^1$ on all of $\mathbb{R}$): if $g \in C^1(\mathbb{R})$ and $g(0) = 0$, then the odd extension is differentiable everywhere with derivative $g'(\lvert x \rvert)$ at $x$.

theorem WaveEquation1D.oddExtension_contDiff_one (g : ℝ → ℝ) (hg : ContDiff ℝ 1 g) (hg0 : g 0 = 0) : ContDiff ℝ 1 (oddExtension g)

If $g \in C^1(\mathbb{R})$ with $g(0) = 0$, then the odd extension of $g$ is in $C^1(\mathbb{R})$.

theorem WaveEquation1D.evenExtension_deriv_hasDerivAt (h : ℝ → ℝ) (hh : ContDiff ℝ 1 h) (hh'0 : deriv h 0 = 0) (x : ℝ) : HasDerivAt (fun (y : ℝ) => h |y|) (oddExtension (deriv h) x) x

Derivative of an even extension (from $C^1$ on all of $\mathbb{R}$): if $h \in C^1(\mathbb{R})$ and $h'(0) = 0$, then $y \mapsto h(\lvert y \rvert)$ is differentiable everywhere with derivative the odd extension of $h'$.

theorem WaveEquation1D.oddExtension_contDiff_two (f : ℝ → ℝ) (hf : ContDiff ℝ 2 f) (hf0 : f 0 = 0) (hf''0 : deriv (deriv f) 0 = 0) : ContDiff ℝ 2 (oddExtension f)

If $f \in C^2(\mathbb{R})$ with $f(0) = 0$ and $f''(0) = 0$, then the odd extension of $f$ is in $C^2(\mathbb{R})$.

theorem WaveEquation1D.dAlembert_halfline_formula_txle (f g : ℝ → ℝ) (_hf : ContDiffOn ℝ 2 f (Set.Ici 0)) (hg : ContDiffOn ℝ 1 g (Set.Ici 0)) (_hf0 : f 0 = 0) (hg0 : g 0 = 0) (t x : ℝ) (ht : 0 ≤ t) (hx : 0 ≤ x) (htx : t ≤ x) : dAlembertHalfLine f g t x = (f (x + t) + f (x - t)) / 2 + (∫ (z : ℝ) in x - t..x + t, g z) / 2

Half-line d'Alembert formula in the case $0 \le t \le x$ (Corollary 4.0.1, first branch): $u(t, x) = \frac{1}{2}(f(x + t) + f(x - t)) + \frac{1}{2}\int_{x-t}^{x+t} g(z)\,dz$.

theorem WaveEquation1D.dAlembert_halfline_formula_xtle (f g : ℝ → ℝ) (_hf : ContDiffOn ℝ 2 f (Set.Ici 0)) (hg : ContDiffOn ℝ 1 g (Set.Ici 0)) (hf0 : f 0 = 0) (hg0 : g 0 = 0) (t x : ℝ) (ht : 0 ≤ t) (hx : 0 ≤ x) (hxt : x ≤ t) : dAlembertHalfLine f g t x = (f (x + t) - f (t - x)) / 2 + (∫ (z : ℝ) in t - x..x + t, g z) / 2

Half-line d'Alembert formula in the case $0 \le x \le t$ (Corollary 4.0.1, second branch): $u(t, x) = \frac{1}{2}(f(x + t) - f(t - x)) + \frac{1}{2}\int_{t - x}^{x + t} g(z)\,dz$.

theorem WaveEquation1D.dAlembert_halfline_regularity_proof (f g : ℝ → ℝ) (_hf : ContDiffOn ℝ 2 f (Set.Ici 0)) (_hg : ContDiffOn ℝ 1 g (Set.Ici 0)) (_hf0 : f 0 = 0) (_hg0 : g 0 = 0) (hcompat : iteratedDerivWithin 2 f (Set.Ici 0) 0 = 0) : ContDiffOn ℝ 2 (fun (p : ℝ × ℝ) => dAlembertHalfLine f g p.1 p.2) (Set.Ici 0 ×ˢ Set.Ici 0)

Regularity for the half-line d'Alembert solution: under the standard assumptions plus the compatibility condition $f''(0) = 0$, the half-line d'Alembert solution is in $C^2$ on $[0, \infty) \times [0, \infty)$.

theorem WaveEquation1D.dAlembert_halfline_regularity (f g : ℝ → ℝ) (hf : ContDiffOn ℝ 2 f (Set.Ici 0)) (hg : ContDiffOn ℝ 1 g (Set.Ici 0)) (hf0 : f 0 = 0) (hg0 : g 0 = 0) (hcompat : iteratedDerivWithin 2 f (Set.Ici 0) 0 = 0) : ContDiffOn ℝ 2 (fun (p : ℝ × ℝ) => dAlembertHalfLine f g p.1 p.2) (Set.Ici 0 ×ˢ Set.Ici 0)

The half-line d'Alembert solution is jointly $C^2$ on $[0, \infty) \times [0, \infty)$ when $f \in C^2$, $g \in C^1$, $f(0) = g(0) = 0$, and $f''(0) = 0$.

theorem WaveEquation1D.deriv_zero_of_even (g : ℝ → ℝ) (heven : ∀ (x : ℝ), g (-x) = g x) : deriv g 0 = 0

The derivative of an even function at the origin vanishes: if $g(-x) = g(x)$ for all $x$, then $g'(0) = 0$.

theorem WaveEquation1D.deriv_even_of_odd (h : ℝ → ℝ) (hodd : ∀ (x : ℝ), h (-x) = -h x) (x : ℝ) : deriv h (-x) = deriv h x

The derivative of an odd function is even: if $h(-x) = -h(x)$ for all $x$, then $h'(-x) = h'(x)$.

theorem WaveEquation1D.odd_extension_second_spatial_deriv_zero (u : ℝ → ℝ → ℝ) (_hu_reg : ContDiffOn ℝ 2 (fun (p : ℝ × ℝ) => u p.1 p.2) (Set.Ici 0 ×ˢ Set.Ici 0)) (_hu_wave : ∀ (t x : ℝ), 0 ≤ t → 0 ≤ x → deriv (fun (t' : ℝ) => deriv (fun (t'' : ℝ) => u t'' x) t') t = deriv (fun (x' : ℝ) => deriv (fun (x'' : ℝ) => u t x'') x') x) (_hu_boundary : ∀ (t : ℝ), u t 0 = 0) (t : ℝ) (_ht : 0 ≤ t) : deriv (fun (x' : ℝ) => deriv (fun (x'' : ℝ) => if 0 ≤ x'' then u t x'' else -u t (-x'')) x') 0 = 0

For a solution $u$ of the half-line wave problem with boundary condition $u(t, 0) = 0$, the second spatial derivative of the odd extension (in $x$) vanishes at $x = 0$, for every fixed $t \ge 0$.

theorem WaveEquation1D.odd_extension_contDiff_two_of_contDiffOn (u : ℝ → ℝ → ℝ) (hu_reg : ContDiffOn ℝ 2 (fun (p : ℝ × ℝ) => u p.1 p.2) (Set.Ici 0 ×ˢ Set.Ici 0)) (hu_boundary : ∀ (t : ℝ), u t 0 = 0) (hu_dxx_zero : ∀ (t : ℝ), 0 ≤ t → deriv (fun (x : ℝ) => deriv (u t) x) 0 = 0) : ContDiff ℝ 2 fun (p : ℝ × ℝ) => (fun (t x : ℝ) => if 0 ≤ x then u t x else -u t (-x)) p.1 p.2

$C^2$ regularity of the joint odd extension in $x$: if $u$ is $C^2$ on $[0, \infty) \times [0, \infty)$ with $u(t, 0) = 0$ and the second spatial derivative vanishing at the boundary, then the extension $(t, x) \mapsto u(t, x)$ for $x \ge 0$ and $-u(t, -x)$ for $x < 0$ is jointly $C^2$ on $\mathbb{R}^2$.

theorem WaveEquation1D.odd_extension_contDiff_two_joint (u : ℝ → ℝ → ℝ) (hu_reg : ContDiffOn ℝ 2 (fun (p : ℝ × ℝ) => u p.1 p.2) (Set.Ici 0 ×ˢ Set.Ici 0)) (_hu_wave : ∀ (t x : ℝ), 0 ≤ t → 0 ≤ x → deriv (fun (t' : ℝ) => deriv (fun (t'' : ℝ) => u t'' x) t') t = deriv (fun (x' : ℝ) => deriv (fun (x'' : ℝ) => u t x'') x') x) (hu_boundary : ∀ (t : ℝ), u t 0 = 0) (hu_dxx_zero : ∀ (t : ℝ), 0 ≤ t → deriv (fun (x : ℝ) => deriv (u t) x) 0 = 0) : ContDiff ℝ 2 fun (p : ℝ × ℝ) => (fun (t x : ℝ) => if 0 ≤ x then u t x else -u t (-x)) p.1 p.2

The joint odd extension (in $x$) of a half-line wave solution is jointly $C^2$ on $\mathbb{R}^2$, under the standard regularity and compatibility hypotheses.

theorem WaveEquation1D.odd_extension_wave_negative_time (u : ℝ → ℝ → ℝ) (_hu_reg : ContDiffOn ℝ 2 (fun (p : ℝ × ℝ) => u p.1 p.2) (Set.Ici 0 ×ˢ Set.Ici 0)) (_hu_wave : ∀ (t x : ℝ), 0 ≤ t → 0 ≤ x → deriv (fun (t' : ℝ) => deriv (fun (t'' : ℝ) => u t'' x) t') t = deriv (fun (x' : ℝ) => deriv (fun (x'' : ℝ) => u t x'') x') x) (_hu_boundary : ∀ (t : ℝ), u t 0 = 0) (t x : ℝ) (_ht : ¬0 ≤ t) : deriv (fun (t' : ℝ) => deriv (fun (t'' : ℝ) => if 0 ≤ x then u t'' x else -u t'' (-x)) t') t = deriv (fun (x' : ℝ) => deriv (fun (x'' : ℝ) => if 0 ≤ x'' then u t x'' else -u t (-x'')) x') x

The joint odd extension (in $x$) of a half-line wave solution continues to satisfy the wave equation $\partial_t^2 = \partial_x^2$ also at negative times $t < 0$.

theorem WaveEquation1D.odd_extension_regularity_and_wave_axiom (u : ℝ → ℝ → ℝ) (_hu_reg : ContDiffOn ℝ 2 (fun (p : ℝ × ℝ) => u p.1 p.2) (Set.Ici 0 ×ˢ Set.Ici 0)) (_hu_wave : ∀ (t x : ℝ), 0 ≤ t → 0 ≤ x → deriv (fun (t' : ℝ) => deriv (fun (t'' : ℝ) => u t'' x) t') t = deriv (fun (x' : ℝ) => deriv (fun (x'' : ℝ) => u t x'') x') x) (_hu_boundary : ∀ (t : ℝ), u t 0 = 0) : (ContDiff ℝ 2 fun (p : ℝ × ℝ) => (fun (t x : ℝ) => if 0 ≤ x then u t x else -u t (-x)) p.1 p.2) ∧ ∀ (t x : ℝ), deriv (fun (t' : ℝ) => deriv (fun (t'' : ℝ) => (fun (t x : ℝ) => if 0 ≤ x then u t x else -u t (-x)) t'' x) t') t = deriv (fun (x' : ℝ) => deriv (fun (x'' : ℝ) => (fun (t x : ℝ) => if 0 ≤ x then u t x else -u t (-x)) t x'') x') x

The joint odd extension (in $x$) of a half-line wave solution is jointly $C^2$ on $\mathbb{R}^2$ and satisfies the wave equation $\partial_t^2 = \partial_x^2$ on all of $\mathbb{R}^2$.

theorem WaveEquation1D.odd_extension_solves_fullline (f g : ℝ → ℝ) (u : ℝ → ℝ → ℝ) (_hf : ContDiffOn ℝ 2 f (Set.Ici 0)) (_hg : ContDiffOn ℝ 1 g (Set.Ici 0)) (_hf0 : f 0 = 0) (hg0 : g 0 = 0) (hu_reg : ContDiffOn ℝ 2 (fun (p : ℝ × ℝ) => u p.1 p.2) (Set.Ici 0 ×ˢ Set.Ici 0)) (hu_wave : ∀ (t x : ℝ), 0 ≤ t → 0 ≤ x → deriv (fun (t' : ℝ) => deriv (fun (t'' : ℝ) => u t'' x) t') t = deriv (fun (x' : ℝ) => deriv (fun (x'' : ℝ) => u t x'') x') x) (hu_boundary : ∀ (t : ℝ), u t 0 = 0) (hu_init_pos : ∀ (x : ℝ), 0 ≤ x → u 0 x = f x) (hu_init_vel : ∀ (x : ℝ), 0 < x → HasDerivAt (fun (t : ℝ) => u t x) (g x) 0) : have ũ := fun (t x : ℝ) => if 0 ≤ x then u t x else -u t (-x); (ContDiff ℝ 2 fun (p : ℝ × ℝ) => ũ p.1 p.2) ∧ (∀ (t x : ℝ), deriv (fun (t' : ℝ) => deriv (fun (t'' : ℝ) => ũ t'' x) t') t = deriv (fun (x' : ℝ) => deriv (fun (x'' : ℝ) => ũ t x'') x') x) ∧ (∀ (x : ℝ), ũ 0 x = oddExtension f x) ∧ ∀ (x : ℝ), HasDerivAt (fun (t : ℝ) => ũ t x) (oddExtension g x) 0

The joint odd extension $\tilde{u}$ (in $x$) of a half-line wave solution $u$ solves the full-line wave equation on $\mathbb{R}^2$ with initial position $\tilde{f}$ (the odd extension of $f$) and initial velocity $\tilde{g}$ (the odd extension of $g$).

theorem WaveEquation1D.dAlembert_halfline_uniqueness (f g : ℝ → ℝ) (u : ℝ → ℝ → ℝ) (hf : ContDiffOn ℝ 2 f (Set.Ici 0)) (hg : ContDiffOn ℝ 1 g (Set.Ici 0)) (hf0 : f 0 = 0) (hg0 : g 0 = 0) (hu_reg : ContDiffOn ℝ 2 (fun (p : ℝ × ℝ) => u p.1 p.2) (Set.Ici 0 ×ˢ Set.Ici 0)) (hu_wave : ∀ (t x : ℝ), 0 ≤ t → 0 ≤ x → deriv (fun (t' : ℝ) => deriv (fun (t'' : ℝ) => u t'' x) t') t = deriv (fun (x' : ℝ) => deriv (fun (x'' : ℝ) => u t x'') x') x) (hu_boundary : ∀ (t : ℝ), u t 0 = 0) (hu_init_pos : ∀ (x : ℝ), 0 ≤ x → u 0 x = f x) (hu_init_vel : ∀ (x : ℝ), 0 < x → HasDerivAt (fun (t : ℝ) => u t x) (g x) 0) (t x : ℝ) : 0 ≤ t → 0 ≤ x → u t x = dAlembertHalfLine f g t x

Uniqueness for the half-line wave equation: any $C^2$ solution $u$ on $[0, \infty) \times [0, \infty)$ with $u(t, 0) = 0$, $u(0, x) = f(x)$ and $\partial_t u(0, x) = g(x)$ must coincide with the half-line d'Alembert solution.

theorem WaveEquation1D.dAlembert_halfline_corollary (f g : ℝ → ℝ) (u : ℝ → ℝ → ℝ) (hf : ContDiffOn ℝ 2 f (Set.Ici 0)) (hg : ContDiffOn ℝ 1 g (Set.Ici 0)) (hf0 : f 0 = 0) (hg0 : g 0 = 0) (hu_reg : ContDiffOn ℝ 2 (fun (p : ℝ × ℝ) => u p.1 p.2) (Set.Ici 0 ×ˢ Set.Ici 0)) (hu_wave : ∀ (t x : ℝ), 0 ≤ t → 0 ≤ x → deriv (fun (t' : ℝ) => deriv (fun (t'' : ℝ) => u t'' x) t') t = deriv (fun (x' : ℝ) => deriv (fun (x'' : ℝ) => u t x'') x') x) (hu_boundary : ∀ (t : ℝ), u t 0 = 0) (hu_init_pos : ∀ (x : ℝ), 0 ≤ x → u 0 x = f x) (hu_init_vel : ∀ (x : ℝ), 0 < x → HasDerivAt (fun (t : ℝ) => u t x) (g x) 0) : (∀ (t x : ℝ), 0 ≤ t → 0 ≤ x → u t x = dAlembertHalfLine f g t x) ∧ ContDiffOn ℝ 2 (fun (p : ℝ × ℝ) => dAlembertHalfLine f g p.1 p.2) (Set.Ici 0 ×ˢ Set.Ici 0) ∧ (∀ (t x : ℝ), 0 ≤ t → 0 ≤ x → t ≤ x → dAlembertHalfLine f g t x = (f (x + t) + f (x - t)) / 2 + (∫ (z : ℝ) in x - t..x + t, g z) / 2) ∧ ∀ (t x : ℝ), 0 ≤ t → 0 ≤ x → x ≤ t → dAlembertHalfLine f g t x = (f (x + t) - f (t - x)) / 2 + (∫ (z : ℝ) in t - x..x + t, g z) / 2

Corollary 4.0.1: the unique $C^2$ solution to the $1+1$ dimensional initial + boundary value problem $-\partial_t^2 u + \partial_x^2 u = 0$ on $[0, \infty) \times [0, \infty)$ with $u(t, 0) = 0$, $u(0, x) = f(x)$, and $\partial_t u(0, x) = g(x)$ is given by the half-line d'Alembert formula. It coincides with $\frac{1}{2}(f(x+t) + f(x-t)) + \frac{1}{2} \int_{x-t}^{x+t} g(z)\,dz$ for $0 \le t \le x$, and with $\frac{1}{2}(f(x+t) - f(t-x)) + \frac{1}{2}\int_{t-x}^{x+t} g(z)\,dz$ for $0 \le x \le t$.