A electrostatics of a point particle in 3d.

In this module we derive properties of the electrostatics of a point particle of charge q sitting in 3d space.

i. Key results

• The electric potential is given by electricPotential q ε r₀.
• The electric field is given by electricField q ε r₀.
• Gauss's law is given in gaussLaw.
• Faraday's law is given in faradaysLaw.

ii. References

• The proof of Gauss' law in this module follows: https://math.stackexchange.com/questions/2409008/

A. Definitions

We start by stating the charge distribution, electric potential and electric field of the point particle. Later on in this module we will prove that these definitions are correct, by showing they satisfy the necessary physical properties.

We have the following definitions:

• The chargeDistribution is q δ(r-r₀).
• The electricPotential is (q/(4 * π * ε)) • ‖r - r₀‖⁻¹.
• The electricField is (q/(4 * π * ε)) • ‖r - r₀‖⁻¹ ^ 3 • (r - r₀).

def Electromagnetism.ThreeDimPointParticle.chargeDistribution (q : ℝ) (r₀ : Space) : ChargeDistribution

The charge distribution of a point particle of charge q in 3d space sitting at the r₀. In the physicists notation this corresponds to the 'function' q δ(r-r₀).

Equations

• Electromagnetism.ThreeDimPointParticle.chargeDistribution q r₀ = q • Distribution.diracDelta ℝ r₀

def Electromagnetism.ThreeDimPointParticle.electricPotential (q ε : ℝ) (r₀ : Space) : StaticElectricPotential

The electric potential of a point particle of charge q in 3d space sitting at the r₀. In physics notation this corresponds to the 'function' (q/(4 * π * ε)) • ‖r - r₀‖⁻¹. Here it is defined as the distribution corresponing to that function.

Equations

• Electromagnetism.ThreeDimPointParticle.electricPotential q ε r₀ = Distribution.ofFunction (fun (r : EuclideanSpace ℝ (Fin (Nat.succ 2))) => (q / (4 * Real.pi * ε)) • ‖r - r₀‖⁻¹) ⋯ ⋯

def Electromagnetism.ThreeDimPointParticle.electricField (q ε : ℝ) (r₀ : Space) : StaticElectricField

The electric field of a point particle of charge q in 3d space sitting at r₀. In physics notation this corresponds to the 'function' (q/(4 * π * ε)) • ‖r - r₀‖⁻¹ ^ 3 • (r - r₀). Here it is defined as the distribution corresponding to that function.

Equations

• Electromagnetism.ThreeDimPointParticle.electricField q ε r₀ = Distribution.ofFunction (fun (r : EuclideanSpace ℝ (Fin (Nat.succ 2))) => (q / (4 * Real.pi * ε)) • ‖r - r₀‖⁻¹ ^ 3 • (r - r₀)) ⋯ ⋯

B. Properties for q = 0

We first prove that the charge distribution, electric potential and electric field are all zero when the charge of the particle is zero.

theorem Electromagnetism.ThreeDimPointParticle.chargeDistribution_eq_zero_of_charge_eq_zero (r₀ : Space) : chargeDistribution 0 r₀ = 0

theorem Electromagnetism.ThreeDimPointParticle.electricPotential_eq_zero_of_charge_eq_zero {ε : ℝ} (r₀ : Space) : electricPotential 0 ε r₀ = 0

theorem Electromagnetism.ThreeDimPointParticle.electricField_eq_zero_of_charge_eq_zero {ε : ℝ} (r₀ : Space) : electricField 0 ε r₀ = 0

C. Translations

We now prove that the charge distribution, electric potential and electric field for the point particle at r₀ is just the translation of the charge distribution, electric potential and electric field for the point particle located at 0.

theorem Electromagnetism.ThreeDimPointParticle.chargeDistribution_eq_translateD (q : ℝ) (r₀ : Space) : chargeDistribution q r₀ = (Space.translateD r₀) (chargeDistribution q 0)

theorem Electromagnetism.ThreeDimPointParticle.electricPotential_eq_translateD (q ε : ℝ) (r₀ : Space) : electricPotential q ε r₀ = (Space.translateD r₀) (electricPotential q ε 0)

theorem Electromagnetism.ThreeDimPointParticle.electricField_eq_translateD (q ε : ℝ) (r₀ : Space) : electricField q ε r₀ = (Space.translateD r₀) (electricField q ε 0)

