Imports
/- Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Joseph Tooby-Smith -/ module public import Physlib.Electromagnetism.Distributional.Dynamics.IsExtrema public import Physlib.SpaceAndTime.Space.Norm.Basic public import Physlib.SpaceAndTime.Space.Translations

Electrostatics of a stationary point particle in 3d

i. Overview

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

ii. Key results

    threeDimPointParticle : The electromagnetic potential of a point particle stationary at a point in 3d space.

    threeDimPointParticle_isExterma : The electric field of a point particle stationary at a point of 3d space satisfies Maxwell's equations

iii. Table of contents

    A. The current density

      A.1. The charge density

      A.2. The 3-current density

    B. The Potentials

      B.1. The electromagnetic potential

      B.2. The scalar potential

      B.3. The vector potential is zero

    C. The electric field

      C.1. the time derivative of the electric field

    D. The magnetic field

    E. Maxwell's equations

iv. References

@[expose] public section

A. The current density

The current density of a point particle in 3d space is given by:

$$J(r) = (c q \delta(r - rโ‚€), 0, 0, 0) $$

where $c$ is the speed light, $q$ is the charge of the particle and $rโ‚€$ is the position of the particle in 3d space.

c:SpeedOfLightq:โ„rโ‚€:SpaceโŠข (SpaceTime.distTimeSlice c).symm (constantTime ((c.val * q) โ€ข diracDelta' โ„ rโ‚€ (Lorentz.Vector.basis (Sum.inl 0)))) = (SpaceTime.distTimeSlice c).symm (constantTime ((distTranslate (basis.repr rโ‚€)) ((c.val * q) โ€ข diracDelta' โ„ 0 (Lorentz.Vector.basis (Sum.inl 0))))) c:SpeedOfLightq:โ„rโ‚€:SpaceโŠข (c.val * q) โ€ข diracDelta' โ„ rโ‚€ (Lorentz.Vector.basis (Sum.inl 0)) = (distTranslate (basis.repr rโ‚€)) ((c.val * q) โ€ข diracDelta' โ„ 0 (Lorentz.Vector.basis (Sum.inl 0))) c:SpeedOfLightq:โ„rโ‚€:Spaceฮท:๐“ข(Space, โ„)iโœ:Fin 1 โŠ• Fin 3โŠข ((c.val * q) โ€ข diracDelta' โ„ rโ‚€ (Lorentz.Vector.basis (Sum.inl 0))) ฮท iโœ = ((distTranslate (basis.repr rโ‚€)) ((c.val * q) โ€ข diracDelta' โ„ 0 (Lorentz.Vector.basis (Sum.inl 0)))) ฮท iโœ All goals completed! ๐Ÿ™

A.1. The charge density

The charge density of a point particle in 3d space is given by: $$ฯ(r) = q \delta(r - rโ‚€) $$

where $q$ is the charge of the particle and $rโ‚€$ is the position of the particle in 3d space.

@[simp] lemma threeDimPointParticleCurrentDensity_chargeDensity (c : SpeedOfLight) (q : โ„) (rโ‚€ : Space 3) : (threeDimPointParticleCurrentDensity c q rโ‚€).chargeDensity c = constantTime (q โ€ข diracDelta โ„ rโ‚€) := c:SpeedOfLightq:โ„rโ‚€:SpaceโŠข (DistLorentzCurrentDensity.chargeDensity c) (threeDimPointParticleCurrentDensity c q rโ‚€) = constantTime (q โ€ข diracDelta โ„ rโ‚€) c:SpeedOfLightq:โ„rโ‚€:Spaceฮต:๐“ข(Time ร— Space, โ„)โŠข ((DistLorentzCurrentDensity.chargeDensity c) (threeDimPointParticleCurrentDensity c q rโ‚€)) ฮต = (constantTime (q โ€ข diracDelta โ„ rโ‚€)) ฮต c:SpeedOfLightq:โ„rโ‚€:Spaceฮต:๐“ข(Time ร— Space, โ„)โŠข c.val * q * (c.valโปยน * (timeIntegralSchwartz ฮต) rโ‚€) = q * (timeIntegralSchwartz ฮต) rโ‚€ All goals completed! ๐Ÿ™

