Wave equation

i. Overview

In this module we define the wave equation in d-dimensional Euclidean space, and prove that plane waves are solutions to the wave equation. By a plne wave we mean a function of the form f(t, x) = f₀(⟪x, s⟫_ℝ - c * t) where s is a direction vector and c is the propagation speed.

ii. Key results

• WaveEquation: The general form of the wave equation where c is the propagation speed.
• planeWave: A vector-valued plane wave travelling in the direction of s with propagation speed c.
• planeWave_waveEquation: The plane wave satisfies the wave equation.

iii. Table of contents

• A. The wave equation
• B. Plane wave solutions
  • B.1. Definition of a plane wave
  • B.2. Differentiablity conditions
  • B.3. Time derivatives of plane waves
  • B.4. Space derivatives of plane waves
  • B.5. Laplacian of plane waves
  • B.6. Plane waves satisfy the wave equation
• C. Old lemmas used throughout files

iv. References

A. The wave equation

def ClassicalMechanics.WaveEquation {d : ℕ} (f : Time → Space d → EuclideanSpace ℝ (Fin d)) (t : Time) (x : Space d) (c : ℝ) : Prop

The general form of the wave equation where c is the propagation speed.

Equations

• ClassicalMechanics.WaveEquation f t x c = (c ^ 2 • Space.laplacianVec (f t) x - Time.deriv (fun (t : Time) => Time.deriv (fun (t : Time) => f t x) t) t = 0)

B. Plane wave solutions

B.1. Definition of a plane wave

noncomputable def ClassicalMechanics.planeWave {d : ℕ} (f₀ : ℝ → EuclideanSpace ℝ (Fin d)) (c : ℝ) (s : Space.Direction d) : Time → Space d → EuclideanSpace ℝ (Fin d)

A vector-valued plane wave travelling in the direction of s with propagation speed c.

Equations

• ClassicalMechanics.planeWave f₀ c s t x = f₀ (inner ℝ x s.unit - c * t.val)

theorem ClassicalMechanics.planeWave_eq {t : Time} {d : ℕ} {f₀ : ℝ → EuclideanSpace ℝ (Fin d)} {c : ℝ} {x : Space d} {s : Space.Direction d} : planeWave f₀ c s t x = f₀ (inner ℝ x s.unit - c * t.val)

B.2. Differentiablity conditions

