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 d⊢ IsExtrema 𝓕 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 d⊢ Space.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))) = 0⊢ Space.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) = 0⊢ Space.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) = 0⊢ Space.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) = 0⊢ Space.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) = 0⊢ Space.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) = 0⊢ Space.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 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 ℝ ∞ 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 i⊢ 1 / (𝓕.μ₀ * 𝓕.ε₀) * ((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 i⊢ DifferentiableAt ℝ (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 i⊢ DifferentiableAt ℝ (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⊢ DifferentiableAt ℝ (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⊢ Differentiable ℝ (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 i⊢ Differentiable ℝ 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 i⊢ ContDiff ℝ ∞ 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 i⊢ ContDiff ℝ ∞ 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 i⊢ 1 / (𝓕.μ₀ * 𝓕.ε₀) * ∑ 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! 🐙