A.2. The 3-current density

The 3-current density of a point particle in 3d space is given by: $$\vec J(r) = 0.$$

In other words, there is no current flow for a point particle at rest.

@[simp] lemma threeDimPointParticleCurrentDensity_currentDensity (c : SpeedOfLight) (q : โ„) (rโ‚€ : Space 3) : (threeDimPointParticleCurrentDensity c q rโ‚€).currentDensity c = 0 := c:SpeedOfLightq:โ„rโ‚€:SpaceโŠข (DistLorentzCurrentDensity.currentDensity c) (threeDimPointParticleCurrentDensity c q rโ‚€) = 0 c:SpeedOfLightq:โ„rโ‚€:Spaceฮต:๐“ข(Time ร— Space, โ„)i:Fin 3โŠข (((DistLorentzCurrentDensity.currentDensity c) (threeDimPointParticleCurrentDensity c q rโ‚€)) ฮต).ofLp i = (0 ฮต).ofLp i All goals completed! ๐Ÿ™

B. The Potentials

B.1. The electromagnetic potential

The 4-potential of a point particle in 3d space is given by:

$$A(r) = \frac{q ฮผโ‚€ c}{4 ฯ€ |r - rโ‚€|} (1, 0, 0, 0) $$

where $ฮผโ‚€$ is the permeability of free space, $c$ is the speed of light, $q$ is the charge of the particle and $rโ‚€$ is the position of the particle in 3d space.

๐“•:FreeSpaceq:โ„rโ‚€:SpaceโŠข (SpaceTime.distTimeSlice ๐“•.c).symm (constantTime (distOfFunction (fun x => (q * ๐“•.ฮผโ‚€ * ๐“•.c.val / (4 * ฯ€) * โ€–x - rโ‚€โ€–โปยน) โ€ข Lorentz.Vector.basis (Sum.inl 0)) โ‹ฏ)) = (SpaceTime.distTimeSlice ๐“•.c).symm (constantTime ((distTranslate (basis.repr rโ‚€)) (distOfFunction (fun x => (q * ๐“•.ฮผโ‚€ * ๐“•.c.val / (4 * ฯ€) * โ€–xโ€–โปยน) โ€ข Lorentz.Vector.basis (Sum.inl 0)) โ‹ฏ))) ๐“•:FreeSpaceq:โ„rโ‚€:SpaceโŠข distOfFunction (fun x => (q * ๐“•.ฮผโ‚€ * ๐“•.c.val / (4 * ฯ€) * โ€–x - rโ‚€โ€–โปยน) โ€ข Lorentz.Vector.basis (Sum.inl 0)) โ‹ฏ = (distTranslate (basis.repr rโ‚€)) (distOfFunction (fun x => (q * ๐“•.ฮผโ‚€ * ๐“•.c.val / (4 * ฯ€) * โ€–xโ€–โปยน) โ€ข Lorentz.Vector.basis (Sum.inl 0)) โ‹ฏ) ๐“•:FreeSpaceq:โ„rโ‚€:Spaceฮท:๐“ข(Space, โ„)iโœ:Fin 1 โŠ• Fin 3โŠข (distOfFunction (fun x => (q * ๐“•.ฮผโ‚€ * ๐“•.c.val / (4 * ฯ€) * โ€–x - rโ‚€โ€–โปยน) โ€ข Lorentz.Vector.basis (Sum.inl 0)) โ‹ฏ) ฮท iโœ = ((distTranslate (basis.repr rโ‚€)) (distOfFunction (fun x => (q * ๐“•.ฮผโ‚€ * ๐“•.c.val / (4 * ฯ€) * โ€–xโ€–โปยน) โ€ข Lorentz.Vector.basis (Sum.inl 0)) โ‹ฏ)) ฮท iโœ All goals completed! ๐Ÿ™

