Electromagnetic wave equation

i. Overview

In this module we define a proposition IsPlaneWave on electromagnetic potentials which is true if the potential corresponds to a plane wave. From this we derive various properties of plane waves including the orthogonality of the electric field, magnetic field and direction of propagation, in general dimensions.

ii. Key results

• IsPlaneWave : The proposition defining plane waves.
• IsPlaneWave.electricFunction : The electric function corresponding to a plane wave.
• IsPlaneWave.magneticFunction : The magnetic function corresponding to a plane wave.
• IsPlaneWave.magneticFieldMatrix_eq_propogator_cross_electricField : The magnetic field expressed in terms of the electric field and direction of propagation.
• IsPlaneWave.electricField_eq_propogator_cross_magneticFieldMatrix : The electric field expressed in terms of the magnetic field and direction of propagation.

iii. Table of contents

• A. The property of being a plane wave
  • A.1. The electric and magnetic functions from a plane wave
    • A.1.1. Electric function and magnetic function in terms of E and B fields
    • A.1.2. Uniquness of the electric function
    • A.1.3. Uniquness of the magnetic function
  • A.2. Differentiability conditions
  • A.3. Time derivative of electric and magnetic fields of a plane wave
  • A.4. Space derivative of electric and magnetic fields of a plane wave
  • A.5. Space derivative in terms of time derivative
• B. The magnetic field in terms of the electric field
  • B.1. Time derivative of the magnetic field in terms of electric field
  • B.2. Space derivative of the magnetic field in terms of electric field
  • B.3. Magnetic field equal propogator cross electric field up to constant
• C. The electric field in terms of the magnetic field
  • C.1. The time derivative of the electric field in terms of magnetic field
  • C.2. The space derivative of the electric field in terms of magnetic field
  • C.3. Electric field equal propogator cross magnetic field up to constant

iv. References

A. The property of being a plane wave

def Electromagnetism.ElectromagneticPotential.IsPlaneWave {d : ℕ} (𝓕 : FreeSpace) (A : ElectromagneticPotential d) (s : Space.Direction d) : Prop

The proposition on a electromagnetic potential which is true if it corresponds to a plane wave.

Equations

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

A.1. The electric and magnetic functions from a plane wave

noncomputable def Electromagnetism.ElectromagneticPotential.IsPlaneWave.electricFunction {d : ℕ} {𝓕 : FreeSpace} {A : ElectromagneticPotential d} {s : Space.Direction d} (hA : IsPlaneWave 𝓕 A s) : ℝ → EuclideanSpace ℝ (Fin d)

The corresponding electric field function from ℝ to EuclideanSpace ℝ (Fin d) of a plane wave.

Equations

• hA.electricFunction = Classical.choose ⋯

theorem Electromagnetism.ElectromagneticPotential.IsPlaneWave.electricField_eq_electricFunction {d : ℕ} {𝓕 : FreeSpace} {A : ElectromagneticPotential d} {s : Space.Direction d} (P : IsPlaneWave 𝓕 A s) (t : Time) (x : Space d) : electricField 𝓕.c A t x = P.electricFunction (inner ℝ x s.unit - 𝓕.c.val * t.val)

noncomputable def Electromagnetism.ElectromagneticPotential.IsPlaneWave.magneticFunction {d : ℕ} {𝓕 : FreeSpace} {A : ElectromagneticPotential d} {s : Space.Direction d} (hA : IsPlaneWave 𝓕 A s) : ℝ → Fin d × Fin d → ℝ

The corresponding magnetic field function from ℝ to Fin d × Fin d → ℝ of a plane wave.

Equations

• hA.magneticFunction = Classical.choose ⋯

theorem Electromagnetism.ElectromagneticPotential.IsPlaneWave.magneticFieldMatrix_eq_magneticFunction {d : ℕ} {𝓕 : FreeSpace} {A : ElectromagneticPotential d} {s : Space.Direction d} (P : IsPlaneWave 𝓕 A s) (t : Time) (x : Space d) : magneticFieldMatrix 𝓕.c A t x = P.magneticFunction (inner ℝ x s.unit - 𝓕.c.val * t.val)

