Electromagnetic wave equation

The electromagnetic wave eqaution as a consequence of the charge and current free Maxwell's Equations in homogeneous isotropic medium.

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.

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.

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

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.

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.

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'.

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'.

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.

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.

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.

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.

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.

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.

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 direciton of B, E and s form an orthonormal traid for an EMwave after subtracting the appropriate constant fields.