Electromagnetic wave equation

i. Overview

The first part of this module shows that the electric and magnetic fields of an electromagnetic field in a homogeneous isotropic medium satisfy the wave equation.

The second part shows orthogonality properties of plane waves.

ii. Key results

• waveEquation_electricField_of_freeMaxwellEquations : The electric field of an EM field in free space satisfies the wave equation.
• waveEquation_magneticField_of_freeMaxwellEquations : The magnetic field of an EM field in free space satisfies the wave equation.
• orthonormal_triad_of_electromagneticplaneWave : The electric field, magnetic field and direction of propagation of an electromagnetic plane wave form an orthonormal triad, up to constant fields.

iii. Table of contents

• A. The wave equation from Maxwell's equations
  • A.1. The electric field of an EM field in free space satisfies the wave equation
  • A.2. The magnetic field of an EM field in free space satisfies the wave equation
• B. Orthogonality properties of plane waves
  • B.1. Definition of the electric and magnetic plane waves
  • B.2. Up to a time-dependent constant, the E field is transverse to the direction of propagation
  • B.3. Up to a time-dependent constant, the B field is transverse to the direction of propagation
  • B.4. E proportional to cross of direction of propagation & B, up to a constant
    • B.4.1. Time derivative of E-field proportional to propagation cross time derivative of B-field
    • B.4.2. Proportional up to a space-dependent constant
    • B.4.3. Proportional up to a constant
  • B.5. B proportional to cross of direction of propagation & B, up to a constant
    • B.5.1. Time derivative of B-field proportional to propagation cross time derivative of E-field
    • B.5.2. Proportional up to a space-dependent constant
    • B.5.3. Proportional up to a constant
  • B.6. E-field orthogonal to direction of propagation up to a constant
  • B.7. B-field orthogonal to direction of propagation up to a constant
  • B.8. E, B and direction of propagation form an orthonormal triad up to constants

iv. References

A. The wave equation from Maxwell's equations

A.1. The electric field of an EM field in free space satisfies the wave equation

theorem Electromagnetism.waveEquation_electricField_of_freeMaxwellEquations (OM : OpticalMedium) {t : Time} {x : Space} (E : ElectricField) (B : MagneticField) (h : OM.FreeMaxwellEquations E B) (hE : ContDiff ℝ 2 ↿E) (hB : ContDiff ℝ 2 ↿B) : ClassicalMechanics.WaveEquation E t x (√(OM.μ • OM.ε))⁻¹

The electromagnetic wave equation for electric field.

A.2. The magnetic field of an EM field in free space satisfies the wave equation

theorem Electromagnetism.waveEquation_magneticField_of_freeMaxwellEquations (OM : OpticalMedium) {t : Time} {x : Space} (E : ElectricField) (B : MagneticField) (h : OM.FreeMaxwellEquations E B) (hE : ContDiff ℝ 2 ↿E) (hB : ContDiff ℝ 2 ↿B) : ClassicalMechanics.WaveEquation B t x (√(OM.μ • OM.ε))⁻¹

The electromagnetic wave equation for magnetic field.

B. Orthogonality properties of plane waves

B.1. Definition of the electric and magnetic plane waves

noncomputable def Electromagnetism.electricPlaneWave (E₀ : ℝ → EuclideanSpace ℝ (Fin 3)) (c : ℝ) (s : Space.Direction) : ElectricField

An electric plane wave travelling in the direction of s with propagation speed c.

Equations

• Electromagnetism.electricPlaneWave E₀ c s = ClassicalMechanics.planeWave E₀ c s

noncomputable def Electromagnetism.magneticPlaneWave (B₀ : ℝ → EuclideanSpace ℝ (Fin 3)) (c : ℝ) (s : Space.Direction) : MagneticField

A magnetic plane wave travelling in the direction of s with propagation speed c.

Equations

• Electromagnetism.magneticPlaneWave B₀ c s = ClassicalMechanics.planeWave B₀ c s

B.2. Up to a time-dependent constant, the E field is transverse to the direction of propagation

