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.Dynamics.Lagrangian

Extrema of the Lagrangian density

i. Overview

In this module we define what it means for an electromagnetic potential to be an extremum of the Lagrangian density in presence of a Lorentz current density.

This is equivalent to the electromagnetic potential satisfying Maxwell's equations with sources, i.e. Gauss's law and Ampère's law.

ii. Key results

    IsExtrema : The condition on an electromagnetic potential to be an extrema of the lagrangian.

    isExtrema_iff_gauss_ampere_magneticFieldMatrix : The electromagnetic potential is an extrema of the lagrangian if and only if Gauss's law and Ampère's law hold (in terms of the magnetic field matrix).

    time_deriv_time_deriv_magneticFieldMatrix_of_isExtrema : A wave-like equation for the magnetic field matrix from the extrema condition.

    time_deriv_time_deriv_electricField_of_isExtrema : A wave-like equation for the electric field from the extrema condition.

iii. Table of contents

    A. The condition for an extrema of the Lagrangian density

      A.1. Extrema condition in terms of the field strength matrix

      A.2. Extrema condition in terms of tensors

      A.3. Equivariance of the extrema condition

    B. Gauss's law and Ampère's law and the extrema condition

    C. Time derivatives from the extrema condition

    D. Second time derivatives from the extrema condition

      D.1. Second time derivatives of the magnetic field from the extrema condition

      D.2. Second time derivatives of the electric field from the extrema condition

iv. References

@[expose] public sectionattribute [-simp] Fintype.sum_sum_typeattribute [-simp] Nat.succ_eq_add_one

A. The condition for an extrema of the Lagrangian density

The condition on an electromagnetic potential to be an extrema of the lagrangian.

def IsExtrema {d} (𝓕 : FreeSpace) (A : ElectromagneticPotential d) (J : LorentzCurrentDensity d) : Prop := gradLagrangian 𝓕 A J = 0
lemma isExtrema_iff_gradLagrangian {𝓕 : FreeSpace} (A : ElectromagneticPotential d) (J : LorentzCurrentDensity d) : IsExtrema 𝓕 A J A.gradLagrangian 𝓕 J = 0 := d:𝓕:FreeSpaceA:ElectromagneticPotential dJ:LorentzCurrentDensity dIsExtrema 𝓕 A J gradLagrangian 𝓕 A J = 0 All goals completed! 🐙

A.1. Extrema condition in terms of the field strength matrix

d:𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff A.valJ:LorentzCurrentDensity dhJ:ContDiff J(∀ (x : SpaceTime d), ν, η ν ν (1 / 𝓕.μ₀ * μ, ∂_ μ (fun x => (A.fieldStrengthMatrix x) (μ, ν)) x - J x ν) Lorentz.Vector.basis ν = 0 x) (x : SpaceTime d) (ν : Fin 1 Fin d), μ, ∂_ μ (fun x => (A.fieldStrengthMatrix x) (μ, ν)) x = 𝓕.μ₀ * J x ν conv_lhs => d:𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff A.valJ:LorentzCurrentDensity dhJ:ContDiff Jx:SpaceTime dν:Fin 1 Fin d| η ν ν (1 / 𝓕.μ₀ * μ, ∂_ μ (fun x => (A.fieldStrengthMatrix x) (μ, ν)) x - J x ν) Lorentz.Vector.basis ν d:𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff A.valJ:LorentzCurrentDensity dhJ:ContDiff Jx:SpaceTime dν:Fin 1 Fin d| (η ν ν * (1 / 𝓕.μ₀ * μ, ∂_ μ (fun x => (A.fieldStrengthMatrix x) (μ, ν)) x - J x ν)) Lorentz.Vector.basis ν conv_lhs => d:𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff A.valJ:LorentzCurrentDensity dhJ:ContDiff Jx:SpaceTime d| ν, (η ν ν * (1 / 𝓕.μ₀ * μ, ∂_ μ (fun x => (A.fieldStrengthMatrix x) (μ, ν)) x - J x ν)) Lorentz.Vector.basis ν = 0 x d:𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff A.valJ:LorentzCurrentDensity dhJ:ContDiff Jx:SpaceTime d| x_1, (η x_1 x_1 * (𝓕.μ₀⁻¹ * μ, ∂_ μ (fun x => (A.fieldStrengthMatrix x) (μ, x_1)) x - J x x_1)) Lorentz.Vector.basis x_1 = 0 d:𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff A.valJ:LorentzCurrentDensity dhJ:ContDiff Jx:SpaceTime d| (μ : Fin 1 Fin d), η μ μ * (𝓕.μ₀⁻¹ * μ_1, ∂_ μ_1 (fun x => (A.fieldStrengthMatrix x) (μ_1, μ)) x - J x μ) = 0 d:𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff A.valJ:LorentzCurrentDensity dhJ:ContDiff J(∀ (x : SpaceTime d) (μ : Fin 1 Fin d), η μ μ * (𝓕.μ₀⁻¹ * μ_1, ∂_ μ_1 (fun x => (A.fieldStrengthMatrix x) (μ_1, μ)) x - J x μ) = 0) (x : SpaceTime d) (ν : Fin 1 Fin d), μ, ∂_ μ (fun x => (A.fieldStrengthMatrix x) (μ, ν)) x = 𝓕.μ₀ * J x νd:𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff A.valJ:LorentzCurrentDensity dhJ:ContDiff J(∀ (x : SpaceTime d) (ν : Fin 1 Fin d), μ, ∂_ μ (fun x => (A.fieldStrengthMatrix x) (μ, ν)) x = 𝓕.μ₀ * J x ν) (x : SpaceTime d) (μ : Fin 1 Fin d), η μ μ * (𝓕.μ₀⁻¹ * μ_1, ∂_ μ_1 (fun x => (A.fieldStrengthMatrix x) (μ_1, μ)) x - J x μ) = 0 d:𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff A.valJ:LorentzCurrentDensity dhJ:ContDiff J(∀ (x : SpaceTime d) (μ : Fin 1 Fin d), η μ μ * (𝓕.μ₀⁻¹ * μ_1, ∂_ μ_1 (fun x => (A.fieldStrengthMatrix x) (μ_1, μ)) x - J x μ) = 0) (x : SpaceTime d) (ν : Fin 1 Fin d), μ, ∂_ μ (fun x => (A.fieldStrengthMatrix x) (μ, ν)) x = 𝓕.μ₀ * J x ν d:𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff A.valJ:LorentzCurrentDensity dhJ:ContDiff Jh: (x : SpaceTime d) (μ : Fin 1 Fin d), η μ μ * (𝓕.μ₀⁻¹ * μ_1, ∂_ μ_1 (fun x => (A.fieldStrengthMatrix x) (μ_1, μ)) x - J x μ) = 0x:SpaceTime dν:Fin 1 Fin d μ, ∂_ μ (fun x => (A.fieldStrengthMatrix x) (μ, ν)) x = 𝓕.μ₀ * J x ν d:𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff A.valJ:LorentzCurrentDensity dhJ:ContDiff Jx:SpaceTime dν:Fin 1 Fin dh:η ν ν * (𝓕.μ₀⁻¹ * μ, ∂_ μ (fun x => (A.fieldStrengthMatrix x) (μ, ν)) x - J x ν) = 0 μ, ∂_ μ (fun x => (A.fieldStrengthMatrix x) (μ, ν)) x = 𝓕.μ₀ * J x ν d:𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff A.valJ:LorentzCurrentDensity dhJ:ContDiff Jx:SpaceTime dν:Fin 1 Fin dh:η ν ν = 0 𝓕.μ₀⁻¹ * μ, ∂_ μ (fun x => (A.fieldStrengthMatrix x) (μ, ν)) x - J x ν = 0 μ, ∂_ μ (fun x => (A.fieldStrengthMatrix x) (μ, ν)) x = 𝓕.μ₀ * J x ν d:𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff A.valJ:LorentzCurrentDensity dhJ:ContDiff Jx:SpaceTime dν:Fin 1 Fin dh:η ν ν = 0 𝓕.μ₀⁻¹ * μ, ∂_ μ (fun x => (A.fieldStrengthMatrix x) (μ, ν)) x - J x ν = 0h':η ν ν 0 μ, ∂_ μ (fun x => (A.fieldStrengthMatrix x) (μ, ν)) x = 𝓕.μ₀ * J x ν d:𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff A.valJ:LorentzCurrentDensity dhJ:ContDiff Jx:SpaceTime dν:Fin 1 Fin dh:𝓕.μ₀⁻¹ * μ, ∂_ μ (fun x => (A.fieldStrengthMatrix x) (μ, ν)) x - J x ν = 0h':¬η ν ν = 0 μ, ∂_ μ (fun x => (A.fieldStrengthMatrix x) (μ, ν)) x = 𝓕.μ₀ * J x ν linear_combination (norm := d:𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff A.valJ:LorentzCurrentDensity dhJ:ContDiff Jx:SpaceTime dν:Fin 1 Fin dh:𝓕.μ₀⁻¹ * μ, ∂_ μ (fun x => (A.fieldStrengthMatrix x) (μ, ν)) x - J x ν = 0h':¬η ν ν = 0 μ, ∂_ μ (fun x => (A.fieldStrengthMatrix x) (μ, ν)) x + 𝓕.μ₀ * 0 - (𝓕.μ₀ * J x ν + ( μ, ∂_ μ (fun x => (A.fieldStrengthMatrix x) (μ, ν)) x - 𝓕.μ₀ * J x ν)) = 0) 𝓕.μ₀ * h All goals completed! 🐙 d:𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff A.valJ:LorentzCurrentDensity dhJ:ContDiff J(∀ (x : SpaceTime d) (ν : Fin 1 Fin d), μ, ∂_ μ (fun x => (A.fieldStrengthMatrix x) (μ, ν)) x = 𝓕.μ₀ * J x ν) (x : SpaceTime d) (μ : Fin 1 Fin d), η μ μ * (𝓕.μ₀⁻¹ * μ_1, ∂_ μ_1 (fun x => (A.fieldStrengthMatrix x) (μ_1, μ)) x - J x μ) = 0 d:𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff A.valJ:LorentzCurrentDensity dhJ:ContDiff Jh: (x : SpaceTime d) (ν : Fin 1 Fin d), μ, ∂_ μ (fun x => (A.fieldStrengthMatrix x) (μ, ν)) x = 𝓕.μ₀ * J x νx:SpaceTime dν:Fin 1 Fin dη ν ν * (𝓕.μ₀⁻¹ * μ, ∂_ μ (fun x => (A.fieldStrengthMatrix x) (μ, ν)) x - J x ν) = 0 d:𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff A.valJ:LorentzCurrentDensity dhJ:ContDiff Jx:SpaceTime dν:Fin 1 Fin dh: μ, ∂_ μ (fun x => (A.fieldStrengthMatrix x) (μ, ν)) x = 𝓕.μ₀ * J x νη ν ν * (𝓕.μ₀⁻¹ * μ, ∂_ μ (fun x => (A.fieldStrengthMatrix x) (μ, ν)) x - J x ν) = 0 d:𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff A.valJ:LorentzCurrentDensity dhJ:ContDiff Jx:SpaceTime dν:Fin 1 Fin dh: μ, ∂_ μ (fun x => (A.fieldStrengthMatrix x) (μ, ν)) x = 𝓕.μ₀ * J x νη ν ν = 0 𝓕.μ₀⁻¹ * μ, ∂_ μ (fun x => (A.fieldStrengthMatrix x) (μ, ν)) x - J x ν = 0 d:𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff A.valJ:LorentzCurrentDensity dhJ:ContDiff Jx:SpaceTime dν:Fin 1 Fin dh: μ, ∂_ μ (fun x => (A.fieldStrengthMatrix x) (μ, ν)) x = 𝓕.μ₀ * J x ν𝓕.μ₀⁻¹ * μ, ∂_ μ (fun x => (A.fieldStrengthMatrix x) (μ, ν)) x - J x ν = 0 linear_combination (norm := d:𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff A.valJ:LorentzCurrentDensity dhJ:ContDiff Jx:SpaceTime dν:Fin 1 Fin dh: μ, ∂_ μ (fun x => (A.fieldStrengthMatrix x) (μ, ν)) x = 𝓕.μ₀ * J x ν μ, ∂_ μ (fun x => (A.fieldStrengthMatrix x) (μ, ν)) x - 𝓕.μ₀ * J x ν + 𝓕.μ₀ * J x ν - (𝓕.μ₀ * 0 + μ, ∂_ μ (fun x => (A.fieldStrengthMatrix x) (μ, ν)) x) = 𝓕.μ₀ * 0) 𝓕.μ₀⁻¹ * h All goals completed! 🐙

A.2. Extrema condition in terms of tensors

The electromagnetic potential is an exterma of the lagrangian if and only if

$$\frac{1}{\mu_0} \partial_\mu F^{\mu \nu} - J^{\nu} = 0.$$

attribute [-simp] Nat.reduceAdd Nat.reduceSucc Fin.isValued:𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff A.valJ:LorentzCurrentDensity dhJ:ContDiff Jh: (x : SpaceTime d), (contrT 1 0 1 ) (Tensorial.toTensor ((1 / 𝓕.μ₀) tensorDeriv A.toFieldStrength x)) + (permT ![0] ) (-Tensorial.toTensor (J x)) = 0x:SpaceTime dν:Fin 1 Fin dη ν ν * Tensorial.toTensor.symm ((permT id ) 0) ν = 0 x ν All goals completed! 🐙

A.3. Equivariance of the extrema condition

If A is an extrema of the lagrangian with current density J, then the Lorentz transformation Λ • A (Λ⁻¹ • x) is an extrema of the lagrangian with current density Λ • J (Λ⁻¹ • x).

Combined with time_deriv_time_deriv_electricField_of_isExtrema, this shows that the speed with which an electromagnetic wave propagates is invariant under Lorentz transformations.

d:𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff A.valJ:LorentzCurrentDensity dhJ:ContDiff JΛ:(LorentzGroup d)x:SpaceTime dh:𝓕.μ₀⁻¹ (contrT 1 0 1 ) (Tensorial.toTensor (tensorDeriv A.toFieldStrength (Λ⁻¹ x))) + -(permT ![0] ) (Tensorial.toTensor (J (Λ⁻¹ x))) = 0Λ 0 = 0 All goals completed! 🐙 d:𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff A.valJ:LorentzCurrentDensity dhJ:ContDiff JΛ:(LorentzGroup d)ContDiff (Λ A).val d:𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff A.valJ:LorentzCurrentDensity dhJ:ContDiff JΛ:(LorentzGroup d)ContDiff ((actionCLM Λ) A.val (actionCLM Λ⁻¹)) d:𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff A.valJ:LorentzCurrentDensity dhJ:ContDiff JΛ:(LorentzGroup d)ContDiff (actionCLM Λ)d:𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff A.valJ:LorentzCurrentDensity dhJ:ContDiff JΛ:(LorentzGroup d)ContDiff (A.val (actionCLM Λ⁻¹)) d:𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff A.valJ:LorentzCurrentDensity dhJ:ContDiff JΛ:(LorentzGroup d)ContDiff (actionCLM Λ) All goals completed! 🐙 d:𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff A.valJ:LorentzCurrentDensity dhJ:ContDiff JΛ:(LorentzGroup d)ContDiff (A.val (actionCLM Λ⁻¹)) d:𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff A.valJ:LorentzCurrentDensity dhJ:ContDiff JΛ:(LorentzGroup d)ContDiff A.vald:𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff A.valJ:LorentzCurrentDensity dhJ:ContDiff JΛ:(LorentzGroup d)ContDiff (actionCLM Λ⁻¹) d:𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff A.valJ:LorentzCurrentDensity dhJ:ContDiff JΛ:(LorentzGroup d)ContDiff A.val All goals completed! 🐙 d:𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff A.valJ:LorentzCurrentDensity dhJ:ContDiff JΛ:(LorentzGroup d)ContDiff (actionCLM Λ⁻¹) All goals completed! 🐙 d:𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff A.valJ:LorentzCurrentDensity dhJ:ContDiff JΛ:(LorentzGroup d)ContDiff fun x => Λ J (Λ⁻¹ x) d:𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff A.valJ:LorentzCurrentDensity dhJ:ContDiff JΛ:(LorentzGroup d)ContDiff ((actionCLM Λ) J (actionCLM Λ⁻¹)) d:𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff A.valJ:LorentzCurrentDensity dhJ:ContDiff JΛ:(LorentzGroup d)ContDiff (actionCLM Λ)d:𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff A.valJ:LorentzCurrentDensity dhJ:ContDiff JΛ:(LorentzGroup d)ContDiff (J (actionCLM Λ⁻¹)) d:𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff A.valJ:LorentzCurrentDensity dhJ:ContDiff JΛ:(LorentzGroup d)ContDiff (actionCLM Λ) All goals completed! 🐙 d:𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff A.valJ:LorentzCurrentDensity dhJ:ContDiff JΛ:(LorentzGroup d)ContDiff (J (actionCLM Λ⁻¹)) d:𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff A.valJ:LorentzCurrentDensity dhJ:ContDiff JΛ:(LorentzGroup d)ContDiff Jd:𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff A.valJ:LorentzCurrentDensity dhJ:ContDiff JΛ:(LorentzGroup d)ContDiff (actionCLM Λ⁻¹) d:𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff A.valJ:LorentzCurrentDensity dhJ:ContDiff JΛ:(LorentzGroup d)ContDiff J All goals completed! 🐙 d:𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff A.valJ:LorentzCurrentDensity dhJ:ContDiff JΛ:(LorentzGroup d)ContDiff (actionCLM Λ⁻¹) All goals completed! 🐙

B. Gauss's law and Ampère's law and the extrema condition

d:𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff A.valJ:LorentzCurrentDensity dhJ:ContDiff J(∀ (x : SpaceTime d), gradLagrangian 𝓕 A J x = 0 x) (t : Time) (x : Space d), Space.div (electricField 𝓕.c A t) x = LorentzCurrentDensity.chargeDensity 𝓕.c J t x / 𝓕.ε₀ (i : Fin d), 𝓕.μ₀ * 𝓕.ε₀ * (∂ₜ (fun t => electricField 𝓕.c A t x) t).ofLp i = j, Space.deriv j (fun x => magneticFieldMatrix 𝓕.c A t x (j, i)) x - 𝓕.μ₀ * (LorentzCurrentDensity.currentDensity 𝓕.c J t x).ofLp i conv_lhs => d:𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff A.valJ:LorentzCurrentDensity dhJ:ContDiff Jx:SpaceTime d| gradLagrangian 𝓕 A J x = 0 x d:𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff A.valJ:LorentzCurrentDensity dhJ:ContDiff Jx:SpaceTime d| (1 / (𝓕.μ₀ * 𝓕.c.val) * Space.div (electricField 𝓕.c A ((time 𝓕.c) x)) (space x) + -𝓕.c.val * LorentzCurrentDensity.chargeDensity 𝓕.c J ((time 𝓕.c) x) (space x)) Lorentz.Vector.basis (Sum.inl 0) + i, (𝓕.μ₀⁻¹ * (𝓕.ε₀ * 𝓕.μ₀ * (∂ₜ (fun x_1 => electricField 𝓕.c A x_1 (space x)) ((time 𝓕.c) x)).ofLp i - j, Space.deriv j (fun x_1 => magneticFieldMatrix 𝓕.c A ((time 𝓕.c) x) x_1 (j, i)) (space x)) + (LorentzCurrentDensity.currentDensity 𝓕.c J ((time 𝓕.c) x) (space x)).ofLp i) Lorentz.Vector.basis (Sum.inr i) = 0 x d:𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff A.valJ:LorentzCurrentDensity dhJ:ContDiff Jx:SpaceTime d| (1 / (𝓕.μ₀ * 𝓕.c.val) * Space.div (electricField 𝓕.c A ((time 𝓕.c) x)) (space x) + -𝓕.c.val * LorentzCurrentDensity.chargeDensity 𝓕.c J ((time 𝓕.c) x) (space x)) Lorentz.Vector.basis (Sum.inl 0) + x_1, (𝓕.μ₀⁻¹ * (𝓕.ε₀ * 𝓕.μ₀ * (∂ₜ (fun x_2 => electricField 𝓕.c A x_2 (space x)) ((time 𝓕.c) x)).ofLp x_1 - j, Space.deriv j (fun x_2 => magneticFieldMatrix 𝓕.c A ((time 𝓕.c) x) x_2 (j, x_1)) (space x)) + (LorentzCurrentDensity.currentDensity 𝓕.c J ((time 𝓕.c) x) (space x)).ofLp x_1) Lorentz.Vector.basis (Sum.inr x_1) = 0 d:𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff A.valJ:LorentzCurrentDensity dhJ:ContDiff Jx:SpaceTime d| 1 / (𝓕.μ₀ * 𝓕.c.val) * Space.div (electricField 𝓕.c A ((time 𝓕.c) x)) (space x) + -𝓕.c.val * LorentzCurrentDensity.chargeDensity 𝓕.c J ((time 𝓕.c) x) (space x) = 0 (i : Fin d), 𝓕.μ₀⁻¹ * (𝓕.ε₀ * 𝓕.μ₀ * (∂ₜ (fun x_1 => electricField 𝓕.c A x_1 (space x)) ((time 𝓕.c) x)).ofLp i - j, Space.deriv j (fun x_1 => magneticFieldMatrix 𝓕.c A ((time 𝓕.c) x) x_1 (j, i)) (space x)) + (LorentzCurrentDensity.currentDensity 𝓕.c J ((time 𝓕.c) x) (space x)).ofLp i = 0 d:𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff A.valJ:LorentzCurrentDensity dhJ:ContDiff J((∀ (x : SpaceTime d), 1 / (𝓕.μ₀ * 𝓕.c.val) * Space.div (electricField 𝓕.c A ((time 𝓕.c) x)) (space x) + -𝓕.c.val * LorentzCurrentDensity.chargeDensity 𝓕.c J ((time 𝓕.c) x) (space x) = 0) (x : SpaceTime d) (i : Fin d), 𝓕.μ₀⁻¹ * (𝓕.ε₀ * 𝓕.μ₀ * (∂ₜ (fun x_1 => electricField 𝓕.c A x_1 (space x)) ((time 𝓕.c) x)).ofLp i - j, Space.deriv j (fun x_1 => magneticFieldMatrix 𝓕.c A ((time 𝓕.c) x) x_1 (j, i)) (space x)) + (LorentzCurrentDensity.currentDensity 𝓕.c J ((time 𝓕.c) x) (space x)).ofLp i = 0) (∀ (x : Time) (x_1 : Space d), Space.div (electricField 𝓕.c A x) x_1 = LorentzCurrentDensity.chargeDensity 𝓕.c J x x_1 / 𝓕.ε₀) (x : Time) (x_1 : Space d) (i : Fin d), 𝓕.μ₀ * 𝓕.ε₀ * (∂ₜ (fun t => electricField 𝓕.c A t x_1) x).ofLp i = j, Space.deriv j (fun x_2 => magneticFieldMatrix 𝓕.c A x x_2 (j, i)) x_1 - 𝓕.μ₀ * (LorentzCurrentDensity.currentDensity 𝓕.c J x x_1).ofLp i d:𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff A.valJ:LorentzCurrentDensity dhJ:ContDiff J(∀ (x : SpaceTime d), 1 / (𝓕.μ₀ * 𝓕.c.val) * Space.div (electricField 𝓕.c A ((time 𝓕.c) x)) (space x) + -𝓕.c.val * LorentzCurrentDensity.chargeDensity 𝓕.c J ((time 𝓕.c) x) (space x) = 0) (x : Time) (x_1 : Space d), Space.div (electricField 𝓕.c A x) x_1 = LorentzCurrentDensity.chargeDensity 𝓕.c J x x_1 / 𝓕.ε₀d:𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff A.valJ:LorentzCurrentDensity dhJ:ContDiff J(∀ (x : SpaceTime d) (i : Fin d), 𝓕.μ₀⁻¹ * (𝓕.ε₀ * 𝓕.μ₀ * (∂ₜ (fun x_1 => electricField 𝓕.c A x_1 (space x)) ((time 𝓕.c) x)).ofLp i - j, Space.deriv j (fun x_1 => magneticFieldMatrix 𝓕.c A ((time 𝓕.c) x) x_1 (j, i)) (space x)) + (LorentzCurrentDensity.currentDensity 𝓕.c J ((time 𝓕.c) x) (space x)).ofLp i = 0) (x : Time) (x_1 : Space d) (i : Fin d), 𝓕.μ₀ * 𝓕.ε₀ * (∂ₜ (fun t => electricField 𝓕.c A t x_1) x).ofLp i = j, Space.deriv j (fun x_2 => magneticFieldMatrix 𝓕.c A x x_2 (j, i)) x_1 - 𝓕.μ₀ * (LorentzCurrentDensity.currentDensity 𝓕.c J x x_1).ofLp i d:𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff A.valJ:LorentzCurrentDensity dhJ:ContDiff J(∀ (x : SpaceTime d), 1 / (𝓕.μ₀ * 𝓕.c.val) * Space.div (electricField 𝓕.c A ((time 𝓕.c) x)) (space x) + -𝓕.c.val * LorentzCurrentDensity.chargeDensity 𝓕.c J ((time 𝓕.c) x) (space x) = 0) (x : Time) (x_1 : Space d), Space.div (electricField 𝓕.c A x) x_1 = LorentzCurrentDensity.chargeDensity 𝓕.c J x x_1 / 𝓕.ε₀ d:𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff A.valJ:LorentzCurrentDensity dhJ:ContDiff J(∀ (x : SpaceTime d), 1 / (𝓕.μ₀ * 𝓕.c.val) * Space.div (electricField 𝓕.c A ((time 𝓕.c) x)) (space x) + -𝓕.c.val * LorentzCurrentDensity.chargeDensity 𝓕.c J ((time 𝓕.c) x) (space x) = 0) (x : Time) (x_1 : Space d), Space.div (electricField 𝓕.c A x) x_1 = LorentzCurrentDensity.chargeDensity 𝓕.c J x x_1 / 𝓕.ε₀d:𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff A.valJ:LorentzCurrentDensity dhJ:ContDiff J(∀ (x : Time) (x_1 : Space d), Space.div (electricField 𝓕.c A x) x_1 = LorentzCurrentDensity.chargeDensity 𝓕.c J x x_1 / 𝓕.ε₀) (x : SpaceTime d), 1 / (𝓕.μ₀ * 𝓕.c.val) * Space.div (electricField 𝓕.c A ((time 𝓕.c) x)) (space x) + -𝓕.c.val * LorentzCurrentDensity.chargeDensity 𝓕.c J ((time 𝓕.c) x) (space x) = 0 d:𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff A.valJ:LorentzCurrentDensity dhJ:ContDiff J(∀ (x : SpaceTime d), 1 / (𝓕.μ₀ * 𝓕.c.val) * Space.div (electricField 𝓕.c A ((time 𝓕.c) x)) (space x) + -𝓕.c.val * LorentzCurrentDensity.chargeDensity 𝓕.c J ((time 𝓕.c) x) (space x) = 0) (x : Time) (x_1 : Space d), Space.div (electricField 𝓕.c A x) x_1 = LorentzCurrentDensity.chargeDensity 𝓕.c J x x_1 / 𝓕.ε₀ d:𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff A.valJ:LorentzCurrentDensity dhJ:ContDiff Jh: (x : SpaceTime d), 1 / (𝓕.μ₀ * 𝓕.c.val) * Space.div (electricField 𝓕.c A ((time 𝓕.c) x)) (space x) + -𝓕.c.val * LorentzCurrentDensity.chargeDensity 𝓕.c J ((time 𝓕.c) x) (space x) = 0t:Timex:Space dSpace.div (electricField 𝓕.c A t) x = LorentzCurrentDensity.chargeDensity 𝓕.c J t x / 𝓕.ε₀ d:𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff A.valJ:LorentzCurrentDensity dhJ:ContDiff Jt:Timex:Space dh:1 / (𝓕.μ₀ * 𝓕.c.val) * Space.div (electricField 𝓕.c A ((time 𝓕.c) ((toTimeAndSpace 𝓕.c).symm (t, x)))) (space ((toTimeAndSpace 𝓕.c).symm (t, x))) + -𝓕.c.val * LorentzCurrentDensity.chargeDensity 𝓕.c J ((time 𝓕.c) ((toTimeAndSpace 𝓕.c).symm (t, x))) (space ((toTimeAndSpace 𝓕.c).symm (t, x))) = 0Space.div (electricField 𝓕.c A t) x = LorentzCurrentDensity.chargeDensity 𝓕.c J t x / 𝓕.ε₀ d:𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff A.valJ:LorentzCurrentDensity dhJ:ContDiff Jt:Timex:Space dh:𝓕.c.val⁻¹ * 𝓕.μ₀⁻¹ * Space.div (electricField 𝓕.c A t) x + -(𝓕.c.val * LorentzCurrentDensity.chargeDensity 𝓕.c J t x) = 0Space.div (electricField 𝓕.c A t) x = LorentzCurrentDensity.chargeDensity 𝓕.c J t x / 𝓕.ε₀ linear_combination (norm := d:𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff A.valJ:LorentzCurrentDensity dhJ:ContDiff Jt:Timex:Space dh:𝓕.c.val⁻¹ * 𝓕.μ₀⁻¹ * Space.div (electricField 𝓕.c A t) x + -(𝓕.c.val * LorentzCurrentDensity.chargeDensity 𝓕.c J t x) = 0Space.div (electricField 𝓕.c A t) x - (LorentzCurrentDensity.chargeDensity 𝓕.c J t x / 𝓕.ε₀ + 𝓕.μ₀ * 𝓕.c.val * (𝓕.c.val⁻¹ * 𝓕.μ₀⁻¹ * Space.div (electricField 𝓕.c A t) x + -(𝓕.c.val * LorentzCurrentDensity.chargeDensity 𝓕.c J t x))) = 0) (𝓕.μ₀ * 𝓕.c) * h d:𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff A.valJ:LorentzCurrentDensity dhJ:ContDiff Jt:Timex:Space dh:𝓕.c.val⁻¹ * 𝓕.μ₀⁻¹ * Space.div (electricField 𝓕.c A t) x + -(𝓕.c.val * LorentzCurrentDensity.chargeDensity 𝓕.c J t x) = 0Space.div (electricField 𝓕.c A t) x * 𝓕.ε₀ - (LorentzCurrentDensity.chargeDensity 𝓕.c J t x + 𝓕.ε₀ * (Space.div (electricField 𝓕.c A t) x + -(LorentzCurrentDensity.chargeDensity 𝓕.c J t x * 𝓕.μ₀ * 𝓕.c.val ^ 2))) = 𝓕.ε₀ * 0 d:𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff A.valJ:LorentzCurrentDensity dhJ:ContDiff Jt:Timex:Space dh:𝓕.c.val⁻¹ * 𝓕.μ₀⁻¹ * Space.div (electricField 𝓕.c A t) x + -(𝓕.c.val * LorentzCurrentDensity.chargeDensity 𝓕.c J t x) = 0Space.div (electricField 𝓕.c A t) x * 𝓕.ε₀ - (LorentzCurrentDensity.chargeDensity 𝓕.c J t x + 𝓕.ε₀ * (Space.div (electricField 𝓕.c A t) x + -(LorentzCurrentDensity.chargeDensity 𝓕.c J t x * 𝓕.μ₀ * (𝓕.μ₀⁻¹ * 𝓕.ε₀⁻¹)))) = 0 d:𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff A.valJ:LorentzCurrentDensity dhJ:ContDiff Jt:Timex:Space dh:𝓕.c.val⁻¹ * 𝓕.μ₀⁻¹ * Space.div (electricField 𝓕.c A t) x + -(𝓕.c.val * LorentzCurrentDensity.chargeDensity 𝓕.c J t x) = 0Space.div (electricField 𝓕.c A t) x * 𝓕.ε₀ - (LorentzCurrentDensity.chargeDensity 𝓕.c J t x + (Space.div (electricField 𝓕.c A t) x * 𝓕.ε₀ + -LorentzCurrentDensity.chargeDensity 𝓕.c J t x)) = 0 All goals completed! 🐙 d:𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff A.valJ:LorentzCurrentDensity dhJ:ContDiff J(∀ (x : Time) (x_1 : Space d), Space.div (electricField 𝓕.c A x) x_1 = LorentzCurrentDensity.chargeDensity 𝓕.c J x x_1 / 𝓕.ε₀) (x : SpaceTime d), 1 / (𝓕.μ₀ * 𝓕.c.val) * Space.div (electricField 𝓕.c A ((time 𝓕.c) x)) (space x) + -𝓕.c.val * LorentzCurrentDensity.chargeDensity 𝓕.c J ((time 𝓕.c) x) (space x) = 0 d:𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff A.valJ:LorentzCurrentDensity dhJ:ContDiff Jh: (x : Time) (x_1 : Space d), Space.div (electricField 𝓕.c A x) x_1 = LorentzCurrentDensity.chargeDensity 𝓕.c J x x_1 / 𝓕.ε₀x:SpaceTime d1 / (𝓕.μ₀ * 𝓕.c.val) * Space.div (electricField 𝓕.c A ((time 𝓕.c) x)) (space x) + -𝓕.c.val * LorentzCurrentDensity.chargeDensity 𝓕.c J ((time 𝓕.c) x) (space x) = 0 d:𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff A.valJ:LorentzCurrentDensity dhJ:ContDiff Jx:SpaceTime dh:Space.div (electricField 𝓕.c A ((time 𝓕.c) x)) (space x) = LorentzCurrentDensity.chargeDensity 𝓕.c J ((time 𝓕.c) x) (space x) / 𝓕.ε₀1 / (𝓕.μ₀ * 𝓕.c.val) * Space.div (electricField 𝓕.c A ((time 𝓕.c) x)) (space x) + -𝓕.c.val * LorentzCurrentDensity.chargeDensity 𝓕.c J ((time 𝓕.c) x) (space x) = 0 linear_combination (norm := d:𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff A.valJ:LorentzCurrentDensity dhJ:ContDiff Jx:SpaceTime dh:Space.div (electricField 𝓕.c A ((time 𝓕.c) x)) (space x) = LorentzCurrentDensity.chargeDensity 𝓕.c J ((time 𝓕.c) x) (space x) / 𝓕.ε₀𝓕.c.val⁻¹ * 𝓕.μ₀⁻¹ * Space.div (electricField 𝓕.c A ((time 𝓕.c) x)) (space x) + -(𝓕.c.val * LorentzCurrentDensity.chargeDensity 𝓕.c J ((time 𝓕.c) x) (space x)) + 𝓕.μ₀⁻¹ * 𝓕.c.val⁻¹ * (LorentzCurrentDensity.chargeDensity 𝓕.c J ((time 𝓕.c) x) (space x) / 𝓕.ε₀) - 𝓕.μ₀⁻¹ * 𝓕.c.val⁻¹ * Space.div (electricField 𝓕.c A ((time 𝓕.c) x)) (space x) = 0) (𝓕.μ₀⁻¹ * 𝓕.c⁻¹) * h d:𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff A.valJ:LorentzCurrentDensity dhJ:ContDiff Jx:SpaceTime dh:Space.div (electricField 𝓕.c A ((time 𝓕.c) x)) (space x) = LorentzCurrentDensity.chargeDensity 𝓕.c J ((time 𝓕.c) x) (space x) / 𝓕.ε₀(Space.div (electricField 𝓕.c A ((time 𝓕.c) x)) (space x) + -(𝓕.c.val ^ 2 * 𝓕.μ₀ * LorentzCurrentDensity.chargeDensity 𝓕.c J ((time 𝓕.c) x) (space x))) * 𝓕.ε₀ + LorentzCurrentDensity.chargeDensity 𝓕.c J ((time 𝓕.c) x) (space x) - Space.div (electricField 𝓕.c A ((time 𝓕.c) x)) (space x) * 𝓕.ε₀ = 𝓕.c.val * 𝓕.μ₀ * 𝓕.ε₀ * 0 d:𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff A.valJ:LorentzCurrentDensity dhJ:ContDiff Jx:SpaceTime dh:Space.div (electricField 𝓕.c A ((time 𝓕.c) x)) (space x) = LorentzCurrentDensity.chargeDensity 𝓕.c J ((time 𝓕.c) x) (space x) / 𝓕.ε₀(Space.div (electricField 𝓕.c A ((time 𝓕.c) x)) (space x) + -(𝓕.μ₀⁻¹ * 𝓕.ε₀⁻¹ * 𝓕.μ₀ * LorentzCurrentDensity.chargeDensity 𝓕.c J ((time 𝓕.c) x) (space x))) * 𝓕.ε₀ + LorentzCurrentDensity.chargeDensity 𝓕.c J ((time 𝓕.c) x) (space x) - Space.div (electricField 𝓕.c A ((time 𝓕.c) x)) (space x) * 𝓕.ε₀ = 0 d:𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff A.valJ:LorentzCurrentDensity dhJ:ContDiff Jx:SpaceTime dh:Space.div (electricField 𝓕.c A ((time 𝓕.c) x)) (space x) = LorentzCurrentDensity.chargeDensity 𝓕.c J ((time 𝓕.c) x) (space x) / 𝓕.ε₀Space.div (electricField 𝓕.c A ((time 𝓕.c) x)) (space x) * 𝓕.ε₀ + -LorentzCurrentDensity.chargeDensity 𝓕.c J ((time 𝓕.c) x) (space x) + LorentzCurrentDensity.chargeDensity 𝓕.c J ((time 𝓕.c) x) (space x) - Space.div (electricField 𝓕.c A ((time 𝓕.c) x)) (space x) * 𝓕.ε₀ = 0 All goals completed! 🐙 d:𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff A.valJ:LorentzCurrentDensity dhJ:ContDiff J(∀ (x : SpaceTime d) (i : Fin d), 𝓕.μ₀⁻¹ * (𝓕.ε₀ * 𝓕.μ₀ * (∂ₜ (fun x_1 => electricField 𝓕.c A x_1 (space x)) ((time 𝓕.c) x)).ofLp i - j, Space.deriv j (fun x_1 => magneticFieldMatrix 𝓕.c A ((time 𝓕.c) x) x_1 (j, i)) (space x)) + (LorentzCurrentDensity.currentDensity 𝓕.c J ((time 𝓕.c) x) (space x)).ofLp i = 0) (x : Time) (x_1 : Space d) (i : Fin d), 𝓕.μ₀ * 𝓕.ε₀ * (∂ₜ (fun t => electricField 𝓕.c A t x_1) x).ofLp i = j, Space.deriv j (fun x_2 => magneticFieldMatrix 𝓕.c A x x_2 (j, i)) x_1 - 𝓕.μ₀ * (LorentzCurrentDensity.currentDensity 𝓕.c J x x_1).ofLp i d:𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff A.valJ:LorentzCurrentDensity dhJ:ContDiff J(∀ (x : SpaceTime d) (i : Fin d), 𝓕.μ₀⁻¹ * (𝓕.ε₀ * 𝓕.μ₀ * (∂ₜ (fun x_1 => electricField 𝓕.c A x_1 (space x)) ((time 𝓕.c) x)).ofLp i - j, Space.deriv j (fun x_1 => magneticFieldMatrix 𝓕.c A ((time 𝓕.c) x) x_1 (j, i)) (space x)) + (LorentzCurrentDensity.currentDensity 𝓕.c J ((time 𝓕.c) x) (space x)).ofLp i = 0) (x : Time) (x_1 : Space d) (i : Fin d), 𝓕.μ₀ * 𝓕.ε₀ * (∂ₜ (fun t => electricField 𝓕.c A t x_1) x).ofLp i = j, Space.deriv j (fun x_2 => magneticFieldMatrix 𝓕.c A x x_2 (j, i)) x_1 - 𝓕.μ₀ * (LorentzCurrentDensity.currentDensity 𝓕.c J x x_1).ofLp id:𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff A.valJ:LorentzCurrentDensity dhJ:ContDiff J(∀ (x : Time) (x_1 : Space d) (i : Fin d), 𝓕.μ₀ * 𝓕.ε₀ * (∂ₜ (fun t => electricField 𝓕.c A t x_1) x).ofLp i = j, Space.deriv j (fun x_2 => magneticFieldMatrix 𝓕.c A x x_2 (j, i)) x_1 - 𝓕.μ₀ * (LorentzCurrentDensity.currentDensity 𝓕.c J x x_1).ofLp i) (x : SpaceTime d) (i : Fin d), 𝓕.μ₀⁻¹ * (𝓕.ε₀ * 𝓕.μ₀ * (∂ₜ (fun x_1 => electricField 𝓕.c A x_1 (space x)) ((time 𝓕.c) x)).ofLp i - j, Space.deriv j (fun x_1 => magneticFieldMatrix 𝓕.c A ((time 𝓕.c) x) x_1 (j, i)) (space x)) + (LorentzCurrentDensity.currentDensity 𝓕.c J ((time 𝓕.c) x) (space x)).ofLp i = 0 d:𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff A.valJ:LorentzCurrentDensity dhJ:ContDiff J(∀ (x : SpaceTime d) (i : Fin d), 𝓕.μ₀⁻¹ * (𝓕.ε₀ * 𝓕.μ₀ * (∂ₜ (fun x_1 => electricField 𝓕.c A x_1 (space x)) ((time 𝓕.c) x)).ofLp i - j, Space.deriv j (fun x_1 => magneticFieldMatrix 𝓕.c A ((time 𝓕.c) x) x_1 (j, i)) (space x)) + (LorentzCurrentDensity.currentDensity 𝓕.c J ((time 𝓕.c) x) (space x)).ofLp i = 0) (x : Time) (x_1 : Space d) (i : Fin d), 𝓕.μ₀ * 𝓕.ε₀ * (∂ₜ (fun t => electricField 𝓕.c A t x_1) x).ofLp i = j, Space.deriv j (fun x_2 => magneticFieldMatrix 𝓕.c A x x_2 (j, i)) x_1 - 𝓕.μ₀ * (LorentzCurrentDensity.currentDensity 𝓕.c J x x_1).ofLp i d:𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff A.valJ:LorentzCurrentDensity dhJ:ContDiff Jh: (x : SpaceTime d) (i : Fin d), 𝓕.μ₀⁻¹ * (𝓕.ε₀ * 𝓕.μ₀ * (∂ₜ (fun x_1 => electricField 𝓕.c A x_1 (space x)) ((time 𝓕.c) x)).ofLp i - j, Space.deriv j (fun x_1 => magneticFieldMatrix 𝓕.c A ((time 𝓕.c) x) x_1 (j, i)) (space x)) + (LorentzCurrentDensity.currentDensity 𝓕.c J ((time 𝓕.c) x) (space x)).ofLp i = 0t:Timex:Space di:Fin d𝓕.μ₀ * 𝓕.ε₀ * (∂ₜ (fun t => electricField 𝓕.c A t x) t).ofLp i = j, Space.deriv j (fun x => magneticFieldMatrix 𝓕.c A t x (j, i)) x - 𝓕.μ₀ * (LorentzCurrentDensity.currentDensity 𝓕.c J t x).ofLp i d:𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff A.valJ:LorentzCurrentDensity dhJ:ContDiff Jt:Timex:Space di:Fin dh:𝓕.μ₀⁻¹ * (𝓕.ε₀ * 𝓕.μ₀ * (∂ₜ (fun x_1 => electricField 𝓕.c A x_1 (space ((toTimeAndSpace 𝓕.c).symm (t, x)))) ((time 𝓕.c) ((toTimeAndSpace 𝓕.c).symm (t, x)))).ofLp i - j, Space.deriv j (fun x_1 => magneticFieldMatrix 𝓕.c A ((time 𝓕.c) ((toTimeAndSpace 𝓕.c).symm (t, x))) x_1 (j, i)) (space ((toTimeAndSpace 𝓕.c).symm (t, x)))) + (LorentzCurrentDensity.currentDensity 𝓕.c J ((time 𝓕.c) ((toTimeAndSpace 𝓕.c).symm (t, x))) (space ((toTimeAndSpace 𝓕.c).symm (t, x)))).ofLp i = 0𝓕.μ₀ * 𝓕.ε₀ * (∂ₜ (fun t => electricField 𝓕.c A t x) t).ofLp i = j, Space.deriv j (fun x => magneticFieldMatrix 𝓕.c A t x (j, i)) x - 𝓕.μ₀ * (LorentzCurrentDensity.currentDensity 𝓕.c J t x).ofLp i d:𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff A.valJ:LorentzCurrentDensity dhJ:ContDiff Jt:Timex:Space di:Fin dh:𝓕.μ₀⁻¹ * (𝓕.ε₀ * 𝓕.μ₀ * (∂ₜ (fun x_1 => electricField 𝓕.c A x_1 x) t).ofLp i - x_1, Space.deriv x_1 (fun x => magneticFieldMatrix 𝓕.c A t x (x_1, i)) x) + (LorentzCurrentDensity.currentDensity 𝓕.c J t x).ofLp i = 0𝓕.μ₀ * 𝓕.ε₀ * (∂ₜ (fun t => electricField 𝓕.c A t x) t).ofLp i = j, Space.deriv j (fun x => magneticFieldMatrix 𝓕.c A t x (j, i)) x - 𝓕.μ₀ * (LorentzCurrentDensity.currentDensity 𝓕.c J t x).ofLp i linear_combination (norm := d:𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff A.valJ:LorentzCurrentDensity dhJ:ContDiff Jt:Timex:Space di:Fin dh:𝓕.μ₀⁻¹ * (𝓕.ε₀ * 𝓕.μ₀ * (∂ₜ (fun x_1 => electricField 𝓕.c A x_1 x) t).ofLp i - x_1, Space.deriv x_1 (fun x => magneticFieldMatrix 𝓕.c A t x (x_1, i)) x) + (LorentzCurrentDensity.currentDensity 𝓕.c J t x).ofLp i = 0𝓕.μ₀ * 𝓕.ε₀ * (∂ₜ (fun t => electricField 𝓕.c A t x) t).ofLp i - ( j, Space.deriv j (fun x => magneticFieldMatrix 𝓕.c A t x (j, i)) x - 𝓕.μ₀ * (LorentzCurrentDensity.currentDensity 𝓕.c J t x).ofLp i + 𝓕.μ₀ * (𝓕.μ₀⁻¹ * (𝓕.ε₀ * 𝓕.μ₀ * (∂ₜ (fun t => electricField 𝓕.c A t x) t).ofLp i - j, Space.deriv j (fun x => magneticFieldMatrix 𝓕.c A t x (j, i)) x) + (LorentzCurrentDensity.currentDensity 𝓕.c J t x).ofLp i)) = 0) (𝓕.μ₀) * h d:𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff A.valJ:LorentzCurrentDensity dhJ:ContDiff Jt:Timex:Space di:Fin dh:𝓕.μ₀⁻¹ * (𝓕.ε₀ * 𝓕.μ₀ * (∂ₜ (fun x_1 => electricField 𝓕.c A x_1 x) t).ofLp i - x_1, Space.deriv x_1 (fun x => magneticFieldMatrix 𝓕.c A t x (x_1, i)) x) + (LorentzCurrentDensity.currentDensity 𝓕.c J t x).ofLp i = 0𝓕.μ₀ * 𝓕.ε₀ * (∂ₜ (fun t => electricField 𝓕.c A t x) t).ofLp i - ( j, Space.deriv j (fun x => magneticFieldMatrix 𝓕.c A t x (j, i)) x - 𝓕.μ₀ * (LorentzCurrentDensity.currentDensity 𝓕.c J t x).ofLp i + (𝓕.μ₀ * 𝓕.ε₀ * (∂ₜ (fun t => electricField 𝓕.c A t x) t).ofLp i - j, Space.deriv j (fun x => magneticFieldMatrix 𝓕.c A t x (j, i)) x + 𝓕.μ₀ * (LorentzCurrentDensity.currentDensity 𝓕.c J t x).ofLp i)) = 0 All goals completed! 🐙 d:𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff A.valJ:LorentzCurrentDensity dhJ:ContDiff J(∀ (x : Time) (x_1 : Space d) (i : Fin d), 𝓕.μ₀ * 𝓕.ε₀ * (∂ₜ (fun t => electricField 𝓕.c A t x_1) x).ofLp i = j, Space.deriv j (fun x_2 => magneticFieldMatrix 𝓕.c A x x_2 (j, i)) x_1 - 𝓕.μ₀ * (LorentzCurrentDensity.currentDensity 𝓕.c J x x_1).ofLp i) (x : SpaceTime d) (i : Fin d), 𝓕.μ₀⁻¹ * (𝓕.ε₀ * 𝓕.μ₀ * (∂ₜ (fun x_1 => electricField 𝓕.c A x_1 (space x)) ((time 𝓕.c) x)).ofLp i - j, Space.deriv j (fun x_1 => magneticFieldMatrix 𝓕.c A ((time 𝓕.c) x) x_1 (j, i)) (space x)) + (LorentzCurrentDensity.currentDensity 𝓕.c J ((time 𝓕.c) x) (space x)).ofLp i = 0 d:𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff A.valJ:LorentzCurrentDensity dhJ:ContDiff Jh: (x : Time) (x_1 : Space d) (i : Fin d), 𝓕.μ₀ * 𝓕.ε₀ * (∂ₜ (fun t => electricField 𝓕.c A t x_1) x).ofLp i = j, Space.deriv j (fun x_2 => magneticFieldMatrix 𝓕.c A x x_2 (j, i)) x_1 - 𝓕.μ₀ * (LorentzCurrentDensity.currentDensity 𝓕.c J x x_1).ofLp ix:SpaceTime di:Fin d𝓕.μ₀⁻¹ * (𝓕.ε₀ * 𝓕.μ₀ * (∂ₜ (fun x_1 => electricField 𝓕.c A x_1 (space x)) ((time 𝓕.c) x)).ofLp i - j, Space.deriv j (fun x_1 => magneticFieldMatrix 𝓕.c A ((time 𝓕.c) x) x_1 (j, i)) (space x)) + (LorentzCurrentDensity.currentDensity 𝓕.c J ((time 𝓕.c) x) (space x)).ofLp i = 0 d:𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff A.valJ:LorentzCurrentDensity dhJ:ContDiff Jx:SpaceTime di:Fin dh:𝓕.μ₀ * 𝓕.ε₀ * (∂ₜ (fun t => electricField 𝓕.c A t (space x)) ((time 𝓕.c) x)).ofLp i = j, Space.deriv j (fun x_1 => magneticFieldMatrix 𝓕.c A ((time 𝓕.c) x) x_1 (j, i)) (space x) - 𝓕.μ₀ * (LorentzCurrentDensity.currentDensity 𝓕.c J ((time 𝓕.c) x) (space x)).ofLp i𝓕.μ₀⁻¹ * (𝓕.ε₀ * 𝓕.μ₀ * (∂ₜ (fun x_1 => electricField 𝓕.c A x_1 (space x)) ((time 𝓕.c) x)).ofLp i - j, Space.deriv j (fun x_1 => magneticFieldMatrix 𝓕.c A ((time 𝓕.c) x) x_1 (j, i)) (space x)) + (LorentzCurrentDensity.currentDensity 𝓕.c J ((time 𝓕.c) x) (space x)).ofLp i = 0 linear_combination (norm := d:𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff A.valJ:LorentzCurrentDensity dhJ:ContDiff Jx:SpaceTime di:Fin dh:𝓕.μ₀ * 𝓕.ε₀ * (∂ₜ (fun t => electricField 𝓕.c A t (space x)) ((time 𝓕.c) x)).ofLp i = j, Space.deriv j (fun x_1 => magneticFieldMatrix 𝓕.c A ((time 𝓕.c) x) x_1 (j, i)) (space x) - 𝓕.μ₀ * (LorentzCurrentDensity.currentDensity 𝓕.c J ((time 𝓕.c) x) (space x)).ofLp i𝓕.μ₀⁻¹ * (𝓕.ε₀ * 𝓕.μ₀ * (∂ₜ (fun x_1 => electricField 𝓕.c A x_1 (space x)) ((time 𝓕.c) x)).ofLp i - j, Space.deriv j (fun x_1 => magneticFieldMatrix 𝓕.c A ((time 𝓕.c) x) x_1 (j, i)) (space x)) + (LorentzCurrentDensity.currentDensity 𝓕.c J ((time 𝓕.c) x) (space x)).ofLp i + 𝓕.μ₀⁻¹ * ( j, Space.deriv j (fun x_1 => magneticFieldMatrix 𝓕.c A ((time 𝓕.c) x) x_1 (j, i)) (space x) - 𝓕.μ₀ * (LorentzCurrentDensity.currentDensity 𝓕.c J ((time 𝓕.c) x) (space x)).ofLp i) - 𝓕.μ₀⁻¹ * (𝓕.μ₀ * 𝓕.ε₀ * (∂ₜ (fun x_1 => electricField 𝓕.c A x_1 (space x)) ((time 𝓕.c) x)).ofLp i) = 0) (𝓕.μ₀⁻¹) * h d:𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff A.valJ:LorentzCurrentDensity dhJ:ContDiff Jx:SpaceTime di:Fin dh:𝓕.μ₀ * 𝓕.ε₀ * (∂ₜ (fun t => electricField 𝓕.c A t (space x)) ((time 𝓕.c) x)).ofLp i = j, Space.deriv j (fun x_1 => magneticFieldMatrix 𝓕.c A ((time 𝓕.c) x) x_1 (j, i)) (space x) - 𝓕.μ₀ * (LorentzCurrentDensity.currentDensity 𝓕.c J ((time 𝓕.c) x) (space x)).ofLp i𝓕.μ₀ * 𝓕.ε₀ * (∂ₜ (fun x_1 => electricField 𝓕.c A x_1 (space x)) ((time 𝓕.c) x)).ofLp i - j, Space.deriv j (fun x_1 => magneticFieldMatrix 𝓕.c A ((time 𝓕.c) x) x_1 (j, i)) (space x) + 𝓕.μ₀ * (LorentzCurrentDensity.currentDensity 𝓕.c J ((time 𝓕.c) x) (space x)).ofLp i + ( j, Space.deriv j (fun x_1 => magneticFieldMatrix 𝓕.c A ((time 𝓕.c) x) x_1 (j, i)) (space x) - 𝓕.μ₀ * (LorentzCurrentDensity.currentDensity 𝓕.c J ((time 𝓕.c) x) (space x)).ofLp i) - 𝓕.μ₀ * 𝓕.ε₀ * (∂ₜ (fun x_1 => electricField 𝓕.c A x_1 (space x)) ((time 𝓕.c) x)).ofLp i = 𝓕.μ₀ * 0 All goals completed! 🐙

C. Time derivatives from the extrema condition

d:A:ElectromagneticPotential d𝓕:FreeSpacehA:ContDiff A.valJ:LorentzCurrentDensity dhJ:ContDiff Jh: (t : Time) (x : Space d), Space.div (electricField 𝓕.c A t) x = LorentzCurrentDensity.chargeDensity 𝓕.c J t x / 𝓕.ε₀ (i : Fin d), 𝓕.μ₀ * 𝓕.ε₀ * (∂ₜ (fun t => electricField 𝓕.c A t x) t).ofLp i = j, Space.deriv j (fun x => magneticFieldMatrix 𝓕.c A t x (j, i)) x - 𝓕.μ₀ * (LorentzCurrentDensity.currentDensity 𝓕.c J t x).ofLp it:Timex:Space di:Fin d(∂ₜ (fun x_1 => electricField 𝓕.c A x_1 x) t).ofLp i = 1 / (𝓕.μ₀ * 𝓕.ε₀) * j, Space.deriv j (fun x => magneticFieldMatrix 𝓕.c A t x (j, i)) x - 1 / 𝓕.ε₀ * (LorentzCurrentDensity.currentDensity 𝓕.c J t x).ofLp i linear_combination (norm := d:A:ElectromagneticPotential d𝓕:FreeSpacehA:ContDiff A.valJ:LorentzCurrentDensity dhJ:ContDiff Jh: (t : Time) (x : Space d), Space.div (electricField 𝓕.c A t) x = LorentzCurrentDensity.chargeDensity 𝓕.c J t x / 𝓕.ε₀ (i : Fin d), 𝓕.μ₀ * 𝓕.ε₀ * (∂ₜ (fun t => electricField 𝓕.c A t x) t).ofLp i = j, Space.deriv j (fun x => magneticFieldMatrix 𝓕.c A t x (j, i)) x - 𝓕.μ₀ * (LorentzCurrentDensity.currentDensity 𝓕.c J t x).ofLp it:Timex:Space di:Fin d(∂ₜ (fun x_1 => electricField 𝓕.c A x_1 x) t).ofLp i + 𝓕.ε₀⁻¹ * 𝓕.μ₀⁻¹ * ( j, Space.deriv j (fun x => magneticFieldMatrix 𝓕.c A t x (j, i)) x - 𝓕.μ₀ * (LorentzCurrentDensity.currentDensity 𝓕.c J t x).ofLp i) - (𝓕.ε₀⁻¹ * 𝓕.μ₀⁻¹ * j, Space.deriv j (fun x => magneticFieldMatrix 𝓕.c A t x (j, i)) x - 𝓕.ε₀⁻¹ * (LorentzCurrentDensity.currentDensity 𝓕.c J t x).ofLp i + 𝓕.ε₀⁻¹ * 𝓕.μ₀⁻¹ * (𝓕.μ₀ * 𝓕.ε₀ * (∂ₜ (fun x_1 => electricField 𝓕.c A x_1 x) t).ofLp i)) = 0) (𝓕.μ₀ * 𝓕.ε₀)⁻¹ * ((h t x).2 i) d:A:ElectromagneticPotential d𝓕:FreeSpacehA:ContDiff A.valJ:LorentzCurrentDensity dhJ:ContDiff Jh: (t : Time) (x : Space d), Space.div (electricField 𝓕.c A t) x = LorentzCurrentDensity.chargeDensity 𝓕.c J t x / 𝓕.ε₀ (i : Fin d), 𝓕.μ₀ * 𝓕.ε₀ * (∂ₜ (fun t => electricField 𝓕.c A t x) t).ofLp i = j, Space.deriv j (fun x => magneticFieldMatrix 𝓕.c A t x (j, i)) x - 𝓕.μ₀ * (LorentzCurrentDensity.currentDensity 𝓕.c J t x).ofLp it:Timex:Space di:Fin d(∂ₜ (fun x_1 => electricField 𝓕.c A x_1 x) t).ofLp i * 𝓕.ε₀ * 𝓕.μ₀ + ( j, Space.deriv j (fun x => magneticFieldMatrix 𝓕.c A t x (j, i)) x - 𝓕.μ₀ * (LorentzCurrentDensity.currentDensity 𝓕.c J t x).ofLp i) - ( j, Space.deriv j (fun x => magneticFieldMatrix 𝓕.c A t x (j, i)) x - 𝓕.μ₀ * (LorentzCurrentDensity.currentDensity 𝓕.c J t x).ofLp i + (∂ₜ (fun x_1 => electricField 𝓕.c A x_1 x) t).ofLp i * 𝓕.ε₀ * 𝓕.μ₀) = 𝓕.ε₀ * 𝓕.μ₀ * 0 All goals completed! 🐙

D. Second time derivatives from the extrema condition

D.1. Second time derivatives of the magnetic field from the extrema condition

We show that the magnetic field matrix $B_{ij}$ satisfies the following wave-like equation

$$\frac{\partial^2 B_{ij}}{\partial t^2} = c^2 \sum_k \frac{\partial^2 B_{ij}}{\partial x_k^2} + \frac{1}{\epsilon_0} \left(\frac{\partial J_i}{\partial x_j} - \frac{\partial J_j}{\partial x_i} \right).$$ When the free current density is zero, this reduces to the wave equation.

d:A:ElectromagneticPotential d𝓕:FreeSpacehA:ContDiff A.valJ:LorentzCurrentDensity dhJ:ContDiff Jh:IsExtrema 𝓕 A Jt:Timex:Space di:Fin dj:Fin dhcd: (ij : Fin d × Fin d), ContDiff 2 fun y => magneticFieldMatrix 𝓕.c A t y ijhsd: (ij : Fin d × Fin d) (k : Fin d), Differentiable (Space.deriv k fun y => magneticFieldMatrix 𝓕.c A t y ij)hJd: (i : Fin d), Differentiable fun x => (LorentzCurrentDensity.currentDensity 𝓕.c J t x).ofLp i((1 / (𝓕.μ₀ * 𝓕.ε₀)) i, fderiv (Space.deriv i fun y => magneticFieldMatrix 𝓕.c A t y (i, j)) x - (1 / 𝓕.ε₀) fderiv (fun x => (LorentzCurrentDensity.currentDensity 𝓕.c J t x).ofLp j) x) (Space.basis i) - Space.deriv j (fun x => 1 / (𝓕.μ₀ * 𝓕.ε₀) * j, Space.deriv j (fun x => magneticFieldMatrix 𝓕.c A t x (j, i)) x - 1 / 𝓕.ε₀ * (LorentzCurrentDensity.currentDensity 𝓕.c J t x).ofLp i) x = 𝓕.c.val ^ 2 * k, Space.deriv k (Space.deriv k fun x => magneticFieldMatrix 𝓕.c A t x (i, j)) x + 𝓕.ε₀⁻¹ * (Space.deriv j (fun x => (LorentzCurrentDensity.currentDensity 𝓕.c J t x).ofLp i) x - Space.deriv i (fun x => (LorentzCurrentDensity.currentDensity 𝓕.c J t x).ofLp j) x) conv_lhs => d:A:ElectromagneticPotential d𝓕:FreeSpacehA:ContDiff A.valJ:LorentzCurrentDensity dhJ:ContDiff Jh:IsExtrema 𝓕 A Jt:Timex:Space di:Fin dj:Fin dhcd: (ij : Fin d × Fin d), ContDiff 2 fun y => magneticFieldMatrix 𝓕.c A t y ijhsd: (ij : Fin d × Fin d) (k : Fin d), Differentiable (Space.deriv k fun y => magneticFieldMatrix 𝓕.c A t y ij)hJd: (i : Fin d), Differentiable fun x => (LorentzCurrentDensity.currentDensity 𝓕.c J t x).ofLp i| Space.deriv j (fun x => 1 / (𝓕.μ₀ * 𝓕.ε₀) * j, Space.deriv j (fun x => magneticFieldMatrix 𝓕.c A t x (j, i)) x - 1 / 𝓕.ε₀ * (LorentzCurrentDensity.currentDensity 𝓕.c J t x).ofLp i) x d:A:ElectromagneticPotential d𝓕:FreeSpacehA:ContDiff A.valJ:LorentzCurrentDensity dhJ:ContDiff Jh:IsExtrema 𝓕 A Jt:Timex:Space di:Fin dj:Fin dhcd: (ij : Fin d × Fin d), ContDiff 2 fun y => magneticFieldMatrix 𝓕.c A t y ijhsd: (ij : Fin d × Fin d) (k : Fin d), Differentiable (Space.deriv k fun y => magneticFieldMatrix 𝓕.c A t y ij)hJd: (i : Fin d), Differentiable fun x => (LorentzCurrentDensity.currentDensity 𝓕.c J t x).ofLp i| (fderiv (fun x => 1 / (𝓕.μ₀ * 𝓕.ε₀) * j, Space.deriv j (fun x => magneticFieldMatrix 𝓕.c A t x (j, i)) x - 1 / 𝓕.ε₀ * (LorentzCurrentDensity.currentDensity 𝓕.c J t x).ofLp i) x) (Space.basis j) d:A:ElectromagneticPotential d𝓕:FreeSpacehA:ContDiff A.valJ:LorentzCurrentDensity dhJ:ContDiff Jh:IsExtrema 𝓕 A Jt:Timex:Space di:Fin dj:Fin dhcd: (ij : Fin d × Fin d), ContDiff 2 fun y => magneticFieldMatrix 𝓕.c A t y ijhsd: (ij : Fin d × Fin d) (k : Fin d), Differentiable (Space.deriv k fun y => magneticFieldMatrix 𝓕.c A t y ij)hJd: (i : Fin d), Differentiable fun x => (LorentzCurrentDensity.currentDensity 𝓕.c J t x).ofLp i| ((1 / (𝓕.μ₀ * 𝓕.ε₀)) i_1, fderiv (Space.deriv i_1 fun y => magneticFieldMatrix 𝓕.c A t y (i_1, i)) x - (1 / 𝓕.ε₀) fderiv (fun x => (LorentzCurrentDensity.currentDensity 𝓕.c J t x).ofLp i) x) (Space.basis j) d:A:ElectromagneticPotential d𝓕:FreeSpacehA:ContDiff A.valJ:LorentzCurrentDensity dhJ:ContDiff Jh:IsExtrema 𝓕 A Jt:Timex:Space di:Fin dj:Fin dhcd: (ij : Fin d × Fin d), ContDiff 2 fun y => magneticFieldMatrix 𝓕.c A t y ijhsd: (ij : Fin d × Fin d) (k : Fin d), Differentiable (Space.deriv k fun y => magneticFieldMatrix 𝓕.c A t y ij)hJd: (i : Fin d), Differentiable fun x => (LorentzCurrentDensity.currentDensity 𝓕.c J t x).ofLp i𝓕.ε₀⁻¹ * 𝓕.μ₀⁻¹ * x_1, Space.deriv i (Space.deriv x_1 fun y => magneticFieldMatrix 𝓕.c A t y (x_1, j)) x - 𝓕.ε₀⁻¹ * Space.deriv i (fun x => (LorentzCurrentDensity.currentDensity 𝓕.c J t x).ofLp j) x - (𝓕.ε₀⁻¹ * 𝓕.μ₀⁻¹ * x_1, Space.deriv j (Space.deriv x_1 fun y => magneticFieldMatrix 𝓕.c A t y (x_1, i)) x - 𝓕.ε₀⁻¹ * Space.deriv j (fun x => (LorentzCurrentDensity.currentDensity 𝓕.c J t x).ofLp i) x) = 𝓕.μ₀⁻¹ * 𝓕.ε₀⁻¹ * k, Space.deriv k (Space.deriv k fun x => magneticFieldMatrix 𝓕.c A t x (i, j)) x + 𝓕.ε₀⁻¹ * (Space.deriv j (fun x => (LorentzCurrentDensity.currentDensity 𝓕.c J t x).ofLp i) x - Space.deriv i (fun x => (LorentzCurrentDensity.currentDensity 𝓕.c J t x).ofLp j) x) d:A:ElectromagneticPotential d𝓕:FreeSpacehA:ContDiff A.valJ:LorentzCurrentDensity dhJ:ContDiff Jh:IsExtrema 𝓕 A Jt:Timex:Space di:Fin dj:Fin dhcd: (ij : Fin d × Fin d), ContDiff 2 fun y => magneticFieldMatrix 𝓕.c A t y ijhsd: (ij : Fin d × Fin d) (k : Fin d), Differentiable (Space.deriv k fun y => magneticFieldMatrix 𝓕.c A t y ij)hJd: (i : Fin d), Differentiable fun x => (LorentzCurrentDensity.currentDensity 𝓕.c J t x).ofLp i x_1, Space.deriv i (Space.deriv x_1 fun y => magneticFieldMatrix 𝓕.c A t y (x_1, j)) x - 𝓕.μ₀ * Space.deriv i (fun x => (LorentzCurrentDensity.currentDensity 𝓕.c J t x).ofLp j) x - ( x_1, Space.deriv j (Space.deriv x_1 fun y => magneticFieldMatrix 𝓕.c A t y (x_1, i)) x - 𝓕.μ₀ * Space.deriv j (fun x => (LorentzCurrentDensity.currentDensity 𝓕.c J t x).ofLp i) x) = k, Space.deriv k (Space.deriv k fun x => magneticFieldMatrix 𝓕.c A t x (i, j)) x + 𝓕.μ₀ * (Space.deriv j (fun x => (LorentzCurrentDensity.currentDensity 𝓕.c J t x).ofLp i) x - Space.deriv i (fun x => (LorentzCurrentDensity.currentDensity 𝓕.c J t x).ofLp j) x) conv_rhs => d:A:ElectromagneticPotential d𝓕:FreeSpacehA:ContDiff A.valJ:LorentzCurrentDensity dhJ:ContDiff Jh:IsExtrema 𝓕 A Jt:Timex✝:Space di:Fin dj:Fin dhcd: (ij : Fin d × Fin d), ContDiff 2 fun y => magneticFieldMatrix 𝓕.c A t y ijhsd: (ij : Fin d × Fin d) (k : Fin d), Differentiable (Space.deriv k fun y => magneticFieldMatrix 𝓕.c A t y ij)hJd: (i : Fin d), Differentiable fun x => (LorentzCurrentDensity.currentDensity 𝓕.c J t x).ofLp ik:Fin dx:Space d| Space.deriv k (fun x => magneticFieldMatrix 𝓕.c A t x (i, j)) x d:A:ElectromagneticPotential d𝓕:FreeSpacehA:ContDiff A.valJ:LorentzCurrentDensity dhJ:ContDiff Jh:IsExtrema 𝓕 A Jt:Timex✝:Space di:Fin dj:Fin dhcd: (ij : Fin d × Fin d), ContDiff 2 fun y => magneticFieldMatrix 𝓕.c A t y ijhsd: (ij : Fin d × Fin d) (k : Fin d), Differentiable (Space.deriv k fun y => magneticFieldMatrix 𝓕.c A t y ij)hJd: (i : Fin d), Differentiable fun x => (LorentzCurrentDensity.currentDensity 𝓕.c J t x).ofLp ik:Fin dx:Space d| Space.deriv i (fun x => magneticFieldMatrix 𝓕.c A t x (k, j)) x - Space.deriv j (fun x => magneticFieldMatrix 𝓕.c A t x (k, i)) x conv_rhs => d:A:ElectromagneticPotential d𝓕:FreeSpacehA:ContDiff A.valJ:LorentzCurrentDensity dhJ:ContDiff Jh:IsExtrema 𝓕 A Jt:Timex:Space di:Fin dj:Fin dhcd: (ij : Fin d × Fin d), ContDiff 2 fun y => magneticFieldMatrix 𝓕.c A t y ijhsd: (ij : Fin d × Fin d) (k : Fin d), Differentiable (Space.deriv k fun y => magneticFieldMatrix 𝓕.c A t y ij)hJd: (i : Fin d), Differentiable fun x => (LorentzCurrentDensity.currentDensity 𝓕.c J t x).ofLp ik:Fin d| Space.deriv k (fun x => Space.deriv i (fun x => magneticFieldMatrix 𝓕.c A t x (k, j)) x - Space.deriv j (fun x => magneticFieldMatrix 𝓕.c A t x (k, i)) x) x d:A:ElectromagneticPotential d𝓕:FreeSpacehA:ContDiff A.valJ:LorentzCurrentDensity dhJ:ContDiff Jh:IsExtrema 𝓕 A Jt:Timex:Space di:Fin dj:Fin dhcd: (ij : Fin d × Fin d), ContDiff 2 fun y => magneticFieldMatrix 𝓕.c A t y ijhsd: (ij : Fin d × Fin d) (k : Fin d), Differentiable (Space.deriv k fun y => magneticFieldMatrix 𝓕.c A t y ij)hJd: (i : Fin d), Differentiable fun x => (LorentzCurrentDensity.currentDensity 𝓕.c J t x).ofLp ik:Fin d| (fderiv (fun x => Space.deriv i (fun x => magneticFieldMatrix 𝓕.c A t x (k, j)) x - Space.deriv j (fun x => magneticFieldMatrix 𝓕.c A t x (k, i)) x) x) (Space.basis k) d:A:ElectromagneticPotential d𝓕:FreeSpacehA:ContDiff A.valJ:LorentzCurrentDensity dhJ:ContDiff Jh:IsExtrema 𝓕 A Jt:Timex:Space di:Fin dj:Fin dhcd: (ij : Fin d × Fin d), ContDiff 2 fun y => magneticFieldMatrix 𝓕.c A t y ijhsd: (ij : Fin d × Fin d) (k : Fin d), Differentiable (Space.deriv k fun y => magneticFieldMatrix 𝓕.c A t y ij)hJd: (i : Fin d), Differentiable fun x => (LorentzCurrentDensity.currentDensity 𝓕.c J t x).ofLp ik:Fin d| (fderiv (Space.deriv i fun y => magneticFieldMatrix 𝓕.c A t y (k, j)) x - fderiv (Space.deriv j fun y => magneticFieldMatrix 𝓕.c A t y (k, i)) x) (Space.basis k) d:A:ElectromagneticPotential d𝓕:FreeSpacehA:ContDiff A.valJ:LorentzCurrentDensity dhJ:ContDiff Jh:IsExtrema 𝓕 A Jt:Timex:Space di:Fin dj:Fin dhcd: (ij : Fin d × Fin d), ContDiff 2 fun y => magneticFieldMatrix 𝓕.c A t y ijhsd: (ij : Fin d × Fin d) (k : Fin d), Differentiable (Space.deriv k fun y => magneticFieldMatrix 𝓕.c A t y ij)hJd: (i : Fin d), Differentiable fun x => (LorentzCurrentDensity.currentDensity 𝓕.c J t x).ofLp ik:Fin d| Space.deriv k (Space.deriv i fun y => magneticFieldMatrix 𝓕.c A t y (k, j)) x - Space.deriv k (Space.deriv j fun y => magneticFieldMatrix 𝓕.c A t y (k, i)) x d:A:ElectromagneticPotential d𝓕:FreeSpacehA:ContDiff A.valJ:LorentzCurrentDensity dhJ:ContDiff Jh:IsExtrema 𝓕 A Jt:Timex:Space di:Fin dj:Fin dhcd: (ij : Fin d × Fin d), ContDiff 2 fun y => magneticFieldMatrix 𝓕.c A t y ijhsd: (ij : Fin d × Fin d) (k : Fin d), Differentiable (Space.deriv k fun y => magneticFieldMatrix 𝓕.c A t y ij)hJd: (i : Fin d), Differentiable fun x => (LorentzCurrentDensity.currentDensity 𝓕.c J t x).ofLp ik:Fin d| Space.deriv i (Space.deriv k fun y => magneticFieldMatrix 𝓕.c A t y (k, j)) x - Space.deriv k (Space.deriv j fun y => magneticFieldMatrix 𝓕.c A t y (k, i)) x d:A:ElectromagneticPotential d𝓕:FreeSpacehA:ContDiff A.valJ:LorentzCurrentDensity dhJ:ContDiff Jh:IsExtrema 𝓕 A Jt:Timex:Space di:Fin dj:Fin dhcd: (ij : Fin d × Fin d), ContDiff 2 fun y => magneticFieldMatrix 𝓕.c A t y ijhsd: (ij : Fin d × Fin d) (k : Fin d), Differentiable (Space.deriv k fun y => magneticFieldMatrix 𝓕.c A t y ij)hJd: (i : Fin d), Differentiable fun x => (LorentzCurrentDensity.currentDensity 𝓕.c J t x).ofLp ik:Fin d| Space.deriv k (Space.deriv j fun y => magneticFieldMatrix 𝓕.c A t y (k, i)) x d:A:ElectromagneticPotential d𝓕:FreeSpacehA:ContDiff A.valJ:LorentzCurrentDensity dhJ:ContDiff Jh:IsExtrema 𝓕 A Jt:Timex:Space di:Fin dj:Fin dhcd: (ij : Fin d × Fin d), ContDiff 2 fun y => magneticFieldMatrix 𝓕.c A t y ijhsd: (ij : Fin d × Fin d) (k : Fin d), Differentiable (Space.deriv k fun y => magneticFieldMatrix 𝓕.c A t y ij)hJd: (i : Fin d), Differentiable fun x => (LorentzCurrentDensity.currentDensity 𝓕.c J t x).ofLp ik:Fin d| Space.deriv j (Space.deriv k fun y => magneticFieldMatrix 𝓕.c A t y (k, i)) x d:A:ElectromagneticPotential d𝓕:FreeSpacehA:ContDiff A.valJ:LorentzCurrentDensity dhJ:ContDiff Jh:IsExtrema 𝓕 A Jt:Timex:Space di:Fin dj:Fin dhcd: (ij : Fin d × Fin d), ContDiff 2 fun y => magneticFieldMatrix 𝓕.c A t y ijhsd: (ij : Fin d × Fin d) (k : Fin d), Differentiable (Space.deriv k fun y => magneticFieldMatrix 𝓕.c A t y ij)hJd: (i : Fin d), Differentiable fun x => (LorentzCurrentDensity.currentDensity 𝓕.c J t x).ofLp i x_1, Space.deriv i (Space.deriv x_1 fun y => magneticFieldMatrix 𝓕.c A t y (x_1, j)) x - 𝓕.μ₀ * Space.deriv i (fun x => (LorentzCurrentDensity.currentDensity 𝓕.c J t x).ofLp j) x - ( x_1, Space.deriv j (Space.deriv x_1 fun y => magneticFieldMatrix 𝓕.c A t y (x_1, i)) x - 𝓕.μ₀ * Space.deriv j (fun x => (LorentzCurrentDensity.currentDensity 𝓕.c J t x).ofLp i) x) = x_1, Space.deriv i (Space.deriv x_1 fun y => magneticFieldMatrix 𝓕.c A t y (x_1, j)) x - x_1, Space.deriv j (Space.deriv x_1 fun y => magneticFieldMatrix 𝓕.c A t y (x_1, i)) x + 𝓕.μ₀ * (Space.deriv j (fun x => (LorentzCurrentDensity.currentDensity 𝓕.c J t x).ofLp i) x - Space.deriv i (fun x => (LorentzCurrentDensity.currentDensity 𝓕.c J t x).ofLp j) x) All goals completed! 🐙

D.2. Second time derivatives of the electric field from the extrema condition

We show that the electric field $E_i$ satisfies the following wave-like equation:

$$\frac{\partial^2 E_{i}}{\partial t^2} = c^2 \sum_k \frac{\partial^2 E_{i}}{\partial x_k^2} - \frac{c ^ 2}{\epsilon_0} \frac{\partial \rho}{\partial x_i} - c ^ 2 μ_0 \frac{\partial J_i}{\partial t}.$$

When the free current density and charge density are zero, this reduces to the wave equation.

d:A:ElectromagneticPotential d𝓕:FreeSpacehA:ContDiff A.valJ:LorentzCurrentDensity dhJ:ContDiff Jh: (t : Time) (x : Space d), Space.div (electricField 𝓕.c A t) x = LorentzCurrentDensity.chargeDensity 𝓕.c J t x / 𝓕.ε₀ (i : Fin d), 𝓕.μ₀ * 𝓕.ε₀ * (∂ₜ (fun t => electricField 𝓕.c A t x) t).ofLp i = j, Space.deriv j (fun x => magneticFieldMatrix 𝓕.c A t x (j, i)) x - 𝓕.μ₀ * (LorentzCurrentDensity.currentDensity 𝓕.c J t x).ofLp it:Timex:Space di:Fin dhEs: (j : Fin d), ContDiff 2 fun y => (electricField 𝓕.c A t y).ofLp jhEd: (j k : Fin d), Differentiable (Space.deriv k fun y => (electricField 𝓕.c A t y).ofLp j)hBt: (j : Fin d), Differentiable fun s => Space.deriv j (fun y => magneticFieldMatrix 𝓕.c A s y (j, i)) xhJt:Differentiable fun s => (LorentzCurrentDensity.currentDensity 𝓕.c J s x).ofLp i1 / (𝓕.μ₀ * 𝓕.ε₀) * ((1 / 𝓕.ε₀) fderiv (LorentzCurrentDensity.chargeDensity 𝓕.c J t) x) (Space.basis i) = 1 / (𝓕.μ₀ * 𝓕.ε₀ ^ 2) * Space.deriv i (fun x => LorentzCurrentDensity.chargeDensity 𝓕.c J t x) xd:A:ElectromagneticPotential d𝓕:FreeSpacehA:ContDiff A.valJ:LorentzCurrentDensity dhJ:ContDiff Jh: (t : Time) (x : Space d), Space.div (electricField 𝓕.c A t) x = LorentzCurrentDensity.chargeDensity 𝓕.c J t x / 𝓕.ε₀ (i : Fin d), 𝓕.μ₀ * 𝓕.ε₀ * (∂ₜ (fun t => electricField 𝓕.c A t x) t).ofLp i = j, Space.deriv j (fun x => magneticFieldMatrix 𝓕.c A t x (j, i)) x - 𝓕.μ₀ * (LorentzCurrentDensity.currentDensity 𝓕.c J t x).ofLp it:Timex:Space di:Fin dhEs: (j : Fin d), ContDiff 2 fun y => (electricField 𝓕.c A t y).ofLp jhEd: (j k : Fin d), Differentiable (Space.deriv k fun y => (electricField 𝓕.c A t y).ofLp j)hBt: (j : Fin d), Differentiable fun s => Space.deriv j (fun y => magneticFieldMatrix 𝓕.c A s y (j, i)) xhJt:Differentiable fun s => (LorentzCurrentDensity.currentDensity 𝓕.c J s x).ofLp iDifferentiableAt (LorentzCurrentDensity.chargeDensity 𝓕.c J t) x d:A:ElectromagneticPotential d𝓕:FreeSpacehA:ContDiff A.valJ:LorentzCurrentDensity dhJ:ContDiff Jh: (t : Time) (x : Space d), Space.div (electricField 𝓕.c A t) x = LorentzCurrentDensity.chargeDensity 𝓕.c J t x / 𝓕.ε₀ (i : Fin d), 𝓕.μ₀ * 𝓕.ε₀ * (∂ₜ (fun t => electricField 𝓕.c A t x) t).ofLp i = j, Space.deriv j (fun x => magneticFieldMatrix 𝓕.c A t x (j, i)) x - 𝓕.μ₀ * (LorentzCurrentDensity.currentDensity 𝓕.c J t x).ofLp it:Timex:Space di:Fin dhEs: (j : Fin d), ContDiff 2 fun y => (electricField 𝓕.c A t y).ofLp jhEd: (j k : Fin d), Differentiable (Space.deriv k fun y => (electricField 𝓕.c A t y).ofLp j)hBt: (j : Fin d), Differentiable fun s => Space.deriv j (fun y => magneticFieldMatrix 𝓕.c A s y (j, i)) xhJt:Differentiable fun s => (LorentzCurrentDensity.currentDensity 𝓕.c J s x).ofLp i𝓕.ε₀⁻¹ * 𝓕.μ₀⁻¹ * (𝓕.ε₀⁻¹ * Space.deriv i (LorentzCurrentDensity.chargeDensity 𝓕.c J t) x) = (𝓕.ε₀ ^ 2)⁻¹ * 𝓕.μ₀⁻¹ * Space.deriv i (fun x => LorentzCurrentDensity.chargeDensity 𝓕.c J t x) xd:A:ElectromagneticPotential d𝓕:FreeSpacehA:ContDiff A.valJ:LorentzCurrentDensity dhJ:ContDiff Jh: (t : Time) (x : Space d), Space.div (electricField 𝓕.c A t) x = LorentzCurrentDensity.chargeDensity 𝓕.c J t x / 𝓕.ε₀ (i : Fin d), 𝓕.μ₀ * 𝓕.ε₀ * (∂ₜ (fun t => electricField 𝓕.c A t x) t).ofLp i = j, Space.deriv j (fun x => magneticFieldMatrix 𝓕.c A t x (j, i)) x - 𝓕.μ₀ * (LorentzCurrentDensity.currentDensity 𝓕.c J t x).ofLp it:Timex:Space di:Fin dhEs: (j : Fin d), ContDiff 2 fun y => (electricField 𝓕.c A t y).ofLp jhEd: (j k : Fin d), Differentiable (Space.deriv k fun y => (electricField 𝓕.c A t y).ofLp j)hBt: (j : Fin d), Differentiable fun s => Space.deriv j (fun y => magneticFieldMatrix 𝓕.c A s y (j, i)) xhJt:Differentiable fun s => (LorentzCurrentDensity.currentDensity 𝓕.c J s x).ofLp iDifferentiableAt (LorentzCurrentDensity.chargeDensity 𝓕.c J t) x d:A:ElectromagneticPotential d𝓕:FreeSpacehA:ContDiff A.valJ:LorentzCurrentDensity dhJ:ContDiff Jh: (t : Time) (x : Space d), Space.div (electricField 𝓕.c A t) x = LorentzCurrentDensity.chargeDensity 𝓕.c J t x / 𝓕.ε₀ (i : Fin d), 𝓕.μ₀ * 𝓕.ε₀ * (∂ₜ (fun t => electricField 𝓕.c A t x) t).ofLp i = j, Space.deriv j (fun x => magneticFieldMatrix 𝓕.c A t x (j, i)) x - 𝓕.μ₀ * (LorentzCurrentDensity.currentDensity 𝓕.c J t x).ofLp it:Timex:Space di:Fin dhEs: (j : Fin d), ContDiff 2 fun y => (electricField 𝓕.c A t y).ofLp jhEd: (j k : Fin d), Differentiable (Space.deriv k fun y => (electricField 𝓕.c A t y).ofLp j)hBt: (j : Fin d), Differentiable fun s => Space.deriv j (fun y => magneticFieldMatrix 𝓕.c A s y (j, i)) xhJt:Differentiable fun s => (LorentzCurrentDensity.currentDensity 𝓕.c J s x).ofLp iDifferentiableAt (LorentzCurrentDensity.chargeDensity 𝓕.c J t) x d:A:ElectromagneticPotential d𝓕:FreeSpacehA:ContDiff A.valJ:LorentzCurrentDensity dhJ:ContDiff Jh: (t : Time) (x : Space d), Space.div (electricField 𝓕.c A t) x = LorentzCurrentDensity.chargeDensity 𝓕.c J t x / 𝓕.ε₀ (i : Fin d), 𝓕.μ₀ * 𝓕.ε₀ * (∂ₜ (fun t => electricField 𝓕.c A t x) t).ofLp i = j, Space.deriv j (fun x => magneticFieldMatrix 𝓕.c A t x (j, i)) x - 𝓕.μ₀ * (LorentzCurrentDensity.currentDensity 𝓕.c J t x).ofLp it:Timex:Space di:Fin dhEs: (j : Fin d), ContDiff 2 fun y => (electricField 𝓕.c A t y).ofLp jhEd: (j k : Fin d), Differentiable (Space.deriv k fun y => (electricField 𝓕.c A t y).ofLp j)hBt: (j : Fin d), Differentiable fun s => Space.deriv j (fun y => magneticFieldMatrix 𝓕.c A s y (j, i)) xhJt:Differentiable fun s => (LorentzCurrentDensity.currentDensity 𝓕.c J s x).ofLp iDifferentiable (LorentzCurrentDensity.chargeDensity 𝓕.c J t) d:A:ElectromagneticPotential d𝓕:FreeSpacehA:ContDiff A.valJ:LorentzCurrentDensity dhJ:ContDiff Jh: (t : Time) (x : Space d), Space.div (electricField 𝓕.c A t) x = LorentzCurrentDensity.chargeDensity 𝓕.c J t x / 𝓕.ε₀ (i : Fin d), 𝓕.μ₀ * 𝓕.ε₀ * (∂ₜ (fun t => electricField 𝓕.c A t x) t).ofLp i = j, Space.deriv j (fun x => magneticFieldMatrix 𝓕.c A t x (j, i)) x - 𝓕.μ₀ * (LorentzCurrentDensity.currentDensity 𝓕.c J t x).ofLp it:Timex:Space di:Fin dhEs: (j : Fin d), ContDiff 2 fun y => (electricField 𝓕.c A t y).ofLp jhEd: (j k : Fin d), Differentiable (Space.deriv k fun y => (electricField 𝓕.c A t y).ofLp j)hBt: (j : Fin d), Differentiable fun s => Space.deriv j (fun y => magneticFieldMatrix 𝓕.c A s y (j, i)) xhJt:Differentiable fun s => (LorentzCurrentDensity.currentDensity 𝓕.c J s x).ofLp iDifferentiable J exact hJ.differentiable (d:A:ElectromagneticPotential d𝓕:FreeSpacehA:ContDiff A.valJ:LorentzCurrentDensity dhJ:ContDiff Jh: (t : Time) (x : Space d), Space.div (electricField 𝓕.c A t) x = LorentzCurrentDensity.chargeDensity 𝓕.c J t x / 𝓕.ε₀ (i : Fin d), 𝓕.μ₀ * 𝓕.ε₀ * (∂ₜ (fun t => electricField 𝓕.c A t x) t).ofLp i = j, Space.deriv j (fun x => magneticFieldMatrix 𝓕.c A t x (j, i)) x - 𝓕.μ₀ * (LorentzCurrentDensity.currentDensity 𝓕.c J t x).ofLp it:Timex:Space di:Fin dhEs: (j : Fin d), ContDiff 2 fun y => (electricField 𝓕.c A t y).ofLp jhEd: (j k : Fin d), Differentiable (Space.deriv k fun y => (electricField 𝓕.c A t y).ofLp j)hBt: (j : Fin d), Differentiable fun s => Space.deriv j (fun y => magneticFieldMatrix 𝓕.c A s y (j, i)) xhJt:Differentiable fun s => (LorentzCurrentDensity.currentDensity 𝓕.c J s x).ofLp i 0 All goals completed! 🐙) d:A:ElectromagneticPotential d𝓕:FreeSpacehA:ContDiff A.valJ:LorentzCurrentDensity dhJ:ContDiff Jh:IsExtrema 𝓕 A Jt:Timex:Space di:Fin dhEs: (j : Fin d), ContDiff 2 fun y => (electricField 𝓕.c A t y).ofLp jhEd: (j k : Fin d), Differentiable (Space.deriv k fun y => (electricField 𝓕.c A t y).ofLp j)hBt: (j : Fin d), Differentiable fun s => Space.deriv j (fun y => magneticFieldMatrix 𝓕.c A s y (j, i)) xhJt:Differentiable fun s => (LorentzCurrentDensity.currentDensity 𝓕.c J s x).ofLp iContDiff A.val All goals completed! 🐙 d:A:ElectromagneticPotential d𝓕:FreeSpacehA:ContDiff A.valJ:LorentzCurrentDensity dhJ:ContDiff Jh:IsExtrema 𝓕 A Jt:Timex:Space di:Fin dhEs: (j : Fin d), ContDiff 2 fun y => (electricField 𝓕.c A t y).ofLp jhEd: (j k : Fin d), Differentiable (Space.deriv k fun y => (electricField 𝓕.c A t y).ofLp j)hBt: (j : Fin d), Differentiable fun s => Space.deriv j (fun y => magneticFieldMatrix 𝓕.c A s y (j, i)) xhJt:Differentiable fun s => (LorentzCurrentDensity.currentDensity 𝓕.c J s x).ofLp iContDiff J All goals completed! 🐙 _ = 𝓕.c ^ 2 * j, (∂[j] (∂[j] (A.electricField 𝓕.c t · i)) x) - 𝓕.c ^ 2 / 𝓕.ε₀ * ∂[i] (J.chargeDensity 𝓕.c t ·) x - 𝓕.c ^ 2 * 𝓕.μ₀ * ∂ₜ (J.currentDensity 𝓕.c · x i) t := d:A:ElectromagneticPotential d𝓕:FreeSpacehA:ContDiff A.valJ:LorentzCurrentDensity dhJ:ContDiff Jh:IsExtrema 𝓕 A Jt:Timex:Space di:Fin dhEs: (j : Fin d), ContDiff 2 fun y => (electricField 𝓕.c A t y).ofLp jhEd: (j k : Fin d), Differentiable (Space.deriv k fun y => (electricField 𝓕.c A t y).ofLp j)hBt: (j : Fin d), Differentiable fun s => Space.deriv j (fun y => magneticFieldMatrix 𝓕.c A s y (j, i)) xhJt:Differentiable fun s => (LorentzCurrentDensity.currentDensity 𝓕.c J s x).ofLp i1 / (𝓕.μ₀ * 𝓕.ε₀) * j, Space.deriv j (Space.deriv j fun x => (electricField 𝓕.c A t x).ofLp i) x - 1 / (𝓕.μ₀ * 𝓕.ε₀ ^ 2) * Space.deriv i (fun x => LorentzCurrentDensity.chargeDensity 𝓕.c J t x) x - 1 / 𝓕.ε₀ * ∂ₜ (fun x_1 => (LorentzCurrentDensity.currentDensity 𝓕.c J x_1 x).ofLp i) t = 𝓕.c.val ^ 2 * j, Space.deriv j (Space.deriv j fun x => (electricField 𝓕.c A t x).ofLp i) x - 𝓕.c.val ^ 2 / 𝓕.ε₀ * Space.deriv i (fun x => LorentzCurrentDensity.chargeDensity 𝓕.c J t x) x - 𝓕.c.val ^ 2 * 𝓕.μ₀ * ∂ₜ (fun x_1 => (LorentzCurrentDensity.currentDensity 𝓕.c J x_1 x).ofLp i) t d:A:ElectromagneticPotential d𝓕:FreeSpacehA:ContDiff A.valJ:LorentzCurrentDensity dhJ:ContDiff Jh:IsExtrema 𝓕 A Jt:Timex:Space di:Fin dhEs: (j : Fin d), ContDiff 2 fun y => (electricField 𝓕.c A t y).ofLp jhEd: (j k : Fin d), Differentiable (Space.deriv k fun y => (electricField 𝓕.c A t y).ofLp j)hBt: (j : Fin d), Differentiable fun s => Space.deriv j (fun y => magneticFieldMatrix 𝓕.c A s y (j, i)) xhJt:Differentiable fun s => (LorentzCurrentDensity.currentDensity 𝓕.c J s x).ofLp i𝓕.ε₀⁻¹ * 𝓕.μ₀⁻¹ * x_1, Space.deriv x_1 (Space.deriv x_1 fun x => (electricField 𝓕.c A t x).ofLp i) x - (𝓕.ε₀ ^ 2)⁻¹ * 𝓕.μ₀⁻¹ * Space.deriv i (fun x => LorentzCurrentDensity.chargeDensity 𝓕.c J t x) x - 𝓕.ε₀⁻¹ * ∂ₜ (fun x_1 => (LorentzCurrentDensity.currentDensity 𝓕.c J x_1 x).ofLp i) t = 𝓕.μ₀⁻¹ * 𝓕.ε₀⁻¹ * x_1, Space.deriv x_1 (Space.deriv x_1 fun x => (electricField 𝓕.c A t x).ofLp i) x - 𝓕.μ₀⁻¹ * 𝓕.ε₀⁻¹ / 𝓕.ε₀ * Space.deriv i (fun x => LorentzCurrentDensity.chargeDensity 𝓕.c J t x) x - 𝓕.μ₀⁻¹ * 𝓕.ε₀⁻¹ * 𝓕.μ₀ * ∂ₜ (fun x_1 => (LorentzCurrentDensity.currentDensity 𝓕.c J x_1 x).ofLp i) t All goals completed! 🐙