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) => -...

The electric field of the electromagnetic potential created from the electric field E and the magnetic field B is E, as long as Gauss's law for magnetism and Faraday's law are satisfied. -/ lemma ofElectromagneticField_electricField {c : SpeedOfLight} (E : Time → Space 3 → EuclideanSpace ℝ (Fin 3)) (B : Time → Space 3 → EuclideanSpace ℝ (Fin 3)) (E_...

The electric field of the electromagnetic potential created from the electric field E and the magnetic field B is E, as long as Gauss's law for magnetism and Faraday's law are satisfied. -/ lemma ofElectromagneticField_electricField {c : SpeedOfLight} (E : Time → Space 3 → EuclideanSpace ℝ (Fin 3)) (B : Time → Space 3 → EuclideanSpace ℝ (Fin 3)) (E_...

The (inl 0, inr i) component of the field strength matrix of the bare-gradient potential B^μ := ∂_μ χ for χ(x) = x⁰·xⁱ equals 2. This witnesses that the bare covariant gradient does not produce a gauge-invariant field strength, so the raised-index contraction η^{μν} ∂_ν χ in ofGradient is necessary (see the module overview).

Index evaluation of the field strength tensor agrees with the corresponding component of the field strength matrix. -/ lemma toFieldStrength_eval_eq_fieldStrengthMatrix {d} (A : ElectromagneticPotential d) (x : SpaceTime d) (μ ν : Fin 1 ⊕ Fin d) : toField {A.toFieldStrength x | [μ] [ν]}ᵀ = A.fieldStrengthMatrix x (μ, ν) := by rw [toFieldStrength_eval_eq_b...

The magnetic field of the electromagnetic potential created from the electric field E and the magnetic field B is B, as long as Gauss's law is satisfied. -/ lemma ofElectromagneticField_magneticField {c : SpeedOfLight} (E : ElectricField) (B : MagneticField) (B_contDiff : ∀ t, ContDiff ℝ 1 (B t)) (B_grad : ∀ t, ∇ ⬝ (B t) = 0) : (ofElectromagneticFie...