B.2. The scalar potential

The first component of the 4-potential is the scalar potential, once one has taken account of factors of the speed of light. It is given by:

$$V(r) = \frac{q}{4 ฯ€ \epsilon_0 |r - r_0|}.$$

๐“•:FreeSpaceq:โ„rโ‚€:Spaceฮต:๐“ข(Time ร— Space, โ„)โŠข ๐“•.c.val * ((q * ๐“•.ฮผโ‚€ * ๐“•.c.val / (4 * ฯ€)) โ€ข distOfFunction (fun x => โ€–x - rโ‚€โ€–โปยน) โ‹ฏ) (timeIntegralSchwartz ฮต) = ((q / (4 * ฯ€ * ๐“•.ฮตโ‚€)) โ€ข distOfFunction (fun x => โ€–x - rโ‚€โ€–โปยน) โ‹ฏ) (timeIntegralSchwartz ฮต) ๐“•:FreeSpaceq:โ„rโ‚€:Spaceฮต:๐“ข(Time ร— Space, โ„)โŠข ๐“•.c.val * (q * ๐“•.ฮผโ‚€ * ๐“•.c.val / (4 * ฯ€) * (distOfFunction (fun x => โ€–x - rโ‚€โ€–โปยน) โ‹ฏ) (timeIntegralSchwartz ฮต)) = q / (4 * ฯ€ * ๐“•.ฮตโ‚€) * (distOfFunction (fun x => โ€–x - rโ‚€โ€–โปยน) โ‹ฏ) (timeIntegralSchwartz ฮต) ๐“•:FreeSpaceq:โ„rโ‚€:Spaceฮต:๐“ข(Time ร— Space, โ„)โŠข ๐“•.c.val ^ 2 * q * ๐“•.ฮผโ‚€ * ฯ€โปยน * (distOfFunction (fun x => โ€–x - rโ‚€โ€–โปยน) โ‹ฏ) (timeIntegralSchwartz ฮต) * (1 / 4) = q * ฯ€โปยน * (distOfFunction (fun x => โ€–x - rโ‚€โ€–โปยน) โ‹ฏ) (timeIntegralSchwartz ฮต) * ๐“•.ฮตโ‚€โปยน * (1 / 4) ๐“•:FreeSpaceq:โ„rโ‚€:Spaceฮต:๐“ข(Time ร— Space, โ„)โŠข ๐“•.ฮผโ‚€โปยน * ๐“•.ฮตโ‚€โปยน * q * ๐“•.ฮผโ‚€ * ฯ€โปยน * (distOfFunction (fun x => โ€–x - rโ‚€โ€–โปยน) โ‹ฏ) (timeIntegralSchwartz ฮต) = q * ฯ€โปยน * (distOfFunction (fun x => โ€–x - rโ‚€โ€–โปยน) โ‹ฏ) (timeIntegralSchwartz ฮต) * ๐“•.ฮตโ‚€โปยน All goals completed! ๐Ÿ™

B.3. The vector potential is zero

The spatial components of the 4-potential give the vector potential, which is zero for a stationary point particle.

$$\vec A(r) = 0.$$

@[simp] lemma threeDimPointParticle_vectorPotential (๐“• : FreeSpace) (q : โ„) (rโ‚€ : Space 3) : (threeDimPointParticle ๐“• q rโ‚€).vectorPotential ๐“•.c = 0 := ๐“•:FreeSpaceq:โ„rโ‚€:SpaceโŠข (vectorPotential ๐“•.c) (threeDimPointParticle ๐“• q rโ‚€) = 0 ๐“•:FreeSpaceq:โ„rโ‚€:Spaceฮต:๐“ข(Time ร— Space, โ„)i:Fin 3โŠข (((vectorPotential ๐“•.c) (threeDimPointParticle ๐“• q rโ‚€)) ฮต).ofLp i = (0 ฮต).ofLp i All goals completed! ๐Ÿ™