D. Proving the gradient of the potential is the electric field

We now prove that the electric field is equal to the negative gradient of the potential, i.e. E = -∇φ.

D.1. Reducing the problem to showing an integral is zero

Until the very end of this problem we will implicitly assume that r₀ = 0. We generalize at the end.

The first step of our proof is to show that E = -∇φ if for any Schwartz map η and direction y the integral ∫ r, d_y η r * ‖r‖⁻¹ + η r * -⟪(‖r‖ ^ 3)⁻¹ • x, r⟫_ℝ = 0 is equal to zero.

Recall that a 'Schwartz map' is a smooth function which, along with all it's derivatives, decays fast. It's presence here is because the electric field and potential are defined as distributions, and distributions are defined by how they act on Schwartz maps.

theorem Electromagnetism.ThreeDimPointParticle.gradD_electricPotential_eq_electricField_of_integral_eq_zero (q ε : ℝ) (h_integral : ∀ (η : SchwartzMap (EuclideanSpace ℝ (Fin 3)) ℝ) (y : EuclideanSpace ℝ (Fin 3)), ∫ (a : EuclideanSpace ℝ (Fin 3)), (((SchwartzMap.fderivCLM ℝ) η) a) y * ‖a‖⁻¹ + η a * -inner ℝ ((‖a‖ ^ 3)⁻¹ • a) y = 0) : -Space.gradD (electricPotential q ε 0) = electricField q ε 0

The relation E = -∇φ holds for the point particle if the integral ∫ x, d_y η x * ‖x‖⁻¹ + η x * -⟪(‖x‖ ^ 3)⁻¹ • x, y⟫_ℝ = 0 is zero.

D.2. A smooth approximation to ‖r‖⁻¹

Notice that in the integral ∫ r, d_y η r * ‖r‖⁻¹ + η r * -⟪(‖r‖ ^ 3)⁻¹ • x, r⟫_ℝ = 0 the integrand is has the structure of the total derivative of the function η r * ‖r‖⁻¹ in the direction y, i.e. d_y (η r * ‖r‖⁻¹).

However, this doesn't quite work because ‖r‖⁻¹ is not differentiable at r = 0. To get around this we define a sequence of functions, which for n : ℕ are given by potentialLimitSeries n r = (‖r‖ ^ 2 + 1/(n + 1))^ (-1/2 : ℝ).

The overall aim will be to write ∫ r, d_y η r * ‖r‖⁻¹ + η r * -⟪(‖r‖ ^ 3)⁻¹ • x, r⟫_ℝ as the limit of the integrals ∫ r, d_y η r * potentialLimitSeries n r + η r * d_y (potentialLimitSeries n) r y as n → ∞, and then show that each of these integrals is zero because they are integrals of total derivatives of differentiable functions.

def Electromagnetism.ThreeDimPointParticle.potentialLimitSeries : ℕ → EuclideanSpace ℝ (Fin 3) → ℝ

A series of functions whose limit is the ‖x‖⁻¹ and for which each function is differentiable everywhere.

Equations

• Electromagnetism.ThreeDimPointParticle.potentialLimitSeries n x = (‖x‖ ^ 2 + 1 / (↑n + 1)) ^ (-1 / 2)

theorem Electromagnetism.ThreeDimPointParticle.potentialLimitSeries_eq (n : ℕ) : potentialLimitSeries n = fun (x : EuclideanSpace ℝ (Fin 3)) => (‖x‖ ^ 2 + 1 / (↑n + 1)) ^ (-1 / 2)

Part D.2.I.

The most important property of potentialLimitSeries is that it converges to ‖x‖⁻¹ as n → ∞. That is, it approximates ‖x‖⁻¹ arbitrarily closely for large enough n.

theorem Electromagnetism.ThreeDimPointParticle.potentialLimitSeries_tendsto (x : EuclideanSpace ℝ (Fin 3)) (hx : x ≠ 0) : Filter.Tendsto (fun (n : ℕ) => potentialLimitSeries n x) Filter.atTop (nhds ‖x‖⁻¹)

Part D.2.II.

Unlike ‖r‖⁻¹, importantly the functions potentialLimitSeries n are differentiable everywhere.

