Imports
/-
Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
module
public import Physlib.Electromagnetism.Kinematics.MagneticField
public import Physlib.SpaceAndTime.SpaceTime.BoostsBoosts 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
@[expose] public sectionA. Boost of the electric field
A.1. Boost of the x-component of the electric field
d:ℕc:SpeedOfLightβ:ℝhβ:|β| < 1A:ElectromagneticPotential d.succhA:Differentiable ℝ A.valt:Timex:Space d.succ⊢ (A.fieldStrengthMatrix
((SpaceTime.toTimeAndSpace c).symm
({ val := γ β * (t.val + β / c.val * x.val 0) },
{
val := fun x_1 =>
match x_1 with
| ⟨0, ⋯⟩ => γ β * (x.val 0 + c.val * β * t.val)
| ⟨n.succ, ih⟩ => x.val ⟨n.succ, ih⟩ })))
(Sum.inl 0, Sum.inr 0) =
(A.fieldStrengthMatrix
((SpaceTime.toTimeAndSpace c).symm
({ val := γ β * (t.val * c.val + β * x.val 0) / c.val },
{
val := fun x_1 =>
match x_1 with
| ⟨0, ⋯⟩ => γ β * (x.val 0 + β * t.val * c.val)
| ⟨n.succ, ih⟩ => x.val ⟨n + 1, ih⟩ })))
(Sum.inl 0, Sum.inr 0)d:ℕc:SpeedOfLightβ:ℝhβ:|β| < 1A:ElectromagneticPotential d.succhA:Differentiable ℝ A.valt:Timex:Space d.succ⊢ Differentiable ℝ (boost 0 β hβ • A).val
d:ℕc:SpeedOfLightβ:ℝhβ:|β| < 1A:ElectromagneticPotential d.succhA:Differentiable ℝ A.valt:Timex:Space d.succ⊢ (A.fieldStrengthMatrix
((SpaceTime.toTimeAndSpace c).symm
({ val := γ β * (t.val * c.val + β * x.val 0) / c.val },
{
val := fun x_1 =>
match x_1 with
| ⟨0, ⋯⟩ => γ β * (x.val 0 + t.val * β * c.val)
| ⟨n.succ, ih⟩ => x.val ⟨n.succ, ih⟩ })))
(Sum.inl 0, Sum.inr 0) =
(A.fieldStrengthMatrix
((SpaceTime.toTimeAndSpace c).symm
({ val := γ β * (t.val * c.val + β * x.val 0) / c.val },
{
val := fun x_1 =>
match x_1 with
| ⟨0, ⋯⟩ => γ β * (x.val 0 + t.val * β * c.val)
| ⟨n.succ, ih⟩ => x.val ⟨n + 1, ih⟩ })))
(Sum.inl 0, Sum.inr 0)d:ℕc:SpeedOfLightβ:ℝhβ:|β| < 1A:ElectromagneticPotential d.succhA:Differentiable ℝ A.valt:Timex:Space d.succ⊢ Differentiable ℝ (boost 0 β hβ • A).val
d:ℕc:SpeedOfLightβ:ℝhβ:|β| < 1A:ElectromagneticPotential d.succhA:Differentiable ℝ A.valt:Timex:Space d.succ⊢ Differentiable ℝ (boost 0 β hβ • A).val
d:ℕc:SpeedOfLightβ:ℝhβ:|β| < 1A:ElectromagneticPotential d.succhA:Differentiable ℝ A.valt:Timex:Space d.succ⊢ Differentiable ℝ (boost 0 β hβ • A).val All goals completed! 🐙A.2. Boost of other components of the electric field
d:ℕc:SpeedOfLightβ:ℝhβ:|β| < 1A:ElectromagneticPotential d.succhA:Differentiable ℝ A.valt:Timex:Space d.succi:Fin d⊢ -(c.val *
(γ β *
(-(1 / c.val) *
(electricField c A
((SpaceTime.time c)
((SpaceTime.toTimeAndSpace c).symm
({ val := γ β * (t.val + β / c.val * x.val 0) },
{
val := fun x_1 =>
match x_1 with
| ⟨0, ⋯⟩ => γ β * (x.val 0 + c.val * β * t.val)
| ⟨n.succ, ih⟩ => x.val ⟨n.succ, ih⟩ })))
(SpaceTime.space
((SpaceTime.toTimeAndSpace c).symm
({ val := γ β * (t.val + β / c.val * x.val 0) },
{
val := fun x_1 =>
match x_1 with
| ⟨0, ⋯⟩ => γ β * (x.val 0 + c.val * β * t.val)
| ⟨n.succ, ih⟩ => x.val ⟨n.succ, ih⟩ })))).ofLp
i.succ) +
-(γ β * β *
magneticFieldMatrix c A
((SpaceTime.time c)
((SpaceTime.toTimeAndSpace c).symm
({ val := γ β * (t.val + β / c.val * x.val 0) },
{
val := fun x_1 =>
match x_1 with
| ⟨0, ⋯⟩ => γ β * (x.val 0 + c.val * β * t.val)
| ⟨n.succ, ih⟩ => x.val ⟨n.succ, ih⟩ })))
(SpaceTime.space
((SpaceTime.toTimeAndSpace c).symm
({ val := γ β * (t.val + β / c.val * x.val 0) },
{
val := fun x_1 =>
match x_1 with
| ⟨0, ⋯⟩ => γ β * (x.val 0 + c.val * β * t.val)
| ⟨n.succ, ih⟩ => x.val ⟨n.succ, ih⟩ })))
(0, i.succ)))) =
γ β *
((electricField c A { val := γ β * (t.val + β / c.val * x.val 0) }
{
val := fun x_1 =>
match x_1 with
| ⟨0, ⋯⟩ => γ β * (x.val 0 + c.val * β * t.val)
| ⟨n.succ, ih⟩ => x.val ⟨n + 1, ih⟩ }).ofLp
i.succ +
c.val * β *
magneticFieldMatrix c A { val := γ β * (t.val + β / c.val * x.val 0) }
{
val := fun x_1 =>
match x_1 with
| ⟨0, ⋯⟩ => γ β * (x.val 0 + c.val * β * t.val)
| ⟨n.succ, ih⟩ => x.val ⟨n + 1, ih⟩ }
(0, i.succ))d:ℕc:SpeedOfLightβ:ℝhβ:|β| < 1A:ElectromagneticPotential d.succhA:Differentiable ℝ A.valt:Timex:Space d.succi:Fin d⊢ Differentiable ℝ (boost 0 β hβ • A).val
d:ℕc:SpeedOfLightβ:ℝhβ:|β| < 1A:ElectromagneticPotential d.succhA:Differentiable ℝ A.valt:Timex:Space d.succi:Fin d⊢ -(c.val *
(-(γ β *
(c.val⁻¹ *
(electricField c A { val := γ β * (t.val + β / c.val * x.val 0) }
{
val := fun x_1 =>
match x_1 with
| ⟨0, ⋯⟩ => γ β * (x.val 0 + c.val * β * t.val)
| ⟨n.succ, ih⟩ => x.val ⟨n + 1, ih⟩ }).ofLp
i.succ)) +
-(γ β * β *
magneticFieldMatrix c A { val := γ β * (t.val + β / c.val * x.val 0) }
{
val := fun x_1 =>
match x_1 with
| ⟨0, ⋯⟩ => γ β * (x.val 0 + c.val * β * t.val)
| ⟨n.succ, ih⟩ => x.val ⟨n + 1, ih⟩ }
(0, i.succ)))) =
γ β *
((electricField c A { val := γ β * (t.val + β / c.val * x.val 0) }
{
val := fun x_1 =>
match x_1 with
| ⟨0, ⋯⟩ => γ β * (x.val 0 + c.val * β * t.val)
| ⟨n.succ, ih⟩ => x.val ⟨n + 1, ih⟩ }).ofLp
i.succ +
c.val * β *
magneticFieldMatrix c A { val := γ β * (t.val + β / c.val * x.val 0) }
{
val := fun x_1 =>
match x_1 with
| ⟨0, ⋯⟩ => γ β * (x.val 0 + c.val * β * t.val)
| ⟨n.succ, ih⟩ => x.val ⟨n + 1, ih⟩ }
(0, i.succ))d:ℕc:SpeedOfLightβ:ℝhβ:|β| < 1A:ElectromagneticPotential d.succhA:Differentiable ℝ A.valt:Timex:Space d.succi:Fin d⊢ Differentiable ℝ (boost 0 β hβ • A).val
d:ℕc:SpeedOfLightβ:ℝhβ:|β| < 1A:ElectromagneticPotential d.succhA:Differentiable ℝ A.valt:Timex:Space d.succi:Fin d⊢ -(γ β *
(-(electricField c A { val := γ β * (c.val * t.val + β * x.val 0) / c.val }
{
val := fun x_1 =>
match x_1 with
| ⟨0, ⋯⟩ => γ β * (x.val 0 + c.val * t.val * β)
| ⟨n.succ, ih⟩ => x.val ⟨n + 1, ih⟩ }).ofLp
i.succ +
-(c.val * β *
magneticFieldMatrix c A { val := γ β * (c.val * t.val + β * x.val 0) / c.val }
{
val := fun x_1 =>
match x_1 with
| ⟨0, ⋯⟩ => γ β * (x.val 0 + c.val * t.val * β)
| ⟨n.succ, ih⟩ => x.val ⟨n + 1, ih⟩ }
(0, i.succ)))) =
γ β *
((electricField c A { val := γ β * (c.val * t.val + β * x.val 0) / c.val }
{
val := fun x_1 =>
match x_1 with
| ⟨0, ⋯⟩ => γ β * (x.val 0 + c.val * t.val * β)
| ⟨n.succ, ih⟩ => x.val ⟨n + 1, ih⟩ }).ofLp
i.succ +
c.val * β *
magneticFieldMatrix c A { val := γ β * (c.val * t.val + β * x.val 0) / c.val }
{
val := fun x_1 =>
match x_1 with
| ⟨0, ⋯⟩ => γ β * (x.val 0 + c.val * t.val * β)
| ⟨n.succ, ih⟩ => x.val ⟨n + 1, ih⟩ }
(0, i.succ))d:ℕc:SpeedOfLightβ:ℝhβ:|β| < 1A:ElectromagneticPotential d.succhA:Differentiable ℝ A.valt:Timex:Space d.succi:Fin d⊢ Differentiable ℝ (boost 0 β hβ • A).val
d:ℕc:SpeedOfLightβ:ℝhβ:|β| < 1A:ElectromagneticPotential d.succhA:Differentiable ℝ A.valt:Timex:Space d.succi:Fin d⊢ γ β * c.val * β *
magneticFieldMatrix c A { val := γ β * c.val * t.val * c.val⁻¹ + γ β * β * x.val 0 * c.val⁻¹ }
{
val := fun x_1 =>
match x_1 with
| ⟨0, ⋯⟩ => γ β * c.val * t.val * β + γ β * x.val 0
| ⟨n.succ, ih⟩ => x.val ⟨1 + n, ⋯⟩ }
(0, i.succ) +
γ β *
(electricField c A { val := γ β * c.val * t.val * c.val⁻¹ + γ β * β * x.val 0 * c.val⁻¹ }
{
val := fun x_1 =>
match x_1 with
| ⟨0, ⋯⟩ => γ β * c.val * t.val * β + γ β * x.val 0
| ⟨n.succ, ih⟩ => x.val ⟨1 + n, ⋯⟩ }).ofLp
i.succ =
γ β * c.val * β *
magneticFieldMatrix c A { val := γ β * c.val * t.val * c.val⁻¹ + γ β * β * x.val 0 * c.val⁻¹ }
{
val := fun x_1 =>
match x_1 with
| ⟨0, ⋯⟩ => γ β * c.val * t.val * β + γ β * x.val 0
| ⟨n.succ, ih⟩ => x.val ⟨1 + n, ⋯⟩ }
(0, i.succ) +
γ β *
(electricField c A { val := γ β * c.val * t.val * c.val⁻¹ + γ β * β * x.val 0 * c.val⁻¹ }
{
val := fun x_1 =>
match x_1 with
| ⟨0, ⋯⟩ => γ β * c.val * t.val * β + γ β * x.val 0
| ⟨n.succ, ih⟩ => x.val ⟨1 + n, ⋯⟩ }).ofLp
i.succd:ℕc:SpeedOfLightβ:ℝhβ:|β| < 1A:ElectromagneticPotential d.succhA:Differentiable ℝ A.valt:Timex:Space d.succi:Fin d⊢ Differentiable ℝ (boost 0 β hβ • A).val
d:ℕc:SpeedOfLightβ:ℝhβ:|β| < 1A:ElectromagneticPotential d.succhA:Differentiable ℝ A.valt:Timex:Space d.succi:Fin d⊢ Differentiable ℝ (boost 0 β hβ • A).val
d:ℕc:SpeedOfLightβ:ℝhβ:|β| < 1A:ElectromagneticPotential d.succhA:Differentiable ℝ A.valt:Timex:Space d.succi:Fin d⊢ Differentiable ℝ (boost 0 β hβ • A).val All goals completed! 🐙B. Boost of the magnetic field
B.1. Boost of the 'x-components' of the magnetic field matrix
d:ℕc:SpeedOfLightβ:ℝhβ:|β| < 1A:ElectromagneticPotential d.succhA:Differentiable ℝ A.valt:Timex:Space d.succi:Fin d⊢ -(γ β * β *
(-(1 / c.val) *
(electricField c A
((SpaceTime.time c)
((SpaceTime.toTimeAndSpace c).symm
({ val := γ β * (t.val + β / c.val * x.val 0) },
{
val := fun x_1 =>
match x_1 with
| ⟨0, ⋯⟩ => γ β * (x.val 0 + c.val * β * t.val)
| ⟨n.succ, ih⟩ => x.val ⟨n.succ, ih⟩ })))
(SpaceTime.space
((SpaceTime.toTimeAndSpace c).symm
({ val := γ β * (t.val + β / c.val * x.val 0) },
{
val := fun x_1 =>
match x_1 with
| ⟨0, ⋯⟩ => γ β * (x.val 0 + c.val * β * t.val)
| ⟨n.succ, ih⟩ => x.val ⟨n.succ, ih⟩ })))).ofLp
i.succ)) +
γ β *
magneticFieldMatrix c A
((SpaceTime.time c)
((SpaceTime.toTimeAndSpace c).symm
({ val := γ β * (t.val + β / c.val * x.val 0) },
{
val := fun x_1 =>
match x_1 with
| ⟨0, ⋯⟩ => γ β * (x.val 0 + c.val * β * t.val)
| ⟨n.succ, ih⟩ => x.val ⟨n.succ, ih⟩ })))
(SpaceTime.space
((SpaceTime.toTimeAndSpace c).symm
({ val := γ β * (t.val + β / c.val * x.val 0) },
{
val := fun x_1 =>
match x_1 with
| ⟨0, ⋯⟩ => γ β * (x.val 0 + c.val * β * t.val)
| ⟨n.succ, ih⟩ => x.val ⟨n.succ, ih⟩ })))
(0, i.succ) =
γ β *
((A.fieldStrengthMatrix
((SpaceTime.toTimeAndSpace c).symm
({ val := γ β * (t.val + β / c.val * x.val 0) },
{
val := fun x_1 =>
match x_1 with
| ⟨0, ⋯⟩ => γ β * (x.val 0 + c.val * β * t.val)
| ⟨n.succ, ih⟩ => x.val ⟨n + 1, ih⟩ })))
(Sum.inr 0, Sum.inr i.succ) +
β / c.val *
(electricField c A { val := γ β * (t.val + β / c.val * x.val 0) }
{
val := fun x_1 =>
match x_1 with
| ⟨0, ⋯⟩ => γ β * (x.val 0 + c.val * β * t.val)
| ⟨n.succ, ih⟩ => x.val ⟨n + 1, ih⟩ }).ofLp
i.succ)
d:ℕc:SpeedOfLightβ:ℝhβ:|β| < 1A:ElectromagneticPotential d.succhA:Differentiable ℝ A.valt:Timex:Space d.succi:Fin d⊢ γ β * β *
(c.val⁻¹ *
(electricField c A { val := γ β * (t.val + β / c.val * x.val 0) }
{
val := fun x_1 =>
match x_1 with
| ⟨0, ⋯⟩ => γ β * (x.val 0 + c.val * β * t.val)
| ⟨n.succ, ih⟩ => x.val ⟨n + 1, ih⟩ }).ofLp
i.succ) +
γ β *
magneticFieldMatrix c A { val := γ β * (t.val + β / c.val * x.val 0) }
{
val := fun x_1 =>
match x_1 with
| ⟨0, ⋯⟩ => γ β * (x.val 0 + c.val * β * t.val)
| ⟨n.succ, ih⟩ => x.val ⟨n + 1, ih⟩ }
(0, i.succ) =
γ β *
((A.fieldStrengthMatrix
((SpaceTime.toTimeAndSpace c).symm
({ val := γ β * (t.val + β / c.val * x.val 0) },
{
val := fun x_1 =>
match x_1 with
| ⟨0, ⋯⟩ => γ β * (x.val 0 + c.val * β * t.val)
| ⟨n.succ, ih⟩ => x.val ⟨n + 1, ih⟩ })))
(Sum.inr 0, Sum.inr i.succ) +
β / c.val *
(electricField c A { val := γ β * (t.val + β / c.val * x.val 0) }
{
val := fun x_1 =>
match x_1 with
| ⟨0, ⋯⟩ => γ β * (x.val 0 + c.val * β * t.val)
| ⟨n.succ, ih⟩ => x.val ⟨n + 1, ih⟩ }).ofLp
i.succ)
d:ℕc:SpeedOfLightβ:ℝhβ:|β| < 1A:ElectromagneticPotential d.succhA:Differentiable ℝ A.valt:Timex:Space d.succi:Fin d⊢ γ β *
(β *
(electricField c A { val := γ β * (c.val * t.val + β * x.val 0) / c.val }
{
val := fun x_1 =>
match x_1 with
| ⟨0, ⋯⟩ => γ β * (x.val 0 + β * c.val * t.val)
| ⟨n.succ, ih⟩ => x.val ⟨n + 1, ih⟩ }).ofLp
i.succ +
c.val *
magneticFieldMatrix c A { val := γ β * (c.val * t.val + β * x.val 0) / c.val }
{
val := fun x_1 =>
match x_1 with
| ⟨0, ⋯⟩ => γ β * (x.val 0 + β * c.val * t.val)
| ⟨n.succ, ih⟩ => x.val ⟨n + 1, ih⟩ }
(0, i.succ)) =
γ β *
(c.val *
(A.fieldStrengthMatrix
((SpaceTime.toTimeAndSpace c).symm
({ val := γ β * (c.val * t.val + β * x.val 0) / c.val },
{
val := fun x_1 =>
match x_1 with
| ⟨0, ⋯⟩ => γ β * (x.val 0 + β * c.val * t.val)
| ⟨n.succ, ih⟩ => x.val ⟨n + 1, ih⟩ })))
(Sum.inr 0, Sum.inr i.succ) +
β *
(electricField c A { val := γ β * (c.val * t.val + β * x.val 0) / c.val }
{
val := fun x_1 =>
match x_1 with
| ⟨0, ⋯⟩ => γ β * (x.val 0 + β * c.val * t.val)
| ⟨n.succ, ih⟩ => x.val ⟨n + 1, ih⟩ }).ofLp
i.succ)
d:ℕc:SpeedOfLightβ:ℝhβ:|β| < 1A:ElectromagneticPotential d.succhA:Differentiable ℝ A.valt:Timex:Space d.succi:Fin d⊢ γ β * β *
(electricField c A { val := γ β * β * x.val 0 * c.val⁻¹ + γ β * c.val * t.val * c.val⁻¹ }
{
val := fun x_1 =>
match x_1 with
| ⟨0, ⋯⟩ => γ β * β * c.val * t.val + γ β * x.val 0
| ⟨n.succ, ih⟩ => x.val ⟨1 + n, ⋯⟩ }).ofLp
i.succ +
γ β * c.val *
magneticFieldMatrix c A { val := γ β * β * x.val 0 * c.val⁻¹ + γ β * c.val * t.val * c.val⁻¹ }
{
val := fun x_1 =>
match x_1 with
| ⟨0, ⋯⟩ => γ β * β * c.val * t.val + γ β * x.val 0
| ⟨n.succ, ih⟩ => x.val ⟨1 + n, ⋯⟩ }
(0, i.succ) =
γ β * β *
(electricField c A { val := γ β * β * x.val 0 * c.val⁻¹ + γ β * c.val * t.val * c.val⁻¹ }
{
val := fun x_1 =>
match x_1 with
| ⟨0, ⋯⟩ => γ β * β * c.val * t.val + γ β * x.val 0
| ⟨n.succ, ih⟩ => x.val ⟨1 + n, ⋯⟩ }).ofLp
i.succ +
γ β * c.val *
(A.fieldStrengthMatrix
((SpaceTime.toTimeAndSpace c).symm
({ val := γ β * β * x.val 0 * c.val⁻¹ + γ β * c.val * t.val * c.val⁻¹ },
{
val := fun x_1 =>
match x_1 with
| ⟨0, ⋯⟩ => γ β * β * c.val * t.val + γ β * x.val 0
| ⟨n.succ, ih⟩ => x.val ⟨1 + n, ⋯⟩ })))
(Sum.inr 0, Sum.inr i.succ)
All goals completed! 🐙B.2. Boost of the other components of the magnetic field matrix
d:ℕc:SpeedOfLightβ:ℝhβ:|β| < 1A:ElectromagneticPotential d.succhA:Differentiable ℝ A.valt:Timex:Space d.succi:Fin dj:Fin d⊢ (A.fieldStrengthMatrix
((SpaceTime.toTimeAndSpace c).symm
({ val := γ β * (t.val + β / c.val * x.val 0) },
{
val := fun x_1 =>
match x_1 with
| ⟨0, ⋯⟩ => γ β * (x.val 0 + c.val * β * t.val)
| ⟨n.succ, ih⟩ => x.val ⟨n.succ, ih⟩ })))
(Sum.inr i.succ, Sum.inr j.succ) =
(A.fieldStrengthMatrix
((SpaceTime.toTimeAndSpace c).symm
({ val := γ β * (t.val + β / c.val * x.val 0) },
{
val := fun x_1 =>
match x_1 with
| ⟨0, ⋯⟩ => γ β * (x.val 0 + c.val * β * t.val)
| ⟨n.succ, ih⟩ => x.val ⟨n + 1, ih⟩ })))
(Sum.inr i.succ, Sum.inr j.succ)
All goals completed! 🐙