Physlib.Electromagnetism.Vacuum.Constant — Physlib

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.IsExtrema

The constant electric and magnetic fields

i. Overview

In this module we define the electromagnetic potential which gives rise to a given constant electric and magnetic field matrix.

We will show that this electromagnetic potential is an extrema of the free-space electromagnetic action.

ii. Key results

iii. Table of contents

A. The definition of the potential

B. Smoothness of the potential

C. The scalar potential

D. The vector potential

D.1. Time derivative of the vector potential

D.2. Space derivative of the vector potential

E. The electric field

F. The magnetic field

G. Is extrema

iv. References

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

A. The definition of the potential

The electromagnetic potential which gives rise to a constant electric field E₀ and a constant magnetic field matrix B₀.

set_option linter.unusedVariables false

An electric potential which gives a given constant E-field and B-field.

@[nolint unusedArguments]
noncomputable def constantEB {d : ℕ} (c : SpeedOfLight)
    (E₀ : EuclideanSpace ℝ (Fin d)) (B₀ : Fin d × Fin d → ℝ)
    (B₀_antisymm : ∀ i j, B₀ (i, j) = - B₀ (j, i)) : ElectromagneticPotential d where
  val := fun x μ =>
  match μ with
  | Sum.inl _ => - (1/c) * ⟪E₀, Space.basis.repr x.space⟫_ℝ
  | Sum.inr i => (1/2) * ∑ j, B₀ (i, j) * x.space j

B. Smoothness of the potential

The potential is smooth.



lemma constantEB_smooth {c : SpeedOfLight}
    {E₀ : EuclideanSpace ℝ (Fin d)} {B₀ : Fin d × Fin d → ℝ}
    {B₀_antisymm : ∀ i j, B₀ (i, j) = - B₀ (j, i)} :
    ContDiff ℝ ∞ (constantEB c E₀ B₀ B₀_antisymm) := byd:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)⊢ ContDiff ℝ ∞ (constantEB c E₀ B₀ B₀_antisymm).val
  rw [← Lorentz.Vector.contDiff_applyd:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)⊢ ∀ (i : Fin 1 ⊕ Fin d), ContDiff ℝ ∞ fun x => (constantEB c E₀ B₀ B₀_antisymm).val x id:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)⊢ ∀ (i : Fin 1 ⊕ Fin d), ContDiff ℝ ∞ fun x => (constantEB c E₀ B₀ B₀_antisymm).val x i]d:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)⊢ ∀ (i : Fin 1 ⊕ Fin d), ContDiff ℝ ∞ fun x => (constantEB c E₀ B₀ B₀_antisymm).val x i
  intro μd:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)μ:Fin 1 ⊕ Fin d⊢ ContDiff ℝ ∞ fun x => (constantEB c E₀ B₀ B₀_antisymm).val x μ
  match μ with
  | Sum.inl _ =>d:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)μ:Fin 1 ⊕ Fin dval✝:Fin 1⊢ ContDiff ℝ ∞ fun x => (constantEB c E₀ B₀ B₀_antisymm).val x (Sum.inl val✝)
      simp [constantEB]d:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)μ:Fin 1 ⊕ Fin dval✝:Fin 1⊢ ContDiff ℝ ∞ fun x => -(c.val⁻¹ * ⟪E₀, Space.basis.repr (space x)⟫_ℝ)
      apply ContDiff.negd:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)μ:Fin 1 ⊕ Fin dval✝:Fin 1⊢ ContDiff ℝ ∞ fun x => c.val⁻¹ * ⟪E₀, Space.basis.repr (space x)⟫_ℝ
      apply ContDiff.mulhfd:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)μ:Fin 1 ⊕ Fin dval✝:Fin 1⊢ ContDiff ℝ ∞ fun x => c.val⁻¹hgd:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)μ:Fin 1 ⊕ Fin dval✝:Fin 1⊢ ContDiff ℝ ∞ fun x => ⟪E₀, Space.basis.repr (space x)⟫_ℝ
      ·hfd:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)μ:Fin 1 ⊕ Fin dval✝:Fin 1⊢ ContDiff ℝ ∞ fun x => c.val⁻¹ fun_propAll goals completed! 🐙
      apply ContDiff.innerhg.hfd:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)μ:Fin 1 ⊕ Fin dval✝:Fin 1⊢ ContDiff ℝ ∞ fun x => E₀hg.hgd:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)μ:Fin 1 ⊕ Fin dval✝:Fin 1⊢ ContDiff ℝ ∞ fun x => Space.basis.repr (space x)
      ·hg.hfd:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)μ:Fin 1 ⊕ Fin dval✝:Fin 1⊢ ContDiff ℝ ∞ fun x => E₀ fun_propAll goals completed! 🐙
      ·hg.hgd:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)μ:Fin 1 ⊕ Fin dval✝:Fin 1⊢ ContDiff ℝ ∞ fun x => Space.basis.repr (space x) fun_propAll goals completed! 🐙
  | Sum.inr i =>d:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)μ:Fin 1 ⊕ Fin di:Fin d⊢ ContDiff ℝ ∞ fun x => (constantEB c E₀ B₀ B₀_antisymm).val x (Sum.inr i)
      simp [constantEB]d:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)μ:Fin 1 ⊕ Fin di:Fin d⊢ ContDiff ℝ ∞ fun x => 2⁻¹ * ∑ j, B₀ (i, j) * (space x).val j
      apply ContDiff.mulhfd:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)μ:Fin 1 ⊕ Fin di:Fin d⊢ ContDiff ℝ ∞ fun x => 2⁻¹hgd:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)μ:Fin 1 ⊕ Fin di:Fin d⊢ ContDiff ℝ ∞ fun x => ∑ j, B₀ (i, j) * (space x).val j
      ·hfd:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)μ:Fin 1 ⊕ Fin di:Fin d⊢ ContDiff ℝ ∞ fun x => 2⁻¹ fun_propAll goals completed! 🐙
      ·hgd:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)μ:Fin 1 ⊕ Fin di:Fin d⊢ ContDiff ℝ ∞ fun x => ∑ j, B₀ (i, j) * (space x).val j apply ContDiff.sumhgd:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)μ:Fin 1 ⊕ Fin di:Fin d⊢ ∀ i_1 ∈ Finset.univ, ContDiff ℝ ∞ fun x => B₀ (i, i_1) * (space x).val i_1
        intro j _hgd:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)μ:Fin 1 ⊕ Fin di:Fin dj:Fin da✝:j ∈ Finset.univ⊢ ContDiff ℝ ∞ fun x => B₀ (i, j) * (space x).val j
        apply ContDiff.mulhg.hfd:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)μ:Fin 1 ⊕ Fin di:Fin dj:Fin da✝:j ∈ Finset.univ⊢ ContDiff ℝ ∞ fun x => B₀ (i, j)hgd:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)μ:Fin 1 ⊕ Fin di:Fin dj:Fin da✝:j ∈ Finset.univ⊢ ContDiff ℝ ∞ fun x => (space x).val j
        ·hg.hfd:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)μ:Fin 1 ⊕ Fin di:Fin dj:Fin da✝:j ∈ Finset.univ⊢ ContDiff ℝ ∞ fun x => B₀ (i, j) fun_propAll goals completed! 🐙
        fun_propAll goals completed! 🐙