theorem Electromagnetism.ThreeDimPointParticle.potentialLimitSeries_differentiable (n : ℕ) : Differentiable ℝ (potentialLimitSeries n)

Part D.2.III.

The derivative of potentialLimitSeries n in the direction y is given by - (‖r‖^1 + 1/(1 + n))^(-3/2) * ⟪r, y⟫_ℝ, or equivalently - (potentialLimitSeries n r) ^ 3 * ⟪r, y⟫_ℝ.

theorem Electromagnetism.ThreeDimPointParticle.potentialLimitSeries_fderiv (x y : EuclideanSpace ℝ (Fin 3)) (n : ℕ) : (fderiv ℝ (potentialLimitSeries n) x) y = -((‖x‖ ^ 2 + (1 + ↑n)⁻¹) ^ (-1 / 2)) ^ 3 * inner ℝ x y

theorem Electromagnetism.ThreeDimPointParticle.potentialLimitSeries_fderiv_eq_potentialLimitseries_mul (x y : EuclideanSpace ℝ (Fin 3)) (n : ℕ) : (fderiv ℝ (potentialLimitSeries n) x) y = -potentialLimitSeries n x ^ 3 * inner ℝ x y

Part D.2.IV.

as n → ∞ the limit of the derivative of potentialLimitSeries n in the direction y is -⟪(‖x‖ ^ 3)⁻¹ • x, y⟫_ℝ. This is exactly the derivative of ‖x‖⁻¹ in the direction y, when it exists (i.e. when x ≠ 0).

theorem Electromagnetism.ThreeDimPointParticle.potentialLimitSeries_fderiv_tendsto (x y : EuclideanSpace ℝ (Fin 3)) (hx : x ≠ 0) : Filter.Tendsto (fun (n : ℕ) => (fderiv ℝ (potentialLimitSeries n) x) y) Filter.atTop (nhds (-inner ℝ ((‖x‖ ^ 3)⁻¹ • x) y))

Part D.2.V

Because we are integrating, we need to show some integrability and measurability properties of potentialLimitSeries and it's derivative.

We first show that they are almost everywhere strongly measurable.

theorem Electromagnetism.ThreeDimPointParticle.potentialLimitSeries_aeStronglyMeasurable (n : ℕ) : MeasureTheory.AEStronglyMeasurable (potentialLimitSeries n) MeasureTheory.volume

theorem Electromagnetism.ThreeDimPointParticle.potentialLimitSeries_fderiv_aeStronglyMeasurable (n : ℕ) (y : EuclideanSpace ℝ (Fin 3)) : MeasureTheory.AEStronglyMeasurable (fun (x : EuclideanSpace ℝ (Fin 3)) => (fderiv ℝ (potentialLimitSeries n) x) y) MeasureTheory.volume

Part D.2.VI.

We now show that potentialLimitSeries satisfies the condition IsDistBounded. Along with the fact it is almost everywhere strongly measurable, this means it can be made into a tempered distribution, but for our purposes means that it is integrable when multiplied by a Schwartz map.

There are a number of precursory lemmas first.

theorem Electromagnetism.ThreeDimPointParticle.potentialLimitSeries_eq_sqrt_inv (n : ℕ) : potentialLimitSeries n = fun (x : EuclideanSpace ℝ (Fin 3)) => √(‖x‖ ^ 2 + 1 / (↑n + 1))⁻¹

theorem Electromagnetism.ThreeDimPointParticle.potentialLimitSeries_nonneg (n : ℕ) (x : EuclideanSpace ℝ (Fin 3)) : 0 ≤ potentialLimitSeries n x

theorem Electromagnetism.ThreeDimPointParticle.potentialLimitSeries_bounded_neq_zero (n : ℕ) (x : EuclideanSpace ℝ (Fin 3)) (hx : x ≠ 0) : ‖potentialLimitSeries n x‖ ≤ ‖x‖⁻¹

theorem Electromagnetism.ThreeDimPointParticle.potentialLimitSeries_bounded (n : ℕ) (x : EuclideanSpace ℝ (Fin 3)) : ‖potentialLimitSeries n x‖ ≤ ‖x‖⁻¹ + √(↑n + 1)

theorem Electromagnetism.ThreeDimPointParticle.potentialLimitSeries_isDistBounded (n : ℕ) : Distribution.IsDistBounded (potentialLimitSeries n)