A.1.1. Electric function and magnetic function in terms of E and B fields

theorem Electromagnetism.ElectromagneticPotential.IsPlaneWave.electricFunction_eq_electricField {d : ℕ} {𝓕 : FreeSpace} {A : ElectromagneticPotential d} {s : Space.Direction d} (P : IsPlaneWave 𝓕 A s) : P.electricFunction = fun (u : ℝ) => electricField 𝓕.c A { val := -u / 𝓕.c.val } 0

theorem Electromagnetism.ElectromagneticPotential.IsPlaneWave.magneticFunction_eq_magneticFieldMatrix {d : ℕ} {𝓕 : FreeSpace} {A : ElectromagneticPotential d} {s : Space.Direction d} (P : IsPlaneWave 𝓕 A s) : P.magneticFunction = fun (u : ℝ) => magneticFieldMatrix 𝓕.c A { val := -u / 𝓕.c.val } 0

A.1.2. Uniquness of the electric function

theorem Electromagnetism.ElectromagneticPotential.IsPlaneWave.electricFunction_unique {d : ℕ} {𝓕 : FreeSpace} {A : ElectromagneticPotential d} {s : Space.Direction d} (P : IsPlaneWave 𝓕 A s) (E1 : ℝ → EuclideanSpace ℝ (Fin d)) (hE₁ : electricField 𝓕.c A = ClassicalMechanics.planeWave E1 𝓕.c.val s) : E1 = P.electricFunction

A.1.3. Uniquness of the magnetic function

theorem Electromagnetism.ElectromagneticPotential.IsPlaneWave.magneticFunction_unique {d : ℕ} {𝓕 : FreeSpace} {A : ElectromagneticPotential d} {s : Space.Direction d} (P : IsPlaneWave 𝓕 A s) (B1 : ℝ → Fin d × Fin d → ℝ) (hB₁ : ∀ (t : Time) (x : Space d), magneticFieldMatrix 𝓕.c A t x = B1 (inner ℝ x s.unit - 𝓕.c.val * t.val)) : B1 = P.magneticFunction

A.2. Differentiability conditions

theorem Electromagnetism.ElectromagneticPotential.IsPlaneWave.electricFunction_differentiable {d : ℕ} {𝓕 : FreeSpace} {A : ElectromagneticPotential d} {s : Space.Direction d} (P : IsPlaneWave 𝓕 A s) (hA : ContDiff ℝ 2 A) : Differentiable ℝ P.electricFunction

theorem Electromagnetism.ElectromagneticPotential.IsPlaneWave.magneticFunction_differentiable {d : ℕ} {𝓕 : FreeSpace} {A : ElectromagneticPotential d} {s : Space.Direction d} (P : IsPlaneWave 𝓕 A s) (hA : ContDiff ℝ 2 A) (ij : Fin d × Fin d) : Differentiable ℝ fun (u : ℝ) => P.magneticFunction u ij

A.3. Time derivative of electric and magnetic fields of a plane wave

theorem Electromagnetism.ElectromagneticPotential.IsPlaneWave.electricField_time_deriv {d : ℕ} {𝓕 : FreeSpace} {A : ElectromagneticPotential d} {s : Space.Direction d} (P : IsPlaneWave 𝓕 A s) (hA : ContDiff ℝ 2 A) (t : Time) (x : Space d) : Time.deriv (fun (x_1 : Time) => electricField 𝓕.c A x_1 x) t = -𝓕.c.val • (fderiv ℝ P.electricFunction (inner ℝ x s.unit - 𝓕.c.val * t.val)) 1

theorem Electromagnetism.ElectromagneticPotential.IsPlaneWave.magneticFieldMatrix_time_deriv {d : ℕ} {𝓕 : FreeSpace} {A : ElectromagneticPotential d} {s : Space.Direction d} (P : IsPlaneWave 𝓕 A s) (hA : ContDiff ℝ 2 A) (t : Time) (x : Space d) (i j : Fin d) : Time.deriv (fun (x_1 : Time) => magneticFieldMatrix 𝓕.c A x_1 x (i, j)) t = -𝓕.c.val • (fderiv ℝ (fun (u : ℝ) => P.magneticFunction u (i, j)) (inner ℝ x s.unit - 𝓕.c.val * t.val)) 1

