Wave equation

The general 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.laplacian_vec (f t) x - Time.deriv (fun (t : Time) => Time.deriv (fun (t : Time) => f t x) t) t = 0)

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)

theorem ClassicalMechanics.wave_dt {d : ℕ} {f₀ : ℝ → EuclideanSpace ℝ (Fin d)} {x : EuclideanSpace ℝ (Fin d)} {c : ℝ} {s : Space.Direction d} {f₀' : ℝ → ℝ →L[ℝ] EuclideanSpace ℝ (Fin d)} (h' : ∀ (x : ℝ), HasFDerivAt f₀ (f₀' x) x) : (Time.deriv fun (t : Time) => f₀ (inner ℝ x s.unit - c * t)) = fun (t : ℝ) => -c • (f₀' (inner ℝ x s.unit - c * t)) 1

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

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

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

theorem ClassicalMechanics.wave_dx2 {d : ℕ} {c t : ℝ} {x : EuclideanSpace ℝ (Fin 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' : EuclideanSpace ℝ (Fin d)) => inner ℝ ((f₀' (inner ℝ x' s.unit - c * t)) (s.unit u)) (EuclideanSpace.single v 1)) x) (EuclideanSpace.single u 1) = inner ℝ (s.unit u ^ 2 • (f₀'' (inner ℝ x s.unit - c * t)) 1) (EuclideanSpace.single v 1)

theorem ClassicalMechanics.planeWave_isWave {d : ℕ} (c : ℝ) (s : Space.Direction d) (f₀ : ℝ → EuclideanSpace ℝ (Fin d)) (f₀' f₀'' : ℝ → ℝ →L[ℝ] EuclideanSpace ℝ (Fin d)) (h' : ∀ (x : ℝ), HasFDerivAt f₀ (f₀' x) x) (h'' : ∀ (x : ℝ), HasFDerivAt (fun (x' : ℝ) => (f₀' x') 1) (f₀'' x) x) (t : Time) (x : Space d) : WaveEquation (planeWave f₀ c s) t x c

The plane wave satisfies the wave equation.

Helper lemmas for further derivation

theorem ClassicalMechanics.space_fderiv_of_inner_product_wave_eq_space_fderiv {d : ℕ} {c t : ℝ} {x : EuclideanSpace ℝ (Fin d)} {f₀ : ℝ → EuclideanSpace ℝ (Fin d)} {s : Space.Direction d} {u v : Fin d} (h' : Differentiable ℝ f₀) : c * (fun (x' : EuclideanSpace ℝ (Fin d)) => (fderiv ℝ (fun (x : EuclideanSpace ℝ (Fin d)) => inner ℝ (f₀ (inner ℝ x s.unit - c * t)) (EuclideanSpace.single v 1)) x') (EuclideanSpace.single u 1)) x = -s.unit u * Time.deriv (fun (t : Time) => f₀ (inner ℝ x s.unit - c * t)) t 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))) (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))) (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 : EuclideanSpace ℝ (Fin d)) : s.unit i * (fderiv ℝ (fun (x : EuclideanSpace ℝ (Fin d)) => f₀ (inner ℝ x s.unit - c * t)) x) y i = inner ℝ y s.unit * (fderiv ℝ (fun (x : EuclideanSpace ℝ (Fin d)) => f₀ (inner ℝ x s.unit - c * t) i) x) (EuclideanSpace.single i 1)

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