theorem ClassicalMechanics.planeWave_differentiable_time {d : ℕ} {f₀ : ℝ → EuclideanSpace ℝ (Fin d)} {c : ℝ} {x : Space d} {s : Space.Direction d} (h' : Differentiable ℝ f₀) : Differentiable ℝ fun (t : Time) => planeWave f₀ c s t x

theorem ClassicalMechanics.planeWave_differentiable_space {d : ℕ} {f₀ : ℝ → EuclideanSpace ℝ (Fin d)} {c : ℝ} {t : Time} {s : Space.Direction d} (h' : Differentiable ℝ f₀) : Differentiable ℝ fun (x : Space d) => planeWave f₀ c s t x

theorem ClassicalMechanics.planeWave_differentiable {d : ℕ} {c : ℝ} {s : Space.Direction d} {f₀ : ℝ → EuclideanSpace ℝ (Fin d)} (h' : Differentiable ℝ f₀) : Differentiable ℝ ↿(planeWave f₀ c s)

B.3. Time derivatives of plane waves

theorem ClassicalMechanics.planeWave_time_deriv {d : ℕ} {f₀ : ℝ → EuclideanSpace ℝ (Fin d)} {c : ℝ} {x : Space d} {s : Space.Direction d} (h' : Differentiable ℝ f₀) : (Time.deriv fun (x_1 : Time) => planeWave f₀ c s x_1 x) = -c • fun (t : Time) => planeWave (fun (x : ℝ) => (fderiv ℝ f₀ x) 1) c s t x

theorem ClassicalMechanics.planeWave_time_deriv_time_deriv {d : ℕ} {f₀ : ℝ → EuclideanSpace ℝ (Fin d)} {c : ℝ} {x : Space d} {s : Space.Direction d} (h' : ContDiff ℝ 2 f₀) : Time.deriv (Time.deriv fun (x_1 : Time) => planeWave f₀ c s x_1 x) = c ^ 2 • fun (t : Time) => planeWave (iteratedDeriv 2 f₀) c s t x

B.4. Space derivatives of plane waves

theorem ClassicalMechanics.planeWave_space_deriv {t : Time} {d : ℕ} {f₀ : ℝ → EuclideanSpace ℝ (Fin d)} {c : ℝ} {s : Space.Direction d} (h' : Differentiable ℝ f₀) (i : Fin d) : Space.deriv i (planeWave f₀ c s t) = s.unit.val i • fun (x : Space d) => planeWave (fun (x : ℝ) => (fderiv ℝ f₀ x) 1) c s t x

theorem ClassicalMechanics.planeWave_apply_space_deriv {t : Time} {d : ℕ} {f₀ : ℝ → EuclideanSpace ℝ (Fin d)} {c : ℝ} {s : Space.Direction d} (h' : Differentiable ℝ f₀) (i j : Fin d) : (Space.deriv i fun (x : Space d) => (planeWave f₀ c s t x).ofLp j) = s.unit.val i • fun (x : Space d) => (planeWave (fun (x : ℝ) => (fderiv ℝ f₀ x) 1) c s t x).ofLp j

theorem ClassicalMechanics.planeWave_space_deriv_space_deriv {t : Time} {d : ℕ} {f₀ : ℝ → EuclideanSpace ℝ (Fin d)} {c : ℝ} {s : Space.Direction d} (h' : ContDiff ℝ 2 f₀) (i : Fin d) : Space.deriv i (Space.deriv i (planeWave f₀ c s t)) = s.unit.val i ^ 2 • fun (x : Space d) => planeWave (fun (x : ℝ) => iteratedDeriv 2 f₀ x) c s t x

theorem ClassicalMechanics.planeWave_apply_space_deriv_space_deriv {t : Time} {d : ℕ} {f₀ : ℝ → EuclideanSpace ℝ (Fin d)} {c : ℝ} {s : Space.Direction d} (h' : ContDiff ℝ 2 f₀) (i j : Fin d) : Space.deriv i (Space.deriv i fun (x : Space d) => (planeWave f₀ c s t x).ofLp j) = s.unit.val i ^ 2 • fun (x : Space d) => (planeWave (fun (x : ℝ) => iteratedDeriv 2 f₀ x) c s t x).ofLp j

B.5. Laplacian of plane waves

theorem ClassicalMechanics.planeWave_laplacian {t : Time} {d : ℕ} {f₀ : ℝ → EuclideanSpace ℝ (Fin d)} {c : ℝ} {s : Space.Direction d} (h' : ContDiff ℝ 2 f₀) : Space.laplacianVec (planeWave f₀ c s t) = fun (x : Space d) => planeWave (fun (x : ℝ) => iteratedDeriv 2 f₀ x) c s t x

B.6. Plane waves satisfy the wave equation

theorem ClassicalMechanics.planeWave_waveEquation {d : ℕ} (c : ℝ) (s : Space.Direction d) (f₀ : ℝ → EuclideanSpace ℝ (Fin d)) (hf₀ : ContDiff ℝ 2 f₀) (t : Time) (x : Space d) : WaveEquation (planeWave f₀ c s) t x c

The plane wave satisfies the wave equation.

C. Old lemmas used throughout files

These lemmas will eventually be moved, renamed and/or replaced.

theorem ClassicalMechanics.wave_differentiable {d : ℕ} {t : ℝ} {s : Space.Direction d} {c : ℝ} {x : Space d} : DifferentiableAt ℝ (fun (x : Space d) => inner ℝ x s.unit - c * t) x

theorem ClassicalMechanics.wave_dx2 {d : ℕ} {c t : ℝ} {x : Space d} {u v : Fin d} {s : Space.Direction d} {f₀' f₀'' : ℝ → ℝ →L[ℝ] EuclideanSpace ℝ (Fin d)} (h'' : ∀ (x : ℝ), HasFDerivAt (fun (x' : ℝ) => (f₀' x') 1) (f₀'' x) x) : (fderiv ℝ (fun (x' : Space d) => inner ℝ ((f₀' (inner ℝ x' s.unit - c * t)) (s.unit.val u)) (EuclideanSpace.single v 1)) x) (Space.basis u) = inner ℝ (s.unit.val u ^ 2 • (f₀'' (inner ℝ x s.unit - c * t)) 1) (EuclideanSpace.single v 1)

theorem ClassicalMechanics.space_fderiv_of_inner_product_wave_eq_space_fderiv {d : ℕ} {c : ℝ} {x : Space d} {t : Time} {f₀ : ℝ → EuclideanSpace ℝ (Fin d)} {s : Space.Direction d} {u v : Fin d} (h' : Differentiable ℝ f₀) : c * (fun (x' : Space d) => (fderiv ℝ (fun (x : Space d) => inner ℝ (f₀ (inner ℝ x s.unit - c * t.val)) (EuclideanSpace.single v 1)) x') (Space.basis u)) x = -s.unit.val u * (Time.deriv (fun (t : Time) => f₀ (inner ℝ x s.unit - c * t.val)) t).ofLp v

If f₀ is a function of (inner ℝ x s - c * t), the fderiv of its components with respect to spatial coordinates is equal to the corresponding component of the propagation direction s times time derivative.

theorem ClassicalMechanics.time_differentiable_of_eq_planewave {d : ℕ} {c : ℝ} {x : Space d} {s : Space.Direction d} {f₀ : ℝ → EuclideanSpace ℝ (Fin d)} {f : Time → Space d → EuclideanSpace ℝ (Fin d)} (h' : Differentiable ℝ f₀) (hf : f = planeWave f₀ c s) : Differentiable ℝ fun (t : Time) => f t x

theorem ClassicalMechanics.crossProduct_time_differentiable_of_right_eq_planewave {c : ℝ} {x : Space} {t : Time} {s : Space.Direction} {f₀ : ℝ → EuclideanSpace ℝ (Fin 3)} {f : Time → Space → EuclideanSpace ℝ (Fin 3)} (h' : Differentiable ℝ f₀) (hf : f = planeWave f₀ c s) : DifferentiableAt ℝ (fun (t : Time) => (fun (a b : WithLp 2 (Fin 3 → ℝ)) => (WithLp.equiv 2 (Fin 3 → ℝ)).symm ((crossProduct ((WithLp.equiv 2 (Fin 3 → ℝ)) a)) ((WithLp.equiv 2 (Fin 3 → ℝ)) b))) (Space.basis.repr (s.unit 3)) (f t x)) t

theorem ClassicalMechanics.crossProduct_differentiable_of_right_eq_planewave {u : ℝ} {s : Space.Direction} {f₀ : ℝ → EuclideanSpace ℝ (Fin 3)} (h' : Differentiable ℝ f₀) : DifferentiableAt ℝ (fun (u : ℝ) => (fun (a b : WithLp 2 (Fin 3 → ℝ)) => (WithLp.equiv 2 (Fin 3 → ℝ)).symm ((crossProduct ((WithLp.equiv 2 (Fin 3 → ℝ)) a)) ((WithLp.equiv 2 (Fin 3 → ℝ)) b))) (Space.basis.repr (s.unit 3)) (f₀ u)) u

theorem ClassicalMechanics.wave_fderiv_inner_eq_inner_fderiv_proj {d : ℕ} {c t : ℝ} {f₀ : ℝ → EuclideanSpace ℝ (Fin d)} {s : Space.Direction d} {i : Fin d} (h' : Differentiable ℝ f₀) (x y : Space d) : s.unit.val i * ((fderiv ℝ (fun (x : Space d) => f₀ (inner ℝ x s.unit - c * t)) x) y).ofLp i = inner ℝ y s.unit * (fderiv ℝ (fun (x : Space d) => (f₀ (inner ℝ x s.unit - c * t)).ofLp i) x) (Space.basis i)