Maxwell's equations

Note that currently the equations are defined for isotropic and homogeneous domains.

structure Electromagnetism.OpticalMedium : Type

An optcial medium refers to an isotropic medium (which may or may not be free space) which consists of the electric permittivity and the magnetic permeability.

• ε : ℝ

  The permittivity.

• μ : ℝ

  The permeability.

• eps_ge_zero : self.ε > 0
• mu_ge_zero : self.μ > 0

def Electromagnetism.GaussLawElectric (𝓔 : OpticalMedium) (ρ : ChargeDensity) (E : ElectricField) : Prop

Gauss's law for the Electric field.

Equations

• Electromagnetism.GaussLawElectric 𝓔 ρ E = ∀ (t : Time) (x : Space), 𝓔.ε * Space.div (E t) x = ρ t x

def Electromagnetism.GaussLawMagnetic (B : MagneticField) : Prop

Gauss's law for the Magnetic field.

Equations

• Electromagnetism.GaussLawMagnetic B = ∀ (t : Time) (x : Space), Space.div (B t) x = 0

def Electromagnetism.AmpereLaw (𝓔 : OpticalMedium) (J : CurrentDensity) (E : ElectricField) (B : MagneticField) : Prop

Ampère's law.

Equations

• Electromagnetism.AmpereLaw 𝓔 J E B = ∀ (t : Time) (x : Space), Space.curl (B t) x = 𝓔.μ • (J t x + 𝓔.ε • Time.deriv (fun (t : Time) => E t x) t)

def Electromagnetism.FaradayLaw (E : ElectricField) (B : MagneticField) : Prop

Faraday's law.

Equations

• Electromagnetism.FaradayLaw E B = ∀ (t : Time) (x : Space), Space.curl (E t) x = -Time.deriv (fun (t : Time) => B t x) t

def Electromagnetism.MaxwellEquations (𝓔 : OpticalMedium) (ρ : ChargeDensity) (J : CurrentDensity) (E : ElectricField) (B : MagneticField) : Prop

Maxwell's equations.

Equations

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