Finite collection of point particles in 3d

This module contains the electrostatics of a finite collection of point particles. Since Gauss' law and Faraday's law are linear, the electrostatic potential and electric field of a finite collection of point particles is just the sum of the potentials and fields of the individual particles.

def Electromagnetism.ThreeDimDiscreteCollection.chargeDistribution {n : ℕ} (q : Fin n → ℝ) (r₀ : Fin n → Space) : ChargeDistribution

The charge distribution for a finite collection of point particles.

Equations

• Electromagnetism.ThreeDimDiscreteCollection.chargeDistribution q r₀ = ∑ i : Fin n, q i • Distribution.diracDelta ℝ (r₀ i)

def Electromagnetism.ThreeDimDiscreteCollection.electricPotential {n : ℕ} (q : Fin n → ℝ) (ε : ℝ) (r₀ : Fin n → Space) : StaticElectricPotential

The electrostatic potential of a finite collection of point particles.

Equations

• Electromagnetism.ThreeDimDiscreteCollection.electricPotential q ε r₀ = ∑ i : Fin n, Electromagnetism.ThreeDimPointParticle.electricPotential (q i) ε (r₀ i)

def Electromagnetism.ThreeDimDiscreteCollection.electricField {n : ℕ} (q : Fin n → ℝ) (ε : ℝ) (r₀ : Fin n → Space) : StaticElectricField

The electric field of a finite collection of point particles.

Equations

• Electromagnetism.ThreeDimDiscreteCollection.electricField q ε r₀ = ∑ i : Fin n, Electromagnetism.ThreeDimPointParticle.electricField (q i) ε (r₀ i)

theorem Electromagnetism.ThreeDimDiscreteCollection.electricField_eq_neg_gradD_electricPotential {n : ℕ} (q : Fin n → ℝ) (ε : ℝ) (r₀ : Fin n → Space) : electricField q ε r₀ = -Space.gradD (electricPotential q ε r₀)

theorem Electromagnetism.ThreeDimDiscreteCollection.electricField_eq_ofPotential_electricPotential {n : ℕ} (q : Fin n → ℝ) (ε : ℝ) (r₀ : Fin n → Space) : electricField q ε r₀ = StaticElectricField.ofPotential (electricPotential q ε r₀)

theorem Electromagnetism.ThreeDimDiscreteCollection.gaussLaw {n : ℕ} (q : Fin n → ℝ) (ε : ℝ) (r₀ : Fin n → Space) : (electricField q ε r₀).GaussLaw ε (chargeDistribution q r₀)

Gauss's law for a finite collection of point particles.

theorem Electromagnetism.ThreeDimDiscreteCollection.faradaysLaw {n : ℕ} (q : Fin n → ℝ) (ε : ℝ) (r₀ : Fin n → Space) : (electricField q ε r₀).FaradaysLaw

Faraday's law for a finite collection of point particles.