C. The scalar potential

The scalar potential of the electromagnetic potential is given by -⟪E₀, x⟫.

lemma constantEB_scalarPotential {c : SpeedOfLight}
    {E₀ : EuclideanSpace ℝ (Fin d)} {B₀ : Fin d × Fin d → ℝ}
    {B₀_antisymm : ∀ i j, B₀ (i, j) = - B₀ (j, i)} :
    (constantEB c E₀ B₀ B₀_antisymm).scalarPotential c = fun _ x =>
      -⟪E₀, Space.basis.repr x⟫_ℝ := byd:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)⊢ scalarPotential c (constantEB c E₀ B₀ B₀_antisymm) = fun x x_1 => -⟪E₀, Space.basis.repr x_1⟫_ℝ
  ext t xd:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)t:Timex:Space d⊢ scalarPotential c (constantEB c E₀ B₀ B₀_antisymm) t x = -⟪E₀, Space.basis.repr x⟫_ℝ
  simp [scalarPotential, timeSlice, constantEB, Equiv.coe_fn_mk,
    Function.curry_apply, Function.comp_apply]All goals completed! 🐙

D. The vector potential

The vector potential of the electromagnetic potential is (1 / 2) * ∑ j, B₀ (i, j) * x j .

lemma constantEB_vectorPotential {c : SpeedOfLight}
    {E₀ : EuclideanSpace ℝ (Fin d)} {B₀ : Fin d × Fin d → ℝ}
    {B₀_antisymm : ∀ i j, B₀ (i, j) = - B₀ (j, i)} :
    (constantEB c E₀ B₀ B₀_antisymm).vectorPotential c = fun _ x => WithLp.toLp 2 fun i =>
      (1 / 2) * ∑ j, B₀ (i, j) * x j := byd:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)⊢ vectorPotential c (constantEB c E₀ B₀ B₀_antisymm) = fun x x_1 =>
  WithLp.toLp 2 fun i => 1 / 2 * ∑ j, B₀ (i, j) * x_1.val j
  ext t x id:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)t:Timex:Space di:Fin d⊢ (vectorPotential c (constantEB c E₀ B₀ B₀_antisymm) t x).ofLp i =
  (WithLp.toLp 2 fun i => 1 / 2 * ∑ j, B₀ (i, j) * x.val j).ofLp i
  simp [vectorPotential, timeSlice, constantEB, space_toCoord_symm, Equiv.coe_fn_mk,
    Function.curry_apply, Function.comp_apply]All goals completed! 🐙

