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.

The electric field is given by the Heaviside step function, and the scalar potential is given by a function proportional to the absolute value of the distance from the particle.

ii. Key results

• oneDimPointParticleCurrentDensity : The Lorentz current density of a point particle stationary at the origin of 1d space.
• oneDimPointParticle : The electromagnetic potential of a point particle stationary at the origin of 1d space.
• oneDimPointParticle_gradLagrangian : The variational gradient of the Lagrangian for a point particle stationary at the origin of 1d space is zero for the given electromagnetic potential. (i.e. Maxwell's equations are satisfied).

iii. Table of contents

• A. The electromagnetic potential
• B. The Potentials
  • B.1. The electromagnetic potential
  • B.2. The vector potential is zero
  • B.3. The scalar potential
• C. The electric field
• D. Maxwell's equations
  • D.1. Gauss' law
  • D.2. The variational gradient of the Lagrangian is zero

iv. References

A. The electromagnetic potential

noncomputable def Electromagnetism.oneDimPointParticleCurrentDensity (q : ℝ) : LorentzCurrentDensityD 1

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

Equations

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

B. The Potentials

B.1. The electromagnetic potential

noncomputable def Electromagnetism.oneDimPointParticle (q : ℝ) : ElectromagneticPotentialD 1

The electromagnetic potential of a point particle stationary at the origin of 1d space.

Equations

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

B.2. The vector potential is zero

@[simp]

theorem Electromagnetism.oneDimPointParticle_vectorPotential (q : ℝ) : ElectromagneticPotentialD.vectorPotential (oneDimPointParticle q) = 0

B.3. The scalar potential

theorem Electromagnetism.oneDimPointParticle_scalarPotential (q : ℝ) : ElectromagneticPotentialD.scalarPotential (oneDimPointParticle q) = Space.constantTime (-Distribution.ofFunction (fun (x : EuclideanSpace ℝ (Fin (Nat.succ 0))) => (q / 2) • ‖x‖) ⋯ ⋯)

C. The electric field

theorem Electromagnetism.oneDimPointParticle_electricField_eq_heavisideStep (q : ℝ) : ElectromagneticPotentialD.electricField (oneDimPointParticle q) = Space.constantTime (q • (ContinuousLinearMap.smulRight (Distribution.heavisideStep 0) (Space.basis 0) - (1 / 2) • Space.constD 1 (Space.basis 0)))

D. Maxwell's equations

D.1. Gauss' law

theorem Electromagnetism.oneDimPointParticle_gaussLaw (q : ℝ) : Space.spaceDivD (ElectromagneticPotentialD.electricField (oneDimPointParticle q)) = Space.constantTime (q • Distribution.diracDelta ℝ 0)

D.2. The variational gradient of the Lagrangian is zero

theorem Electromagnetism.oneDimPointParticle_gradLagrangian (q : ℝ) : (oneDimPointParticle q).gradLagrangian (oneDimPointParticleCurrentDensity q) = 0