Harmonic Wave in Vacuum

i. Overview

In this module we define the electromagnetic potential for a monochromatic harmonic wave travelling in the x-direction in free space, and prove various properties about it, including that it satisfies Maxwell's equations in free space, that it is a plane wave.

We work here in a general dimension d so we use the magnetic field is the form of a matrix rather than a vector.

ii. Key results

• harmonicWaveX : Definition of the electromagnetic potential for a harmonic wave travelling in the x-direction.
• harmonicWaveX_isExtrema : The harmonic wave satisfies Maxwell's equations in free space.
• harmonicWaveX_isPlaneWave : The harmonic wave is a plane wave.
• harmonicWaveX_polarization_ellipse : The polarization ellipse equation for the harmonic wave.

iii. Table of contents

• A. The electromagnetic potential for a harmonic wave
  • A.1. Differentiability of the electromagnetic potential
  • A.2. Smoothness of the electromagnetic potential
• B. The scalar potential
• C. The vector potential
  • C.1. Components of the vector potential
  • C.2. Space derivatives of the vector potential
• D. The electric field
  • D.1. Components of the electric field
  • D.2. Spatial derivatives of the electric field
  • D.3. Time derivatives of the electric field
  • D.4. Divergence of the electric field
• E. The magnetic field matrix for a harmonic wave
  • E.1. Components of the magnetic field matrix
  • E.2. Space derivatives of the magnetic field matrix
• F. Maxwell's equations for a harmonic wave
• G. The harmonic wave is a plane wave
• H. Polarization ellipse of the harmonic wave

iv. References

A. The electromagnetic potential for a harmonic wave

noncomputable def Electromagnetism.ElectromagneticPotential.harmonicWaveX {d : ℕ} (𝓕 : FreeSpace) (k : ℝ) (E₀ φ : Fin d → ℝ) : ElectromagneticPotential d.succ

The electromagnetic potential for a Harmonic wave travelling in the x-direction with wave number k.

Equations

• One or more equations did not get rendered due to their size.
• Electromagnetism.ElectromagneticPotential.harmonicWaveX 𝓕 k E₀ φ x (Sum.inl 0) = 0
• Electromagnetism.ElectromagneticPotential.harmonicWaveX 𝓕 k E₀ φ x (Sum.inr ⟨0, ⋯⟩) = 0

A.1. Differentiability of the electromagnetic potential

theorem Electromagnetism.ElectromagneticPotential.harmonicWaveX_differentiable {d : ℕ} (𝓕 : FreeSpace) (k : ℝ) (E₀ φ : Fin d → ℝ) : Differentiable ℝ (harmonicWaveX 𝓕 k E₀ φ)

A.2. Smoothness of the electromagnetic potential

theorem Electromagnetism.ElectromagneticPotential.harmonicWaveX_contDiff {d : ℕ} (n : WithTop ℕ∞) (𝓕 : FreeSpace) (k : ℝ) (E₀ φ : Fin d → ℝ) : ContDiff ℝ n (harmonicWaveX 𝓕 k E₀ φ)

B. The scalar potential

The scalar potential of the harmonic wave is zero.

@[simp]

theorem Electromagnetism.ElectromagneticPotential.harmonicWaveX_scalarPotential_eq_zero {d : ℕ} (𝓕 : FreeSpace) (k : ℝ) (E₀ φ : Fin d → ℝ) : scalarPotential 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) = 0

C. The vector potential

C.1. Components of the vector potential

@[simp]

theorem Electromagnetism.ElectromagneticPotential.harmonicWaveX_vectorPotential_zero_eq_zero {d : ℕ} (𝓕 : FreeSpace) (k : ℝ) (E₀ φ : Fin d → ℝ) (t : Time) (x : Space d.succ) : (vectorPotential 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x).ofLp 0 = 0

theorem Electromagnetism.ElectromagneticPotential.harmonicWaveX_vectorPotential_succ {d : ℕ} (𝓕 : FreeSpace) (k : ℝ) (E₀ φ : Fin d → ℝ) (t : Time) (x : Space d.succ) (i : Fin d) : (vectorPotential 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x).ofLp i.succ = -E₀ i * 1 / (𝓕.c.val * k) * Real.sin (k * (t.val * 𝓕.c.val - x.val 0) + φ i)