Part D.2.VII.

In a similar fashion, and for the same reason, we now show that the derivative of potentialLimitSeries satisfies the condition IsDistBounded.

theorem Electromagnetism.ThreeDimPointParticle.potentialLimitSeries_fderiv_bounded (n : ℕ) (x y : EuclideanSpace ℝ (Fin 3)) : ‖(fderiv ℝ (potentialLimitSeries n) x) y‖ ≤ ‖x‖⁻¹ ^ 2 * ‖y‖

theorem Electromagnetism.ThreeDimPointParticle.potentialLimitSeries_fderiv_isDistBounded (n : ℕ) (y : EuclideanSpace ℝ (Fin 3)) : Distribution.IsDistBounded fun (x : EuclideanSpace ℝ (Fin (Nat.succ 2))) => (fderiv ℝ (potentialLimitSeries n) x) y

D.3. A series of integrals

We now show that the integral ∫ r, d_y η r * ‖r‖⁻¹ + η r * -⟪(‖r‖ ^ 3)⁻¹ • x, r⟫_ℝ is the limit of the integrals ∫ r, d_y (η r * potentialLimitSeries n r) as n → ∞.

Part D.3.I.

We first define a series of functions which are the integrands of ∫ r, d_y (η r * potentialLimitSeries n r). These functions are potentialLimitSeriesFDerivSchwartz y η n r.

def Electromagnetism.ThreeDimPointParticle.potentialLimitSeriesFDerivSchwartz (y : EuclideanSpace ℝ (Fin 3)) (η : SchwartzMap (EuclideanSpace ℝ (Fin 3)) ℝ) (n : ℕ) (x : EuclideanSpace ℝ (Fin 3)) : ℝ

A series of functions of the form fderiv ℝ (fun x => η x * potentialLimitSeries n x) x y.

Equations

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

theorem Electromagnetism.ThreeDimPointParticle.potentialLimitSeriesFDerivSchwartz_eq (y : EuclideanSpace ℝ (Fin 3)) (η : SchwartzMap (EuclideanSpace ℝ (Fin 3)) ℝ) (n : ℕ) (x : EuclideanSpace ℝ (Fin 3)) : potentialLimitSeriesFDerivSchwartz y η n x = (fderiv ℝ (⇑η) x) y * potentialLimitSeries n x + η x * (fderiv ℝ (potentialLimitSeries n) x) y

Part D.3.II.

We show that these integrands converge to the integrand of ∫ r, d_y η r * ‖r‖⁻¹ + η r * -⟪(‖r‖ ^ 3)⁻¹ • x, r⟫_ℝ as n → ∞.

theorem Electromagnetism.ThreeDimPointParticle.potentialLimitSeriesFDerivSchwartz_tendsto (y : EuclideanSpace ℝ (Fin 3)) (η : SchwartzMap (EuclideanSpace ℝ (Fin 3)) ℝ) : ∀ᵐ (a : EuclideanSpace ℝ (Fin 3)), Filter.Tendsto (fun (n : ℕ) => potentialLimitSeriesFDerivSchwartz y η n a) Filter.atTop (nhds ((fderiv ℝ (⇑η) a) y * ‖a‖⁻¹ + η a * -inner ℝ ((‖a‖ ^ 3)⁻¹ • a) y))

Part D.3.III.

We use 'Lebesgue dominated convergence theorem' to show that the integrals ∫ r, d_y (η r * potentialLimitSeries n r) converge to the integral ∫ r, d_y η r * ‖r‖⁻¹ + η r * -⟪(‖r‖ ^ 3)⁻¹ • x, r⟫_ℝ as n → ∞.

This requires some measurability properties of potentialLimitSeriesFDerivSchwartz and uses the integrability properties of potentialLimitSeries and its derivative shown above.

theorem Electromagnetism.ThreeDimPointParticle.potentialLimitSeriesFDerivSchwartz_aeStronglyMeasurable (y : EuclideanSpace ℝ (Fin 3)) (η : SchwartzMap (EuclideanSpace ℝ (Fin 3)) ℝ) (n : ℕ) : MeasureTheory.AEStronglyMeasurable (fun (x : EuclideanSpace ℝ (Fin 3)) => potentialLimitSeriesFDerivSchwartz y η n x) MeasureTheory.volume

