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.ScalarPotential
public import Physlib.Electromagnetism.Kinematics.FieldStrength
public import Physlib.Electromagnetism.BasicThe Electric Field
i. Overview
The electric field is defined in terms of the electromagnetic potential A as
E = - ∇ φ - ∂ₜ \vec A.
In this module we define the electric field, and prove lemmas about it.
ii. Key results
electricField : The electric field from the electromagnetic potential.
electricField_eq_fieldStrengthMatrix : The electric field expressed in terms of the
field strength tensor.
iii. Table of contents
A. Definition of the Electric Field
B. Relation to the field strength tensor
C. Smoothness of the electric field
D. Differentiability of the electric field
E. Time derivative of the vector potential in terms of the electric field
F. Derivatives of the electric field in terms of field strength tensor
iv. References
@[expose] public sectionattribute [-simp] Fintype.sum_sum_typeattribute [-simp] Nat.succ_eq_add_oneA. Definition of the Electric Field
lemma electricField_eq {c : SpeedOfLight} (A : ElectromagneticPotential d) :
A.electricField c = fun t x =>
- ∇ (A.scalarPotential c t) x - ∂ₜ (fun t => A.vectorPotential c t x) t := rflB. Relation to constructors
B. Relation to the field strength tensor
The electric field can be expressed in terms of the field strength tensor as
E_i = - c * F_0^i.
d:ℕc:SpeedOfLightA:ElectromagneticPotential dt:Timex:Space di:Fin dhA:Differentiable ℝ A.valh_congr_thm✝:∀ {p : ENNReal} {V : Type} (self self_1 : WithLp p V), self = self_1 → self.ofLp = self_1.ofLp⊢ Differentiable ℝ fun t => WithLp.toLp 2 fun i => A.val ((toTimeAndSpace c).symm (t, x)) (Sum.inr i)d:ℕc:SpeedOfLightA:ElectromagneticPotential dt:Timex:Space di:Fin dhA:Differentiable ℝ A.valh_congr_thm✝:∀ {p : ENNReal} {V : Type} (self self_1 : WithLp p V), self = self_1 → self.ofLp = self_1.ofLp⊢ Differentiable ℝ fun t => A.val ((toTimeAndSpace c).symm (t, x))d:ℕc:SpeedOfLightA:ElectromagneticPotential dt:Timex:Space di:Fin dhA:Differentiable ℝ A.valh_congr_thm✝:∀ {p : ENNReal} {V : Type} (self self_1 : WithLp p V), self = self_1 → self.ofLp = self_1.ofLp⊢ Differentiable ℝ A.val
d:ℕc:SpeedOfLightA:ElectromagneticPotential dt:Timex:Space di:Fin dhA:Differentiable ℝ A.valh_congr_thm✝:∀ {p : ENNReal} {V : Type} (self self_1 : WithLp p V), self = self_1 → self.ofLp = self_1.ofLp⊢ Differentiable ℝ fun t => WithLp.toLp 2 fun i => A.val ((toTimeAndSpace c).symm (t, x)) (Sum.inr i) d:ℕc:SpeedOfLightA:ElectromagneticPotential dt:Timex:Space di:Fin dhA:Differentiable ℝ A.valh_congr_thm✝:∀ {p : ENNReal} {V : Type} (self self_1 : WithLp p V), self = self_1 → self.ofLp = self_1.ofLp⊢ ∀ (i : Fin d),
Differentiable ℝ fun t => (WithLp.toLp 2 fun i => A.val ((toTimeAndSpace c).symm (t, x)) (Sum.inr i)).ofLp i
d:ℕc:SpeedOfLightA:ElectromagneticPotential dt:Timex:Space di✝:Fin dhA:Differentiable ℝ A.valh_congr_thm✝:∀ {p : ENNReal} {V : Type} (self self_1 : WithLp p V), self = self_1 → self.ofLp = self_1.ofLpi:Fin d⊢ Differentiable ℝ fun t => (WithLp.toLp 2 fun i => A.val ((toTimeAndSpace c).symm (t, x)) (Sum.inr i)).ofLp i
d:ℕc:SpeedOfLightA:ElectromagneticPotential dt:Timex:Space di✝:Fin dhA:Differentiable ℝ A.valh_congr_thm✝:∀ {p : ENNReal} {V : Type} (self self_1 : WithLp p V), self = self_1 → self.ofLp = self_1.ofLpi:Fin d⊢ Differentiable ℝ fun t => A.val ((toTimeAndSpace c).symm (t, x)) (Sum.inr i)
All goals completed! 🐙
d:ℕc:SpeedOfLightA:ElectromagneticPotential dt:Timex:Space di:Fin dhA:Differentiable ℝ A.valh_congr_thm✝:∀ {p : ENNReal} {V : Type} (self self_1 : WithLp p V), self = self_1 → self.ofLp = self_1.ofLp⊢ Differentiable ℝ fun t => A.val ((toTimeAndSpace c).symm (t, x)) All goals completed! 🐙
d:ℕc:SpeedOfLightA:ElectromagneticPotential dt:Timex:Space di:Fin dhA:Differentiable ℝ A.valh_congr_thm✝:∀ {p : ENNReal} {V : Type} (self self_1 : WithLp p V), self = self_1 → self.ofLp = self_1.ofLp⊢ Differentiable ℝ A.val All goals completed! 🐙
d:ℕc:SpeedOfLightA:ElectromagneticPotential dt:Timex:Space di:Fin dhA:Differentiable ℝ A.val⊢ ENNReal All goals completed! 🐙d:ℕc:SpeedOfLightA:ElectromagneticPotential dx:SpaceTime di:Fin dhA:Differentiable ℝ A.val⊢ (A.fieldStrengthMatrix x) (Sum.inl 0, Sum.inr i) =
-(1 / c.val) *
(-c.val * (A.fieldStrengthMatrix ((toTimeAndSpace c).symm ((time c) x, space x))) (Sum.inl 0, Sum.inr i))
All goals completed! 🐙d:ℕc:SpeedOfLightA:ElectromagneticPotential dx:SpaceTime di:Fin dhA:Differentiable ℝ A.val⊢ -(-(1 / SpeedOfLight.val ?m.49) * (electricField ?m.49 A ((time ?m.49) x) (space x)).ofLp i) =
1 / c.val * (electricField c A ((time c) x) (space x)).ofLp id:ℕc:SpeedOfLightA:ElectromagneticPotential dx:SpaceTime di:Fin dhA:Differentiable ℝ A.val⊢ SpeedOfLight
All goals completed! 🐙C. Smoothness of the electric field
d:ℕn:WithTop ℕ∞c:SpeedOfLightA:ElectromagneticPotential dhA:ContDiff ℝ (n + 1) A.val⊢ ∀ (i : Fin d), ContDiff ℝ n fun x => (↿(electricField c A) x).ofLp i
d:ℕn:WithTop ℕ∞c:SpeedOfLightA:ElectromagneticPotential dhA:ContDiff ℝ (n + 1) A.vali:Fin d⊢ ContDiff ℝ n fun x => (↿(electricField c A) x).ofLp i
d:ℕn:WithTop ℕ∞c:SpeedOfLightA:ElectromagneticPotential dhA:ContDiff ℝ (n + 1) A.vali:Fin d| ContDiff ℝ n fun x => (↿(electricField c A) x).ofLp i
d:ℕn:WithTop ℕ∞c:SpeedOfLightA:ElectromagneticPotential dhA:ContDiff ℝ (n + 1) A.vali:Fin dx:Time × Space d| (↿(electricField c A) x).ofLp i;
d:ℕn:WithTop ℕ∞c:SpeedOfLightA:ElectromagneticPotential dhA:ContDiff ℝ (n + 1) A.vali:Fin dx:Time × Space d| (electricField c A x.1 x.2).ofLp i
rw [electricField_eq_fieldStrengthMatrix (A) x.1 x.2 i (hA.differentiable (d:ℕn:WithTop ℕ∞c:SpeedOfLightA:ElectromagneticPotential dhA:ContDiff ℝ (n + 1) A.vali:Fin dx:Time × Space d⊢ n + 1 ≠ 0 All goals completed! 🐙))]
d:ℕn:WithTop ℕ∞c:SpeedOfLightA:ElectromagneticPotential dhA:ContDiff ℝ (n + 1) A.vali:Fin dx:Time × Space d| -c.val * (A.fieldStrengthMatrix ((toTimeAndSpace c).symm (x.1, x.2))) (Sum.inl 0, Sum.inr i)
d:ℕn:WithTop ℕ∞c:SpeedOfLightA:ElectromagneticPotential dhA:ContDiff ℝ (n + 1) A.vali:Fin d⊢ ContDiff ℝ n fun x => -c.vald:ℕn:WithTop ℕ∞c:SpeedOfLightA:ElectromagneticPotential dhA:ContDiff ℝ (n + 1) A.vali:Fin d⊢ ContDiff ℝ n fun x => (A.fieldStrengthMatrix ((toTimeAndSpace c).symm (x.1, x.2))) (Sum.inl 0, Sum.inr i)
d:ℕn:WithTop ℕ∞c:SpeedOfLightA:ElectromagneticPotential dhA:ContDiff ℝ (n + 1) A.vali:Fin d⊢ ContDiff ℝ n fun x => -c.val All goals completed! 🐙
All goals completed! 🐙lemma electricField_apply_contDiff {n} {c : SpeedOfLight} {A : ElectromagneticPotential d}
(hA : ContDiff ℝ (n + 1) A) : ContDiff ℝ n (↿(fun t x => A.electricField c t x i)) :=
(ContinuousLinearMap.contDiff (𝕜 := ℝ) (EuclideanSpace.proj i)).comp (electricField_contDiff hA)lemma electricField_apply_contDiff_space {n} {A : ElectromagneticPotential d}
{c : SpeedOfLight}
(hA : ContDiff ℝ (n + 1) A) (t : Time) :
ContDiff ℝ n (fun x => A.electricField c t x i) :=
(electricField_apply_contDiff hA).comp (f := fun x => (t, x)) (d:ℕi:Fin dn:WithTop ℕ∞A:ElectromagneticPotential dc:SpeedOfLighthA:ContDiff ℝ (n + 1) A.valt:Time⊢ ContDiff ℝ n fun x => (t, x) All goals completed! 🐙)lemma electricField_apply_contDiff_time {n} {c : SpeedOfLight} {A : ElectromagneticPotential d}
(hA : ContDiff ℝ (n + 1) A) (x : Space d) :
ContDiff ℝ n (fun t => A.electricField c t x i) :=
(electricField_apply_contDiff hA).comp (f := fun t => (t, x)) (d:ℕi:Fin dn:WithTop ℕ∞c:SpeedOfLightA:ElectromagneticPotential dhA:ContDiff ℝ (n + 1) A.valx:Space d⊢ ContDiff ℝ n fun t => (t, x) All goals completed! 🐙)D. Differentiability of the electric field
lemma electricField_differentiable {A : ElectromagneticPotential d} {c : SpeedOfLight}
(hA : ContDiff ℝ 2 A) : Differentiable ℝ (↿(A.electricField c)) :=
(electricField_contDiff (n := 1) hA).differentiable one_ne_zerolemma electricField_differentiable_time {A : ElectromagneticPotential d} {c : SpeedOfLight}
(hA : ContDiff ℝ 2 A) (x : Space d) : Differentiable ℝ (A.electricField c · x) :=
(electricField_differentiable hA).comp (f := fun t => (t, x)) (d:ℕA:ElectromagneticPotential dc:SpeedOfLighthA:ContDiff ℝ 2 A.valx:Space d⊢ Differentiable ℝ fun t => (t, x) All goals completed! 🐙)lemma electricField_differentiable_space {A : ElectromagneticPotential d} {c : SpeedOfLight}
(hA : ContDiff ℝ 2 A) (t : Time) : Differentiable ℝ (A.electricField c t) :=
(electricField_differentiable hA).comp (f := fun x => (t, x)) (d:ℕA:ElectromagneticPotential dc:SpeedOfLighthA:ContDiff ℝ 2 A.valt:Time⊢ Differentiable ℝ fun x => (t, x) All goals completed! 🐙)lemma electricField_apply_differentiable {A : ElectromagneticPotential d}
{c : SpeedOfLight}
(hA : ContDiff ℝ 2 A) :
Differentiable ℝ (fun (tx : Time × Space d) => A.electricField c tx.1 tx.2 i) :=
(ContinuousLinearMap.differentiable (𝕜 := ℝ) (EuclideanSpace.proj i)).comp
(electricField_differentiable hA)lemma electricField_apply_differentiable_space {A : ElectromagneticPotential d}
{c : SpeedOfLight}
(hA : ContDiff ℝ 2 A) (t : Time) (i : Fin d) :
Differentiable ℝ (fun x => A.electricField c t x i) :=
(electricField_apply_differentiable hA).comp (f := fun x => (t, x)) (d:ℕA:ElectromagneticPotential dc:SpeedOfLighthA:ContDiff ℝ 2 A.valt:Timei:Fin d⊢ Differentiable ℝ fun x => (t, x) All goals completed! 🐙)lemma electricField_apply_differentiable_time {A : ElectromagneticPotential d}
{c : SpeedOfLight}
(hA : ContDiff ℝ 2 A) (x : Space d) (i : Fin d) :
Differentiable ℝ (fun t => A.electricField c t x i) :=
(electricField_apply_differentiable hA).comp (f := fun t => (t, x)) (d:ℕA:ElectromagneticPotential dc:SpeedOfLighthA:ContDiff ℝ 2 A.valx:Space di:Fin d⊢ Differentiable ℝ fun t => (t, x) All goals completed! 🐙)E. Time derivative of the vector potential in terms of the electric field
d:ℕc:SpeedOfLightA:ElectromagneticPotential dt:Timex:Space d⊢ ∂ₜ (fun t => vectorPotential c A t x) t =
-(-∇ (scalarPotential c A t) x - ∂ₜ (fun t => vectorPotential c A t x) t) - ∇ (scalarPotential c A t) x
All goals completed! 🐙d:ℕA:ElectromagneticPotential dc:SpeedOfLighthA:Differentiable ℝ A.valt:Timex:Space di:Fin d⊢ (-electricField c A t x - ∇ (scalarPotential c A t) x).ofLp i =
-(electricField c A t x).ofLp i - Space.deriv i (scalarPotential c A t) xd:ℕA:ElectromagneticPotential dc:SpeedOfLighthA:Differentiable ℝ A.valt:Timex:Space di:Fin d⊢ Differentiable ℝ fun t => vectorPotential c A t x
d:ℕA:ElectromagneticPotential dc:SpeedOfLighthA:Differentiable ℝ A.valt:Timex:Space di:Fin d⊢ (∇ (scalarPotential c A t) x).ofLp i = Space.deriv i (scalarPotential c A t) xd:ℕA:ElectromagneticPotential dc:SpeedOfLighthA:Differentiable ℝ A.valt:Timex:Space di:Fin d⊢ Differentiable ℝ fun t => vectorPotential c A t x
d:ℕA:ElectromagneticPotential dc:SpeedOfLighthA:Differentiable ℝ A.valt:Timex:Space di:Fin d⊢ Differentiable ℝ fun t => vectorPotential c A t x
All goals completed! 🐙F. Derivatives of the electric field in terms of field strength tensor
d:ℕA:ElectromagneticPotential dc:SpeedOfLighthA:ContDiff ℝ 2 A.valt:Timex:Space di:Fin d⊢ (-c.val • fderiv ℝ (fun t => (A.fieldStrengthMatrix ((toTimeAndSpace c).symm (t, x))) (Sum.inl 0, Sum.inr i)) t) 1 =
-(c.val ^ 2 *
(c.val⁻¹ * ∂ₜ (fun t => (A.fieldStrengthMatrix ((toTimeAndSpace c).symm (t, x))) (Sum.inl 0, Sum.inr i)) t))d:ℕA:ElectromagneticPotential dc:SpeedOfLighthA:ContDiff ℝ 2 A.valt:Timex:Space di:Fin d⊢ DifferentiableAt ℝ (fun t => (A.fieldStrengthMatrix ((toTimeAndSpace c).symm (t, x))) (Sum.inl 0, Sum.inr i)) td:ℕA:ElectromagneticPotential dc:SpeedOfLighthA:ContDiff ℝ 2 A.valt:Timex:Space di:Fin d⊢ Differentiable ℝ fun t => electricField c A t xd:ℕA:ElectromagneticPotential dc:SpeedOfLighthA:ContDiff ℝ 2 A.valt:Timex:Space di:Fin d⊢ Differentiable ℝ fun x => (A.fieldStrengthMatrix x) (Sum.inl 0, Sum.inr i)
d:ℕA:ElectromagneticPotential dc:SpeedOfLighthA:ContDiff ℝ 2 A.valt:Timex:Space di:Fin d⊢ c.val * ∂ₜ (fun t => (A.fieldStrengthMatrix ((toTimeAndSpace c).symm (t, x))) (Sum.inl 0, Sum.inr i)) t =
c.val ^ 2 *
(c.val⁻¹ * ∂ₜ (fun t => (A.fieldStrengthMatrix ((toTimeAndSpace c).symm (t, x))) (Sum.inl 0, Sum.inr i)) t)d:ℕA:ElectromagneticPotential dc:SpeedOfLighthA:ContDiff ℝ 2 A.valt:Timex:Space di:Fin d⊢ DifferentiableAt ℝ (fun t => (A.fieldStrengthMatrix ((toTimeAndSpace c).symm (t, x))) (Sum.inl 0, Sum.inr i)) td:ℕA:ElectromagneticPotential dc:SpeedOfLighthA:ContDiff ℝ 2 A.valt:Timex:Space di:Fin d⊢ Differentiable ℝ fun t => electricField c A t xd:ℕA:ElectromagneticPotential dc:SpeedOfLighthA:ContDiff ℝ 2 A.valt:Timex:Space di:Fin d⊢ Differentiable ℝ fun x => (A.fieldStrengthMatrix x) (Sum.inl 0, Sum.inr i)
d:ℕA:ElectromagneticPotential dc:SpeedOfLighthA:ContDiff ℝ 2 A.valt:Timex:Space di:Fin d⊢ DifferentiableAt ℝ (fun t => (A.fieldStrengthMatrix ((toTimeAndSpace c).symm (t, x))) (Sum.inl 0, Sum.inr i)) td:ℕA:ElectromagneticPotential dc:SpeedOfLighthA:ContDiff ℝ 2 A.valt:Timex:Space di:Fin d⊢ Differentiable ℝ fun t => electricField c A t xd:ℕA:ElectromagneticPotential dc:SpeedOfLighthA:ContDiff ℝ 2 A.valt:Timex:Space di:Fin d⊢ Differentiable ℝ fun x => (A.fieldStrengthMatrix x) (Sum.inl 0, Sum.inr i)
d:ℕA:ElectromagneticPotential dc:SpeedOfLighthA:ContDiff ℝ 2 A.valt:Timex:Space di:Fin d⊢ DifferentiableAt ℝ (fun t => (A.fieldStrengthMatrix ((toTimeAndSpace c).symm (t, x))) (Sum.inl 0, Sum.inr i)) t All goals completed! 🐙
d:ℕA:ElectromagneticPotential dc:SpeedOfLighthA:ContDiff ℝ 2 A.valt:Timex:Space di:Fin d⊢ Differentiable ℝ fun t => electricField c A t x All goals completed! 🐙
d:ℕA:ElectromagneticPotential dc:SpeedOfLighthA:ContDiff ℝ 2 A.valt:Timex:Space di:Fin d⊢ Differentiable ℝ fun x => (A.fieldStrengthMatrix x) (Sum.inl 0, Sum.inr i) All goals completed! 🐙d:ℕA:ElectromagneticPotential dc:SpeedOfLighthA:ContDiff ℝ 2 A.valt:Timex:Space di:Fin d⊢ (-c.val • fderiv ℝ (fun y => -(A.fieldStrengthMatrix ((toTimeAndSpace c).symm (t, y))) (Sum.inr i, Sum.inl 0)) x)
(Space.basis i) =
c.val * Space.deriv i (fun y => (A.fieldStrengthMatrix ((toTimeAndSpace c).symm (t, y))) (Sum.inr i, Sum.inl 0)) xd:ℕA:ElectromagneticPotential dc:SpeedOfLighthA:ContDiff ℝ 2 A.valt:Timex:Space di:Fin d⊢ DifferentiableAt ℝ (fun y => -(A.fieldStrengthMatrix ((toTimeAndSpace c).symm (t, y))) (Sum.inr i, Sum.inl 0)) x
d:ℕA:ElectromagneticPotential dc:SpeedOfLighthA:ContDiff ℝ 2 A.valt:Timex:Space di:Fin d⊢ DifferentiableAt ℝ (fun y => -(A.fieldStrengthMatrix ((toTimeAndSpace c).symm (t, y))) (Sum.inr i, Sum.inl 0)) x
All goals completed! 🐙