Electromagnetism in Homogeneous medium

Basic properties for homogeneous medium and free space.

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

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