theorem Electromagnetism.ThreeDimPointParticle.potentialLimitSeriesFDerivSchwartz_integral_tendsto_eq_integral (y : EuclideanSpace ℝ (Fin 3)) (η : SchwartzMap (EuclideanSpace ℝ (Fin 3)) ℝ) : Filter.Tendsto (fun (n : ℕ) => ∫ (x : EuclideanSpace ℝ (Fin 3)), potentialLimitSeriesFDerivSchwartz y η n x) Filter.atTop (nhds (∫ (x : EuclideanSpace ℝ (Fin 3)), (fderiv ℝ (⇑η) x) y * ‖x‖⁻¹ + η x * -inner ℝ ((‖x‖ ^ 3)⁻¹ • x) y))

D.4. The limit of the series of integrals is zero

Above we showed that the limit of the integrals ∫ r, d_y (η r * potentialLimitSeries n r) as n → ∞ is ∫ r, d_y η r * ‖r‖⁻¹ + η r * -⟪(‖r‖ ^ 3)⁻¹ • x, r⟫_ℝ. We now show that this same limit is zero.

Part D.4.I.

The integral ∫ r, d_y (η r * potentialLimitSeries n r) is zero for each n : ℕ. This follows because this integrand is the total derivative of a differentiable function.

theorem Electromagnetism.ThreeDimPointParticle.potentialLimitSeriesFDerivSchwartz_integral_eq_zero (y : EuclideanSpace ℝ (Fin 3)) (η : SchwartzMap (EuclideanSpace ℝ (Fin 3)) ℝ) (n : ℕ) : ∫ (x : EuclideanSpace ℝ (Fin 3)), potentialLimitSeriesFDerivSchwartz y η n x = 0

Part D.4.II.

From part D.4.I it follows that the limit of the integrals ∫ r, d_y (η r * potentialLimitSeries n r) as n → ∞ is zero, since each individual integral is zero.

theorem Electromagnetism.ThreeDimPointParticle.potentialLimitSeriesFDerivSchwartz_integral_tendsto_eq_zero (y : EuclideanSpace ℝ (Fin 3)) (η : SchwartzMap (EuclideanSpace ℝ (Fin 3)) ℝ) : Filter.Tendsto (fun (n : ℕ) => ∫ (x : EuclideanSpace ℝ (Fin 3)), potentialLimitSeriesFDerivSchwartz y η n x) Filter.atTop (nhds 0)

D.5. E = -∇ V for a particle at the origin

We now put everything together. In part D.1 we showed that E = -∇ V follows from the integral ∫ r, d_y η r * ‖r‖⁻¹ + η r * -⟪(‖r‖ ^ 3)⁻¹ • x, r⟫_ℝ = 0 for all Schwartz maps η and directions y. In part D.3 we showed that this integral is the limit of the integrals ∫ r, d_y (η r * potentialLimitSeries n r) as n → ∞. In part D.4 we showed that this limit is zero, and therefore this integral itself must be zero.

It follows that E = -∇ V for a particle at the origin.

theorem Electromagnetism.ThreeDimPointParticle.electricField_eq_neg_gradD_electricPotential_origin (q ε : ℝ) : electricField q ε 0 = -Space.gradD (electricPotential q ε 0)

D.6. E = -∇ V for a particle at r₀

The general case of a particle at r₀ follows from the case of a particle at the origin by using that the gradient commutes with translation.

theorem Electromagnetism.ThreeDimPointParticle.electricField_eq_neg_gradD_electricPotential (q ε : ℝ) (r₀ : EuclideanSpace ℝ (Fin 3)) : electricField q ε r₀ = -Space.gradD (electricPotential q ε r₀)

theorem Electromagnetism.ThreeDimPointParticle.electricField_eq_ofPotential_electricPotential (q ε : ℝ) (r₀ : EuclideanSpace ℝ (Fin 3)) : electricField q ε r₀ = StaticElectricField.ofPotential (electricPotential q ε r₀)

E. Faraday's law

Faraday's law, which says that ∇ × E = 0, is an immediate consequence of the fact that E = -∇ V, because the curl of a gradient is always zero.

theorem Electromagnetism.ThreeDimPointParticle.faradaysLaw (q ε : ℝ) (r₀ : Space) : (electricField q ε r₀).FaradaysLaw