D.1. Time derivative of the vector potential



@[simp]
lemma constantEB_vectorPotential_time_deriv {c : SpeedOfLight}
    {E₀ : EuclideanSpace ℝ (Fin d)} {B₀ : Fin d × Fin d → ℝ}
    {B₀_antisymm : ∀ i j, B₀ (i, j) = - B₀ (j, i)} (t : Time) (x : Space d) :
    ∂ₜ ((constantEB c E₀ B₀ B₀_antisymm).vectorPotential c · x) t = 0 := byd:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)t:Timex:Space d⊢ ∂ₜ (fun x_1 => vectorPotential c (constantEB c E₀ B₀ B₀_antisymm) x_1 x) t = 0
  rw [constantEB_vectorPotentiald:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)t:Timex:Space d⊢ ∂ₜ (fun x_1 => (fun x x_2 => WithLp.toLp 2 fun i => 1 / 2 * ∑ j, B₀ (i, j) * x_2.val j) x_1 x) t = 0d:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)t:Timex:Space d⊢ ∂ₜ (fun x_1 => (fun x x_2 => WithLp.toLp 2 fun i => 1 / 2 * ∑ j, B₀ (i, j) * x_2.val j) x_1 x) t = 0]d:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)t:Timex:Space d⊢ ∂ₜ (fun x_1 => (fun x x_2 => WithLp.toLp 2 fun i => 1 / 2 * ∑ j, B₀ (i, j) * x_2.val j) x_1 x) t = 0
  simpAll goals completed! 🐙

D.2. Space derivative of the vector potential



