The magnetic field around a infinite wire

i. Overview

In this module we verify the electromagnetic properties of an infinite wire carrying a steady current along the x-axis.

ii. Key results

• wireCurrentDensity : The current density associated with an infinite wire carrying a current I along the x-axis.
• infiniteWire : The electromagnetic potential associated with an infinite wire carrying a current I along the x-axis.
• infiniteWire_isExterma : The electromagnetic potential of an infinite wire carrying a current I along the x-axis satisfies Maxwell's equations.

iii. Table of contents

• A. The current density
• B. The electromagnetic potential
  • B.1. The scalar potential
  • B.2. The vector potential
• C. The electric field
• D. Maxwell's equations

iv. References

A. The current density

The 4-current density of an infinite wire carrying a current I along the x-axis is given by

$$J(t, x, y, z) = (0, I δ((y, z)), 0, 0).$$

noncomputable def Electromagnetism.DistElectromagneticPotential.wireCurrentDensity (c : SpeedOfLight) : ℝ →ₗ[ℝ] DistLorentzCurrentDensity

The current density associated with an infinite wire carrying a current I along the x-axis.

Equations

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

@[simp]

theorem Electromagnetism.DistElectromagneticPotential.wireCurrentDensity_chargeDesnity (c : SpeedOfLight) (I : ℝ) : (DistLorentzCurrentDensity.chargeDensity c) ((wireCurrentDensity c) I) = 0

theorem Electromagnetism.DistElectromagneticPotential.wireCurrentDensity_currentDensity_fst (c : SpeedOfLight) (I : ℝ) (η : SchwartzMap (Time × Space) ℝ) : (((DistLorentzCurrentDensity.currentDensity c) ((wireCurrentDensity c) I)) η).ofLp 0 = (Space.constantTime ((Space.constantSliceDist 0) (I • Distribution.diracDelta ℝ 0))) η

@[simp]

theorem Electromagnetism.DistElectromagneticPotential.wireCurrentDensity_currentDensity_snd (c : SpeedOfLight) (I : ℝ) (ε : SchwartzMap (Time × Space) ℝ) : (((DistLorentzCurrentDensity.currentDensity c) ((wireCurrentDensity c) I)) ε).ofLp 1 = 0

@[simp]

theorem Electromagnetism.DistElectromagneticPotential.wireCurrentDensity_currentDensity_thrd (c : SpeedOfLight) (I : ℝ) (ε : SchwartzMap (Time × Space) ℝ) : (((DistLorentzCurrentDensity.currentDensity c) ((wireCurrentDensity c) I)) ε).ofLp 2 = 0

B. The electromagnetic potential

The electromagnetic potential of an infinite wire carrying a current I along the x-axis is given by

$$A(t, x, y, z) = \left(0, -\frac{μ_0 I}{2\pi} \log (\sqrt{y^2 + z^2}), 0, 0\right).$$

noncomputable def Electromagnetism.DistElectromagneticPotential.infiniteWire (𝓕 : FreeSpace) (I : ℝ) : DistElectromagneticPotential

The electromagnetic potential of an infinite wire along the x-axis carrying a current I.

Equations

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

B.1. The scalar potential

THe scalar potential of an infinite wire carrying a current I along the x-axis is zero:

$$V(t, x, y, z) = 0.$$

@[simp]

theorem Electromagnetism.DistElectromagneticPotential.infiniteWire_scalarPotential (𝓕 : FreeSpace) (I : ℝ) : (scalarPotential 𝓕.c) (infiniteWire 𝓕 I) = 0

B.2. The vector potential

The vector potential of an infinite wire carrying a current I along the x-axis is given by $$\vec A(t, x, y, z) = \left(-\frac{μ_0 I}{2\pi} \log (\sqrt{y^2 + z^2}), 0, 0\right).$$

The time derivative $\partial_t \vec A$ is zero, as expected for a steady current, and the spatial derivative $\partial_x \vec A$ is also zero, as expected for a system with translational symmetry along the x-axis.

theorem Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential (𝓕 : FreeSpace) (I : ℝ) : (vectorPotential 𝓕.c) (infiniteWire 𝓕 I) = Space.constantTime ((Space.constantSliceDist 0) ((-I * 𝓕.μ₀ / (2 * Real.pi)) • Space.distOfFunction (fun (x : Space 2) => Real.log ‖x‖ • EuclideanSpace.single 0 1) ⋯))

theorem Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential_fst (𝓕 : FreeSpace) (I : ℝ) (η : SchwartzMap (Time × Space) ℝ) : (((vectorPotential 𝓕.c) (infiniteWire 𝓕 I)) η).ofLp 0 = (Space.constantTime ((Space.constantSliceDist 0) ((-I * 𝓕.μ₀ / (2 * Real.pi)) • Space.distOfFunction (fun (x : Space 2) => Real.log ‖x‖) ⋯))) η

@[simp]

theorem Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential_snd {η : SchwartzMap (Time × Space) ℝ} (𝓕 : FreeSpace) (I : ℝ) : (((vectorPotential 𝓕.c) (infiniteWire 𝓕 I)) η).ofLp 1 = 0

@[simp]

theorem Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential_thrd {η : SchwartzMap (Time × Space) ℝ} (𝓕 : FreeSpace) (I : ℝ) : (((vectorPotential 𝓕.c) (infiniteWire 𝓕 I)) η).ofLp 2 = 0

@[simp]

theorem Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential_distTimeDeriv (𝓕 : FreeSpace) (I : ℝ) : Space.distTimeDeriv ((vectorPotential 𝓕.c) (infiniteWire 𝓕 I)) = 0

@[simp]

theorem Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential_distSpaceDeriv_0 (𝓕 : FreeSpace) (I : ℝ) : (Space.distSpaceDeriv 0) ((vectorPotential 𝓕.c) (infiniteWire 𝓕 I)) = 0

C. The electric field

The electric field of an infinite wire carrying a current I along the x-axis is zero: $$\vec E(t, x, y, z) = 0.$$

@[simp]

theorem Electromagnetism.DistElectromagneticPotential.infiniteWire_electricField (𝓕 : FreeSpace) (I : ℝ) : (electricField 𝓕.c) (infiniteWire 𝓕 I) = 0

D. Maxwell's equations

theorem Electromagnetism.DistElectromagneticPotential.infiniteWire_isExterma {𝓕 : FreeSpace} {I : ℝ} : IsExtrema 𝓕 (infiniteWire 𝓕 I) ((wireCurrentDensity 𝓕.c) I)