therefore
Sign up
Open navigation

Source-pinned research

Research proof index

Search theorem names, mathematical ideas, modules, topics, projects, and role-labelled researchers. Open a result for its complete indexed Lean declaration and source record.

This index contains 591 research declarations. Search 10,000 more complete Mathlib declarations.

All topics

591 results

Clear filters
Project-declaredLean 4.32.0

Magnetic Field Matrix basis repr eq field Strength

Electromagnetism.DistElectromagneticPotential.magneticFieldMatrix_basis_repr_eq_fieldStrength

Project documentation

The magnetic field matrix of an electromagnetic potential which is a distribution. -/ noncomputable def magneticFieldMatrix {d} (c : SpeedOfLight) : DistElectromagneticPotential d →ₗ[ℝ] (Time × Space d) →d[ℝ] (EuclideanSpace ℝ (Fin d) ⊗[ℝ] EuclideanSpace ℝ (Fin d)) where toFun A := ⟨TensorProduct.map (Lorentz.Vector.spatialCLM d).toLinearMap (Lorentz.Vect...

physicsquantum field theoryrelativity

Source project: Physlib

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Magnetic Field Matrix eq vector Potential

Electromagnetism.DistElectromagneticPotential.magneticFieldMatrix_eq_vectorPotential

Project documentation

The magnetic field matrix of an electromagnetic potential which is a distribution. -/ noncomputable def magneticFieldMatrix {d} (c : SpeedOfLight) : DistElectromagneticPotential d →ₗ[ℝ] (Time × Space d) →d[ℝ] (EuclideanSpace ℝ (Fin d) ⊗[ℝ] EuclideanSpace ℝ (Fin d)) where toFun A := ⟨TensorProduct.map (Lorentz.Vector.spatialCLM d).toLinearMap (Lorentz.Vect...

physicsquantum field theoryrelativity

Source project: Physlib

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

One Dim Point Particle div electric Field

Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_div_electricField

Project documentation

The electromagnetic potential of a point particle stationary at r₀ of 1d space. -/ noncomputable def oneDimPointParticle (𝓕 : FreeSpace) (q : ℝ) (r₀ : Space 1) : DistElectromagneticPotential 1 := (SpaceTime.distTimeSlice 𝓕.c).symm <| Space.constantTime <| distOfFunction (fun x => ((- (q * 𝓕.μ₀ * 𝓕.c)/ 2) * ‖x - r₀‖) • Lorentz.Vector.basis (Sum.inl 0...

physicsquantum field theoryrelativity

Source project: Physlib

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

One Dim Point Particle electric Field

Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_electricField

Project documentation

The electromagnetic potential of a point particle stationary at r₀ of 1d space. -/ noncomputable def oneDimPointParticle (𝓕 : FreeSpace) (q : ℝ) (r₀ : Space 1) : DistElectromagneticPotential 1 := (SpaceTime.distTimeSlice 𝓕.c).symm <| Space.constantTime <| distOfFunction (fun x => ((- (q * 𝓕.μ₀ * 𝓕.c)/ 2) * ‖x - r₀‖) • Lorentz.Vector.basis (Sum.inl 0...

physicsquantum field theoryrelativity

Source project: Physlib

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

One Dim Point Particle scalar Potential

Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_scalarPotential

Project documentation

The electromagnetic potential of a point particle stationary at r₀ of 1d space. -/ noncomputable def oneDimPointParticle (𝓕 : FreeSpace) (q : ℝ) (r₀ : Space 1) : DistElectromagneticPotential 1 := (SpaceTime.distTimeSlice 𝓕.c).symm <| Space.constantTime <| distOfFunction (fun x => ((- (q * 𝓕.μ₀ * 𝓕.c)/ 2) * ‖x - r₀‖) • Lorentz.Vector.basis (Sum.inl 0...

physicsquantum field theoryrelativity

Source project: Physlib

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Three Dim Point Particle div electric Field

Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_div_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