Boosts on the electric and magnetic fields

i. Overview

We find the transformations of the electric and magnetic field matrix under boosts in the 'x' direction. We do this in full-generality for d+1 space dimensions.

ii. Key results

• electricField_apply_x_boost_zero : The transformation of the x-component of the electric field under a boost in the 'x' direction.
• electricField_apply_x_boost_succ : The transformation of the other components of the electric field under a boost in the 'x' direction.
• magneticFieldMatrix_apply_x_boost_zero_succ : The transformation of the 'x-components' of the magnetic field matrix under a boost in the 'x' direction
• magneticFieldMatrix_apply_x_boost_succ_succ : The transformation of the other components of the magnetic field matrix under a boost in the 'x' direction.

iii. Table of contents

• A. Boost of the electric field
  • A.1. Boost of the x-component of the electric field
  • A.2. Boost of other components of the electric field
• B. Boost of the magnetic field
  • B.1. Boost of the 'x-components' of the magnetic field matrix
  • B.2. Boost of the other components of the magnetic field matrix

iv. References

See e.g.

• https://en.wikipedia.org/wiki/Classical_electromagnetism_and_special_relativity

A. Boost of the electric field

A.1. Boost of the x-component of the electric field

theorem Electromagnetism.ElectromagneticPotential.electricField_apply_x_boost_zero {d : ℕ} {c : SpeedOfLight} (β : ℝ) (hβ : |β| < 1) (A : ElectromagneticPotential d.succ) (hA : Differentiable ℝ A) (t : Time) (x : Space d.succ) : have Λ := LorentzGroup.boost 0 β hβ; have t' := { val := LorentzGroup.γ β * (t.val + β / c.val * x 0) }; have x' := fun (x_1 : Fin d.succ) => match x_1 with | ⟨0, ⋯⟩ => LorentzGroup.γ β * (x 0 + c.val * β * t.val) | ⟨n.succ, ih⟩ => x ⟨n.succ, ih⟩; electricField c (fun (x : SpaceTime d.succ) => Λ • A (Λ⁻¹ • x)) t x 0 = electricField c A t' x' 0

A.2. Boost of other components of the electric field

theorem Electromagnetism.ElectromagneticPotential.electricField_apply_x_boost_succ {d : ℕ} {c : SpeedOfLight} (β : ℝ) (hβ : |β| < 1) (A : ElectromagneticPotential d.succ) (hA : Differentiable ℝ A) (t : Time) (x : Space d.succ) (i : Fin d) : have Λ := LorentzGroup.boost 0 β hβ; have t' := { val := LorentzGroup.γ β * (t.val + β / c.val * x 0) }; have x' := fun (x_1 : Fin d.succ) => match x_1 with | ⟨0, ⋯⟩ => LorentzGroup.γ β * (x 0 + c.val * β * t.val) | ⟨n.succ, ih⟩ => x ⟨n.succ, ih⟩; electricField c (fun (x : SpaceTime d.succ) => Λ • A (Λ⁻¹ • x)) t x i.succ = LorentzGroup.γ β * (electricField c A t' x' i.succ + c.val * β * magneticFieldMatrix c A t' x' (0, i.succ))

B. Boost of the magnetic field

B.1. Boost of the 'x-components' of the magnetic field matrix

theorem Electromagnetism.ElectromagneticPotential.magneticFieldMatrix_apply_x_boost_zero_succ {d : ℕ} {c : SpeedOfLight} (β : ℝ) (hβ : |β| < 1) (A : ElectromagneticPotential d.succ) (hA : Differentiable ℝ A) (t : Time) (x : Space d.succ) (i : Fin d) : have Λ := LorentzGroup.boost 0 β hβ; have t' := { val := LorentzGroup.γ β * (t.val + β / c.val * x 0) }; have x' := fun (x_1 : Fin d.succ) => match x_1 with | ⟨0, ⋯⟩ => LorentzGroup.γ β * (x 0 + c.val * β * t.val) | ⟨n.succ, ih⟩ => x ⟨n.succ, ih⟩; magneticFieldMatrix c (fun (x : SpaceTime d.succ) => Λ • A (Λ⁻¹ • x)) t x (0, i.succ) = LorentzGroup.γ β * (magneticFieldMatrix c A t' x' (0, i.succ) + β / c.val * electricField c A t' x' i.succ)

B.2. Boost of the other components of the magnetic field matrix

theorem Electromagnetism.ElectromagneticPotential.magneticFieldMatrix_apply_x_boost_succ_succ {d : ℕ} {c : SpeedOfLight} (β : ℝ) (hβ : |β| < 1) (A : ElectromagneticPotential d.succ) (hA : Differentiable ℝ A) (t : Time) (x : Space d.succ) (i j : Fin d) : have Λ := LorentzGroup.boost 0 β hβ; have t' := { val := LorentzGroup.γ β * (t.val + β / c.val * x 0) }; have x' := fun (x_1 : Fin d.succ) => match x_1 with | ⟨0, ⋯⟩ => LorentzGroup.γ β * (x 0 + c.val * β * t.val) | ⟨n.succ, ih⟩ => x ⟨n.succ, ih⟩; magneticFieldMatrix c (fun (x : SpaceTime d.succ) => Λ • A (Λ⁻¹ • x)) t x (i.succ, j.succ) = magneticFieldMatrix c A t' x' (i.succ, j.succ)