lemma constantEB_vectorPotential_space_deriv {c : SpeedOfLight}
    {E₀ : EuclideanSpace ℝ (Fin d)} {B₀ : Fin d × Fin d → ℝ}
    {B₀_antisymm : ∀ i j, B₀ (i, j) = - B₀ (j, i)} (t : Time) (x : Space d) (i j : Fin d) :
    Space.deriv i ((constantEB c E₀ B₀ B₀_antisymm).vectorPotential c t · j) x =
    (1 / 2) * B₀ (j, i) := byd:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)t:Timex:Space di:Fin dj:Fin d⊢ Space.deriv i (fun x => (vectorPotential c (constantEB c E₀ B₀ B₀_antisymm) t x).ofLp j) x = 1 / 2 * B₀ (j, i)
  rw [constantEB_vectorPotentiald:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)t:Timex:Space di:Fin dj:Fin d⊢ Space.deriv i (fun x => ((fun x x_1 => WithLp.toLp 2 fun i => 1 / 2 * ∑ j, B₀ (i, j) * x_1.val j) t x).ofLp j) x =
  1 / 2 * B₀ (j, i)d:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)t:Timex:Space di:Fin dj:Fin d⊢ Space.deriv i (fun x => ((fun x x_1 => WithLp.toLp 2 fun i => 1 / 2 * ∑ j, B₀ (i, j) * x_1.val j) t x).ofLp j) x =
  1 / 2 * B₀ (j, i)]d:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)t:Timex:Space di:Fin dj:Fin d⊢ Space.deriv i (fun x => ((fun x x_1 => WithLp.toLp 2 fun i => 1 / 2 * ∑ j, B₀ (i, j) * x_1.val j) t x).ofLp j) x =
  1 / 2 * B₀ (j, i)
  rw [Space.deriv_eqd:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)t:Timex:Space di:Fin dj:Fin d⊢ (fderiv ℝ (fun x => ((fun x x_1 => WithLp.toLp 2 fun i => 1 / 2 * ∑ j, B₀ (i, j) * x_1.val j) t x).ofLp j) x)
    (Space.basis i) =
  1 / 2 * B₀ (j, i)d:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)t:Timex:Space di:Fin dj:Fin d⊢ (fderiv ℝ (fun x => ((fun x x_1 => WithLp.toLp 2 fun i => 1 / 2 * ∑ j, B₀ (i, j) * x_1.val j) t x).ofLp j) x)
    (Space.basis i) =
  1 / 2 * B₀ (j, i)]d:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)t:Timex:Space di:Fin dj:Fin d⊢ (fderiv ℝ (fun x => ((fun x x_1 => WithLp.toLp 2 fun i => 1 / 2 * ∑ j, B₀ (i, j) * x_1.val j) t x).ofLp j) x)
    (Space.basis i) =
  1 / 2 * B₀ (j, i)
  rw [fderiv_const_mul (byd:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)t:Timex:Space di:Fin dj:Fin d⊢ DifferentiableAt ℝ (fun x => ∑ j_1, B₀ (j, j_1) * x.val j_1) xd:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)t:Timex:Space di:Fin dj:Fin d⊢ ((1 / 2) • fderiv ℝ (fun x => ∑ j_1, B₀ (j, j_1) * x.val j_1) x) (Space.basis i) = 1 / 2 * B₀ (j, i) fun_propAll goals completed! 🐙d:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)t:Timex:Space di:Fin dj:Fin d⊢ ((1 / 2) • fderiv ℝ (fun x => ∑ j_1, B₀ (j, j_1) * x.val j_1) x) (Space.basis i) = 1 / 2 * B₀ (j, i))]d:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)t:Timex:Space di:Fin dj:Fin d⊢ ((1 / 2) • fderiv ℝ (fun x => ∑ j_1, B₀ (j, j_1) * x.val j_1) x) (Space.basis i) = 1 / 2 * B₀ (j, i)
  rw [fderiv_fun_sum (byd:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)t:Timex:Space di:Fin dj:Fin d⊢ ∀ i ∈ Finset.univ, DifferentiableAt ℝ (fun x => B₀ (j, i) * x.val i) xd:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)t:Timex:Space di:Fin dj:Fin d⊢ ((1 / 2) • ∑ i, fderiv ℝ (fun x => B₀ (j, i) * x.val i) x) (Space.basis i) = 1 / 2 * B₀ (j, i) fun_propAll goals completed! 🐙d:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)t:Timex:Space di:Fin dj:Fin d⊢ ((1 / 2) • ∑ i, fderiv ℝ (fun x => B₀ (j, i) * x.val i) x) (Space.basis i) = 1 / 2 * B₀ (j, i))]d:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)t:Timex:Space di:Fin dj:Fin d⊢ ((1 / 2) • ∑ i, fderiv ℝ (fun x => B₀ (j, i) * x.val i) x) (Space.basis i) = 1 / 2 * B₀ (j, i)
  simp only [one_div, FunLike.coe_smul, FunLike.coe_sum, Pi.smul_apply,
    Finset.sum_apply, smul_eq_mul, mul_eq_mul_left_iff, inv_eq_zero, OfNat.ofNat_ne_zero, or_false]d:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)t:Timex:Space di:Fin dj:Fin d⊢ ∑ c, (fderiv ℝ (fun x => B₀ (j, c) * x.val c) x) (Space.basis i) = B₀ (j, i)
  rw [Finset.sum_eq_single id:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)t:Timex:Space di:Fin dj:Fin d⊢ (fderiv ℝ (fun x => B₀ (j, i) * x.val i) x) (Space.basis i) = B₀ (j, i)h₀d:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)t:Timex:Space di:Fin dj:Fin d⊢ ∀ b ∈ Finset.univ, b ≠ i → (fderiv ℝ (fun x => B₀ (j, b) * x.val b) x) (Space.basis i) = 0h₁d:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)t:Timex:Space di:Fin dj:Fin d⊢ i ∉ Finset.univ → (fderiv ℝ (fun x => B₀ (j, i) * x.val i) x) (Space.basis i) = 0d:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)t:Timex:Space di:Fin dj:Fin d⊢ (fderiv ℝ (fun x => B₀ (j, i) * x.val i) x) (Space.basis i) = B₀ (j, i)h₀d:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)t:Timex:Space di:Fin dj:Fin d⊢ ∀ b ∈ Finset.univ, b ≠ i → (fderiv ℝ (fun x => B₀ (j, b) * x.val b) x) (Space.basis i) = 0h₁d:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)t:Timex:Space di:Fin dj:Fin d⊢ i ∉ Finset.univ → (fderiv ℝ (fun x => B₀ (j, i) * x.val i) x) (Space.basis i) = 0]d:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)t:Timex:Space di:Fin dj:Fin d⊢ (fderiv ℝ (fun x => B₀ (j, i) * x.val i) x) (Space.basis i) = B₀ (j, i)h₀d:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)t:Timex:Space di:Fin dj:Fin d⊢ ∀ b ∈ Finset.univ, b ≠ i → (fderiv ℝ (fun x => B₀ (j, b) * x.val b) x) (Space.basis i) = 0h₁d:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)t:Timex:Space di:Fin dj:Fin d⊢ i ∉ Finset.univ → (fderiv ℝ (fun x => B₀ (j, i) * x.val i) x) (Space.basis i) = 0
  ·d:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)t:Timex:Space di:Fin dj:Fin d⊢ (fderiv ℝ (fun x => B₀ (j, i) * x.val i) x) (Space.basis i) = B₀ (j, i) rw [fderiv_const_mul (byd:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)t:Timex:Space di:Fin dj:Fin d⊢ DifferentiableAt ℝ (fun x => x.val i) xd:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)t:Timex:Space di:Fin dj:Fin d⊢ (B₀ (j, i) • fderiv ℝ (fun x => x.val i) x) (Space.basis i) = B₀ (j, i) fun_propAll goals completed! 🐙d:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)t:Timex:Space di:Fin dj:Fin d⊢ (B₀ (j, i) • fderiv ℝ (fun x => x.val i) x) (Space.basis i) = B₀ (j, i))]d:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)t:Timex:Space di:Fin dj:Fin d⊢ (B₀ (j, i) • fderiv ℝ (fun x => x.val i) x) (Space.basis i) = B₀ (j, i)
    simp [← Space.deriv_eq]All goals completed! 🐙
  ·h₀d:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)t:Timex:Space di:Fin dj:Fin d⊢ ∀ b ∈ Finset.univ, b ≠ i → (fderiv ℝ (fun x => B₀ (j, b) * x.val b) x) (Space.basis i) = 0 intro k _ hkh₀d:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)t:Timex:Space di:Fin dj:Fin dk:Fin da✝:k ∈ Finset.univhk:k ≠ i⊢ (fderiv ℝ (fun x => B₀ (j, k) * x.val k) x) (Space.basis i) = 0
    rw [fderiv_const_mul (byd:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)t:Timex:Space di:Fin dj:Fin dk:Fin da✝:k ∈ Finset.univhk:k ≠ i⊢ DifferentiableAt ℝ (fun x => x.val k) xh₀d:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)t:Timex:Space di:Fin dj:Fin dk:Fin da✝:k ∈ Finset.univhk:k ≠ i⊢ (B₀ (j, k) • fderiv ℝ (fun x => x.val k) x) (Space.basis i) = 0 fun_propAll goals completed! 🐙h₀d:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)t:Timex:Space di:Fin dj:Fin dk:Fin da✝:k ∈ Finset.univhk:k ≠ i⊢ (B₀ (j, k) • fderiv ℝ (fun x => x.val k) x) (Space.basis i) = 0)]h₀d:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)t:Timex:Space di:Fin dj:Fin dk:Fin da✝:k ∈ Finset.univhk:k ≠ i⊢ (B₀ (j, k) • fderiv ℝ (fun x => x.val k) x) (Space.basis i) = 0
    simp [← Space.deriv_eq]h₀d:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)t:Timex:Space di:Fin dj:Fin dk:Fin da✝:k ∈ Finset.univhk:k ≠ i⊢ B₀ (j, k) = 0 ∨ Space.deriv i (fun x => x.val k) x = 0
    rw [Space.deriv_component_diffh₀d:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)t:Timex:Space di:Fin dj:Fin dk:Fin da✝:k ∈ Finset.univhk:k ≠ i⊢ B₀ (j, k) = 0 ∨ 0 = 0h₀.hd:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)t:Timex:Space di:Fin dj:Fin dk:Fin da✝:k ∈ Finset.univhk:k ≠ i⊢ i ≠ kh₀d:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)t:Timex:Space di:Fin dj:Fin dk:Fin da✝:k ∈ Finset.univhk:k ≠ i⊢ B₀ (j, k) = 0 ∨ 0 = 0h₀.hd:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)t:Timex:Space di:Fin dj:Fin dk:Fin da✝:k ∈ Finset.univhk:k ≠ i⊢ i ≠ k]h₀d:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)t:Timex:Space di:Fin dj:Fin dk:Fin da✝:k ∈ Finset.univhk:k ≠ i⊢ B₀ (j, k) = 0 ∨ 0 = 0h₀.hd:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)t:Timex:Space di:Fin dj:Fin dk:Fin da✝:k ∈ Finset.univhk:k ≠ i⊢ i ≠ k
    simp only [or_true]h₀.hd:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)t:Timex:Space di:Fin dj:Fin dk:Fin da✝:k ∈ Finset.univhk:k ≠ i⊢ i ≠ k
    exact id (Ne.symm hk)All goals completed! 🐙
  ·h₁d:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)t:Timex:Space di:Fin dj:Fin d⊢ i ∉ Finset.univ → (fderiv ℝ (fun x => B₀ (j, i) * x.val i) x) (Space.basis i) = 0 simpAll goals completed! 🐙

