Electromagnetism

In this file we define the electric field, the magnetic field, and the field strength tensor.

@[reducible, inline]

abbrev Electromagnetism.ElectricField (d : ℕ := 3) : Type

The electric field is a map from d+1 dimensional spacetime to the vector space ℝ^d.

Equations

• Electromagnetism.ElectricField d = (Time → Space d → EuclideanSpace ℝ (Fin d))

@[reducible, inline]

abbrev Electromagnetism.MagneticField (d : ℕ := 3) : Type

The magnetic field is a map from d+1 dimensional spacetime to the vector space ℝ^d.

Equations

• Electromagnetism.MagneticField d = (Time → Space d → EuclideanSpace ℝ (Fin d))

@[reducible, inline]

abbrev Electromagnetism.VectorPotential (d : ℕ := 3) : Type

The vector potential of an electromagnetic field

Equations

• Electromagnetism.VectorPotential d = (SpaceTime d → (realLorentzTensor d).Tensor ![realLorentzTensor.Color.up])

structure Electromagnetism.EMSystem : Type

The electric permittivity and the magnetic permeability of free space.

• ε₀ : ℝ

  The permittivity of free space.

• μ₀ : ℝ

  The permeability of free space.

@[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.c (𝓔 : EMSystem) : ℝ

The speed of light.

Equations

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

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

Coulomb's constant.

Equations

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