theorem Electromagnetism.ElectromagneticPotential.harmonicWaveX_vectorPotential_succ' {d : ℕ} (𝓕 : FreeSpace) (k : ℝ) (E₀ φ : Fin d → ℝ) (t : Time) (x : Space d.succ) (i : ℕ) (hi : i.succ < d.succ) : (vectorPotential 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x).ofLp ⟨i.succ, hi⟩ = -E₀ ⟨i, ⋯⟩ * 1 / (𝓕.c.val * k) * Real.sin (k * (t.val * 𝓕.c.val - x.val 0) + φ ⟨i, ⋯⟩)

C.2. Space derivatives of the vector potential

@[simp]

theorem Electromagnetism.ElectromagneticPotential.harmonicWaveX_vectorPotential_space_deriv_succ {d : ℕ} (𝓕 : FreeSpace) (k : ℝ) (E₀ φ : Fin d → ℝ) (t : Time) (x : Space d.succ) (j : Fin d) (i : Fin d.succ) : Space.deriv j.succ (fun (x : Space (d + 1)) => (vectorPotential 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x).ofLp i) x = 0

@[simp]

theorem Electromagnetism.ElectromagneticPotential.harmonicWaveX_vectorPotential_succ_space_deriv_zero {d : ℕ} (𝓕 : FreeSpace) (k : ℝ) (hk : k ≠ 0) (E₀ φ : Fin d → ℝ) (t : Time) (x : Space d.succ) (i : Fin d) : Space.deriv 0 (fun (x : Space d.succ) => (vectorPotential 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x).ofLp i.succ) x = E₀ i / 𝓕.c.val * Real.cos (𝓕.c.val * k * t.val - k * x.val 0 + φ i)

D. The electric field

D.1. Components of the electric field

theorem Electromagnetism.ElectromagneticPotential.harmonicWaveX_electricField_zero {d : ℕ} (𝓕 : FreeSpace) (k : ℝ) (E₀ φ : Fin d → ℝ) (t : Time) (x : Space d.succ) : (electricField 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x).ofLp 0 = 0

theorem Electromagnetism.ElectromagneticPotential.harmonicWaveX_electricField_succ {d : ℕ} (𝓕 : FreeSpace) (k : ℝ) (hk : k ≠ 0) (E₀ φ : Fin d → ℝ) (t : Time) (x : Space d.succ) (i : Fin d) : (electricField 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x).ofLp i.succ = E₀ i * Real.cos (k * 𝓕.c.val * t.val - k * x.val 0 + φ i)

D.2. Spatial derivatives of the electric field

theorem Electromagnetism.ElectromagneticPotential.harmonicWaveX_electricField_space_deriv_same {d : ℕ} (𝓕 : FreeSpace) (k : ℝ) (hk : k ≠ 0) (E₀ φ : Fin d → ℝ) (t : Time) (x : Space d.succ) (i : Fin d.succ) : Space.deriv i (fun (x : Space d.succ) => (electricField 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x).ofLp i) x = 0

D.3. Time derivatives of the electric field

theorem Electromagnetism.ElectromagneticPotential.harmonicWaveX_electricField_succ_time_deriv {d : ℕ} (𝓕 : FreeSpace) (k : ℝ) (hk : k ≠ 0) (E₀ φ : Fin d → ℝ) (t : Time) (x : Space d.succ) (i : Fin d) : Time.deriv (fun (t : Time) => (electricField 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x).ofLp i.succ) t = -k * 𝓕.c.val * E₀ i * Real.sin (k * 𝓕.c.val * t.val - k * x.val 0 + φ i)

D.4. Divergence of the electric field

@[simp]

theorem Electromagnetism.ElectromagneticPotential.harmonicWaveX_div_electricField_eq_zero {d : ℕ} (𝓕 : FreeSpace) (k : ℝ) (hk : k ≠ 0) (E₀ φ : Fin d → ℝ) (t : Time) (x : Space d.succ) : Space.div (fun (x : Space d.succ) => electricField 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x) x = 0

E. The magnetic field matrix for a harmonic wave

E.1. Components of the magnetic field matrix

@[simp]