A.4. Space derivative of electric and magnetic fields of a plane wave

theorem Electromagnetism.ElectromagneticPotential.IsPlaneWave.electricField_space_deriv {d : ℕ} {𝓕 : FreeSpace} {A : ElectromagneticPotential d} {s : Space.Direction d} (P : IsPlaneWave 𝓕 A s) (hA : ContDiff ℝ 2 A) (t : Time) (x : Space d) (i : Fin d) : Space.deriv i (fun (x : Space d) => electricField 𝓕.c A t x) x = s.unit.val i • (fderiv ℝ P.electricFunction (inner ℝ x s.unit - 𝓕.c.val * t.val)) 1

theorem Electromagnetism.ElectromagneticPotential.IsPlaneWave.magneticFieldMatrix_space_deriv {d : ℕ} {𝓕 : FreeSpace} {A : ElectromagneticPotential d} {s : Space.Direction d} (P : IsPlaneWave 𝓕 A s) (hA : ContDiff ℝ 2 A) (t : Time) (x : Space d) (i j k : Fin d) : Space.deriv k (fun (x : Space d) => magneticFieldMatrix 𝓕.c A t x (i, j)) x = s.unit.val k • (fderiv ℝ (fun (u : ℝ) => P.magneticFunction u (i, j)) (inner ℝ x s.unit - 𝓕.c.val * t.val)) 1

A.5. Space derivative in terms of time derivative

theorem Electromagnetism.ElectromagneticPotential.IsPlaneWave.electricField_space_deriv_eq_time_deriv {d : ℕ} {𝓕 : FreeSpace} {A : ElectromagneticPotential d} {s : Space.Direction d} (P : IsPlaneWave 𝓕 A s) (hA : ContDiff ℝ 2 A) (t : Time) (x : Space d) (i k : Fin d) : Space.deriv k (fun (x : Space d) => (electricField 𝓕.c A t x).ofLp i) x = -(s.unit.val k / 𝓕.c.val) • Time.deriv (fun (x_1 : Time) => (electricField 𝓕.c A x_1 x).ofLp i) t

theorem Electromagnetism.ElectromagneticPotential.IsPlaneWave.magneticFieldMatrix_space_deriv_eq_time_deriv {d : ℕ} {𝓕 : FreeSpace} {A : ElectromagneticPotential d} {s : Space.Direction d} (P : IsPlaneWave 𝓕 A s) (hA : ContDiff ℝ 2 A) (t : Time) (x : Space d) (i j k : Fin d) : Space.deriv k (fun (x : Space d) => magneticFieldMatrix 𝓕.c A t x (i, j)) x = -(s.unit.val k / 𝓕.c.val) • Time.deriv (fun (x_1 : Time) => magneticFieldMatrix 𝓕.c A x_1 x (i, j)) t

B. The magnetic field in terms of the electric field

B.1. Time derivative of the magnetic field in terms of electric field

theorem Electromagnetism.ElectromagneticPotential.IsPlaneWave.time_deriv_magneticFieldMatrix_eq_electricField_mul_propogator {d : ℕ} {𝓕 : FreeSpace} {A : ElectromagneticPotential d} {s : Space.Direction d} (P : IsPlaneWave 𝓕 A s) (hA : ContDiff ℝ 2 A) (t : Time) (x : Space d) (i j : Fin d) : Time.deriv (fun (x_1 : Time) => magneticFieldMatrix 𝓕.c A x_1 x (i, j)) t = Time.deriv (fun (t : Time) => s.unit.val j / 𝓕.c.val * (electricField 𝓕.c A t x).ofLp i - s.unit.val i / 𝓕.c.val * (electricField 𝓕.c A t x).ofLp j) t

B.2. Space derivative of the magnetic field in terms of electric field

