Research proof index

The electromagnetic potential from an electric and a magnetic field. This defines the electromagnetic potential in the Poincare gauge. -/ noncomputable def ofElectromagneticField (c : SpeedOfLight) (E : Time → Space 3 → EuclideanSpace ℝ (Fin 3)) (B : Time → Space 3 → EuclideanSpace ℝ (Fin 3)) : ElectromagneticPotential 3 := let A := fun t (x : Space) => -...

Evaluation of the tensor components of ∂_ μ A x ν.

The matrix corresponding to the magnetic field in general dimensions. In 3 space-dimensions this reduces to a vector. -/ noncomputable def magneticFieldMatrix (c : SpeedOfLight := 1) (A : ElectromagneticPotential d) : Time → Space d → (Fin d × Fin d) → ℝ := timeSlice c <| fun x ij => A.fieldStrengthMatrix x (Sum.inr ij.1, Sum.inr ij.2) lemma magneticFie...

The condition on an electromagnetic potential to be an extrema of the lagrangian. -/ def IsExtrema {d} (𝓕 : FreeSpace) (A : ElectromagneticPotential d) (J : LorentzCurrentDensity d) : Prop := gradLagrangian 𝓕 A J = 0 lemma isExtrema_iff_gradLagrangian {𝓕 : FreeSpace} (A : ElectromagneticPotential d) (J : LorentzCurrentDensity d) : IsExtrema 𝓕 A J ↔ A....

The condition on an electromagnetic potential to be an extrema of the lagrangian. -/ def IsExtrema {d} (𝓕 : FreeSpace) (A : ElectromagneticPotential d) (J : LorentzCurrentDensity d) : Prop := gradLagrangian 𝓕 A J = 0 lemma isExtrema_iff_gradLagrangian {𝓕 : FreeSpace} (A : ElectromagneticPotential d) (J : LorentzCurrentDensity d) : IsExtrema 𝓕 A J ↔ A....

This lemma expresses the component form of the transformed field strength tensor: when a Lorentz transformation Λ acts on the potential A, the resulting field strength tensor's components are given by the standard tensor transformation rule involving the Lorentz matrix elements Λ^μ_κ and Λ^ν_ρ applied to the original field components.