C. The electric field

The electric field of a point particle in 3d space is given by: $$\vec E(r) = \frac{q}{4 ฯ€ \epsilon_0} \frac{\vec r - \vec rโ‚€}{|\vec r - \vec rโ‚€|^3}.$$

๐“•:FreeSpaceq:โ„rโ‚€:Spacethis:โˆ‡แตˆ (distOfFunction (fun x => โ€–xโ€– ^ (-1)) โ‹ฏ) = distOfFunction (fun x => (โ†‘(-1) * โ€–xโ€– ^ (-1 - 2)) โ€ข basis.repr x) โ‹ฏโŠข -(q / (4 * ฯ€ * ๐“•.ฮตโ‚€)) โ€ข constantTime ((distTranslate (basis.repr rโ‚€)) (โˆ‡แตˆ (distOfFunction (fun x => โ€–xโ€–โปยน) โ‹ฏ))) = (q / (4 * ฯ€ * ๐“•.ฮตโ‚€)) โ€ข constantTime (distOfFunction (fun x => (โ€–x - rโ‚€โ€– ^ 3)โปยน โ€ข basis.repr (x - rโ‚€)) โ‹ฏ) All goals completed! ๐Ÿ™

C.1. the time derivative of the electric field

๐“•:FreeSpaceq:โ„rโ‚€:SpaceโŠข (q / (4 * ฯ€ * ๐“•.ฮตโ‚€)) โ€ข 0 = 0 All goals completed! ๐Ÿ™

D. The magnetic field

Given that the vector potential is zero, the magnetic field is also zero.

@[simp] lemma threeDimPointParticle_magneticFieldMatrix (q : โ„) (rโ‚€ : Space 3) : (threeDimPointParticle ๐“• q rโ‚€).magneticFieldMatrix ๐“•.c = 0 := ๐“•:FreeSpaceq:โ„rโ‚€:SpaceโŠข (magneticFieldMatrix ๐“•.c) (threeDimPointParticle ๐“• q rโ‚€) = 0 ๐“•:FreeSpaceq:โ„rโ‚€:Spaceฮท:๐“ข(Time ร— Space, โ„)โŠข ((magneticFieldMatrix ๐“•.c) (threeDimPointParticle ๐“• q rโ‚€)) ฮท = 0 ฮท All goals completed! ๐Ÿ™

E. Maxwell's equations

The divergence of the electric field of a point particle in 3d space is given by: $$โˆ‡ ยท \vec E(r) = \frac{1}{\epsilon_0} q \delta(r - rโ‚€).$$

From this, it follows that the electromagnetic potential of a point particle in 3d space satisfies Maxwell's equations for a point particle at rest.

