Maxwell's equations

structure Electromagnetism.EMSystem : Type

An electromagnetic system consists of charge density, a current density, the speed of light and the electric permittivity.

• c : ℝ

  The speed of light.

• ε₀ : ℝ

  The permittivity.

@[reducible, inline]

abbrev Electromagnetism.ChargeDensity : Type

The charge density.

Equations

• Electromagnetism.ChargeDensity = (Time → Space → ℝ)

@[reducible, inline]

abbrev Electromagnetism.CurrentDensity : Type

Current density.

Equations

• Electromagnetism.CurrentDensity = (Time → Space → EuclideanSpace ℝ (Fin 3))

noncomputable def Electromagnetism.EMSystem.μ₀ (𝓔 : EMSystem) : ℝ

The permeability.

Equations

• 𝓔.μ₀ = 1 / (𝓔.c ^ 2 * 𝓔.ε₀)

noncomputable def Electromagnetism.EMSystem.coulombConstant (𝓔 : EMSystem) : ℝ

Coulomb's constant.

Equations

• 𝓔.coulombConstant = 1 / (4 * Real.pi * 𝓔.ε₀)

def Electromagnetism.GaussLawElectric (𝓔 : EMSystem) (ρ : 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 (𝓔 : EMSystem) (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 (𝓔 : EMSystem) (ρ : ChargeDensity) (J : CurrentDensity) (E : ElectricField) (B : MagneticField) : Prop

Maxwell's equations.

Equations

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