theorem Electromagnetism.ElectromagneticPotential.IsPlaneWave.space_deriv_magneticFieldMatrix_eq_electricField_mul_propogator {d : ℕ} {𝓕 : FreeSpace} {A : ElectromagneticPotential d} {s : Space.Direction d} (P : IsPlaneWave 𝓕 A s) (hA : ContDiff ℝ 2 A) (t : Time) (x : Space d) (i j k : Fin d) : Space.deriv k (fun (x : Space d) => magneticFieldMatrix 𝓕.c A t x (i, j)) x = Space.deriv k (fun (x : Space d) => s.unit.val j / 𝓕.c.val * (electricField 𝓕.c A t x).ofLp i - s.unit.val i / 𝓕.c.val * (electricField 𝓕.c A t x).ofLp j) x

B.3. Magnetic field equal propogator cross electric field up to constant

theorem Electromagnetism.ElectromagneticPotential.IsPlaneWave.magneticFieldMatrix_eq_propogator_cross_electricField {d : ℕ} {𝓕 : FreeSpace} {A : ElectromagneticPotential d} {s : Space.Direction d} (P : IsPlaneWave 𝓕 A s) (hA : ContDiff ℝ 2 A) (i j : Fin d) : ∃ (C : ℝ), ∀ (t : Time) (x : Space d), magneticFieldMatrix 𝓕.c A t x (i, j) = 1 / 𝓕.c.val * (s.unit.val j * (electricField 𝓕.c A t x).ofLp i - s.unit.val i * (electricField 𝓕.c A t x).ofLp j) + C

C. The electric field in terms of the magnetic field

C.1. The time derivative of the electric field in terms of magnetic field

theorem Electromagnetism.ElectromagneticPotential.IsPlaneWave.time_deriv_electricField_eq_magneticFieldMatrix {d : ℕ} {𝓕 : FreeSpace} {A : ElectromagneticPotential d} {s : Space.Direction d} (P : IsPlaneWave 𝓕 A s) (hA : ContDiff ℝ (↑⊤) A) (h : IsExtrema 𝓕 A 0) (t : Time) (x : Space d) (i : Fin d) : Time.deriv (fun (x_1 : Time) => (electricField 𝓕.c A x_1 x).ofLp i) t = Time.deriv (fun (t : Time) => 𝓕.c.val * ∑ j : Fin d, magneticFieldMatrix 𝓕.c A t x (i, j) * s.unit.val j) t

C.2. The space derivative of the electric field in terms of magnetic field

theorem Electromagnetism.ElectromagneticPotential.IsPlaneWave.space_deriv_electricField_eq_magneticFieldMatrix {d : ℕ} {𝓕 : FreeSpace} {A : ElectromagneticPotential d} {s : Space.Direction d} (P : IsPlaneWave 𝓕 A s) (hA : ContDiff ℝ (↑⊤) A) (h : IsExtrema 𝓕 A 0) (t : Time) (x : Space d) (i k : Fin d) : Space.deriv k (fun (x : Space d) => (electricField 𝓕.c A t x).ofLp i) x = Space.deriv k (fun (x : Space d) => 𝓕.c.val * ∑ j : Fin d, magneticFieldMatrix 𝓕.c A t x (i, j) * s.unit.val j) x

C.3. Electric field equal propogator cross magnetic field up to constant

theorem Electromagnetism.ElectromagneticPotential.IsPlaneWave.electricField_eq_propogator_cross_magneticFieldMatrix {d : ℕ} {𝓕 : FreeSpace} {A : ElectromagneticPotential d} {s : Space.Direction d} (P : IsPlaneWave 𝓕 A s) (hA : ContDiff ℝ (↑⊤) A) (h : IsExtrema 𝓕 A 0) (i : Fin d) : ∃ (C : (fun (x : Fin d) => ℝ) i), ∀ (t : Time) (x : Space d), (electricField 𝓕.c A t x).ofLp i = 𝓕.c.val * ∑ j : Fin d, magneticFieldMatrix 𝓕.c A t x (i, j) * s.unit.val j + C