theorem Electromagnetism.transverse_upto_time_fun_of_eq_electricPlaneWave (OM : OpticalMedium) {c : ℝ} {E₀ : ℝ → EuclideanSpace ℝ (Fin 3)} {s : Space.Direction} {E : ElectricField} {B : MagneticField} (hEwave : E = electricPlaneWave E₀ c s) (h' : Differentiable ℝ E₀) (hm : OM.FreeMaxwellEquations E B) : ∃ (c : Time → EuclideanSpace ℝ (Fin 3)), ∀ (t : Time) (x : Space), inner ℝ (E t x) (s.unit 3) = inner ℝ (c t) (s.unit 3)

An electric plane wave minus a constant field is transverse for all x.

B.3. Up to a time-dependent constant, the B field is transverse to the direction of propagation

theorem Electromagnetism.transverse_upto_time_fun_of_eq_magneticPlaneWave (OM : OpticalMedium) {c : ℝ} {B₀ : ℝ → EuclideanSpace ℝ (Fin 3)} {s : Space.Direction} {E : ElectricField} {B : MagneticField} (hBwave : B = magneticPlaneWave B₀ c s) (h' : Differentiable ℝ B₀) (hm : OM.FreeMaxwellEquations E B) : ∃ (c : Time → EuclideanSpace ℝ (Fin 3)), ∀ (t : Time) (x : Space), inner ℝ (B t x) (s.unit 3) = inner ℝ (c t) (s.unit 3)

An magnetic plane wave minus a constant field is transverse for all x.

B.4. E proportional to cross of direction of propagation & B, up to a constant

B.4.1. Time derivative of E-field proportional to propagation cross time derivative of B-field

theorem Electromagnetism.time_deriv_electricPlaneWave_eq_cross_time_deriv_magneticPlaneWave (OM : OpticalMedium) {c : ℝ} {t : Time} {x : Space} {B₀ : ℝ → EuclideanSpace ℝ (Fin 3)} {s : Space.Direction} {E : ElectricField} {B : MagneticField} (hc : c = (√(OM.μ • OM.ε))⁻¹) (hBwave : B = magneticPlaneWave B₀ c s) (h' : Differentiable ℝ B₀) (hm : OM.FreeMaxwellEquations E B) : Time.deriv (fun (t : Time) => E t x) t = -(√(OM.μ • OM.ε))⁻¹ • (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) (Time.deriv (fun (t : Time) => B t x) t)

The time derivative of a magnetic planewave induces an electric field with time derivative equal to - s ⨯ₑ₃ B'.

B.4.2. Proportional up to a space-dependent constant

theorem Electromagnetism.electricPlaneWave_eq_cross_magneticPlaneWave_upto_space_fun (OM : OpticalMedium) {c : ℝ} {B₀ : ℝ → EuclideanSpace ℝ (Fin 3)} {s : Space.Direction} {E : ElectricField} {B : MagneticField} (hc : c = (√(OM.μ • OM.ε))⁻¹) (hBwave : B = magneticPlaneWave B₀ c s) (h' : Differentiable ℝ B₀) (hm : OM.FreeMaxwellEquations E B) (hE : Differentiable ℝ ↿E) : ∃ (c : Space → EuclideanSpace ℝ (Fin 3)), ∀ (t : Time) (x : Space), E t x = -(√(OM.μ • OM.ε))⁻¹ • (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) (B t x) + c x

A magnetic planewave induces an electric field equal to - s ⨯ₑ₃ B plus a constant field.

B.4.3. Proportional up to a constant

theorem Electromagnetism.electricField_add_cross_magneticField_eq_const_of_planeWave (OM : OpticalMedium) {c : ℝ} {s : Space.Direction} {E₀ B₀ : ℝ → EuclideanSpace ℝ (Fin 3)} {E : ElectricField} {B : MagneticField} (hc : c = (√(OM.μ • OM.ε))⁻¹) (hEwave : E = electricPlaneWave E₀ c s) (hBwave : B = magneticPlaneWave B₀ c s) (hE' : Differentiable ℝ E₀) (hB' : Differentiable ℝ B₀) (hm : OM.FreeMaxwellEquations E B) : ∃ (Ec : EuclideanSpace ℝ (Fin 3)), ∀ (t : Time) (x : Space), E t x + (√(OM.μ • OM.ε))⁻¹ • (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) (B t x) = Ec

E + s ⨯ₑ₃ B is constant for an EMwave.

B.5. B proportional to cross of direction of propagation & B, up to a constant

B.5.1. Time derivative of B-field proportional to propagation cross time derivative of E-field

theorem Electromagnetism.time_deriv_magneticPlaneWave_eq_cross_time_deriv_electricPlaneWave (OM : OpticalMedium) {c : ℝ} {t : Time} {x : Space} {E₀ : ℝ → EuclideanSpace ℝ (Fin 3)} {s : Space.Direction} {E : ElectricField} {B : MagneticField} (hc : c = (√(OM.μ • OM.ε))⁻¹) (hEwave : E = electricPlaneWave E₀ c s) (h' : Differentiable ℝ E₀) (hm : OM.FreeMaxwellEquations E B) : Time.deriv (fun (t : Time) => B t x) t = √(OM.μ • OM.ε) • (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) (Time.deriv (fun (t : Time) => E t x) t)

The time derivative of an electric planewave induces a magnetic field with time derivative equal to s ⨯ₑ₃ E'.

B.5.2. Proportional up to a space-dependent constant

theorem Electromagnetism.magneticPlaneWave_eq_cross_electricPlaneWave_upto_space_fun (OM : OpticalMedium) {c : ℝ} {E₀ : ℝ → EuclideanSpace ℝ (Fin 3)} {s : Space.Direction} {E : ElectricField} {B : MagneticField} (hc : c = (√(OM.μ • OM.ε))⁻¹) (hEwave : E = electricPlaneWave E₀ c s) (h' : Differentiable ℝ E₀) (hm : OM.FreeMaxwellEquations E B) (hB : Differentiable ℝ ↿B) : ∃ (c : Space → EuclideanSpace ℝ (Fin 3)), ∀ (t : Time) (x : Space), B t x = √(OM.μ • OM.ε) • (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) (E t x) + c x

An electric planewave induces an magnetic field equal to s ×₃ E plus a constant field.

B.5.3. Proportional up to a constant

theorem Electromagnetism.magneticField_sub_cross_electricField_eq_const_of_planeWave (OM : OpticalMedium) {c : ℝ} {s : Space.Direction} {E₀ B₀ : ℝ → EuclideanSpace ℝ (Fin 3)} {E : ElectricField} {B : MagneticField} (hc : c = (√(OM.μ • OM.ε))⁻¹) (hEwave : E = electricPlaneWave E₀ c s) (hBwave : B = magneticPlaneWave B₀ c s) (hE' : Differentiable ℝ E₀) (hB' : Differentiable ℝ B₀) (hm : OM.FreeMaxwellEquations E B) : ∃ (Ec : EuclideanSpace ℝ (Fin 3)), ∀ (t : Time) (x : Space), B t x - √(OM.μ • OM.ε) • (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) (E t x) = Ec

B - s ⨯ₑ₃ E is constant for an EMwave.

B.6. E-field orthogonal to direction of propagation up to a constant

theorem Electromagnetism.electricField_transverse_upto_const_of_EMwave (OM : OpticalMedium) {c : ℝ} {s : Space.Direction} {E₀ B₀ : ℝ → EuclideanSpace ℝ (Fin 3)} {E : ElectricField} {B : MagneticField} (hc : c = (√(OM.μ • OM.ε))⁻¹) (hEwave : E = electricPlaneWave E₀ c s) (hBwave : B = magneticPlaneWave B₀ c s) (hE' : Differentiable ℝ E₀) (hB' : Differentiable ℝ B₀) (hm : OM.FreeMaxwellEquations E B) : ∃ (c : EuclideanSpace ℝ (Fin 3)), ∀ (t : Time) (x : Space), inner ℝ (E t x - c) (s.unit 3) = 0

The electric field of an EMwave minus a constant field is transverse.

B.7. B-field orthogonal to direction of propagation up to a constant

theorem Electromagnetism.magneticField_transverse_upto_const_of_EMwave (OM : OpticalMedium) {c : ℝ} {s : Space.Direction} {E₀ B₀ : ℝ → EuclideanSpace ℝ (Fin 3)} {E : ElectricField} {B : MagneticField} (hc : c = (√(OM.μ • OM.ε))⁻¹) (hEwave : E = electricPlaneWave E₀ c s) (hBwave : B = magneticPlaneWave B₀ c s) (hE' : Differentiable ℝ E₀) (hB' : Differentiable ℝ B₀) (hm : OM.FreeMaxwellEquations E B) : ∃ (c : EuclideanSpace ℝ (Fin 3)), ∀ (t : Time) (x : Space), inner ℝ (B t x - c) (s.unit 3) = 0

The magnetic field of an EMwave minus a constant field is transverse.

B.8. E, B and direction of propagation form an orthonormal triad up to constants

theorem Electromagnetism.orthonormal_triad_of_electromagneticplaneWave (OM : OpticalMedium) {c : ℝ} {s : Space.Direction} {E₀ B₀ : ℝ → EuclideanSpace ℝ (Fin 3)} {E : ElectricField} {B : MagneticField} (hc : c = (√(OM.μ • OM.ε))⁻¹) (hEwave : E = electricPlaneWave E₀ c s) (hBwave : B = magneticPlaneWave B₀ c s) (hE' : Differentiable ℝ E₀) (hB' : Differentiable ℝ B₀) (hm : OM.FreeMaxwellEquations E B) : ∃ (Ep : EuclideanSpace ℝ (Fin 3)) (Bp : EuclideanSpace ℝ (Fin 3)), ∀ (t : Time) (x : Space), E t x - Ep ≠ 0 ∧ B t x - Bp ≠ 0 → Orthonormal ℝ ![‖E t x - Ep‖⁻¹ • (E t x - Ep), ‖B t x - Bp‖⁻¹ • (B t x - Bp), s.unit 3]

Unit vectors in the direction of B, E and s form an orthonormal triad for an EMwave after subtracting the appropriate constant fields.