Electromagnetism in Homogeneous medium

Basic properties for homogeneous medium and free space.

Variables are bundled in structure, for unbundled version use PhysLean.Electromagnetism.MaxwellEquations.

This module is old, and will soon be replaced.

structure Electromagnetism.ChargedMediumextends Electromagnetism.OpticalMedium : Type

Charged Medium is defined as Optical Medium with charge and current.

• ε : ℝ
• μ : ℝ
• eps_ge_zero : self.ε > 0
• mu_ge_zero : self.μ > 0
• ρ : ChargeDensity

  The charge density.

• J : CurrentDensity

  The current density.

@[reducible, inline]

abbrev Electromagnetism.ChargedMedium.GaussLawElectric (CM : ChargedMedium) (E : ElectricField) : Prop

Gauss's law for the Electric field in homogeneous medium.

Equations

• CM.GaussLawElectric E = Electromagnetism.GaussLawElectric CM.toOpticalMedium CM.ρ E

@[reducible, inline]

abbrev Electromagnetism.ChargedMedium.GaussLawMagnetic (B : MagneticField) : Prop

Gauss's law for the Magnetic field in homogeneous medium.

Equations

• Electromagnetism.ChargedMedium.GaussLawMagnetic B = Electromagnetism.GaussLawMagnetic B

@[reducible, inline]

abbrev Electromagnetism.ChargedMedium.AmpereLaw (CM : ChargedMedium) (E : ElectricField) (B : MagneticField) : Prop

Ampère's law in homogeneous medium.

Equations

• CM.AmpereLaw E B = Electromagnetism.AmpereLaw CM.toOpticalMedium CM.J E B

@[reducible, inline]

abbrev Electromagnetism.ChargedMedium.FaradayLaw (E : ElectricField) (B : MagneticField) : Prop

Faraday's law in homogeneous medium.

Equations

• Electromagnetism.ChargedMedium.FaradayLaw E B = Electromagnetism.FaradayLaw E B

Maxwell's equations for charge and current free medium

def Electromagnetism.OpticalMedium.free (OM : OpticalMedium) : ChargedMedium

Optical medium defined as charge and current free charged medium.

Equations

• OM.free = { toOpticalMedium := OM, ρ := fun (x : Time) (x : Space) => 0, J := fun (x : Time) (x : Space) => 0 }

def Electromagnetism.OpticalMedium.FreeMaxwellEquations (OM : OpticalMedium) (E : ElectricField) (B : MagneticField) : Prop

The Maxwell equations for charge and current free medium.

Equations

• OM.FreeMaxwellEquations E B = Electromagnetism.MaxwellEquations OM OM.free.ρ OM.free.J E B

theorem Electromagnetism.OpticalMedium.gaussLawElectric_of_free (OM : OpticalMedium) {t : Time} {x : Space} (E : ElectricField) (B : MagneticField) (h : OM.FreeMaxwellEquations E B) : Space.div (E t) x = 0

theorem Electromagnetism.OpticalMedium.gaussLawMagnetic_of_free (OM : OpticalMedium) {t : Time} {x : Space} (E : ElectricField) (B : MagneticField) (h : OM.FreeMaxwellEquations E B) : Space.div (B t) x = 0

theorem Electromagnetism.OpticalMedium.ampereLaw_of_free (OM : OpticalMedium) {t : Time} {x : Space} (E : ElectricField) (B : MagneticField) (h : OM.FreeMaxwellEquations E B) : Space.curl (B t) x = OM.μ • OM.ε • Time.deriv (fun (t : Time) => E t x) t

theorem Electromagnetism.OpticalMedium.faradayLaw_of_free (OM : OpticalMedium) {t : Time} {x : Space} (E : ElectricField) (B : MagneticField) (h : OM.FreeMaxwellEquations E B) : Space.curl (E t) x = -Time.deriv (fun (t : Time) => B t x) t