E. The electric field



@[simp]
lemma constantEB_electricField {c : SpeedOfLight}
    {E₀ : EuclideanSpace ℝ (Fin d)} {B₀ : Fin d × Fin d → ℝ}
    {B₀_antisymm : ∀ i j, B₀ (i, j) = - B₀ (j, i)} :
    (constantEB c E₀ B₀ B₀_antisymm).electricField c = fun _ _ => E₀ := byd:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)⊢ electricField c (constantEB c E₀ B₀ B₀_antisymm) = fun x x_1 => E₀
  funext t xd:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)t:Timex:Space d⊢ electricField c (constantEB c E₀ B₀ B₀_antisymm) t x = E₀
  rw [electricField_eqd:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)t:Timex:Space d⊢ (fun t x =>
      -Space.grad (scalarPotential c (constantEB c E₀ B₀ B₀_antisymm) t) x -
        ∂ₜ (fun t => vectorPotential c (constantEB c E₀ B₀ B₀_antisymm) t x) t)
    t x =
  E₀d:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)t:Timex:Space d⊢ (fun t x =>
      -Space.grad (scalarPotential c (constantEB c E₀ B₀ B₀_antisymm) t) x -
        ∂ₜ (fun t => vectorPotential c (constantEB c E₀ B₀ B₀_antisymm) t x) t)
    t x =
  E₀]d:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)t:Timex:Space d⊢ (fun t x =>
      -Space.grad (scalarPotential c (constantEB c E₀ B₀ B₀_antisymm) t) x -
        ∂ₜ (fun t => vectorPotential c (constantEB c E₀ B₀ B₀_antisymm) t x) t)
    t x =
  E₀
  simp [constantEB_scalarPotential]d:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)t:Timex:Space d⊢ -Space.grad (fun x => -⟪E₀, Space.basis.repr x⟫_ℝ) x = E₀
  erw [Space.grad_negd:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)t:Timex:Space d⊢ -(-Space.grad fun x => ⟪E₀, Space.basis.repr x⟫_ℝ) x = E₀]d:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)t:Timex:Space d⊢ -(-Space.grad fun x => ⟪E₀, Space.basis.repr x⟫_ℝ) x = E₀
  conv_lhs =>
    enter [1, 1,1, x]d:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)t:Timex✝:Space dx:Space d| ⟪E₀, Space.basis.repr x⟫_ℝ
    rw [real_inner_comm, Space.basis_repr_inner_eq, real_inner_comm]d:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)t:Timex✝:Space dx:Space d| ⟪Space.basis.repr.symm E₀, x⟫_ℝ
  rw [Space.grad_inner_rightd:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)t:Timex:Space d⊢ -(-fun x => Space.basis.repr (Space.basis.repr.symm E₀)) x = E₀d:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)t:Timex:Space d⊢ -(-fun x => Space.basis.repr (Space.basis.repr.symm E₀)) x = E₀]d:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)t:Timex:Space d⊢ -(-fun x => Space.basis.repr (Space.basis.repr.symm E₀)) x = E₀
  simpAll goals completed! 🐙

