Physlib.Electromagnetism.Basic

Imports

/-
Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
module

public import Physlib.SpaceAndTime.SpaceTime.Basic

Electromagnetism

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

This module is old and parts of it will soon be replaced.

@[expose] public section

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

abbrev ElectricField (d : ℕ := 3) := Time → Space d → EuclideanSpace ℝ (Fin d)

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

abbrev MagneticField (d : ℕ := 3) := Time → Space d → EuclideanSpace ℝ (Fin d)

The vector potential of an electromagnetic field

abbrev VectorPotential (d : ℕ := 3) := SpaceTime d → ℝT[d, .up]

The electric permittivity and the magnetic permeability of free space.

The permittivity of free space.

The permeability of free space.

              structure EMSystem where  ε₀ : ℝ  μ₀ : ℝ

TODO "Charge density and current density should be generalized to signed measures,
  in such a way
  that they are still easy to work with and can be integrated with with tensor notation.
  See here:
  https://leanprover.zulipchat.com/#narrow/channel/479953-Physlib/topic/Maxwell's.20Equations"

The charge density.

abbrev ChargeDensity := Time → Space → ℝ

Current density.

abbrev CurrentDensity := Time → Space → EuclideanSpace ℝ (Fin 3)