๐“•:FreeSpaceq:โ„rโ‚€:Spaceh1:distDiv (distOfFunction (fun x => (โ€–xโ€– ^ 3)โปยน โ€ข basis.repr x) โ‹ฏ) = (3 * (4 / 3 * ฯ€)) โ€ข diracDelta โ„ 0โŠข (q / (4 * ฯ€ * ๐“•.ฮตโ‚€)) โ€ข constantTime ((distTranslate (basis.repr rโ‚€)) ((3 * (4 / 3 * ฯ€)) โ€ข diracDelta โ„ 0)) = (๐“•.ฮตโ‚€โปยน * q) โ€ข constantTime (diracDelta โ„ rโ‚€) ๐“•:FreeSpaceq:โ„rโ‚€:Spaceh1:distDiv (distOfFunction (fun x => (โ€–xโ€– ^ 3)โปยน โ€ข basis.repr x) โ‹ฏ) = (3 * (4 / 3 * ฯ€)) โ€ข diracDelta โ„ 0โŠข (q / (4 * ฯ€ * ๐“•.ฮตโ‚€) * (3 * (4 / 3 * ฯ€))) โ€ข constantTime ((distTranslate (basis.repr rโ‚€)) (diracDelta โ„ 0)) = (๐“•.ฮตโ‚€โปยน * q) โ€ข constantTime (diracDelta โ„ rโ‚€) ๐“•:FreeSpaceq:โ„rโ‚€:Spaceh1:distDiv (distOfFunction (fun x => (โ€–xโ€– ^ 3)โปยน โ€ข basis.repr x) โ‹ฏ) = (3 * (4 / 3 * ฯ€)) โ€ข diracDelta โ„ 0ฮท:๐“ข(Time ร— Space, โ„)โŠข ((q / (4 * ฯ€ * ๐“•.ฮตโ‚€) * (3 * (4 / 3 * ฯ€))) โ€ข constantTime ((distTranslate (basis.repr rโ‚€)) (diracDelta โ„ 0))) ฮท = ((๐“•.ฮตโ‚€โปยน * q) โ€ข constantTime (diracDelta โ„ rโ‚€)) ฮท ๐“•:FreeSpaceq:โ„rโ‚€:Spaceh1:distDiv (distOfFunction (fun x => (โ€–xโ€– ^ 3)โปยน โ€ข basis.repr x) โ‹ฏ) = (3 * (4 / 3 * ฯ€)) โ€ข diracDelta โ„ 0ฮท:๐“ข(Time ร— Space, โ„)โŠข q / (4 * ฯ€ * ๐“•.ฮตโ‚€) * (3 * (4 / 3 * ฯ€)) = ๐“•.ฮตโ‚€โปยน * q โˆจ (timeIntegralSchwartz ฮท) rโ‚€ = 0 ๐“•:FreeSpaceq:โ„rโ‚€:Spaceh1:distDiv (distOfFunction (fun x => (โ€–xโ€– ^ 3)โปยน โ€ข basis.repr x) โ‹ฏ) = (3 * (4 / 3 * ฯ€)) โ€ข diracDelta โ„ 0ฮท:๐“ข(Time ร— Space, โ„)โŠข q / (4 * ฯ€ * ๐“•.ฮตโ‚€) * (3 * (4 / 3 * ฯ€)) = ๐“•.ฮตโ‚€โปยน * q ๐“•:FreeSpaceq:โ„rโ‚€:Spaceh1:distDiv (distOfFunction (fun x => (โ€–xโ€– ^ 3)โปยน โ€ข basis.repr x) โ‹ฏ) = (3 * (4 / 3 * ฯ€)) โ€ข diracDelta โ„ 0ฮท:๐“ข(Time ร— Space, โ„)โŠข q * ฯ€ * ฯ€โปยน * ๐“•.ฮตโ‚€โปยน = q * ๐“•.ฮตโ‚€โปยน All goals completed! ๐Ÿ™๐“•:FreeSpaceq:โ„rโ‚€:Spaceฮต:๐“ข(SpaceTime, โ„)i:Fin 3โŠข ๐“•.ฮผโ‚€โปยน * (1 / ๐“•.c.val ^ 2 * (((SpaceTime.distTimeSlice ๐“•.c).symm (distTimeDeriv ((electricField ๐“•.c) (threeDimPointParticle ๐“• q rโ‚€)))) ฮต).ofLp i - โˆ‘ j, (((PiLp.basisFun 2 โ„ (Fin 3)).tensorProduct (PiLp.basisFun 2 โ„ (Fin 3))).repr (((SpaceTime.distTimeSlice ๐“•.c).symm ((distSpaceDeriv j) ((magneticFieldMatrix ๐“•.c) (threeDimPointParticle ๐“• q rโ‚€)))) ฮต)) (j, i)) + (((SpaceTime.distTimeSlice ๐“•.c).symm ((DistLorentzCurrentDensity.currentDensity ๐“•.c) (threeDimPointParticleCurrentDensity ๐“•.c q rโ‚€))) ฮต).ofLp i = 0 All goals completed! ๐Ÿ™