F. The magnetic field



@[simp]
lemma constantEB_magneticFieldMatrix {c : SpeedOfLight}
    {E₀ : EuclideanSpace ℝ (Fin d)} {B₀ : Fin d × Fin d → ℝ}
    {B₀_antisymm : ∀ i j, B₀ (i, j) = - B₀ (j, i)} :
    (constantEB c E₀ B₀ B₀_antisymm).magneticFieldMatrix c = fun _ _ => B₀ := byd:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)⊢ magneticFieldMatrix c (constantEB c E₀ B₀ B₀_antisymm) = fun x x_1 => B₀
  funext t xd:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)t:Timex:Space d⊢ magneticFieldMatrix c (constantEB c E₀ B₀ B₀_antisymm) t x = B₀
  funext id:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)t:Timex:Space di:Fin d × Fin d⊢ magneticFieldMatrix c (constantEB c E₀ B₀ B₀_antisymm) t x i = B₀ i
  match i with
  | (i, j) =>d:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)t:Timex:Space di✝:Fin d × Fin di:Fin dj:Fin d⊢ magneticFieldMatrix c (constantEB c E₀ B₀ B₀_antisymm) t x (i, j) = B₀ (i, j)
  rw [magneticFieldMatrix_eq_vectorPotentiald:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)t:Timex:Space di✝:Fin d × Fin di:Fin dj:Fin d⊢ Space.deriv j (fun x => (vectorPotential c (constantEB c E₀ B₀ B₀_antisymm) t x).ofLp i) x -
    Space.deriv i (fun x => (vectorPotential c (constantEB c E₀ B₀ B₀_antisymm) t x).ofLp j) x =
  B₀ (i, j)hAd:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)t:Timex:Space di✝:Fin d × Fin di:Fin dj:Fin d⊢ Differentiable ℝ (constantEB c E₀ B₀ B₀_antisymm).vald:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)t:Timex:Space di✝:Fin d × Fin di:Fin dj:Fin d⊢ Space.deriv j (fun x => (vectorPotential c (constantEB c E₀ B₀ B₀_antisymm) t x).ofLp i) x -
    Space.deriv i (fun x => (vectorPotential c (constantEB c E₀ B₀ B₀_antisymm) t x).ofLp j) x =
  B₀ (i, j)hAd:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)t:Timex:Space di✝:Fin d × Fin di:Fin dj:Fin d⊢ Differentiable ℝ (constantEB c E₀ B₀ B₀_antisymm).val]d:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)t:Timex:Space di✝:Fin d × Fin di:Fin dj:Fin d⊢ Space.deriv j (fun x => (vectorPotential c (constantEB c E₀ B₀ B₀_antisymm) t x).ofLp i) x -
    Space.deriv i (fun x => (vectorPotential c (constantEB c E₀ B₀ B₀_antisymm) t x).ofLp j) x =
  B₀ (i, j)hAd:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)t:Timex:Space di✝:Fin d × Fin di:Fin dj:Fin d⊢ Differentiable ℝ (constantEB c E₀ B₀ B₀_antisymm).val
  rw [constantEB_vectorPotential_space_deriv,d:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)t:Timex:Space di✝:Fin d × Fin di:Fin dj:Fin d⊢ 1 / 2 * B₀ (i, j) - Space.deriv i (fun x => (vectorPotential c (constantEB c E₀ B₀ B₀_antisymm) t x).ofLp j) x =
  B₀ (i, j)hAd:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)t:Timex:Space di✝:Fin d × Fin di:Fin dj:Fin d⊢ Differentiable ℝ (constantEB c E₀ B₀ B₀_antisymm).vald:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)t:Timex:Space di✝:Fin d × Fin di:Fin dj:Fin d⊢ 1 / 2 * B₀ (i, j) - 1 / 2 * B₀ (j, i) = B₀ (i, j)hAd:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)t:Timex:Space di✝:Fin d × Fin di:Fin dj:Fin d⊢ Differentiable ℝ (constantEB c E₀ B₀ B₀_antisymm).val constantEB_vectorPotential_space_derivd:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)t:Timex:Space di✝:Fin d × Fin di:Fin dj:Fin d⊢ 1 / 2 * B₀ (i, j) - 1 / 2 * B₀ (j, i) = B₀ (i, j)hAd:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)t:Timex:Space di✝:Fin d × Fin di:Fin dj:Fin d⊢ Differentiable ℝ (constantEB c E₀ B₀ B₀_antisymm).vald:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)t:Timex:Space di✝:Fin d × Fin di:Fin dj:Fin d⊢ 1 / 2 * B₀ (i, j) - 1 / 2 * B₀ (j, i) = B₀ (i, j)hAd:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)t:Timex:Space di✝:Fin d × Fin di:Fin dj:Fin d⊢ Differentiable ℝ (constantEB c E₀ B₀ B₀_antisymm).val]d:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)t:Timex:Space di✝:Fin d × Fin di:Fin dj:Fin d⊢ 1 / 2 * B₀ (i, j) - 1 / 2 * B₀ (j, i) = B₀ (i, j)hAd:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)t:Timex:Space di✝:Fin d × Fin di:Fin dj:Fin d⊢ Differentiable ℝ (constantEB c E₀ B₀ B₀_antisymm).val
  conv_lhs =>
    enter [2]d:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)t:Timex:Space di✝:Fin d × Fin di:Fin dj:Fin d| 1 / 2 * B₀ (j, i)
    rw [B₀_antisymm]d:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)t:Timex:Space di✝:Fin d × Fin di:Fin dj:Fin d| 1 / 2 * -B₀ (i, j)
  ringhAd:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)t:Timex:Space di✝:Fin d × Fin di:Fin dj:Fin d⊢ Differentiable ℝ (constantEB c E₀ B₀ B₀_antisymm).val
  apply constantEB_smooth.differentiable (byd:ℕc:SpeedOfLightE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)t:Timex:Space di✝:Fin d × Fin di:Fin dj:Fin d⊢ ∞ ≠ 0 simpAll goals completed! 🐙)

