The 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 #
A. Definition of the Electric Field #
noncomputable def
Electromagnetism.ElectromagneticPotential.electricField
{d : ℕ}
(c : SpeedOfLight := 1)
(A : ElectromagneticPotential d)
:
The electric field from the electromagnetic potential.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Electromagnetism.ElectromagneticPotential.electricField_eq
{d : ℕ}
{c : SpeedOfLight}
(A : ElectromagneticPotential d)
:
electricField c A = fun (t : Time) (x : Space d) =>
-Space.grad (scalarPotential c A t) x - Time.deriv (fun (t : Time) => vectorPotential c A t x) t
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.
theorem
Electromagnetism.ElectromagneticPotential.electricField_eq_fieldStrengthMatrix
{d : ℕ}
{c : SpeedOfLight}
(A : ElectromagneticPotential d)
(t : Time)
(x : Space d)
(i : Fin d)
(hA : Differentiable ℝ A)
:
theorem
Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_inl_inr_eq_electricField
{d : ℕ}
{c : SpeedOfLight}
(A : ElectromagneticPotential d)
(x : SpaceTime d)
(i : Fin d)
(hA : Differentiable ℝ A)
:
(A.fieldStrengthMatrix x) (Sum.inl 0, Sum.inr i) = -(1 / c.val) * electricField c A ((SpaceTime.time c) x) (SpaceTime.space x) i
theorem
Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_inr_inl_eq_electricField
{d : ℕ}
{c : SpeedOfLight}
(A : ElectromagneticPotential d)
(x : SpaceTime d)
(i : Fin d)
(hA : Differentiable ℝ A)
:
(A.fieldStrengthMatrix x) (Sum.inr i, Sum.inl 0) = 1 / c.val * electricField c A ((SpaceTime.time c) x) (SpaceTime.space x) i
C. Smoothness of the electric field #
theorem
Electromagnetism.ElectromagneticPotential.electricField_contDiff
{d : ℕ}
{n : WithTop ℕ∞}
{c : SpeedOfLight}
{A : ElectromagneticPotential d}
(hA : ContDiff ℝ (n + 1) A)
:
ContDiff ℝ n ↿(electricField c A)
theorem
Electromagnetism.ElectromagneticPotential.electricField_apply_contDiff
{d : ℕ}
{i : Fin d}
{n : WithTop ℕ∞}
{c : SpeedOfLight}
{A : ElectromagneticPotential d}
(hA : ContDiff ℝ (n + 1) A)
:
theorem
Electromagnetism.ElectromagneticPotential.electricField_apply_contDiff_space
{d : ℕ}
{i : Fin d}
{n : WithTop ℕ∞}
{A : ElectromagneticPotential d}
{c : SpeedOfLight}
(hA : ContDiff ℝ (n + 1) A)
(t : Time)
:
ContDiff ℝ n fun (x : Space d) => electricField c A t x i
theorem
Electromagnetism.ElectromagneticPotential.electricField_apply_contDiff_time
{d : ℕ}
{i : Fin d}
{n : WithTop ℕ∞}
{c : SpeedOfLight}
{A : ElectromagneticPotential d}
(hA : ContDiff ℝ (n + 1) A)
(x : Space d)
:
ContDiff ℝ n fun (t : Time) => electricField c A t x i
D. Differentiability of the electric field #
theorem
Electromagnetism.ElectromagneticPotential.electricField_differentiable
{d : ℕ}
{A : ElectromagneticPotential d}
{c : SpeedOfLight}
(hA : ContDiff ℝ 2 A)
:
Differentiable ℝ ↿(electricField c A)
theorem
Electromagnetism.ElectromagneticPotential.electricField_differentiable_time
{d : ℕ}
{A : ElectromagneticPotential d}
{c : SpeedOfLight}
(hA : ContDiff ℝ 2 A)
(x : Space d)
:
Differentiable ℝ fun (x_1 : Time) => electricField c A x_1 x
theorem
Electromagnetism.ElectromagneticPotential.electricField_differentiable_space
{d : ℕ}
{A : ElectromagneticPotential d}
{c : SpeedOfLight}
(hA : ContDiff ℝ 2 A)
(t : Time)
:
Differentiable ℝ (electricField c A t)
theorem
Electromagnetism.ElectromagneticPotential.electricField_apply_differentiable_space
{d : ℕ}
{A : ElectromagneticPotential d}
{c : SpeedOfLight}
(hA : ContDiff ℝ 2 A)
(t : Time)
(i : Fin d)
:
Differentiable ℝ fun (x : Space d) => electricField c A t x i
E. Time derivative of the vector potential in terms of the electric field #
theorem
Electromagnetism.ElectromagneticPotential.time_deriv_vectorPotential_eq_electricField
{d : ℕ}
{c : SpeedOfLight}
(A : ElectromagneticPotential d)
(t : Time)
(x : Space d)
:
Time.deriv (fun (t : Time) => vectorPotential c A t x) t = -electricField c A t x - Space.grad (scalarPotential c A t) x
theorem
Electromagnetism.ElectromagneticPotential.time_deriv_comp_vectorPotential_eq_electricField
{d : ℕ}
{A : ElectromagneticPotential d}
{c : SpeedOfLight}
(hA : Differentiable ℝ A)
(t : Time)
(x : Space d)
(i : Fin d)
:
Time.deriv (fun (t : Time) => vectorPotential c A t x i) t = -electricField c A t x i - Space.deriv i (scalarPotential c A t) x
F. Derivatives of the electric field in terms of field strength tensor #
theorem
Electromagnetism.ElectromagneticPotential.time_deriv_electricField_eq_fieldStrengthMatrix
{d : ℕ}
{A : ElectromagneticPotential d}
{c : SpeedOfLight}
(hA : ContDiff ℝ 2 A)
(t : Time)
(x : Space d)
(i : Fin d)
:
Time.deriv (fun (t : Time) => electricField c A t x) t i = -c.val ^ 2 * SpaceTime.deriv (Sum.inl 0) (fun (x : SpaceTime d) => (A.fieldStrengthMatrix x) (Sum.inl 0, Sum.inr i))
((SpaceTime.toTimeAndSpace c).symm (t, x))
theorem
Electromagnetism.ElectromagneticPotential.div_electricField_eq_fieldStrengthMatrix
{d : ℕ}
{A : ElectromagneticPotential d}
{c : SpeedOfLight}
(hA : ContDiff ℝ 2 A)
(t : Time)
(x : Space d)
:
Space.div (electricField c A t) x = c.val * ∑ μ : Fin 1 ⊕ Fin d,
SpaceTime.deriv μ (fun (x : SpaceTime d) => (A.fieldStrengthMatrix x) (μ, Sum.inl 0))
((SpaceTime.toTimeAndSpace c).symm (t, x))