theorem Electromagnetism.ElectromagneticPotential.harmonicWaveX_magneticFieldMatrix_succ_succ {d : ℕ} (𝓕 : FreeSpace) (k : ℝ) (E₀ φ : Fin d → ℝ) (t : Time) (x : Space d.succ) (i j : Fin d) : magneticFieldMatrix 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x (i.succ, j.succ) = 0

theorem Electromagnetism.ElectromagneticPotential.harmonicWaveX_magneticFieldMatrix_zero_succ {d : ℕ} (𝓕 : FreeSpace) (k : ℝ) (hk : k ≠ 0) (E₀ φ : Fin d → ℝ) (t : Time) (x : Space d.succ) (i : Fin d) : magneticFieldMatrix 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x (0, i.succ) = -E₀ i / 𝓕.c.val * Real.cos (𝓕.c.val * k * t.val - k * x.val 0 + φ i)

theorem Electromagnetism.ElectromagneticPotential.harmonicWaveX_magneticFieldMatrix_succ_zero {d : ℕ} (𝓕 : FreeSpace) (k : ℝ) (hk : k ≠ 0) (E₀ φ : Fin d → ℝ) (t : Time) (x : Space d.succ) (i : Fin d) : magneticFieldMatrix 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x (i.succ, 0) = E₀ i / 𝓕.c.val * Real.cos (𝓕.c.val * k * t.val - k * x.val 0 + φ i)

E.2. Space derivatives of the magnetic field matrix

theorem Electromagnetism.ElectromagneticPotential.harmonicWaveX_magneticFieldMatrix_space_deriv_succ {d : ℕ} (𝓕 : FreeSpace) (k : ℝ) (hk : k ≠ 0) (E₀ φ : Fin d → ℝ) (t : Time) (x : Space d.succ) (i j : Fin d.succ) (l : Fin d) : Space.deriv l.succ (fun (x : Space (d + 1)) => magneticFieldMatrix 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x (i, j)) x = 0

theorem Electromagnetism.ElectromagneticPotential.harmonicWaveX_magneticFieldMatrix_zero_succ_space_deriv_zero {d : ℕ} (𝓕 : FreeSpace) (k : ℝ) (hk : k ≠ 0) (E₀ φ : Fin d → ℝ) (t : Time) (x : Space d.succ) (i : Fin d) : Space.deriv 0 (fun (x : Space d.succ) => magneticFieldMatrix 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x (0, i.succ)) x = -E₀ i * k / 𝓕.c.val * Real.sin (𝓕.c.val * k * t.val - k * x.val 0 + φ i)

F. Maxwell's equations for a harmonic wave

theorem Electromagnetism.ElectromagneticPotential.harmonicWaveX_isExtrema {d : ℕ} (𝓕 : FreeSpace) (k : ℝ) (hk : k ≠ 0) (E₀ φ : Fin d → ℝ) : IsExtrema 𝓕 (harmonicWaveX 𝓕 k E₀ φ) 0

G. The harmonic wave is a plane wave

theorem Electromagnetism.ElectromagneticPotential.harmonicWaveX_isPlaneWave {d : ℕ} (𝓕 : FreeSpace) (k : ℝ) (hk : k ≠ 0) (E₀ φ : Fin d → ℝ) : IsPlaneWave 𝓕 (harmonicWaveX 𝓕 k E₀ φ) { unit := Space.basis 0, norm := ⋯ }

H. Polarization ellipse of the harmonic wave

theorem Electromagnetism.ElectromagneticPotential.harmonicWaveX_polarization_ellipse {d : ℕ} (𝓕 : FreeSpace) (k : ℝ) (hk : k ≠ 0) (E₀ φ : Fin d → ℝ) (t : Time) (x : Space d.succ) (hi : ∀ (i : Fin d), E₀ i ≠ 0) : 2 * ↑d * ∑ i : Fin d, ((electricField 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x).ofLp i.succ / E₀ i) ^ 2 - 2 * ∑ i : Fin d, ∑ j : Fin d, (electricField 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x).ofLp i.succ / E₀ i * ((electricField 𝓕.c (harmonicWaveX 𝓕 k E₀ φ) t x).ofLp j.succ / E₀ j) * Real.cos (φ j - φ i) = ∑ i : Fin d, ∑ j : Fin d, Real.sin (φ j - φ i) ^ 2