Harmonic Wave

Time-harmonic waves.

Note TODO EGU3E may require considerable effort to be made rigorous and may heavily depend on the status of Fourier theory in Mathlib.

@[reducible, inline]

abbrev ClassicalMechanics.WaveVector (d : ℕ := 3) : Type

The wavevector which indicates a direction and has magnitude 2π/λ.

Equations

• ClassicalMechanics.WaveVector d = EuclideanSpace ℝ (Fin d)

noncomputable def ClassicalMechanics.WaveVector.toDirection {d : ℕ} (k : WaveVector d) (h : k ≠ 0) : Space.Direction d

Direction of a wavevector.

Equations

• k.toDirection h = { unit := ‖k‖⁻¹ • k, norm := ⋯ }

noncomputable def ClassicalMechanics.harmonicWave {d : ℕ} (a g : ℝ → Space d → ℝ) (ω : WaveVector d → ℝ) (k : WaveVector d) : Time → Space d → ℝ

General form of time-harmonic wave in terms of angular frequency ω and wave vector k.

Equations

• ClassicalMechanics.harmonicWave a g ω k t r = a (ω k) r * Real.cos (ω k * t - g (ω k) r)

noncomputable def ClassicalMechanics.transverseHarmonicPlaneWave {c : ℝ} (k : WaveVector) (f₀x f₀y ω δx δy : ℝ) (hk : k = EuclideanSpace.single 2 (ω / c)) : Time → Space → EuclideanSpace ℝ (Fin 3)

Transverse monochromatic time-harmonic plane wave where the direction of propagation is taken to be EuclideanSpace.single 2 1. f₀x and f₀y are the respective amplitudes, ω is the angular frequency, δx and δy are the respective phases for fx and fy.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem WithLp.equiv_symm_eq_zero_iff {p : ENNReal} {V : Type u_1} [AddCommGroup V] {v : V} : (WithLp.equiv p V).symm v = 0 ↔ v = 0

Pending #25552.

@[simp]

theorem WithLp.equiv_eq_zero_iff {p : ENNReal} {V : Type u_1} [AddCommGroup V] {v : WithLp p V} : (WithLp.equiv p V) v = 0 ↔ v = 0

@[simp]

theorem EuclideanSpace.single_eq_zero_iff {ι : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [DecidableEq ι] {i : ι} {x : 𝕜} : single i x = 0 ↔ x = 0

theorem ClassicalMechanics.transverseHarmonicPlaneWave_eq_planeWave {c : ℝ} {k : WaveVector} {f₀x f₀y ω δx δy : ℝ} (hc_ge_zero : 0 < c) (hω_ge_zero : 0 < ω) (hk : k = EuclideanSpace.single 2 (ω / c)) : transverseHarmonicPlaneWave k f₀x f₀y ω δx δy hk = planeWave (fun (p : ℝ) => (f₀x * Real.cos (-(ω / c) * p + δx)) • EuclideanSpace.single 0 1 + (f₀y * Real.cos (-(ω / c) * p + δy)) • EuclideanSpace.single 1 1) c (k.toDirection ⋯)

The transverse harmonic planewave representation is equivalent to the general planewave expression with ‖k‖ = ω/c.