F. Gauss' law

We now prove Gauss' law for a point particle in 3-dimensions. Recall that Gauss' law states that the divergence of the electric field is equal to the charge density divided by the permittivity, i.e. ∇ • E = ρ/ε.

In this case, this result is related to the sometimes confusing fact that ∇ • ((‖r‖⁻¹) ^ 3 • r) ∝ δ(r).

We first prove Gauss' law for a point particle at the origin, and then use translation to prove it for a point particle at r₀.

F.1. Gauss' law for a point particle at the origin

The proof of Gauss' law for a point particle at the origin follows the proof given here: https://math.stackexchange.com/questions/2409008/

We highlight the main steps of the proof here (the below comments also appear in-line within the proof) :

• Step 1: ∇ ⬝ E = 1/ε ρ if for all Schwartz mapsη, ∇ ⬝ E η = (1/ε ρ) η.
• Step 2: We focus on rewriting the LHS, by definition it is equal to - ∫ d³r ⟪(q/(4 * π * ε)) • ‖r‖⁻¹ ^ 3 • r, (∇ η) r⟫
• Step 3: We rearrange the integral to - q/(4 * π * ε) * ∫ d³r ‖r‖⁻¹ ^ 2 * ⟪‖r‖⁻¹ • r), (∇ η) r⟫
• Step 4: We use that ⟪‖r‖⁻¹ • r), (∇ η) r⟫ = (d(η (a • ‖r‖⁻¹ • r))/d a)_‖r‖ to rewrite the integral as - q/(4 * π * ε) * ∫ d³r ‖r‖⁻¹ ^ 2 * (d(η (a • ‖r‖⁻¹ • r))/d a)_‖r‖.
• Step 5: We move over to spherical coordinates rewriting d³r as r² dr dn where dn is the integral over the unit vectors n. In d³r the r is a vector whilst in r² dr dn the r is a scalar (the distance). - q/(4 * π * ε) * ∫ dr² dr dn r⁻¹ ^ 2 * (d(η (a • n))/d a)_r
• Step 6: The integral is rearanged to - q/(4 * π * ε) * ∫ dn (∫_0^∞ r² dr r⁻¹ ^ 2 * (d(η (a • n))/d a)_r)
• Step 7: The integral is further rearanged to - q/(4 * π * ε) * ∫ dn (∫_0^∞ dr (d(η (a • n))/d a)_r)
• Step 8: The inner integral (∫_0^∞ dr (d(η (a • n))/d a)_r) is an integral over a total derivative of a function which tends to zero at infinity, and so is equal to -η 0. Thus the integral is equal to - q/(4 * π * ε) * ∫ dn (-η 0).
• Step 9: The integral ∫ dn is equal to the surface area of the unit sphere, which is 4 * π. And thus we get after some simplification (q/ε) * η 0.
• Step 10: This is manifestly equal to the right hand side 1/ε ρ η since ρ = q δ(r), thereby proving the result.

theorem Electromagnetism.ThreeDimPointParticle.gaussLaw_origin (q ε : ℝ) : (electricField q ε 0).GaussLaw ε (chargeDistribution q 0)

Guass' law for a point particle in 3-dimensions at the origin, that is this theorem states that the divergence of (q/(4 * π * ε)) • ‖r‖⁻¹ ^ 3 • r is equal to q • δ(r).

F.2. Gauss' law for a point particle at r₀

We now show Gauss' law for a point particle at r₀. This follows from the case of a point particle at the origin by using that the divergence commutes with translation.

theorem Electromagnetism.ThreeDimPointParticle.gaussLaw (q ε : ℝ) (r₀ : EuclideanSpace ℝ (Fin 3)) : (electricField q ε r₀).GaussLaw ε (chargeDistribution q r₀)

G. Rotational invaraiance

We now prove the electric field, charge distribution and potential of a point particle are rotationally invariant.

This is yet to be done, and is a TODO item.

def Electromagnetism.ThreeDimPointParticle.electricField_rotationally_invariant : InformalLemma

The electrostatic field of a point particle is rotationally invariant.

Equations

• Electromagnetism.ThreeDimPointParticle.electricField_rotationally_invariant = { deps := [`Electromagnetism.ThreeDimPointParticle.electricField], tag := "L7NXF" }