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.ElectricFieldThe Magnetic Field
i. Overview
In 3-spatial dimensions from the electromagnetic potential we can define the magnetic field
\vec B as (∇ ⨯ (A.vectorPotential t)) x.
In this module we define this magnetic field from the electromagnetic potential.
In general dimensions we define the magnetic field matrix from the spatial components of the field strength matrix. This is an antisymmetric matrix.
ii. Key results
ElectromagneticPotential.magneticField : The magnetic field from the electromagnetic potential
in 3 spatial dimensions.
ElectromagneticPotential.magneticFieldMatrix : The magnetic field matrix from the
electromagnetic potential in general spatial dimensions.
ElectromagneticPotential.time_deriv_magneticFieldMatrix : The time derivative of the magnetic
field matrix in terms of the vector potential. (Aka Faraday's law).
iii. Table of contents
A. The magnetic field
A.1. Relation between the magnetic field and the field strength matrix
A.2. Divergence of the magnetic field
B. The field strength matrix in terms of the electric and magnetic fields
C. Magnetic field matrix
C.1. Antisymmetry of the magnetic field matrix
C.2. Magnetic field in terms of the magnetic field matrix
C.3. Magnetic field matrix in terms of vector potentials
C.4. Smoothness of the magnetic field matrix
C.5. Differentiablity of the magnetic field matrix
C.6. Spatial derivative of the magnetic field matrix
C.7. Temporal derivative of the magnetic field matrix
C.8. curl of the magnetic field matrix
iv. References
@[expose] public sectionattribute [-simp] Fintype.sum_sum_typeattribute [-simp] Nat.succ_eq_add_oneA. The magnetic field
lemma magneticField_eq {c : SpeedOfLight} (A : ElectromagneticPotential) :
A.magneticField c = fun t x => (∇ ⨯ (A.vectorPotential c t)) x := rflA.1. Relation between the magnetic field and the field strength matrix
i:Fin 3c:SpeedOfLightA:ElectromagneticPotentialt:Timex:SpacehA:Differentiable ℝ (A.val 3)⊢ (fderiv ℝ (fun x => (vectorPotential c A t x).ofLp (i + 1)) x) (Space.basis (i + 2)) =
(fderiv ℝ (fun y => A.val 3 ((toTimeAndSpace c).symm (t, y)) (Sum.inr (i + 1))) x) (Space.basis (i + 2))i:Fin 3c:SpeedOfLightA:ElectromagneticPotentialt:Timex:SpacehA:Differentiable ℝ (A.val 3)⊢ Differentiable ℝ fun y => A.val 3 ((toTimeAndSpace c).symm (t, y))
i:Fin 3c:SpeedOfLightA:ElectromagneticPotentialt:Timex:SpacehA:Differentiable ℝ (A.val 3)⊢ Differentiable ℝ fun y => A.val 3 ((toTimeAndSpace c).symm (t, y))
i:Fin 3c:SpeedOfLightA:ElectromagneticPotentialt:Timex:SpacehA:Differentiable ℝ (A.val 3)⊢ Differentiable ℝ fun y => A.val 3 ((toTimeAndSpace c).symm (t, y)) All goals completed! 🐙A.2. Divergence of the magnetic field
c:SpeedOfLightA:ElectromagneticPotentialhA:ContDiff ℝ 2 (A.val 3)t:Time⊢ ContDiff ℝ 2 (vectorPotential c A t)
All goals completed! 🐙A.4. The magnetic field on constructors
B. The field strength matrix in terms of the electric and magnetic fields
All goals completed! 🐙c:SpeedOfLightA:ElectromagneticPotentialx:SpaceTimehA:Differentiable ℝ (A.val 3)μ:Fin 1 ⊕ Fin 3ν:Fin 1 ⊕ Fin 3⊢ (A.fieldStrengthMatrix x) (μ, ν) =
(A.fieldStrengthMatrix ((toTimeAndSpace c).symm (((toTimeAndSpace c) x).1, ((toTimeAndSpace c) x).2))) (μ, ν)c:SpeedOfLightA:ElectromagneticPotentialx:SpaceTimehA:Differentiable ℝ (A.val 3)μ:Fin 1 ⊕ Fin 3ν:Fin 1 ⊕ Fin 3⊢ Differentiable ℝ (A.val 3)
c:SpeedOfLightA:ElectromagneticPotentialx:SpaceTimehA:Differentiable ℝ (A.val 3)μ:Fin 1 ⊕ Fin 3ν:Fin 1 ⊕ Fin 3⊢ Differentiable ℝ (A.val 3)
All goals completed! 🐙C. Magnetic field matrix
lemma magneticFieldMatrix_eq {c : SpeedOfLight} (A : ElectromagneticPotential d) :
A.magneticFieldMatrix c = fun t x ij =>
A.fieldStrengthMatrix ((toTimeAndSpace c).symm (t, x)) (Sum.inr ij.1, Sum.inr ij.2) := rfllemma fieldStrengthMatrix_inr_inr_eq_magneticFieldMatrix {c : SpeedOfLight}
(A : ElectromagneticPotential d)
(x : SpaceTime d) (i j : Fin d) :
A.fieldStrengthMatrix x (Sum.inr i, Sum.inr j) =
A.magneticFieldMatrix c (x.time c) x.space (i, j) := d:ℕc:SpeedOfLightA:ElectromagneticPotential dx:SpaceTime di:Fin dj:Fin d⊢ (A.fieldStrengthMatrix x) (Sum.inr i, Sum.inr j) = magneticFieldMatrix c A ((time c) x) (space x) (i, j)
All goals completed! 🐙C.1. Antisymmetry of the magnetic field matrix
lemma magneticFieldMatrix_antisymm {c : SpeedOfLight}
(A : ElectromagneticPotential d) (t : Time)
(x : Space d) (i j : Fin d) :
A.magneticFieldMatrix c t x (i, j) = - A.magneticFieldMatrix c t x (j, i) :=
fieldStrengthMatrix_antisymm A ((toTimeAndSpace c).symm (t, x)) (Sum.inr i) (Sum.inr j)@[simp]
lemma magneticFieldMatrix_diag_eq_zero {c : SpeedOfLight}
(A : ElectromagneticPotential d) (t : Time)
(x : Space d) (i : Fin d) :
A.magneticFieldMatrix c t x (i, i) = 0 :=
fieldStrengthMatrix_diag_eq_zero A ((toTimeAndSpace c).symm (t, x)) (Sum.inr i)C.2. Magnetic field in terms of the magnetic field matrix
lemma magneticField_eq_magneticFieldMatrix {c : SpeedOfLight} (A : ElectromagneticPotential)
(hA : Differentiable ℝ A) :
A.magneticField c = fun t x => WithLp.toLp 2 fun i =>
- A.magneticFieldMatrix c t x ((i+1), (i+2)) := c:SpeedOfLightA:ElectromagneticPotentialhA:Differentiable ℝ (A.val 3)⊢ magneticField c A = fun t x => WithLp.toLp 2 fun i => -magneticFieldMatrix c A t x (i + 1, i + 2)
c:SpeedOfLightA:ElectromagneticPotentialhA:Differentiable ℝ (A.val 3)t:Timex:Spacei✝:Fin 3⊢ (magneticField c A t x).ofLp i✝ = (WithLp.toLp 2 fun i => -magneticFieldMatrix c A t x (i + 1, i + 2)).ofLp i✝
All goals completed! 🐙x:Spacei:Fin 3c:SpeedOfLightA:ElectromagneticPotentialhA:ContDiff ℝ 2 (A.val 3)t:Time⊢ (curl ((fun t x => WithLp.toLp 2 fun i => -magneticFieldMatrix c A t x (i + 1, i + 2)) t) x).ofLp i =
∑ j, Space.deriv j (fun x => magneticFieldMatrix c A t x (j, i)) x
x:Spacei:Fin 3c:SpeedOfLightA:ElectromagneticPotentialhA:ContDiff ℝ 2 (A.val 3)t:Time⊢ -(fderiv ℝ (fun y => magneticFieldMatrix c A t y (i + 2 + 1, i + 2 + 2)) x) (Space.basis (i + 1)) +
(fderiv ℝ (fun y => magneticFieldMatrix c A t y (i + 1 + 1, i + 1 + 2)) x) (Space.basis (i + 2)) =
(fderiv ℝ (fun x => magneticFieldMatrix c A t x (0, i)) x) (Space.basis 0) +
(fderiv ℝ (fun x => magneticFieldMatrix c A t x (1, i)) x) (Space.basis 1) +
(fderiv ℝ (fun x => magneticFieldMatrix c A t x (2, i)) x) (Space.basis 2)
x:Spacec:SpeedOfLightA:ElectromagneticPotentialhA:ContDiff ℝ 2 (A.val 3)t:Time⊢ -(fderiv ℝ (fun y => magneticFieldMatrix c A t y ((fun i => i) ⟨0, ⋯⟩ + 2 + 1, (fun i => i) ⟨0, ⋯⟩ + 2 + 2)) x)
(Space.basis ((fun i => i) ⟨0, ⋯⟩ + 1)) +
(fderiv ℝ (fun y => magneticFieldMatrix c A t y ((fun i => i) ⟨0, ⋯⟩ + 1 + 1, (fun i => i) ⟨0, ⋯⟩ + 1 + 2)) x)
(Space.basis ((fun i => i) ⟨0, ⋯⟩ + 2)) =
(fderiv ℝ (fun x => magneticFieldMatrix c A t x (0, (fun i => i) ⟨0, ⋯⟩)) x) (Space.basis 0) +
(fderiv ℝ (fun x => magneticFieldMatrix c A t x (1, (fun i => i) ⟨0, ⋯⟩)) x) (Space.basis 1) +
(fderiv ℝ (fun x => magneticFieldMatrix c A t x (2, (fun i => i) ⟨0, ⋯⟩)) x) (Space.basis 2)x:Spacec:SpeedOfLightA:ElectromagneticPotentialhA:ContDiff ℝ 2 (A.val 3)t:Time⊢ -(fderiv ℝ (fun y => magneticFieldMatrix c A t y ((fun i => i) ⟨1, ⋯⟩ + 2 + 1, (fun i => i) ⟨1, ⋯⟩ + 2 + 2)) x)
(Space.basis ((fun i => i) ⟨1, ⋯⟩ + 1)) +
(fderiv ℝ (fun y => magneticFieldMatrix c A t y ((fun i => i) ⟨1, ⋯⟩ + 1 + 1, (fun i => i) ⟨1, ⋯⟩ + 1 + 2)) x)
(Space.basis ((fun i => i) ⟨1, ⋯⟩ + 2)) =
(fderiv ℝ (fun x => magneticFieldMatrix c A t x (0, (fun i => i) ⟨1, ⋯⟩)) x) (Space.basis 0) +
(fderiv ℝ (fun x => magneticFieldMatrix c A t x (1, (fun i => i) ⟨1, ⋯⟩)) x) (Space.basis 1) +
(fderiv ℝ (fun x => magneticFieldMatrix c A t x (2, (fun i => i) ⟨1, ⋯⟩)) x) (Space.basis 2)x:Spacec:SpeedOfLightA:ElectromagneticPotentialhA:ContDiff ℝ 2 (A.val 3)t:Time⊢ -(fderiv ℝ (fun y => magneticFieldMatrix c A t y ((fun i => i) ⟨2, ⋯⟩ + 2 + 1, (fun i => i) ⟨2, ⋯⟩ + 2 + 2)) x)
(Space.basis ((fun i => i) ⟨2, ⋯⟩ + 1)) +
(fderiv ℝ (fun y => magneticFieldMatrix c A t y ((fun i => i) ⟨2, ⋯⟩ + 1 + 1, (fun i => i) ⟨2, ⋯⟩ + 1 + 2)) x)
(Space.basis ((fun i => i) ⟨2, ⋯⟩ + 2)) =
(fderiv ℝ (fun x => magneticFieldMatrix c A t x (0, (fun i => i) ⟨2, ⋯⟩)) x) (Space.basis 0) +
(fderiv ℝ (fun x => magneticFieldMatrix c A t x (1, (fun i => i) ⟨2, ⋯⟩)) x) (Space.basis 1) +
(fderiv ℝ (fun x => magneticFieldMatrix c A t x (2, (fun i => i) ⟨2, ⋯⟩)) x) (Space.basis 2) x:Spacec:SpeedOfLightA:ElectromagneticPotentialhA:ContDiff ℝ 2 (A.val 3)t:Time⊢ -(fderiv ℝ (fun y => magneticFieldMatrix c A t y ((fun i => i) ⟨0, ⋯⟩ + 2 + 1, (fun i => i) ⟨0, ⋯⟩ + 2 + 2)) x)
(Space.basis ((fun i => i) ⟨0, ⋯⟩ + 1)) +
(fderiv ℝ (fun y => magneticFieldMatrix c A t y ((fun i => i) ⟨0, ⋯⟩ + 1 + 1, (fun i => i) ⟨0, ⋯⟩ + 1 + 2)) x)
(Space.basis ((fun i => i) ⟨0, ⋯⟩ + 2)) =
(fderiv ℝ (fun x => magneticFieldMatrix c A t x (0, (fun i => i) ⟨0, ⋯⟩)) x) (Space.basis 0) +
(fderiv ℝ (fun x => magneticFieldMatrix c A t x (1, (fun i => i) ⟨0, ⋯⟩)) x) (Space.basis 1) +
(fderiv ℝ (fun x => magneticFieldMatrix c A t x (2, (fun i => i) ⟨0, ⋯⟩)) x) (Space.basis 2)x:Spacec:SpeedOfLightA:ElectromagneticPotentialhA:ContDiff ℝ 2 (A.val 3)t:Time⊢ -(fderiv ℝ (fun y => magneticFieldMatrix c A t y ((fun i => i) ⟨1, ⋯⟩ + 2 + 1, (fun i => i) ⟨1, ⋯⟩ + 2 + 2)) x)
(Space.basis ((fun i => i) ⟨1, ⋯⟩ + 1)) +
(fderiv ℝ (fun y => magneticFieldMatrix c A t y ((fun i => i) ⟨1, ⋯⟩ + 1 + 1, (fun i => i) ⟨1, ⋯⟩ + 1 + 2)) x)
(Space.basis ((fun i => i) ⟨1, ⋯⟩ + 2)) =
(fderiv ℝ (fun x => magneticFieldMatrix c A t x (0, (fun i => i) ⟨1, ⋯⟩)) x) (Space.basis 0) +
(fderiv ℝ (fun x => magneticFieldMatrix c A t x (1, (fun i => i) ⟨1, ⋯⟩)) x) (Space.basis 1) +
(fderiv ℝ (fun x => magneticFieldMatrix c A t x (2, (fun i => i) ⟨1, ⋯⟩)) x) (Space.basis 2)x:Spacec:SpeedOfLightA:ElectromagneticPotentialhA:ContDiff ℝ 2 (A.val 3)t:Time⊢ -(fderiv ℝ (fun y => magneticFieldMatrix c A t y ((fun i => i) ⟨2, ⋯⟩ + 2 + 1, (fun i => i) ⟨2, ⋯⟩ + 2 + 2)) x)
(Space.basis ((fun i => i) ⟨2, ⋯⟩ + 1)) +
(fderiv ℝ (fun y => magneticFieldMatrix c A t y ((fun i => i) ⟨2, ⋯⟩ + 1 + 1, (fun i => i) ⟨2, ⋯⟩ + 1 + 2)) x)
(Space.basis ((fun i => i) ⟨2, ⋯⟩ + 2)) =
(fderiv ℝ (fun x => magneticFieldMatrix c A t x (0, (fun i => i) ⟨2, ⋯⟩)) x) (Space.basis 0) +
(fderiv ℝ (fun x => magneticFieldMatrix c A t x (1, (fun i => i) ⟨2, ⋯⟩)) x) (Space.basis 1) +
(fderiv ℝ (fun x => magneticFieldMatrix c A t x (2, (fun i => i) ⟨2, ⋯⟩)) x) (Space.basis 2)
x:Spacec:SpeedOfLightA:ElectromagneticPotentialhA:ContDiff ℝ 2 (A.val 3)t:Time⊢ -(fderiv ℝ (fun y => magneticFieldMatrix c A t y ((fun i => i) ⟨2, ⋯⟩ + 2 + 1, (fun i => i) ⟨2, ⋯⟩ + 2 + 2)) x)
(Space.basis ((fun i => i) ⟨2, ⋯⟩ + 1)) +
(fderiv ℝ (fun y => magneticFieldMatrix c A t y ((fun i => i) ⟨2, ⋯⟩ + 1 + 1, (fun i => i) ⟨2, ⋯⟩ + 1 + 2)) x)
(Space.basis ((fun i => i) ⟨2, ⋯⟩ + 2)) =
(fderiv ℝ (fun x => magneticFieldMatrix c A t x (0, (fun i => i) ⟨2, ⋯⟩)) x) (Space.basis 0) +
(fderiv ℝ (fun x => magneticFieldMatrix c A t x (1, (fun i => i) ⟨2, ⋯⟩)) x) (Space.basis 1) +
(fderiv ℝ (fun x => magneticFieldMatrix c A t x (2, (fun i => i) ⟨2, ⋯⟩)) x) (Space.basis 2) x:Spacec:SpeedOfLightA:ElectromagneticPotentialhA:ContDiff ℝ 2 (A.val 3)t:Time⊢ -(fderiv ℝ (fun y => magneticFieldMatrix c A t y (2, 0)) x) (Space.basis 0) +
(fderiv ℝ (fun y => magneticFieldMatrix c A t y (1, 2)) x) (Space.basis 1) =
(fderiv ℝ (fun x => magneticFieldMatrix c A t x (0, 2)) x) (Space.basis 0) +
(fderiv ℝ (fun y => magneticFieldMatrix c A t y (1, 2)) x) (Space.basis 1)
conv_lhs =>
x✝:Spacec:SpeedOfLightA:ElectromagneticPotentialhA:ContDiff ℝ 2 (A.val 3)t:Timex:Space| magneticFieldMatrix c A t x (2, 0)
x✝:Spacec:SpeedOfLightA:ElectromagneticPotentialhA:ContDiff ℝ 2 (A.val 3)t:Timex:Space| -magneticFieldMatrix c A t x (0, 2)
All goals completed! 🐙C.3. Magnetic field matrix in terms of vector potentials
d:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:Differentiable ℝ A.valt:Timex:Space di:Fin dj:Fin d⊢ Space.deriv i (fun x => A.val ((toTimeAndSpace c).symm (t, x)) (Sum.inr j)) x =
Space.deriv i (fun x => ((timeSlice c) (fun x => WithLp.toLp 2 fun i => A.val x (Sum.inr i)) t x).ofLp j) xd:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:Differentiable ℝ A.valt:Timex:Space di:Fin dj:Fin d⊢ Differentiable ℝ fun y => A.val ((toTimeAndSpace c).symm (t, y))
d:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:Differentiable ℝ A.valt:Timex:Space di:Fin dj:Fin d⊢ Differentiable ℝ fun y => A.val ((toTimeAndSpace c).symm (t, y))
All goals completed! 🐙C.4. Smoothness of the magnetic field matrix
lemma magneticFieldMatrix_contDiff {n} {c : SpeedOfLight} (A : ElectromagneticPotential d)
(hA : ContDiff ℝ (n + 1) A) (ij) :
ContDiff ℝ n ↿(fun t x => A.magneticFieldMatrix c t x ij) := d:ℕn:WithTop ℕ∞c:SpeedOfLightA:ElectromagneticPotential dhA:ContDiff ℝ (n + 1) A.valij:Fin d × Fin d⊢ ContDiff ℝ n ↿fun t x => magneticFieldMatrix c A t x ij
All goals completed! 🐙lemma magneticFieldMatrix_space_contDiff {n} {c : SpeedOfLight} (A : ElectromagneticPotential d)
(hA : ContDiff ℝ (n + 1) A) (t : Time) (ij) :
ContDiff ℝ n (fun x => A.magneticFieldMatrix c t x ij) := d:ℕn:WithTop ℕ∞c:SpeedOfLightA:ElectromagneticPotential dhA:ContDiff ℝ (n + 1) A.valt:Timeij:Fin d × Fin d⊢ ContDiff ℝ n fun x => magneticFieldMatrix c A t x ij
exact (magneticFieldMatrix_contDiff A hA ij).comp (f := fun x => (t, x)) (d:ℕn:WithTop ℕ∞c:SpeedOfLightA:ElectromagneticPotential dhA:ContDiff ℝ (n + 1) A.valt:Timeij:Fin d × Fin d⊢ ContDiff ℝ n fun x => (t, x) All goals completed! 🐙)lemma magneticFieldMatrix_time_contDiff {n} {c : SpeedOfLight} (A : ElectromagneticPotential d)
(hA : ContDiff ℝ (n + 1) A) (x : Space d) (ij) :
ContDiff ℝ n (fun t => A.magneticFieldMatrix c t x ij) := d:ℕn:WithTop ℕ∞c:SpeedOfLightA:ElectromagneticPotential dhA:ContDiff ℝ (n + 1) A.valx:Space dij:Fin d × Fin d⊢ ContDiff ℝ n fun t => magneticFieldMatrix c A t x ij
exact (magneticFieldMatrix_contDiff A hA ij).comp (f := fun t => (t, x)) (d:ℕn:WithTop ℕ∞c:SpeedOfLightA:ElectromagneticPotential dhA:ContDiff ℝ (n + 1) A.valx:Space dij:Fin d × Fin d⊢ ContDiff ℝ n fun t => (t, x) All goals completed! 🐙)C.5. Differentiablity of the magnetic field matrix
lemma magneticFieldMatrix_differentiable {c : SpeedOfLight} (A : ElectromagneticPotential d)
(hA : ContDiff ℝ 2 A) (ij) : Differentiable ℝ ↿(fun t x => A.magneticFieldMatrix c t x ij) := d:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valij:Fin d × Fin d⊢ Differentiable ℝ ↿fun t x => magneticFieldMatrix c A t x ij
All goals completed! 🐙lemma magneticFieldMatrix_differentiable_space {c : SpeedOfLight} (A : ElectromagneticPotential d)
(hA : ContDiff ℝ 2 A) (t : Time) (ij) :
Differentiable ℝ (fun x => A.magneticFieldMatrix c t x ij) := d:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valt:Timeij:Fin d × Fin d⊢ Differentiable ℝ fun x => magneticFieldMatrix c A t x ij
exact (magneticFieldMatrix_differentiable A hA ij).comp (f := fun x => (t, x)) (d:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valt:Timeij:Fin d × Fin d⊢ Differentiable ℝ fun x => (t, x) All goals completed! 🐙)lemma magneticFieldMatrix_differentiable_time {c : SpeedOfLight} (A : ElectromagneticPotential d)
(hA : ContDiff ℝ 2 A) (x : Space d) (ij) :
Differentiable ℝ (fun t => A.magneticFieldMatrix c t x ij) := d:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valx:Space dij:Fin d × Fin d⊢ Differentiable ℝ fun t => magneticFieldMatrix c A t x ij
exact (magneticFieldMatrix_differentiable A hA ij).comp (f := fun t => (t, x)) (d:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valx:Space dij:Fin d × Fin d⊢ Differentiable ℝ fun t => (t, x) All goals completed! 🐙)C.6. Spatial derivative of the magnetic field matrix
d:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valt:Timex:Space di:Fin dj:Fin dk:Fin d⊢ (fun i_1 =>
Space.deriv j (Space.deriv k fun x => (vectorPotential c A t x).ofLp i) i_1 -
Space.deriv i (Space.deriv k fun x => (vectorPotential c A t x).ofLp j) i_1)
x =
(fun i_1 =>
Space.deriv j (Space.deriv i fun x => (vectorPotential c A t x).ofLp k) i_1 -
Space.deriv i (Space.deriv k fun x => (vectorPotential c A t x).ofLp j) i_1)
x -
(fun i_1 =>
Space.deriv j (Space.deriv i fun x => (vectorPotential c A t x).ofLp k) i_1 -
Space.deriv j (Space.deriv k fun x => (vectorPotential c A t x).ofLp i) i_1)
xd:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valt:Timex:Space di:Fin dj:Fin dk:Fin d⊢ Differentiable ℝ (Space.deriv i fun x => (vectorPotential c A t x).ofLp k)d:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valt:Timex:Space di:Fin dj:Fin dk:Fin d⊢ Differentiable ℝ (Space.deriv k fun x => (vectorPotential c A t x).ofLp i)d:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valt:Timex:Space di:Fin dj:Fin dk:Fin d⊢ Differentiable ℝ (Space.deriv j fun x => (vectorPotential c A t x).ofLp k)d:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valt:Timex:Space di:Fin dj:Fin dk:Fin d⊢ Differentiable ℝ (Space.deriv k fun x => (vectorPotential c A t x).ofLp j)d:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valt:Timex:Space di:Fin dj:Fin dk:Fin d⊢ Differentiable ℝ (Space.deriv j fun x => (vectorPotential c A t x).ofLp i)d:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valt:Timex:Space di:Fin dj:Fin dk:Fin d⊢ Differentiable ℝ (Space.deriv i fun x => (vectorPotential c A t x).ofLp j)
d:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valt:Timex:Space di:Fin dj:Fin dk:Fin d⊢ Differentiable ℝ (Space.deriv i fun x => (vectorPotential c A t x).ofLp k)d:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valt:Timex:Space di:Fin dj:Fin dk:Fin d⊢ Differentiable ℝ (Space.deriv k fun x => (vectorPotential c A t x).ofLp i)d:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valt:Timex:Space di:Fin dj:Fin dk:Fin d⊢ Differentiable ℝ (Space.deriv j fun x => (vectorPotential c A t x).ofLp k)d:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valt:Timex:Space di:Fin dj:Fin dk:Fin d⊢ Differentiable ℝ (Space.deriv k fun x => (vectorPotential c A t x).ofLp j)d:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valt:Timex:Space di:Fin dj:Fin dk:Fin d⊢ Differentiable ℝ (Space.deriv j fun x => (vectorPotential c A t x).ofLp i)d:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valt:Timex:Space di:Fin dj:Fin dk:Fin d⊢ Differentiable ℝ (Space.deriv i fun x => (vectorPotential c A t x).ofLp j)
all_goals
d:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valt:Timex:Space di:Fin dj:Fin dk:Fin d⊢ Differentiable ℝ (Space.deriv i fun x => (vectorPotential c A t x).ofLp j) d:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valt:Timex:Space di:Fin dj:Fin dk:Fin d⊢ ContDiff ℝ 2 fun x => (vectorPotential c A t x).ofLp j
All goals completed! 🐙C.7. Temporal derivative of the magnetic field matrix
d:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valt:Timex:Space di:Fin dj:Fin dhφ:ContDiff ℝ 2 (scalarPotential c A t)hd1:∀ (k : Fin d), DifferentiableAt ℝ (fun x => -(electricField c A t x).ofLp k) xhd2:∀ (k : Fin d), DifferentiableAt ℝ (Space.deriv k (scalarPotential c A t)) x⊢ -Space.deriv j (fun x => (electricField c A t x).ofLp i) x - Space.deriv i (Space.deriv j (scalarPotential c A t)) x -
(-Space.deriv i (fun x => (electricField c A t x).ofLp j) x -
Space.deriv i (Space.deriv j (scalarPotential c A t)) x) =
Space.deriv i (fun x => (electricField c A t x).ofLp j) x - Space.deriv j (fun x => (electricField c A t x).ofLp i) x
All goals completed! 🐙d:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:ContDiff ℝ 3 A.valt:Timex✝:Space di:Fin dj:Fin dx:Space d⊢ Differentiable ℝ fun t' => electricField c A t' x
All goals completed! 🐙)
| d:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:ContDiff ℝ 3 A.valt:Timex:Space di:Fin dj:Fin d⊢ DifferentiableAt ℝ (fun t => Space.deriv j (fun x => (electricField c A t x).ofLp i) x) t
| (d:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:ContDiff ℝ 3 A.valt:Timex:Space di:Fin dj:Fin d⊢ Differentiable ℝ fun t => Space.deriv j (fun x => (electricField c A t x).ofLp i) x
d:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:ContDiff ℝ 3 A.valt:Timex:Space di:Fin dj:Fin d⊢ ContDiff ℝ 2 ↿fun t x => (electricField c A t x).ofLp i
All goals completed! 🐙)
C.8. curl of the magnetic field matrix
d:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valt:Timex:Space di:Fin dj:Fin d⊢ Space.deriv j (fun x => magneticFieldMatrix c A t x (j, i)) x =
Space.deriv j
(fun y =>
(A.fieldStrengthMatrix ((toTimeAndSpace c).symm (((toTimeAndSpace c) ((toTimeAndSpace c).symm (t, x))).1, y)))
(Sum.inr j, Sum.inr i))
((toTimeAndSpace c) ((toTimeAndSpace c).symm (t, x))).2d:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valt:Timex:Space di:Fin dj:Fin d⊢ Differentiable ℝ fun x => (A.fieldStrengthMatrix x) (Sum.inr j, Sum.inr i)
d:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valt:Timex:Space di:Fin dj:Fin d⊢ Space.deriv j (fun x => magneticFieldMatrix c A t x (j, i)) x =
Space.deriv j (fun y => (A.fieldStrengthMatrix ((toTimeAndSpace c).symm (t, y))) (Sum.inr j, Sum.inr i)) xd:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valt:Timex:Space di:Fin dj:Fin d⊢ Differentiable ℝ fun x => (A.fieldStrengthMatrix x) (Sum.inr j, Sum.inr i)
d:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valt:Timex:Space di:Fin dj:Fin d⊢ Differentiable ℝ fun x => (A.fieldStrengthMatrix x) (Sum.inr j, Sum.inr i)
d:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valt:Timex:Space di:Fin dj:Fin d⊢ Differentiable ℝ fun x => (A.fieldStrengthMatrix x) (Sum.inr j, Sum.inr i) All goals completed! 🐙