G. Is extrema



lemma constantEB_isExtrema {𝓕 : FreeSpace}
    {E₀ : EuclideanSpace ℝ (Fin d)} {B₀ : Fin d × Fin d → ℝ}
    {B₀_antisymm : ∀ i j, B₀ (i, j) = - B₀ (j, i)} :
    IsExtrema 𝓕 (constantEB 𝓕.c E₀ B₀ B₀_antisymm) 0 := byd:ℕ𝓕:FreeSpaceE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)⊢ IsExtrema 𝓕 (constantEB 𝓕.c E₀ B₀ B₀_antisymm) 0
  rw [isExtrema_iff_gauss_ampere_magneticFieldMatrixd:ℕ𝓕:FreeSpaceE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)⊢ ∀ (t : Time) (x : Space d),
  Space.div (electricField 𝓕.c (constantEB 𝓕.c E₀ B₀ B₀_antisymm) t) x =
      LorentzCurrentDensity.chargeDensity 𝓕.c 0 t x / 𝓕.ε₀ ∧
    ∀ (i : Fin d),
      𝓕.μ₀ * 𝓕.ε₀ * (∂ₜ (fun t => electricField 𝓕.c (constantEB 𝓕.c E₀ B₀ B₀_antisymm) t x) t).ofLp i =
        ∑ j, Space.deriv j (fun x => magneticFieldMatrix 𝓕.c (constantEB 𝓕.c E₀ B₀ B₀_antisymm) t x (j, i)) x -
          𝓕.μ₀ * (LorentzCurrentDensity.currentDensity 𝓕.c 0 t x).ofLp ihAd:ℕ𝓕:FreeSpaceE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)⊢ ContDiff ℝ ∞ (constantEB 𝓕.c E₀ B₀ B₀_antisymm).valhJd:ℕ𝓕:FreeSpaceE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)⊢ ContDiff ℝ ∞ 0d:ℕ𝓕:FreeSpaceE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)⊢ ∀ (t : Time) (x : Space d),
  Space.div (electricField 𝓕.c (constantEB 𝓕.c E₀ B₀ B₀_antisymm) t) x =
      LorentzCurrentDensity.chargeDensity 𝓕.c 0 t x / 𝓕.ε₀ ∧
    ∀ (i : Fin d),
      𝓕.μ₀ * 𝓕.ε₀ * (∂ₜ (fun t => electricField 𝓕.c (constantEB 𝓕.c E₀ B₀ B₀_antisymm) t x) t).ofLp i =
        ∑ j, Space.deriv j (fun x => magneticFieldMatrix 𝓕.c (constantEB 𝓕.c E₀ B₀ B₀_antisymm) t x (j, i)) x -
          𝓕.μ₀ * (LorentzCurrentDensity.currentDensity 𝓕.c 0 t x).ofLp ihAd:ℕ𝓕:FreeSpaceE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)⊢ ContDiff ℝ ∞ (constantEB 𝓕.c E₀ B₀ B₀_antisymm).valhJd:ℕ𝓕:FreeSpaceE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)⊢ ContDiff ℝ ∞ 0]d:ℕ𝓕:FreeSpaceE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)⊢ ∀ (t : Time) (x : Space d),
  Space.div (electricField 𝓕.c (constantEB 𝓕.c E₀ B₀ B₀_antisymm) t) x =
      LorentzCurrentDensity.chargeDensity 𝓕.c 0 t x / 𝓕.ε₀ ∧
    ∀ (i : Fin d),
      𝓕.μ₀ * 𝓕.ε₀ * (∂ₜ (fun t => electricField 𝓕.c (constantEB 𝓕.c E₀ B₀ B₀_antisymm) t x) t).ofLp i =
        ∑ j, Space.deriv j (fun x => magneticFieldMatrix 𝓕.c (constantEB 𝓕.c E₀ B₀ B₀_antisymm) t x (j, i)) x -
          𝓕.μ₀ * (LorentzCurrentDensity.currentDensity 𝓕.c 0 t x).ofLp ihAd:ℕ𝓕:FreeSpaceE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)⊢ ContDiff ℝ ∞ (constantEB 𝓕.c E₀ B₀ B₀_antisymm).valhJd:ℕ𝓕:FreeSpaceE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)⊢ ContDiff ℝ ∞ 0
  ·d:ℕ𝓕:FreeSpaceE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)⊢ ∀ (t : Time) (x : Space d),
  Space.div (electricField 𝓕.c (constantEB 𝓕.c E₀ B₀ B₀_antisymm) t) x =
      LorentzCurrentDensity.chargeDensity 𝓕.c 0 t x / 𝓕.ε₀ ∧
    ∀ (i : Fin d),
      𝓕.μ₀ * 𝓕.ε₀ * (∂ₜ (fun t => electricField 𝓕.c (constantEB 𝓕.c E₀ B₀ B₀_antisymm) t x) t).ofLp i =
        ∑ j, Space.deriv j (fun x => magneticFieldMatrix 𝓕.c (constantEB 𝓕.c E₀ B₀ B₀_antisymm) t x (j, i)) x -
          𝓕.μ₀ * (LorentzCurrentDensity.currentDensity 𝓕.c 0 t x).ofLp i intro t xd:ℕ𝓕:FreeSpaceE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)t:Timex:Space d⊢ Space.div (electricField 𝓕.c (constantEB 𝓕.c E₀ B₀ B₀_antisymm) t) x =
    LorentzCurrentDensity.chargeDensity 𝓕.c 0 t x / 𝓕.ε₀ ∧
  ∀ (i : Fin d),
    𝓕.μ₀ * 𝓕.ε₀ * (∂ₜ (fun t => electricField 𝓕.c (constantEB 𝓕.c E₀ B₀ B₀_antisymm) t x) t).ofLp i =
      ∑ j, Space.deriv j (fun x => magneticFieldMatrix 𝓕.c (constantEB 𝓕.c E₀ B₀ B₀_antisymm) t x (j, i)) x -
        𝓕.μ₀ * (LorentzCurrentDensity.currentDensity 𝓕.c 0 t x).ofLp i
    simpAll goals completed! 🐙
  ·hAd:ℕ𝓕:FreeSpaceE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)⊢ ContDiff ℝ ∞ (constantEB 𝓕.c E₀ B₀ B₀_antisymm).val exact constantEB_smoothAll goals completed! 🐙
  ·hJd:ℕ𝓕:FreeSpaceE₀:EuclideanSpace ℝ (Fin d)B₀:Fin d × Fin d → ℝB₀_antisymm:∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)⊢ ContDiff ℝ ∞ 0 exact contDiff_zero_funAll goals completed! 🐙