The electrostatics of a stationary point particle in 1d

i. Overview

In this module we give the electromagnetic properties of a point particle sitting at the origin in 1d space.

ii. Key results

• oneDimPointParticle : The electromagnetic potential of a point particle stationary at the origin of 1d space.
• oneDimPointParticle_isExterma : The electric field of a point particle stationary at the origin of 1d space satisfies Maxwell's equations

iii. Table of contents

• A. The current density
• B. The Potentials
  • B.1. The electromagnetic potential
  • B.2. The vector potential is zero
  • B.3. The scalar potential
• C. The electric field
  • C.1. The time derivative of the electric field
• D. The magnetic field
• E. Maxwell's equations

iv. References

A. The current density

noncomputable def Electromagnetism.DistElectromagneticPotential.oneDimPointParticleCurrentDensity (c : SpeedOfLight) (q : ℝ) (r₀ : Space 1) : DistLorentzCurrentDensity 1

The current density of a point particle stationary at the origin of 1d space.

Equations

• One or more equations did not get rendered due to their size.

theorem Electromagnetism.DistElectromagneticPotential.oneDimPointParticleCurrentDensity_eq_distTranslate (c : SpeedOfLight) (q : ℝ) (r₀ : Space 1) : oneDimPointParticleCurrentDensity c q r₀ = (SpaceTime.distTimeSlice c).symm (Space.constantTime ((Space.distTranslate (Space.basis.repr r₀)) ((c.val * q) • Distribution.diracDelta' ℝ 0 (Lorentz.Vector.basis (Sum.inl 0)))))

@[simp]

theorem Electromagnetism.DistElectromagneticPotential.oneDimPointParticleCurrentDensity_currentDensity (c : SpeedOfLight) (q : ℝ) (r₀ : Space 1) : (DistLorentzCurrentDensity.currentDensity c) (oneDimPointParticleCurrentDensity c q r₀) = 0

@[simp]

theorem Electromagnetism.DistElectromagneticPotential.oneDimPointParticleCurrentDensity_chargeDensity (c : SpeedOfLight) (q : ℝ) (r₀ : Space 1) : (DistLorentzCurrentDensity.chargeDensity c) (oneDimPointParticleCurrentDensity c q r₀) = Space.constantTime (q • Distribution.diracDelta ℝ r₀)

B. The Potentials

B.1. The electromagnetic potential

noncomputable def Electromagnetism.DistElectromagneticPotential.oneDimPointParticle (𝓕 : FreeSpace) (q : ℝ) (r₀ : Space 1) : DistElectromagneticPotential 1

The electromagnetic potential of a point particle stationary at r₀ of 1d space.

Equations

• One or more equations did not get rendered due to their size.

theorem Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_eq_distTranslate (𝓕 : FreeSpace) (q : ℝ) (r₀ : Space 1) : oneDimPointParticle 𝓕 q r₀ = (SpaceTime.distTimeSlice 𝓕.c).symm (Space.constantTime ((Space.distTranslate (Space.basis.repr r₀)) (Space.distOfFunction (fun (x : Space 1) => (-(q * 𝓕.μ₀ * 𝓕.c.val) / 2 * ‖x‖) • Lorentz.Vector.basis (Sum.inl 0)) ⋯)))

@[simp]

theorem Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_vectorPotential (𝓕 : FreeSpace) (q : ℝ) (r₀ : Space 1) : (vectorPotential 𝓕.c) (oneDimPointParticle 𝓕 q r₀) = 0

B.3. The scalar potential

theorem Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_scalarPotential (𝓕 : FreeSpace) (q : ℝ) (r₀ : Space 1) : (scalarPotential 𝓕.c) (oneDimPointParticle 𝓕 q r₀) = Space.constantTime (Space.distOfFunction (fun (x : Space 1) => -(q * 𝓕.μ₀ * 𝓕.c.val ^ 2 / 2) • ‖x - r₀‖) ⋯)

C. The electric field

theorem Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_electricField (𝓕 : FreeSpace) (q : ℝ) (r₀ : Space 1) : (electricField 𝓕.c) (oneDimPointParticle 𝓕 q r₀) = (q * 𝓕.μ₀ * 𝓕.c.val ^ 2 / 2) • Space.constantTime (Space.distOfFunction (fun (x : Space 1) => ‖x - r₀‖ ^ (-1) • Space.basis.repr (x - r₀)) ⋯)

C.1. The time derivative of the electric field

@[simp]

theorem Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_electricField_timeDeriv (𝓕 : FreeSpace) (q : ℝ) (r₀ : Space 1) : Space.distTimeDeriv ((electricField 𝓕.c) (oneDimPointParticle 𝓕 q r₀)) = 0

D. The magnetic field

theorem Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_magneticFieldMatrix {𝓕 : FreeSpace} (q : ℝ) (r₀ : Space 1) : (magneticFieldMatrix 𝓕.c) (oneDimPointParticle 𝓕 q r₀) = 0

E. Maxwell's equations

theorem Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_div_electricField {𝓕 : FreeSpace} (q : ℝ) (r₀ : Space 1) : Space.distSpaceDiv ((electricField 𝓕.c) (oneDimPointParticle 𝓕 q r₀)) = (𝓕.μ₀ * 𝓕.c.val ^ 2) • Space.constantTime (q • Distribution.diracDelta ℝ r₀)

theorem Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_isExterma (𝓕 : FreeSpace) (q : ℝ) (r₀ : Space 1) : IsExtrema 𝓕 (oneDimPointParticle 𝓕 q r₀) (oneDimPointParticleCurrentDensity 𝓕.c q r₀)