therefore

Project-declaredLean 4.32.0

Three Dim Point Particle electric Field

Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_electricField

Project documentation

The electromagnetic potential of a point particle stationary at r₀ of 3d space. -/ noncomputable def threeDimPointParticle (𝓕 : FreeSpace) (q : ℝ) (r₀ : Space 3) : DistElectromagneticPotential 3 := (SpaceTime.distTimeSlice 𝓕.c).symm <| Space.constantTime <| distOfFunction (fun x => (((q * 𝓕.μ₀ * 𝓕.c)/ (4 * π)) * ‖x - r₀‖⁻¹) • Lorentz.Vector.basis (S...

physicsquantum field theoryrelativity

Source project: Physlib

Person-level attribution pending.

View proof record

Project-declaredLean 4.32.0

Three Dim Point Particle scalar Potential

Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_scalarPotential

Project documentation

The electromagnetic potential of a point particle stationary at r₀ of 3d space. -/ noncomputable def threeDimPointParticle (𝓕 : FreeSpace) (q : ℝ) (r₀ : Space 3) : DistElectromagneticPotential 3 := (SpaceTime.distTimeSlice 𝓕.c).symm <| Space.constantTime <| distOfFunction (fun x => (((q * 𝓕.μ₀ * 𝓕.c)/ (4 * π)) * ‖x - r₀‖⁻¹) • Lorentz.Vector.basis (S...

physicsquantum field theoryrelativity

Source project: Physlib

Person-level attribution pending.

View proof record

Project-declaredLean 4.32.0

Three Dim Point Particle Current Density charge Density

Electromagnetism.DistElectromagneticPotential.threeDimPointParticleCurrentDensity_chargeDensity

Project documentation

The current density of a point particle stationary at a point r₀ of 3d space. -/ noncomputable def threeDimPointParticleCurrentDensity (c : SpeedOfLight) (q : ℝ) (r₀ : Space 3) : DistLorentzCurrentDensity 3 := (SpaceTime.distTimeSlice c).symm <| constantTime ((c * q) • diracDelta' ℝ r₀ (Lorentz.Vector.basis (Sum.inl 0))) lemma threeDimPointParticleCurre...

physicsquantum field theoryrelativity

Source project: Physlib

Person-level attribution pending.

View proof record

Project-declaredLean 4.32.0

Canonical Momentum eq

Electromagnetism.ElectromagneticPotential.canonicalMomentum_eq

Project documentation

The canonical momentum associated with the lagrangian of an electromagnetic potential and a Lorentz current density. -/ noncomputable def canonicalMomentum (𝓕 : FreeSpace) (A : ElectromagneticPotential d) (J : LorentzCurrentDensity d) : SpaceTime d → Lorentz.Vector d := fun x => gradient (fun (v : Lorentz.Vector d) => lagrangian 𝓕 ⟨fun x => A x + x (Sum...

physicsquantum field theoryrelativity

Source project: Physlib

Person-level attribution pending.

View proof record

Project-declaredLean 4.32.0

Canonical Momentum eq electric Field

Electromagnetism.ElectromagneticPotential.canonicalMomentum_eq_electricField

Project documentation

The canonical momentum associated with the lagrangian of an electromagnetic potential and a Lorentz current density. -/ noncomputable def canonicalMomentum (𝓕 : FreeSpace) (A : ElectromagneticPotential d) (J : LorentzCurrentDensity d) : SpaceTime d → Lorentz.Vector d := fun x => gradient (fun (v : Lorentz.Vector d) => lagrangian 𝓕 ⟨fun x => A x + x (Sum...

physicsquantum field theoryrelativity

Source project: Physlib

Person-level attribution pending.

View proof record

Project-declaredLean 4.32.0

Canonical Momentum eq gradient kinetic Term

Electromagnetism.ElectromagneticPotential.canonicalMomentum_eq_gradient_kineticTerm

Project documentation

The canonical momentum associated with the lagrangian of an electromagnetic potential and a Lorentz current density. -/ noncomputable def canonicalMomentum (𝓕 : FreeSpace) (A : ElectromagneticPotential d) (J : LorentzCurrentDensity d) : SpaceTime d → Lorentz.Vector d := fun x => gradient (fun (v : Lorentz.Vector d) => lagrangian 𝓕 ⟨fun x => A x + x (Sum...

physicsquantum field theoryrelativity

Source project: Physlib

Person-level attribution pending.

View proof record