Three-Dimensional Electromagnetism

This directory provides a three-dimensional, vector-calculus-facing layer for electromagnetism.

The backend theory is formulated in a tensorial and dimension-general way. Here we re-express the relevant constructions in the familiar language of scalar and vector potentials, electric and magnetic fields, and spatial derivatives.

Fields from potentials

In this section we rewrite the electric and magnetic fields associated to an electromagnetic potential in terms of the scalar and vector potentials, using the standard vector-calculus expressions.

theorem Electromagnetism.ThreeDimension.electricField_eq_3D (c : SpeedOfLight) (V : ElectromagneticPotential) : ElectromagneticPotential.electricField c V = fun (t : Time) (x : Space) => -Space.grad (ElectromagneticPotential.scalarPotential c V t) x - Time.deriv (fun (t : Time) => ElectromagneticPotential.vectorPotential c V t x) t

The electric field written in terms of the scalar and vector potentials as - ∇ φ - ∂ₜ A.

theorem Electromagnetism.ThreeDimension.magneticField_eq_3D (c : SpeedOfLight) (V : ElectromagneticPotential) : ElectromagneticPotential.magneticField c V = fun (t : Time) (x : Space) => Space.curl (ElectromagneticPotential.vectorPotential c V t) x

The magnetic field written as the curl of the vector potential as ∇ ⨯ A.