Electrostatics

Electrostatics corresponds to the study of electric fields and potentials in the absence of time variation or magnetic fields.

The study of electrostatics usually necessitates the use of distributions, since point charges are often used to model charged particles. The formal definition of such distributions are often glossed over in physics. As a result some of the definitions or proofs within PhysLean's electrostatics may seem over the top - but this is necessary for complete mathematical correctness.

@[reducible, inline]

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

The type of static electric fields (i.e. time-independent electric fields), defined as distributions from Space d to EuclideanSpace ℝ (Fin d).

Equations

• Electromagnetism.StaticElectricField d = ((Space d)→d[ℝ] EuclideanSpace ℝ (Fin d))

@[reducible, inline]

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

The type of charge distributions. Mathematically this is equivalent to the type of distributions from Space d to ℝ.

Equations

• Electromagnetism.ChargeDistribution d = ((Space d)→d[ℝ] ℝ)

@[reducible, inline]

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

The type of static electric potentials. Mathematically defined as distributions from Space d to ℝ.

Equations

• Electromagnetism.StaticElectricPotential d = ((Space d)→d[ℝ] ℝ)

noncomputable def Electromagnetism.StaticElectricField.ofPotential {d : ℕ} (φ : StaticElectricPotential d) : StaticElectricField d

The static electric field associated with a static electric potential.

Equations

• Electromagnetism.StaticElectricField.ofPotential φ = -Space.gradD φ

def Electromagnetism.StaticElectricField.GaussLaw {d : ℕ} (E : StaticElectricField d) (ε : ℝ) (ρ : ChargeDistribution d) : Prop

Gauss's law for static electric fields.

Equations

• E.GaussLaw ε ρ = (Space.divD E = (1 / ε) • ρ)

theorem Electromagnetism.StaticElectricField.gaussLaw_iff {d : ℕ} (E : StaticElectricField d) (ε : ℝ) (ρ : ChargeDistribution d) : E.GaussLaw ε ρ ↔ Space.divD E = (1 / ε) • ρ

def Electromagnetism.StaticElectricField.FaradaysLaw (E : StaticElectricField) : Prop

Faraday's law in 3d for static electric fields.

Equations

• E.FaradaysLaw = (Space.curlD E = 0)

theorem Electromagnetism.StaticElectricField.ofPotential_faradaysLaw (φ : StaticElectricPotential) : (ofPotential φ).FaradaysLaw

If the electric field is of the form -∇φ then Faraday's law holds.