Physlib.Electromagnetism.Kinematics.EMPotential

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.Mathematics.VariationalCalculus.HasVarAdjDeriv
public import Physlib.SpaceAndTime.SpaceTime.TimeSlice
public import Physlib.Mathematics.Calculus.ParametricIntegration

The Electromagnetic Potential

i. Overview

The electromagnetic potential A^μ is the fundamental objects in electromagnetism. Mathematically it is related to a connection on a U(1)-bundle.

We define the electromagnetic potential as a function from spacetime to contravariant Lorentz vectors.

ii. Key results

ElectromagneticPotential : is the type of electromagnetic potentials.

ElectromagneticPotential.deriv : the derivative tensor ∂_μ A^ν.

iii. Table of contents

A. The electromagnetic potential

A.1. Basic instances on the type of electromagnetic potentials

A.2. Basic constructors of the electromagnetic potential

A.3. The group action on the ElectromagneticPotential

A.4. Differentiability

A.5. The action on the space-time derivatives

A.6. Variational adjoint derivative of component

A.7. Variational adjoint derivative of derivatives of the potential

B. The derivative tensor of the electromagnetic potential

B.1. Equivariance of the derivative tensor

B.2. The elements of the derivative tensor in terms of the basis

iv. References

https://quantummechanics.ucsd.edu/ph130a/130_notes/node452.html

https://ph.qmul.ac.uk/sites/default/files/EMT10new.pdf

@[expose] public section

A. The electromagnetic potential

We define the electromagnetic potential as a function from spacetime to contravariant Lorentz vectors, and prove some simple results about it.

The electromagnetic potential is a tensor A^μ.

The underlying map from SpaceTime d to Lorentz.Vector d associated with an electromagnetic potential.

structure ElectromagneticPotential (d : ℕ := 3) where val : SpaceTime d → Lorentz.Vector d

              attribute [-simp] Fintype.sum_sum_typeattribute [-simp] Nat.succ_eq_add_one@[ext]
lemma eq_of_val_eq (A B : ElectromagneticPotential d) (h : A.val = B.val) : A = B :=
  congrArg ElectromagneticPotential.mk h

A.1. Basic instances on the type of electromagnetic potentials

              instance {d} : CoeFun (ElectromagneticPotential d)
    (fun _ => SpaceTime d → Lorentz.Vector d) where
  coe A := A.valinstance {d} : Zero (ElectromagneticPotential d) where
  zero := ⟨fun _ => 0⟩@[simp]
lemma zero_val {d} : (0 : ElectromagneticPotential d).val = 0 := rfl@[simp]
lemma zero_apply {d} (x : SpaceTime d) : (0 : ElectromagneticPotential d) x = 0 := rflinstance {d} : Add (ElectromagneticPotential d) where
  add A B := ⟨fun x => A x + B x⟩@[simp]
lemma add_val {d} (A B : ElectromagneticPotential d) :
    (A + B).val = A.val + B.val := rfl@[simp]
lemma add_apply {d} (A B : ElectromagneticPotential d) (x : SpaceTime d) :
    (A + B) x = A x + B x := byd:ℕA:ElectromagneticPotential dB:ElectromagneticPotential dx:SpaceTime d⊢ (A + B).val x = A.val x + B.val x simpAll goals completed! 🐙instance {d} : Neg (ElectromagneticPotential d) where
  neg A := ⟨fun x => - A x⟩@[simp]
lemma neg_val {d} (A : ElectromagneticPotential d) :
    (- A).val = - A.val := rfl@[simp]
lemma neg_apply {d} (A : ElectromagneticPotential d) (x : SpaceTime d) :
    (- A) x = - A x := rflinstance {d} : Sub (ElectromagneticPotential d) where
  sub A B := ⟨fun x => A x - B x⟩@[simp]
lemma sub_val {d} (A B : ElectromagneticPotential d) :
    (A - B).val = A.val - B.val := rfl@[simp]
lemma sub_apply {d} (A B : ElectromagneticPotential d) (x : SpaceTime d) :
    (A - B) x = A x - B x := rflinstance {d} : AddCommGroup (ElectromagneticPotential d) where
  add_assoc A B C := byd:ℕA:ElectromagneticPotential dB:ElectromagneticPotential dC:ElectromagneticPotential d⊢ A + B + C = A + (B + C)
    ext x μd:ℕA:ElectromagneticPotential dB:ElectromagneticPotential dC:ElectromagneticPotential dx:SpaceTime dμ:Fin 1 ⊕ Fin d⊢ (A + B + C).val x μ = (A + (B + C)).val x μ
    simp [add_assoc]All goals completed! 🐙
  zero_add A := byd:ℕA:ElectromagneticPotential d⊢ 0 + A = A
    ext x μd:ℕA:ElectromagneticPotential dx:SpaceTime dμ:Fin 1 ⊕ Fin d⊢ (0 + A).val x μ = A.val x μ
    simpAll goals completed! 🐙
  add_zero A := byd:ℕA:ElectromagneticPotential d⊢ A + 0 = A
    ext x μd:ℕA:ElectromagneticPotential dx:SpaceTime dμ:Fin 1 ⊕ Fin d⊢ (A + 0).val x μ = A.val x μ
    simpAll goals completed! 🐙
  neg_add_cancel A := byd:ℕA:ElectromagneticPotential d⊢ -A + A = 0
    ext x μd:ℕA:ElectromagneticPotential dx:SpaceTime dμ:Fin 1 ⊕ Fin d⊢ (-A + A).val x μ = val 0 x μ
    simpAll goals completed! 🐙
  add_comm A B := byd:ℕA:ElectromagneticPotential dB:ElectromagneticPotential d⊢ A + B = B + A
    ext x μd:ℕA:ElectromagneticPotential dB:ElectromagneticPotential dx:SpaceTime dμ:Fin 1 ⊕ Fin d⊢ (A + B).val x μ = (B + A).val x μ
    simp [add_comm]All goals completed! 🐙
  nsmul := nsmulRec
  zsmul := zsmulRec@[simp]
lemma smul_val {d} (r : ℝ) (A : ElectromagneticPotential d) :
    (r • A).val = r • A.val := rfl@[simp]
lemma smul_apply {d} (r : ℝ) (A : ElectromagneticPotential d) (x : SpaceTime d) :
    (r • A) x = r • A x := byd:ℕr:ℝA:ElectromagneticPotential dx:SpaceTime d⊢ (r • A).val x = r • A.val x simpAll goals completed! 🐙

A.2. Basic constructors of the electromagnetic potential

              lemma ofPotentials_eq_add {d} (c : SpeedOfLight) (ϕ : Time → Space d → ℝ)
    (A : Time → Space d → EuclideanSpace ℝ (Fin d)) :
    ofPotentials c ϕ A = ofScalarPotential c ϕ + ofVectorPotential c A := byd:ℕc:SpeedOfLightϕ:Time → Space d → ℝA:Time → Space d → EuclideanSpace ℝ (Fin d)⊢ ofPotentials c ϕ A = ofScalarPotential c ϕ + ofVectorPotential c A
  ext1d:ℕc:SpeedOfLightϕ:Time → Space d → ℝA:Time → Space d → EuclideanSpace ℝ (Fin d)⊢ (ofPotentials c ϕ A).val = (ofScalarPotential c ϕ + ofVectorPotential c A).val
  ext1 xd:ℕc:SpeedOfLightϕ:Time → Space d → ℝA:Time → Space d → EuclideanSpace ℝ (Fin d)x:SpaceTime d⊢ (ofPotentials c ϕ A).val x = (ofScalarPotential c ϕ + ofVectorPotential c A).val x
  refine Lorentz.Vector.ext_of_apply (fun i => ?_)d:ℕc:SpeedOfLightϕ:Time → Space d → ℝA:Time → Space d → EuclideanSpace ℝ (Fin d)x:SpaceTime di:Fin 1 ⊕ Fin d⊢ (ofPotentials c ϕ A).val x i = (ofScalarPotential c ϕ + ofVectorPotential c A).val x i
  match i with
  | Sum.inl 0 | Sum.inr _ =>d:ℕc:SpeedOfLightϕ:Time → Space d → ℝA:Time → Space d → EuclideanSpace ℝ (Fin d)x:SpaceTime di:Fin 1 ⊕ Fin dval✝:Fin d⊢ (ofPotentials c ϕ A).val x (Sum.inr val✝) = (ofScalarPotential c ϕ + ofVectorPotential c A).val x (Sum.inr val✝)d:ℕc:SpeedOfLightϕ:Time → Space d → ℝA:Time → Space d → EuclideanSpace ℝ (Fin d)x:SpaceTime di:Fin 1 ⊕ Fin d⊢ (ofPotentials c ϕ A).val x (Sum.inl 0) = (ofScalarPotential c ϕ + ofVectorPotential c A).val x (Sum.inl 0) simp [ofPotentials, ofScalarPotential, ofVectorPotential]All goals completed! 🐙lemma ofStaticPotentials_eq_ofPotentials {d} (c : SpeedOfLight) (ϕ : Space d → ℝ)
    (A : Space d → EuclideanSpace ℝ (Fin d)) :
    ofStaticPotentials c ϕ A = ofPotentials c (fun _ => ϕ) (fun _ => A) := byd:ℕc:SpeedOfLightϕ:Space d → ℝA:Space d → EuclideanSpace ℝ (Fin d)⊢ ofStaticPotentials c ϕ A = ofPotentials c (fun x => ϕ) fun x => A
  simp [ofStaticPotentials, ofStaticScalarPotential, ofStaticVectorPotential, ofPotentials_eq_add]All goals completed! 🐙TODO "Write lemmas for the various properties (e.g. the electric field) of
  the electromagnetic potential from the various constructors."

A.3. The group action on the ElectromagneticPotential

lemma action_val {d} (Λ : LorentzGroup d) (A : ElectromagneticPotential d) :
    (Λ • A).val = fun x => Λ • A (Λ⁻¹ • x) := rfl

@[simp]
lemma action_apply {d} (Λ : LorentzGroup d) (A : ElectromagneticPotential d)
    (x : SpaceTime d) :
    (Λ • A) x = Λ • A (Λ⁻¹ • x) := rfl

A.4. Differentiability

We show that the components of field strength tensor are differentiable if the potential is.

              @[fun_prop]
lemma differentiable_component {d : ℕ}
    (A : ElectromagneticPotential d) (hA : Differentiable ℝ A) (μ : Fin 1 ⊕ Fin d) :
    Differentiable ℝ (fun x => A x μ) := byd:ℕA:ElectromagneticPotential dhA:Differentiable ℝ A.valμ:Fin 1 ⊕ Fin d⊢ Differentiable ℝ fun x => A.val x μ
  exact (SpaceTime.differentiable_vector _).mpr hA μAll goals completed! 🐙@[fun_prop]
lemma differentiable_action {d} (Λ : LorentzGroup d) (A : ElectromagneticPotential d)
    (hA : Differentiable ℝ A) : Differentiable ℝ (fun x => Λ • A (Λ⁻¹ • x)) := byd:ℕΛ:↑(LorentzGroup d)A:ElectromagneticPotential dhA:Differentiable ℝ A.val⊢ Differentiable ℝ fun x => Λ • A.val (Λ⁻¹ • x)
  exact (ContinuousLinearMap.differentiable (Lorentz.Vector.actionCLM Λ)).comp
    (hA.comp (ContinuousLinearMap.differentiable (Lorentz.Vector.actionCLM Λ⁻¹)))All goals completed! 🐙@[fun_prop]
lemma contDiff_action {d} (Λ : LorentzGroup d) (A : ElectromagneticPotential d)
    (hA : ContDiff ℝ n A) : ContDiff ℝ n (fun x => Λ • A (Λ⁻¹ • x)) := byn:ℕ∞ωd:ℕΛ:↑(LorentzGroup d)A:ElectromagneticPotential dhA:ContDiff ℝ n A.val⊢ ContDiff ℝ n fun x => Λ • A.val (Λ⁻¹ • x)
  exact (ContinuousLinearMap.contDiff (Lorentz.Vector.actionCLM Λ)).comp
    (hA.comp (ContinuousLinearMap.contDiff (Lorentz.Vector.actionCLM Λ⁻¹)))All goals completed! 🐙

@[fun_prop]
lemma differentiable_deriv {d} {A : ElectromagneticPotential d}
    (hA : ContDiff ℝ 2 A) (μ ν : Fin 1 ⊕ Fin d) :
    Differentiable ℝ (fun x => ∂_ μ A x ν) := byd:ℕA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d⊢ Differentiable ℝ fun x => ∂_ μ A.val x ν
  have h : ∀ ν, Differentiable ℝ fun x => (fderiv ℝ A x) (Lorentz.Vector.basis μ) ν := by
    rw [SpaceTime.differentiable_vectord:ℕA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d⊢ Differentiable ℝ fun x => (fderiv ℝ A.val x) (Lorentz.Vector.basis μ)d:ℕA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d⊢ Differentiable ℝ fun x => (fderiv ℝ A.val x) (Lorentz.Vector.basis μ)d:ℕA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin dh:∀ (ν : Fin 1 ⊕ Fin d), Differentiable ℝ fun x => (fderiv ℝ A.val x) (Lorentz.Vector.basis μ) ν⊢ Differentiable ℝ fun x => ∂_ μ A.val x ν]d:ℕA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d⊢ Differentiable ℝ fun x => (fderiv ℝ A.val x) (Lorentz.Vector.basis μ)d:ℕA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin dh:∀ (ν : Fin 1 ⊕ Fin d), Differentiable ℝ fun x => (fderiv ℝ A.val x) (Lorentz.Vector.basis μ) ν⊢ Differentiable ℝ fun x => ∂_ μ A.val x ν
    fun_propd:ℕA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin dh:∀ (ν : Fin 1 ⊕ Fin d), Differentiable ℝ fun x => (fderiv ℝ A.val x) (Lorentz.Vector.basis μ) ν⊢ Differentiable ℝ fun x => ∂_ μ A.val x νd:ℕA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin dh:∀ (ν : Fin 1 ⊕ Fin d), Differentiable ℝ fun x => (fderiv ℝ A.val x) (Lorentz.Vector.basis μ) ν⊢ Differentiable ℝ fun x => ∂_ μ A.val x ν
  exact h νAll goals completed! 🐙@[fun_prop]
lemma differentiable_deriv_of_smooth {d} {A : ElectromagneticPotential d}
    (hA : ContDiff ℝ ∞ A) (μ ν : Fin 1 ⊕ Fin d) :
    Differentiable ℝ (fun x => ∂_ μ A x ν) := byd:ℕA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d⊢ Differentiable ℝ fun x => ∂_ μ A.val x ν
  apply differentiable_deriv (hA.of_le (ENat.LEInfty.out)) μ νAll goals completed! 🐙

@[fun_prop]
lemma contDiff_deriv {n} {d} {A : ElectromagneticPotential d}
    (hA : ContDiff ℝ (n + 1) A) (μ ν : Fin 1 ⊕ Fin d) :
    ContDiff ℝ n (fun x => ∂_ μ A x ν) := byn:ℕ∞ωd:ℕA:ElectromagneticPotential dhA:ContDiff ℝ (n + 1) A.valμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d⊢ ContDiff ℝ n fun x => ∂_ μ A.val x ν
  have h : ∀ ν, ContDiff ℝ n fun x => (fderiv ℝ A x) (Lorentz.Vector.basis μ) ν := by
    rw [SpaceTime.contDiff_vectorn:ℕ∞ωd:ℕA:ElectromagneticPotential dhA:ContDiff ℝ (n + 1) A.valμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d⊢ ContDiff ℝ n fun x => (fderiv ℝ A.val x) (Lorentz.Vector.basis μ)n:ℕ∞ωd:ℕA:ElectromagneticPotential dhA:ContDiff ℝ (n + 1) A.valμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d⊢ ContDiff ℝ n fun x => (fderiv ℝ A.val x) (Lorentz.Vector.basis μ)n:ℕ∞ωd:ℕA:ElectromagneticPotential dhA:ContDiff ℝ (n + 1) A.valμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin dh:∀ (ν : Fin 1 ⊕ Fin d), ContDiff ℝ n fun x => (fderiv ℝ A.val x) (Lorentz.Vector.basis μ) ν⊢ ContDiff ℝ n fun x => ∂_ μ A.val x ν]n:ℕ∞ωd:ℕA:ElectromagneticPotential dhA:ContDiff ℝ (n + 1) A.valμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d⊢ ContDiff ℝ n fun x => (fderiv ℝ A.val x) (Lorentz.Vector.basis μ)n:ℕ∞ωd:ℕA:ElectromagneticPotential dhA:ContDiff ℝ (n + 1) A.valμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin dh:∀ (ν : Fin 1 ⊕ Fin d), ContDiff ℝ n fun x => (fderiv ℝ A.val x) (Lorentz.Vector.basis μ) ν⊢ ContDiff ℝ n fun x => ∂_ μ A.val x ν
    fun_propn:ℕ∞ωd:ℕA:ElectromagneticPotential dhA:ContDiff ℝ (n + 1) A.valμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin dh:∀ (ν : Fin 1 ⊕ Fin d), ContDiff ℝ n fun x => (fderiv ℝ A.val x) (Lorentz.Vector.basis μ) ν⊢ ContDiff ℝ n fun x => ∂_ μ A.val x νn:ℕ∞ωd:ℕA:ElectromagneticPotential dhA:ContDiff ℝ (n + 1) A.valμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin dh:∀ (ν : Fin 1 ⊕ Fin d), ContDiff ℝ n fun x => (fderiv ℝ A.val x) (Lorentz.Vector.basis μ) ν⊢ ContDiff ℝ n fun x => ∂_ μ A.val x ν
  exact h νAll goals completed! 🐙TODO "Add results related to the differentiability of the
  derivative of the Electromagnetic potential."

A.5. Differentiablity in terms of constructors

              

lemma differentiable_ofScalarPotential {d} (c : SpeedOfLight) (φ : Time → Space d → ℝ)
    (hϕ : Differentiable ℝ ↿φ) : Differentiable ℝ (ofScalarPotential c φ) := byd:ℕc:SpeedOfLightφ:Time → Space d → ℝhϕ:Differentiable ℝ ↿φ⊢ Differentiable ℝ (ofScalarPotential c φ).val
  simp [ofScalarPotential]d:ℕc:SpeedOfLightφ:Time → Space d → ℝhϕ:Differentiable ℝ ↿φ⊢ Differentiable ℝ fun x μ =>
  match μ with
  | Sum.inl 0 => (timeSlice c).symm φ x / c.val
  | Sum.inr val => 0
  rw [← SpaceTime.differentiable_vectord:ℕc:SpeedOfLightφ:Time → Space d → ℝhϕ:Differentiable ℝ ↿φ⊢ ∀ (ν : Fin 1 ⊕ Fin d),
  Differentiable ℝ fun x =>
    match ν with
    | Sum.inl 0 => (timeSlice c).symm φ x / c.val
    | Sum.inr val => 0d:ℕc:SpeedOfLightφ:Time → Space d → ℝhϕ:Differentiable ℝ ↿φ⊢ ∀ (ν : Fin 1 ⊕ Fin d),
  Differentiable ℝ fun x =>
    match ν with
    | Sum.inl 0 => (timeSlice c).symm φ x / c.val
    | Sum.inr val => 0]d:ℕc:SpeedOfLightφ:Time → Space d → ℝhϕ:Differentiable ℝ ↿φ⊢ ∀ (ν : Fin 1 ⊕ Fin d),
  Differentiable ℝ fun x =>
    match ν with
    | Sum.inl 0 => (timeSlice c).symm φ x / c.val
    | Sum.inr val => 0
  intro μd:ℕc:SpeedOfLightφ:Time → Space d → ℝhϕ:Differentiable ℝ ↿φμ:Fin 1 ⊕ Fin d⊢ Differentiable ℝ fun x =>
  match μ with
  | Sum.inl 0 => (timeSlice c).symm φ x / c.val
  | Sum.inr val => 0
  match μ with
  | Sum.inl 0 | Sum.inr _ =>d:ℕc:SpeedOfLightφ:Time → Space d → ℝhϕ:Differentiable ℝ ↿φμ:Fin 1 ⊕ Fin dval✝:Fin d⊢ Differentiable ℝ fun x =>
  match Sum.inr val✝ with
  | Sum.inl 0 => (timeSlice c).symm φ x / c.val
  | Sum.inr val => 0d:ℕc:SpeedOfLightφ:Time → Space d → ℝhϕ:Differentiable ℝ ↿φμ:Fin 1 ⊕ Fin d⊢ Differentiable ℝ fun x =>
  match Sum.inl 0 with
  | Sum.inl 0 => (timeSlice c).symm φ x / c.val
  | Sum.inr val => 0 fun_propAll goals completed! 🐙

lemma contDiff_ofScalarPotential {n} {d} (c : SpeedOfLight) (φ : Time → Space d → ℝ)
    (hϕ : ContDiff ℝ n ↿φ) : ContDiff ℝ n (ofScalarPotential c φ) := byn:ℕ∞ωd:ℕc:SpeedOfLightφ:Time → Space d → ℝhϕ:ContDiff ℝ n ↿φ⊢ ContDiff ℝ n (ofScalarPotential c φ).val
  simp [ofScalarPotential]n:ℕ∞ωd:ℕc:SpeedOfLightφ:Time → Space d → ℝhϕ:ContDiff ℝ n ↿φ⊢ ContDiff ℝ n fun x μ =>
  match μ with
  | Sum.inl 0 => (timeSlice c).symm φ x / c.val
  | Sum.inr val => 0
  rw [← SpaceTime.contDiff_vectorn:ℕ∞ωd:ℕc:SpeedOfLightφ:Time → Space d → ℝhϕ:ContDiff ℝ n ↿φ⊢ ∀ (ν : Fin 1 ⊕ Fin d),
  ContDiff ℝ n fun x =>
    match ν with
    | Sum.inl 0 => (timeSlice c).symm φ x / c.val
    | Sum.inr val => 0n:ℕ∞ωd:ℕc:SpeedOfLightφ:Time → Space d → ℝhϕ:ContDiff ℝ n ↿φ⊢ ∀ (ν : Fin 1 ⊕ Fin d),
  ContDiff ℝ n fun x =>
    match ν with
    | Sum.inl 0 => (timeSlice c).symm φ x / c.val
    | Sum.inr val => 0]n:ℕ∞ωd:ℕc:SpeedOfLightφ:Time → Space d → ℝhϕ:ContDiff ℝ n ↿φ⊢ ∀ (ν : Fin 1 ⊕ Fin d),
  ContDiff ℝ n fun x =>
    match ν with
    | Sum.inl 0 => (timeSlice c).symm φ x / c.val
    | Sum.inr val => 0
  intro μn:ℕ∞ωd:ℕc:SpeedOfLightφ:Time → Space d → ℝhϕ:ContDiff ℝ n ↿φμ:Fin 1 ⊕ Fin d⊢ ContDiff ℝ n fun x =>
  match μ with
  | Sum.inl 0 => (timeSlice c).symm φ x / c.val
  | Sum.inr val => 0
  match μ with
  | Sum.inl 0 | Sum.inr _ =>n:ℕ∞ωd:ℕc:SpeedOfLightφ:Time → Space d → ℝhϕ:ContDiff ℝ n ↿φμ:Fin 1 ⊕ Fin dval✝:Fin d⊢ ContDiff ℝ n fun x =>
  match Sum.inr val✝ with
  | Sum.inl 0 => (timeSlice c).symm φ x / c.val
  | Sum.inr val => 0n:ℕ∞ωd:ℕc:SpeedOfLightφ:Time → Space d → ℝhϕ:ContDiff ℝ n ↿φμ:Fin 1 ⊕ Fin d⊢ ContDiff ℝ n fun x =>
  match Sum.inl 0 with
  | Sum.inl 0 => (timeSlice c).symm φ x / c.val
  | Sum.inr val => 0 fun_propAll goals completed! 🐙

lemma differentiable_ofVectorPotential {d} (c : SpeedOfLight)
    (A : Time → Space d → EuclideanSpace ℝ (Fin d))
    (hA : Differentiable ℝ ↿A) : Differentiable ℝ (ofVectorPotential c A) := byd:ℕc:SpeedOfLightA:Time → Space d → EuclideanSpace ℝ (Fin d)hA:Differentiable ℝ ↿A⊢ Differentiable ℝ (ofVectorPotential c A).val
  simp [ofVectorPotential]d:ℕc:SpeedOfLightA:Time → Space d → EuclideanSpace ℝ (Fin d)hA:Differentiable ℝ ↿A⊢ Differentiable ℝ fun x μ =>
  match μ with
  | Sum.inl 0 => 0
  | Sum.inr i => ((timeSlice c).symm A x).ofLp i
  rw [← SpaceTime.differentiable_vectord:ℕc:SpeedOfLightA:Time → Space d → EuclideanSpace ℝ (Fin d)hA:Differentiable ℝ ↿A⊢ ∀ (ν : Fin 1 ⊕ Fin d),
  Differentiable ℝ fun x =>
    match ν with
    | Sum.inl 0 => 0
    | Sum.inr i => ((timeSlice c).symm A x).ofLp id:ℕc:SpeedOfLightA:Time → Space d → EuclideanSpace ℝ (Fin d)hA:Differentiable ℝ ↿A⊢ ∀ (ν : Fin 1 ⊕ Fin d),
  Differentiable ℝ fun x =>
    match ν with
    | Sum.inl 0 => 0
    | Sum.inr i => ((timeSlice c).symm A x).ofLp i]d:ℕc:SpeedOfLightA:Time → Space d → EuclideanSpace ℝ (Fin d)hA:Differentiable ℝ ↿A⊢ ∀ (ν : Fin 1 ⊕ Fin d),
  Differentiable ℝ fun x =>
    match ν with
    | Sum.inl 0 => 0
    | Sum.inr i => ((timeSlice c).symm A x).ofLp i
  intro μd:ℕc:SpeedOfLightA:Time → Space d → EuclideanSpace ℝ (Fin d)hA:Differentiable ℝ ↿Aμ:Fin 1 ⊕ Fin d⊢ Differentiable ℝ fun x =>
  match μ with
  | Sum.inl 0 => 0
  | Sum.inr i => ((timeSlice c).symm A x).ofLp i
  match μ with
  | Sum.inl 0 | Sum.inr _ =>d:ℕc:SpeedOfLightA:Time → Space d → EuclideanSpace ℝ (Fin d)hA:Differentiable ℝ ↿Aμ:Fin 1 ⊕ Fin dval✝:Fin d⊢ Differentiable ℝ fun x =>
  match Sum.inr val✝ with
  | Sum.inl 0 => 0
  | Sum.inr i => ((timeSlice c).symm A x).ofLp id:ℕc:SpeedOfLightA:Time → Space d → EuclideanSpace ℝ (Fin d)hA:Differentiable ℝ ↿Aμ:Fin 1 ⊕ Fin d⊢ Differentiable ℝ fun x =>
  match Sum.inl 0 with
  | Sum.inl 0 => 0
  | Sum.inr i => ((timeSlice c).symm A x).ofLp i fun_propAll goals completed! 🐙

lemma contDiff_ofVectorPotential {n} {d} (c : SpeedOfLight)
    (A : Time → Space d → EuclideanSpace ℝ (Fin d))
    (hA : ContDiff ℝ n ↿A) : ContDiff ℝ n (ofVectorPotential c A) := byn:ℕ∞ωd:ℕc:SpeedOfLightA:Time → Space d → EuclideanSpace ℝ (Fin d)hA:ContDiff ℝ n ↿A⊢ ContDiff ℝ n (ofVectorPotential c A).val
  simp [ofVectorPotential]n:ℕ∞ωd:ℕc:SpeedOfLightA:Time → Space d → EuclideanSpace ℝ (Fin d)hA:ContDiff ℝ n ↿A⊢ ContDiff ℝ n fun x μ =>
  match μ with
  | Sum.inl 0 => 0
  | Sum.inr i => ((timeSlice c).symm A x).ofLp i
  rw [← SpaceTime.contDiff_vectorn:ℕ∞ωd:ℕc:SpeedOfLightA:Time → Space d → EuclideanSpace ℝ (Fin d)hA:ContDiff ℝ n ↿A⊢ ∀ (ν : Fin 1 ⊕ Fin d),
  ContDiff ℝ n fun x =>
    match ν with
    | Sum.inl 0 => 0
    | Sum.inr i => ((timeSlice c).symm A x).ofLp in:ℕ∞ωd:ℕc:SpeedOfLightA:Time → Space d → EuclideanSpace ℝ (Fin d)hA:ContDiff ℝ n ↿A⊢ ∀ (ν : Fin 1 ⊕ Fin d),
  ContDiff ℝ n fun x =>
    match ν with
    | Sum.inl 0 => 0
    | Sum.inr i => ((timeSlice c).symm A x).ofLp i]n:ℕ∞ωd:ℕc:SpeedOfLightA:Time → Space d → EuclideanSpace ℝ (Fin d)hA:ContDiff ℝ n ↿A⊢ ∀ (ν : Fin 1 ⊕ Fin d),
  ContDiff ℝ n fun x =>
    match ν with
    | Sum.inl 0 => 0
    | Sum.inr i => ((timeSlice c).symm A x).ofLp i
  intro μn:ℕ∞ωd:ℕc:SpeedOfLightA:Time → Space d → EuclideanSpace ℝ (Fin d)hA:ContDiff ℝ n ↿Aμ:Fin 1 ⊕ Fin d⊢ ContDiff ℝ n fun x =>
  match μ with
  | Sum.inl 0 => 0
  | Sum.inr i => ((timeSlice c).symm A x).ofLp i
  match μ with
  | Sum.inl 0 | Sum.inr _ =>n:ℕ∞ωd:ℕc:SpeedOfLightA:Time → Space d → EuclideanSpace ℝ (Fin d)hA:ContDiff ℝ n ↿Aμ:Fin 1 ⊕ Fin dval✝:Fin d⊢ ContDiff ℝ n fun x =>
  match Sum.inr val✝ with
  | Sum.inl 0 => 0
  | Sum.inr i => ((timeSlice c).symm A x).ofLp in:ℕ∞ωd:ℕc:SpeedOfLightA:Time → Space d → EuclideanSpace ℝ (Fin d)hA:ContDiff ℝ n ↿Aμ:Fin 1 ⊕ Fin d⊢ ContDiff ℝ n fun x =>
  match Sum.inl 0 with
  | Sum.inl 0 => 0
  | Sum.inr i => ((timeSlice c).symm A x).ofLp i fun_propAll goals completed! 🐙

lemma differentiable_ofPotentials {d} (c : SpeedOfLight) (φ : Time → Space d → ℝ)
    (A : Time → Space d → EuclideanSpace ℝ (Fin d)) (hϕ : Differentiable ℝ ↿φ)
    (hA : Differentiable ℝ ↿A) : Differentiable ℝ (ofPotentials c φ A) := byd:ℕc:SpeedOfLightφ:Time → Space d → ℝA:Time → Space d → EuclideanSpace ℝ (Fin d)hϕ:Differentiable ℝ ↿φhA:Differentiable ℝ ↿A⊢ Differentiable ℝ (ofPotentials c φ A).val
  simp [ofPotentials]d:ℕc:SpeedOfLightφ:Time → Space d → ℝA:Time → Space d → EuclideanSpace ℝ (Fin d)hϕ:Differentiable ℝ ↿φhA:Differentiable ℝ ↿A⊢ Differentiable ℝ fun x μ =>
  match μ with
  | Sum.inl 0 => (timeSlice c).symm φ x / c.val
  | Sum.inr i => ((timeSlice c).symm A x).ofLp i
  rw [← SpaceTime.differentiable_vectord:ℕc:SpeedOfLightφ:Time → Space d → ℝA:Time → Space d → EuclideanSpace ℝ (Fin d)hϕ:Differentiable ℝ ↿φhA:Differentiable ℝ ↿A⊢ ∀ (ν : Fin 1 ⊕ Fin d),
  Differentiable ℝ fun x =>
    match ν with
    | Sum.inl 0 => (timeSlice c).symm φ x / c.val
    | Sum.inr i => ((timeSlice c).symm A x).ofLp id:ℕc:SpeedOfLightφ:Time → Space d → ℝA:Time → Space d → EuclideanSpace ℝ (Fin d)hϕ:Differentiable ℝ ↿φhA:Differentiable ℝ ↿A⊢ ∀ (ν : Fin 1 ⊕ Fin d),
  Differentiable ℝ fun x =>
    match ν with
    | Sum.inl 0 => (timeSlice c).symm φ x / c.val
    | Sum.inr i => ((timeSlice c).symm A x).ofLp i]d:ℕc:SpeedOfLightφ:Time → Space d → ℝA:Time → Space d → EuclideanSpace ℝ (Fin d)hϕ:Differentiable ℝ ↿φhA:Differentiable ℝ ↿A⊢ ∀ (ν : Fin 1 ⊕ Fin d),
  Differentiable ℝ fun x =>
    match ν with
    | Sum.inl 0 => (timeSlice c).symm φ x / c.val
    | Sum.inr i => ((timeSlice c).symm A x).ofLp i
  intro μd:ℕc:SpeedOfLightφ:Time → Space d → ℝA:Time → Space d → EuclideanSpace ℝ (Fin d)hϕ:Differentiable ℝ ↿φhA:Differentiable ℝ ↿Aμ:Fin 1 ⊕ Fin d⊢ Differentiable ℝ fun x =>
  match μ with
  | Sum.inl 0 => (timeSlice c).symm φ x / c.val
  | Sum.inr i => ((timeSlice c).symm A x).ofLp i
  match μ with
  | Sum.inl 0 | Sum.inr _ =>d:ℕc:SpeedOfLightφ:Time → Space d → ℝA:Time → Space d → EuclideanSpace ℝ (Fin d)hϕ:Differentiable ℝ ↿φhA:Differentiable ℝ ↿Aμ:Fin 1 ⊕ Fin dval✝:Fin d⊢ Differentiable ℝ fun x =>
  match Sum.inr val✝ with
  | Sum.inl 0 => (timeSlice c).symm φ x / c.val
  | Sum.inr i => ((timeSlice c).symm A x).ofLp id:ℕc:SpeedOfLightφ:Time → Space d → ℝA:Time → Space d → EuclideanSpace ℝ (Fin d)hϕ:Differentiable ℝ ↿φhA:Differentiable ℝ ↿Aμ:Fin 1 ⊕ Fin d⊢ Differentiable ℝ fun x =>
  match Sum.inl 0 with
  | Sum.inl 0 => (timeSlice c).symm φ x / c.val
  | Sum.inr i => ((timeSlice c).symm A x).ofLp i fun_propAll goals completed! 🐙

lemma contDiff_ofPotentials {n} {d} (c : SpeedOfLight) (φ : Time → Space d → ℝ)
    (A : Time → Space d → EuclideanSpace ℝ (Fin d)) (hϕ : ContDiff ℝ n ↿φ)
    (hA : ContDiff ℝ n ↿A) : ContDiff ℝ n (ofPotentials c φ A) := byn:ℕ∞ωd:ℕc:SpeedOfLightφ:Time → Space d → ℝA:Time → Space d → EuclideanSpace ℝ (Fin d)hϕ:ContDiff ℝ n ↿φhA:ContDiff ℝ n ↿A⊢ ContDiff ℝ n (ofPotentials c φ A).val
  simp [ofPotentials]n:ℕ∞ωd:ℕc:SpeedOfLightφ:Time → Space d → ℝA:Time → Space d → EuclideanSpace ℝ (Fin d)hϕ:ContDiff ℝ n ↿φhA:ContDiff ℝ n ↿A⊢ ContDiff ℝ n fun x μ =>
  match μ with
  | Sum.inl 0 => (timeSlice c).symm φ x / c.val
  | Sum.inr i => ((timeSlice c).symm A x).ofLp i
  rw [← SpaceTime.contDiff_vectorn:ℕ∞ωd:ℕc:SpeedOfLightφ:Time → Space d → ℝA:Time → Space d → EuclideanSpace ℝ (Fin d)hϕ:ContDiff ℝ n ↿φhA:ContDiff ℝ n ↿A⊢ ∀ (ν : Fin 1 ⊕ Fin d),
  ContDiff ℝ n fun x =>
    match ν with
    | Sum.inl 0 => (timeSlice c).symm φ x / c.val
    | Sum.inr i => ((timeSlice c).symm A x).ofLp in:ℕ∞ωd:ℕc:SpeedOfLightφ:Time → Space d → ℝA:Time → Space d → EuclideanSpace ℝ (Fin d)hϕ:ContDiff ℝ n ↿φhA:ContDiff ℝ n ↿A⊢ ∀ (ν : Fin 1 ⊕ Fin d),
  ContDiff ℝ n fun x =>
    match ν with
    | Sum.inl 0 => (timeSlice c).symm φ x / c.val
    | Sum.inr i => ((timeSlice c).symm A x).ofLp i]n:ℕ∞ωd:ℕc:SpeedOfLightφ:Time → Space d → ℝA:Time → Space d → EuclideanSpace ℝ (Fin d)hϕ:ContDiff ℝ n ↿φhA:ContDiff ℝ n ↿A⊢ ∀ (ν : Fin 1 ⊕ Fin d),
  ContDiff ℝ n fun x =>
    match ν with
    | Sum.inl 0 => (timeSlice c).symm φ x / c.val
    | Sum.inr i => ((timeSlice c).symm A x).ofLp i
  intro μn:ℕ∞ωd:ℕc:SpeedOfLightφ:Time → Space d → ℝA:Time → Space d → EuclideanSpace ℝ (Fin d)hϕ:ContDiff ℝ n ↿φhA:ContDiff ℝ n ↿Aμ:Fin 1 ⊕ Fin d⊢ ContDiff ℝ n fun x =>
  match μ with
  | Sum.inl 0 => (timeSlice c).symm φ x / c.val
  | Sum.inr i => ((timeSlice c).symm A x).ofLp i
  match μ with
  | Sum.inl 0 | Sum.inr _ =>n:ℕ∞ωd:ℕc:SpeedOfLightφ:Time → Space d → ℝA:Time → Space d → EuclideanSpace ℝ (Fin d)hϕ:ContDiff ℝ n ↿φhA:ContDiff ℝ n ↿Aμ:Fin 1 ⊕ Fin dval✝:Fin d⊢ ContDiff ℝ n fun x =>
  match Sum.inr val✝ with
  | Sum.inl 0 => (timeSlice c).symm φ x / c.val
  | Sum.inr i => ((timeSlice c).symm A x).ofLp in:ℕ∞ωd:ℕc:SpeedOfLightφ:Time → Space d → ℝA:Time → Space d → EuclideanSpace ℝ (Fin d)hϕ:ContDiff ℝ n ↿φhA:ContDiff ℝ n ↿Aμ:Fin 1 ⊕ Fin d⊢ ContDiff ℝ n fun x =>
  match Sum.inl 0 with
  | Sum.inl 0 => (timeSlice c).symm φ x / c.val
  | Sum.inr i => ((timeSlice c).symm A x).ofLp i fun_propAll goals completed! 🐙

A.5. The action on the space-time derivatives

Given a ElectromagneticPotential A^μ, we can consider its derivative ∂_μ A^ν. Under a Lorentz transformation Λ, this transforms as ∂_ μ (Λ • A), we write an expression for this in terms of the tensor. ∂_ ρ A (Λ⁻¹ • x) κ.



lemma spaceTime_deriv_action_eq_sum {d} {μ ν : Fin 1 ⊕ Fin d} {x : SpaceTime d}
    (Λ : LorentzGroup d) (A : ElectromagneticPotential d) (hA : Differentiable ℝ A) :
    ∂_ μ (Λ • A) x ν = ∑ κ, ∑ ρ, (Λ.1 ν κ * Λ⁻¹.1 ρ μ) * ∂_ ρ A (Λ⁻¹ • x) κ := byd:ℕμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin dx:SpaceTime dΛ:↑(LorentzGroup d)A:ElectromagneticPotential dhA:Differentiable ℝ A.val⊢ ∂_ μ (Λ • A).val x ν = ∑ κ, ∑ ρ, ↑Λ ν κ * ↑Λ⁻¹ ρ μ * ∂_ ρ A.val (Λ⁻¹ • x) κ
  rw [action_val,d:ℕμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin dx:SpaceTime dΛ:↑(LorentzGroup d)A:ElectromagneticPotential dhA:Differentiable ℝ A.val⊢ ∂_ μ (fun x => Λ • A.val (Λ⁻¹ • x)) x ν = ∑ κ, ∑ ρ, ↑Λ ν κ * ↑Λ⁻¹ ρ μ * ∂_ ρ A.val (Λ⁻¹ • x) κd:ℕμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin dx:SpaceTime dΛ:↑(LorentzGroup d)A:ElectromagneticPotential dhA:Differentiable ℝ A.val⊢ ∑ j, (↑Λ⁻¹ j μ • Λ • ∂_ j A.val (Λ⁻¹ • x)) ν = ∑ y, ∑ x_1, ↑Λ ν x_1 * ↑Λ⁻¹ y μ * ∂_ y A.val (Λ⁻¹ • x) x_1 SpaceTime.deriv_equivariant A.val Λ x hA μ,d:ℕμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin dx:SpaceTime dΛ:↑(LorentzGroup d)A:ElectromagneticPotential dhA:Differentiable ℝ A.val⊢ (∑ ν, ↑Λ⁻¹ ν μ • Λ • ∂_ ν A.val (Λ⁻¹ • x)) ν = ∑ κ, ∑ ρ, ↑Λ ν κ * ↑Λ⁻¹ ρ μ * ∂_ ρ A.val (Λ⁻¹ • x) κd:ℕμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin dx:SpaceTime dΛ:↑(LorentzGroup d)A:ElectromagneticPotential dhA:Differentiable ℝ A.val⊢ ∑ j, (↑Λ⁻¹ j μ • Λ • ∂_ j A.val (Λ⁻¹ • x)) ν = ∑ y, ∑ x_1, ↑Λ ν x_1 * ↑Λ⁻¹ y μ * ∂_ y A.val (Λ⁻¹ • x) x_1 Lorentz.Vector.apply_sum,d:ℕμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin dx:SpaceTime dΛ:↑(LorentzGroup d)A:ElectromagneticPotential dhA:Differentiable ℝ A.val⊢ ∑ j, (↑Λ⁻¹ j μ • Λ • ∂_ j A.val (Λ⁻¹ • x)) ν = ∑ κ, ∑ ρ, ↑Λ ν κ * ↑Λ⁻¹ ρ μ * ∂_ ρ A.val (Λ⁻¹ • x) κd:ℕμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin dx:SpaceTime dΛ:↑(LorentzGroup d)A:ElectromagneticPotential dhA:Differentiable ℝ A.val⊢ ∑ j, (↑Λ⁻¹ j μ • Λ • ∂_ j A.val (Λ⁻¹ • x)) ν = ∑ y, ∑ x_1, ↑Λ ν x_1 * ↑Λ⁻¹ y μ * ∂_ y A.val (Λ⁻¹ • x) x_1
    Finset.sum_commd:ℕμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin dx:SpaceTime dΛ:↑(LorentzGroup d)A:ElectromagneticPotential dhA:Differentiable ℝ A.val⊢ ∑ j, (↑Λ⁻¹ j μ • Λ • ∂_ j A.val (Λ⁻¹ • x)) ν = ∑ y, ∑ x_1, ↑Λ ν x_1 * ↑Λ⁻¹ y μ * ∂_ y A.val (Λ⁻¹ • x) x_1d:ℕμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin dx:SpaceTime dΛ:↑(LorentzGroup d)A:ElectromagneticPotential dhA:Differentiable ℝ A.val⊢ ∑ j, (↑Λ⁻¹ j μ • Λ • ∂_ j A.val (Λ⁻¹ • x)) ν = ∑ y, ∑ x_1, ↑Λ ν x_1 * ↑Λ⁻¹ y μ * ∂_ y A.val (Λ⁻¹ • x) x_1]d:ℕμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin dx:SpaceTime dΛ:↑(LorentzGroup d)A:ElectromagneticPotential dhA:Differentiable ℝ A.val⊢ ∑ j, (↑Λ⁻¹ j μ • Λ • ∂_ j A.val (Λ⁻¹ • x)) ν = ∑ y, ∑ x_1, ↑Λ ν x_1 * ↑Λ⁻¹ y μ * ∂_ y A.val (Λ⁻¹ • x) x_1
  refine Finset.sum_congr rfl (fun ρ _ => ?_)d:ℕμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin dx:SpaceTime dΛ:↑(LorentzGroup d)A:ElectromagneticPotential dhA:Differentiable ℝ A.valρ:Fin 1 ⊕ Fin dx✝:ρ ∈ Finset.univ⊢ (↑Λ⁻¹ ρ μ • Λ • ∂_ ρ A.val (Λ⁻¹ • x)) ν = ∑ x_1, ↑Λ ν x_1 * ↑Λ⁻¹ ρ μ * ∂_ ρ A.val (Λ⁻¹ • x) x_1
  rw [Lorentz.Vector.apply_smul,d:ℕμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin dx:SpaceTime dΛ:↑(LorentzGroup d)A:ElectromagneticPotential dhA:Differentiable ℝ A.valρ:Fin 1 ⊕ Fin dx✝:ρ ∈ Finset.univ⊢ ↑Λ⁻¹ ρ μ * (Λ • ∂_ ρ A.val (Λ⁻¹ • x)) ν = ∑ x_1, ↑Λ ν x_1 * ↑Λ⁻¹ ρ μ * ∂_ ρ A.val (Λ⁻¹ • x) x_1d:ℕμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin dx:SpaceTime dΛ:↑(LorentzGroup d)A:ElectromagneticPotential dhA:Differentiable ℝ A.valρ:Fin 1 ⊕ Fin dx✝:ρ ∈ Finset.univ⊢ ∑ i, ↑Λ⁻¹ ρ μ * (↑Λ ν i * ∂_ ρ A.val (Λ⁻¹ • x) i) = ∑ x_1, ↑Λ ν x_1 * ↑Λ⁻¹ ρ μ * ∂_ ρ A.val (Λ⁻¹ • x) x_1 Lorentz.Vector.smul_eq_sum,d:ℕμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin dx:SpaceTime dΛ:↑(LorentzGroup d)A:ElectromagneticPotential dhA:Differentiable ℝ A.valρ:Fin 1 ⊕ Fin dx✝:ρ ∈ Finset.univ⊢ ↑Λ⁻¹ ρ μ * ∑ j, ↑Λ ν j * ∂_ ρ A.val (Λ⁻¹ • x) j = ∑ x_1, ↑Λ ν x_1 * ↑Λ⁻¹ ρ μ * ∂_ ρ A.val (Λ⁻¹ • x) x_1d:ℕμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin dx:SpaceTime dΛ:↑(LorentzGroup d)A:ElectromagneticPotential dhA:Differentiable ℝ A.valρ:Fin 1 ⊕ Fin dx✝:ρ ∈ Finset.univ⊢ ∑ i, ↑Λ⁻¹ ρ μ * (↑Λ ν i * ∂_ ρ A.val (Λ⁻¹ • x) i) = ∑ x_1, ↑Λ ν x_1 * ↑Λ⁻¹ ρ μ * ∂_ ρ A.val (Λ⁻¹ • x) x_1 Finset.mul_sumd:ℕμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin dx:SpaceTime dΛ:↑(LorentzGroup d)A:ElectromagneticPotential dhA:Differentiable ℝ A.valρ:Fin 1 ⊕ Fin dx✝:ρ ∈ Finset.univ⊢ ∑ i, ↑Λ⁻¹ ρ μ * (↑Λ ν i * ∂_ ρ A.val (Λ⁻¹ • x) i) = ∑ x_1, ↑Λ ν x_1 * ↑Λ⁻¹ ρ μ * ∂_ ρ A.val (Λ⁻¹ • x) x_1d:ℕμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin dx:SpaceTime dΛ:↑(LorentzGroup d)A:ElectromagneticPotential dhA:Differentiable ℝ A.valρ:Fin 1 ⊕ Fin dx✝:ρ ∈ Finset.univ⊢ ∑ i, ↑Λ⁻¹ ρ μ * (↑Λ ν i * ∂_ ρ A.val (Λ⁻¹ • x) i) = ∑ x_1, ↑Λ ν x_1 * ↑Λ⁻¹ ρ μ * ∂_ ρ A.val (Λ⁻¹ • x) x_1]d:ℕμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin dx:SpaceTime dΛ:↑(LorentzGroup d)A:ElectromagneticPotential dhA:Differentiable ℝ A.valρ:Fin 1 ⊕ Fin dx✝:ρ ∈ Finset.univ⊢ ∑ i, ↑Λ⁻¹ ρ μ * (↑Λ ν i * ∂_ ρ A.val (Λ⁻¹ • x) i) = ∑ x_1, ↑Λ ν x_1 * ↑Λ⁻¹ ρ μ * ∂_ ρ A.val (Λ⁻¹ • x) x_1
  refine Finset.sum_congr rfl (fun κ _ => ?_)d:ℕμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin dx:SpaceTime dΛ:↑(LorentzGroup d)A:ElectromagneticPotential dhA:Differentiable ℝ A.valρ:Fin 1 ⊕ Fin dx✝¹:ρ ∈ Finset.univκ:Fin 1 ⊕ Fin dx✝:κ ∈ Finset.univ⊢ ↑Λ⁻¹ ρ μ * (↑Λ ν κ * ∂_ ρ A.val (Λ⁻¹ • x) κ) = ↑Λ ν κ * ↑Λ⁻¹ ρ μ * ∂_ ρ A.val (Λ⁻¹ • x) κ
  ringAll goals completed! 🐙

A.6. Variational adjoint derivative of component

We find the variational adjoint derivative of the components of the potential. This will be used to find e.g. the variational derivative of the kinetic term, and derive the equations of motion.

lemma hasVarAdjDerivAt_component {d : ℕ} (μ : Fin 1 ⊕ Fin d) (A : SpaceTime d → Lorentz.Vector d)
    (hA : ContDiff ℝ ∞ A) :
        HasVarAdjDerivAt (fun (A' : SpaceTime d → Lorentz.Vector d) x => A' x μ)
          (fun (A' : SpaceTime d → ℝ) x => A' x • Lorentz.Vector.basis μ) A := byd:ℕμ:Fin 1 ⊕ Fin dA:SpaceTime d → Lorentz.Vector dhA:ContDiff ℝ ∞ A⊢ HasVarAdjDerivAt (fun A' x => A' x μ) (fun A' x => A' x • Lorentz.Vector.basis μ) A
  let f : SpaceTime d → Lorentz.Vector d → ℝ := fun x v => v μd:ℕμ:Fin 1 ⊕ Fin dA:SpaceTime d → Lorentz.Vector dhA:ContDiff ℝ ∞ Af:SpaceTime d → Lorentz.Vector d → ℝ := fun x v => v μ⊢ HasVarAdjDerivAt (fun A' x => A' x μ) (fun A' x => A' x • Lorentz.Vector.basis μ) A
  let f' : SpaceTime d → Lorentz.Vector d → ℝ → Lorentz.Vector d := fun x _ c =>
    c • Lorentz.Vector.basis μd:ℕμ:Fin 1 ⊕ Fin dA:SpaceTime d → Lorentz.Vector dhA:ContDiff ℝ ∞ Af:SpaceTime d → Lorentz.Vector d → ℝ := fun x v => v μf':SpaceTime d → Lorentz.Vector d → ℝ → Lorentz.Vector d := fun x x_1 c => c • Lorentz.Vector.basis μ⊢ HasVarAdjDerivAt (fun A' x => A' x μ) (fun A' x => A' x • Lorentz.Vector.basis μ) A
  change HasVarAdjDerivAt (fun A' x => f x (A' x)) (fun ψ x => f' x (A x) (ψ x)) Ad:ℕμ:Fin 1 ⊕ Fin dA:SpaceTime d → Lorentz.Vector dhA:ContDiff ℝ ∞ Af:SpaceTime d → Lorentz.Vector d → ℝ := fun x v => v μf':SpaceTime d → Lorentz.Vector d → ℝ → Lorentz.Vector d := fun x x_1 c => c • Lorentz.Vector.basis μ⊢ HasVarAdjDerivAt (fun A' x => f x (A' x)) (fun ψ x => f' x (A x) (ψ x)) A
  apply HasVarAdjDerivAt.fmaphud:ℕμ:Fin 1 ⊕ Fin dA:SpaceTime d → Lorentz.Vector dhA:ContDiff ℝ ∞ Af:SpaceTime d → Lorentz.Vector d → ℝ := fun x v => v μf':SpaceTime d → Lorentz.Vector d → ℝ → Lorentz.Vector d := fun x x_1 c => c • Lorentz.Vector.basis μ⊢ ContDiff ℝ ∞ Ahf'd:ℕμ:Fin 1 ⊕ Fin dA:SpaceTime d → Lorentz.Vector dhA:ContDiff ℝ ∞ Af:SpaceTime d → Lorentz.Vector d → ℝ := fun x v => v μf':SpaceTime d → Lorentz.Vector d → ℝ → Lorentz.Vector d := fun x x_1 c => c • Lorentz.Vector.basis μ⊢ ContDiff ℝ ∞ ↿fhfd:ℕμ:Fin 1 ⊕ Fin dA:SpaceTime d → Lorentz.Vector dhA:ContDiff ℝ ∞ Af:SpaceTime d → Lorentz.Vector d → ℝ := fun x v => v μf':SpaceTime d → Lorentz.Vector d → ℝ → Lorentz.Vector d := fun x x_1 c => c • Lorentz.Vector.basis μ⊢ ∀ (x : SpaceTime d) (u : Lorentz.Vector d), HasAdjFDerivAt ℝ (f x) (f' x u) u
  ·hud:ℕμ:Fin 1 ⊕ Fin dA:SpaceTime d → Lorentz.Vector dhA:ContDiff ℝ ∞ Af:SpaceTime d → Lorentz.Vector d → ℝ := fun x v => v μf':SpaceTime d → Lorentz.Vector d → ℝ → Lorentz.Vector d := fun x x_1 c => c • Lorentz.Vector.basis μ⊢ ContDiff ℝ ∞ A fun_propAll goals completed! 🐙
  ·hf'd:ℕμ:Fin 1 ⊕ Fin dA:SpaceTime d → Lorentz.Vector dhA:ContDiff ℝ ∞ Af:SpaceTime d → Lorentz.Vector d → ℝ := fun x v => v μf':SpaceTime d → Lorentz.Vector d → ℝ → Lorentz.Vector d := fun x x_1 c => c • Lorentz.Vector.basis μ⊢ ContDiff ℝ ∞ ↿f fun_propAll goals completed! 🐙
  intro x Ahfd:ℕμ:Fin 1 ⊕ Fin dA✝:SpaceTime d → Lorentz.Vector dhA:ContDiff ℝ ∞ Af:SpaceTime d → Lorentz.Vector d → ℝ := fun x v => v μf':SpaceTime d → Lorentz.Vector d → ℝ → Lorentz.Vector d := fun x x_1 c => c • Lorentz.Vector.basis μx:SpaceTime dA:Lorentz.Vector d⊢ HasAdjFDerivAt ℝ (f x) (f' x A) A
  refine { differentiableAt := ?_, hasAdjoint_fderiv := ?_ }hf.refine_1d:ℕμ:Fin 1 ⊕ Fin dA✝:SpaceTime d → Lorentz.Vector dhA:ContDiff ℝ ∞ Af:SpaceTime d → Lorentz.Vector d → ℝ := fun x v => v μf':SpaceTime d → Lorentz.Vector d → ℝ → Lorentz.Vector d := fun x x_1 c => c • Lorentz.Vector.basis μx:SpaceTime dA:Lorentz.Vector d⊢ DifferentiableAt ℝ (f x) Ahf.refine_2d:ℕμ:Fin 1 ⊕ Fin dA✝:SpaceTime d → Lorentz.Vector dhA:ContDiff ℝ ∞ Af:SpaceTime d → Lorentz.Vector d → ℝ := fun x v => v μf':SpaceTime d → Lorentz.Vector d → ℝ → Lorentz.Vector d := fun x x_1 c => c • Lorentz.Vector.basis μx:SpaceTime dA:Lorentz.Vector d⊢ HasAdjoint ℝ (⇑(fderiv ℝ (f x) A)) (f' x A)
  ·hf.refine_1d:ℕμ:Fin 1 ⊕ Fin dA✝:SpaceTime d → Lorentz.Vector dhA:ContDiff ℝ ∞ Af:SpaceTime d → Lorentz.Vector d → ℝ := fun x v => v μf':SpaceTime d → Lorentz.Vector d → ℝ → Lorentz.Vector d := fun x x_1 c => c • Lorentz.Vector.basis μx:SpaceTime dA:Lorentz.Vector d⊢ DifferentiableAt ℝ (f x) A fun_propAll goals completed! 🐙
  refine { adjoint_inner_left := ?_ }hf.refine_2d:ℕμ:Fin 1 ⊕ Fin dA✝:SpaceTime d → Lorentz.Vector dhA:ContDiff ℝ ∞ Af:SpaceTime d → Lorentz.Vector d → ℝ := fun x v => v μf':SpaceTime d → Lorentz.Vector d → ℝ → Lorentz.Vector d := fun x x_1 c => c • Lorentz.Vector.basis μx:SpaceTime dA:Lorentz.Vector d⊢ ∀ (x_1 : Lorentz.Vector d) (y : ℝ), Inner.inner ℝ (f' x A y) x_1 = Inner.inner ℝ y ((fderiv ℝ (f x) A) x_1)
  intro u vhf.refine_2d:ℕμ:Fin 1 ⊕ Fin dA✝:SpaceTime d → Lorentz.Vector dhA:ContDiff ℝ ∞ Af:SpaceTime d → Lorentz.Vector d → ℝ := fun x v => v μf':SpaceTime d → Lorentz.Vector d → ℝ → Lorentz.Vector d := fun x x_1 c => c • Lorentz.Vector.basis μx:SpaceTime dA:Lorentz.Vector du:Lorentz.Vector dv:ℝ⊢ Inner.inner ℝ (f' x A v) u = Inner.inner ℝ v ((fderiv ℝ (f x) A) u)
  simp [f, f', inner_smul_left, Lorentz.Vector.basis_inner, Lorentz.Vector.coordCLM_apply]hf.refine_2d:ℕμ:Fin 1 ⊕ Fin dA✝:SpaceTime d → Lorentz.Vector dhA:ContDiff ℝ ∞ Af:SpaceTime d → Lorentz.Vector d → ℝ := fun x v => v μf':SpaceTime d → Lorentz.Vector d → ℝ → Lorentz.Vector d := fun x x_1 c => c • Lorentz.Vector.basis μx:SpaceTime dA:Lorentz.Vector du:Lorentz.Vector dv:ℝ⊢ v * u μ = u μ * v
  ringAll goals completed! 🐙

A.7. Variational adjoint derivative of derivatives of the potential

We find the variational adjoint derivative of the derivatives of the components of the potential. This will again be used to find the variational derivative of the kinetic term, and derive the equations of motion (Maxwell's equations).



lemma deriv_hasVarAdjDerivAt {d} (μ ν : Fin 1 ⊕ Fin d) (A : SpaceTime d → Lorentz.Vector d)
    (hA : ContDiff ℝ ∞ A) :
    HasVarAdjDerivAt (fun (A : SpaceTime d → Lorentz.Vector d) x => ∂_ μ A x ν)
      (fun ψ x => - (fderiv ℝ ψ x) (Lorentz.Vector.basis μ) • Lorentz.Vector.basis ν) A := byd:ℕμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin dA:SpaceTime d → Lorentz.Vector dhA:ContDiff ℝ ∞ A⊢ HasVarAdjDerivAt (fun A x => ∂_ μ A x ν) (fun ψ x => -(fderiv ℝ ψ x) (Lorentz.Vector.basis μ) • Lorentz.Vector.basis ν)
  A
  have h0' := HasVarAdjDerivAt.fderiv' _ _
        (hF := hasVarAdjDerivAt_component ν A hA) A (Lorentz.Vector.basis μ)d:ℕμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin dA:SpaceTime d → Lorentz.Vector dhA:ContDiff ℝ ∞ Ah0':HasVarAdjDerivAt (fun φ x => (fderiv ℝ (fun x => φ x ν) x) (Lorentz.Vector.basis μ))
  (fun ψ x => (fun x' => -(fderiv ℝ ψ x') (Lorentz.Vector.basis μ)) x • Lorentz.Vector.basis ν) A⊢ HasVarAdjDerivAt (fun A x => ∂_ μ A x ν) (fun ψ x => -(fderiv ℝ ψ x) (Lorentz.Vector.basis μ) • Lorentz.Vector.basis ν)
  A
  refine HasVarAdjDerivAt.congr (G := (fun (A : SpaceTime d →
    Lorentz.Vector d) x => ∂_ μ A x ν)) h0' ?_d:ℕμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin dA:SpaceTime d → Lorentz.Vector dhA:ContDiff ℝ ∞ Ah0':HasVarAdjDerivAt (fun φ x => (fderiv ℝ (fun x => φ x ν) x) (Lorentz.Vector.basis μ))
  (fun ψ x => (fun x' => -(fderiv ℝ ψ x') (Lorentz.Vector.basis μ)) x • Lorentz.Vector.basis ν) A⊢ ∀ (φ : SpaceTime d → Lorentz.Vector d),
  ContDiff ℝ ∞ φ → (fun x => (fderiv ℝ (fun x => φ x ν) x) (Lorentz.Vector.basis μ)) = fun x => ∂_ μ φ x ν
  intro φ hφd:ℕμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin dA:SpaceTime d → Lorentz.Vector dhA:ContDiff ℝ ∞ Ah0':HasVarAdjDerivAt (fun φ x => (fderiv ℝ (fun x => φ x ν) x) (Lorentz.Vector.basis μ))
  (fun ψ x => (fun x' => -(fderiv ℝ ψ x') (Lorentz.Vector.basis μ)) x • Lorentz.Vector.basis ν) Aφ:SpaceTime d → Lorentz.Vector dhφ:ContDiff ℝ ∞ φ⊢ (fun x => (fderiv ℝ (fun x => φ x ν) x) (Lorentz.Vector.basis μ)) = fun x => ∂_ μ φ x ν
  funext xd:ℕμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin dA:SpaceTime d → Lorentz.Vector dhA:ContDiff ℝ ∞ Ah0':HasVarAdjDerivAt (fun φ x => (fderiv ℝ (fun x => φ x ν) x) (Lorentz.Vector.basis μ))
  (fun ψ x => (fun x' => -(fderiv ℝ ψ x') (Lorentz.Vector.basis μ)) x • Lorentz.Vector.basis ν) Aφ:SpaceTime d → Lorentz.Vector dhφ:ContDiff ℝ ∞ φx:SpaceTime d⊢ (fderiv ℝ (fun x => φ x ν) x) (Lorentz.Vector.basis μ) = ∂_ μ φ x ν
  rw [deriv_apply_eq μ ν φd:ℕμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin dA:SpaceTime d → Lorentz.Vector dhA:ContDiff ℝ ∞ Ah0':HasVarAdjDerivAt (fun φ x => (fderiv ℝ (fun x => φ x ν) x) (Lorentz.Vector.basis μ))
  (fun ψ x => (fun x' => -(fderiv ℝ ψ x') (Lorentz.Vector.basis μ)) x • Lorentz.Vector.basis ν) Aφ:SpaceTime d → Lorentz.Vector dhφ:ContDiff ℝ ∞ φx:SpaceTime d⊢ (fderiv ℝ (fun x => φ x ν) x) (Lorentz.Vector.basis μ) = (fderiv ℝ (fun x => φ x ν) x) (Lorentz.Vector.basis μ)hfd:ℕμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin dA:SpaceTime d → Lorentz.Vector dhA:ContDiff ℝ ∞ Ah0':HasVarAdjDerivAt (fun φ x => (fderiv ℝ (fun x => φ x ν) x) (Lorentz.Vector.basis μ))
  (fun ψ x => (fun x' => -(fderiv ℝ ψ x') (Lorentz.Vector.basis μ)) x • Lorentz.Vector.basis ν) Aφ:SpaceTime d → Lorentz.Vector dhφ:ContDiff ℝ ∞ φx:SpaceTime d⊢ Differentiable ℝ φhfd:ℕμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin dA:SpaceTime d → Lorentz.Vector dhA:ContDiff ℝ ∞ Ah0':HasVarAdjDerivAt (fun φ x => (fderiv ℝ (fun x => φ x ν) x) (Lorentz.Vector.basis μ))
  (fun ψ x => (fun x' => -(fderiv ℝ ψ x') (Lorentz.Vector.basis μ)) x • Lorentz.Vector.basis ν) Aφ:SpaceTime d → Lorentz.Vector dhφ:ContDiff ℝ ∞ φx:SpaceTime d⊢ Differentiable ℝ φ]hfd:ℕμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin dA:SpaceTime d → Lorentz.Vector dhA:ContDiff ℝ ∞ Ah0':HasVarAdjDerivAt (fun φ x => (fderiv ℝ (fun x => φ x ν) x) (Lorentz.Vector.basis μ))
  (fun ψ x => (fun x' => -(fderiv ℝ ψ x') (Lorentz.Vector.basis μ)) x • Lorentz.Vector.basis ν) Aφ:SpaceTime d → Lorentz.Vector dhφ:ContDiff ℝ ∞ φx:SpaceTime d⊢ Differentiable ℝ φ
  exact hφ.differentiable (byd:ℕμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin dA:SpaceTime d → Lorentz.Vector dhA:ContDiff ℝ ∞ Ah0':HasVarAdjDerivAt (fun φ x => (fderiv ℝ (fun x => φ x ν) x) (Lorentz.Vector.basis μ))
  (fun ψ x => (fun x' => -(fderiv ℝ ψ x') (Lorentz.Vector.basis μ)) x • Lorentz.Vector.basis ν) Aφ:SpaceTime d → Lorentz.Vector dhφ:ContDiff ℝ ∞ φx:SpaceTime d⊢ ∞ ≠ 0 simpAll goals completed! 🐙)

B. The derivative tensor of the electromagnetic potential

We define the derivative as a tensor in Lorentz.CoVector ⊗[ℝ] Lorentz.Vector for the electromagnetic potential A^μ. We then prove that this tensor transforms correctly under Lorentz transformations.



lemma deriv_eq_tensorDeriv {d} (A : ElectromagneticPotential d)
    (hA : Differentiable ℝ A) (x : SpaceTime d) :
    A.deriv x = tensorDeriv A.val x := byd:ℕA:ElectromagneticPotential dhA:Differentiable ℝ A.valx:SpaceTime d⊢ A.deriv x = tensorDeriv A.val x
  rw [deriv,d:ℕA:ElectromagneticPotential dhA:Differentiable ℝ A.valx:SpaceTime d⊢ ∑ μ, ∑ ν, ∂_ μ A.val x ν • Lorentz.CoVector.basis μ ⊗ₜ[ℝ] Lorentz.Vector.basis ν = tensorDeriv A.val xd:ℕA:ElectromagneticPotential dhA:Differentiable ℝ A.valx:SpaceTime d⊢ ∑ μ, ∑ ν, ∂_ μ A.val x ν • Lorentz.CoVector.basis μ ⊗ₜ[ℝ] Lorentz.Vector.basis ν =
  ∑ b,
    ∂_ (Lorentz.CoVector.indexEquiv (ComponentIdx.prod b).1)
        (fun x => ((basis ![Color.up]).repr (Tensorial.toTensor (A.val x))) (ComponentIdx.prod b).2) x •
      Tensorial.toTensor.symm ((basis (Fin.append ![Color.down] ![Color.up])) b) tensorDeriv_eq_sum_tensor_basis (byd:ℕA:ElectromagneticPotential dhA:Differentiable ℝ A.valx:SpaceTime d⊢ Differentiable ℝ A.vald:ℕA:ElectromagneticPotential dhA:Differentiable ℝ A.valx:SpaceTime d⊢ ∑ μ, ∑ ν, ∂_ μ A.val x ν • Lorentz.CoVector.basis μ ⊗ₜ[ℝ] Lorentz.Vector.basis ν =
  ∑ b,
    ∂_ (Lorentz.CoVector.indexEquiv (ComponentIdx.prod b).1)
        (fun x => ((basis ![Color.up]).repr (Tensorial.toTensor (A.val x))) (ComponentIdx.prod b).2) x •
      Tensorial.toTensor.symm ((basis (Fin.append ![Color.down] ![Color.up])) b) fun_propAll goals completed! 🐙d:ℕA:ElectromagneticPotential dhA:Differentiable ℝ A.valx:SpaceTime d⊢ ∑ μ, ∑ ν, ∂_ μ A.val x ν • Lorentz.CoVector.basis μ ⊗ₜ[ℝ] Lorentz.Vector.basis ν =
  ∑ b,
    ∂_ (Lorentz.CoVector.indexEquiv (ComponentIdx.prod b).1)
        (fun x => ((basis ![Color.up]).repr (Tensorial.toTensor (A.val x))) (ComponentIdx.prod b).2) x •
      Tensorial.toTensor.symm ((basis (Fin.append ![Color.down] ![Color.up])) b))]d:ℕA:ElectromagneticPotential dhA:Differentiable ℝ A.valx:SpaceTime d⊢ ∑ μ, ∑ ν, ∂_ μ A.val x ν • Lorentz.CoVector.basis μ ⊗ₜ[ℝ] Lorentz.Vector.basis ν =
  ∑ b,
    ∂_ (Lorentz.CoVector.indexEquiv (ComponentIdx.prod b).1)
        (fun x => ((basis ![Color.up]).repr (Tensorial.toTensor (A.val x))) (ComponentIdx.prod b).2) x •
      Tensorial.toTensor.symm ((basis (Fin.append ![Color.down] ![Color.up])) b)
  /- Match the basis sum. -/
  let e : ComponentIdx (Fin.append ![Color.down] ![Color.up])
      ≃ (Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d) := ComponentIdx.prod.trans <|
    Lorentz.CoVector.indexEquiv.prodCongr Lorentz.Vector.indexEquivd:ℕA:ElectromagneticPotential dhA:Differentiable ℝ A.valx:SpaceTime de:ComponentIdx (Fin.append ![Color.down] ![Color.up]) ≃ (Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d) := ComponentIdx.prod.trans (Lorentz.CoVector.indexEquiv.prodCongr Lorentz.Vector.indexEquiv)⊢ ∑ μ, ∑ ν, ∂_ μ A.val x ν • Lorentz.CoVector.basis μ ⊗ₜ[ℝ] Lorentz.Vector.basis ν =
  ∑ b,
    ∂_ (Lorentz.CoVector.indexEquiv (ComponentIdx.prod b).1)
        (fun x => ((basis ![Color.up]).repr (Tensorial.toTensor (A.val x))) (ComponentIdx.prod b).2) x •
      Tensorial.toTensor.symm ((basis (Fin.append ![Color.down] ![Color.up])) b)
  rw [← e.symm.sum_comp,d:ℕA:ElectromagneticPotential dhA:Differentiable ℝ A.valx:SpaceTime de:ComponentIdx (Fin.append ![Color.down] ![Color.up]) ≃ (Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d) := ComponentIdx.prod.trans (Lorentz.CoVector.indexEquiv.prodCongr Lorentz.Vector.indexEquiv)⊢ ∑ μ, ∑ ν, ∂_ μ A.val x ν • Lorentz.CoVector.basis μ ⊗ₜ[ℝ] Lorentz.Vector.basis ν =
  ∑ i,
    ∂_ (Lorentz.CoVector.indexEquiv (ComponentIdx.prod (e.symm i)).1)
        (fun x => ((basis ![Color.up]).repr (Tensorial.toTensor (A.val x))) (ComponentIdx.prod (e.symm i)).2) x •
      Tensorial.toTensor.symm ((basis (Fin.append ![Color.down] ![Color.up])) (e.symm i))d:ℕA:ElectromagneticPotential dhA:Differentiable ℝ A.valx:SpaceTime de:ComponentIdx (Fin.append ![Color.down] ![Color.up]) ≃ (Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d) := ComponentIdx.prod.trans (Lorentz.CoVector.indexEquiv.prodCongr Lorentz.Vector.indexEquiv)⊢ ∑ μ, ∑ ν, ∂_ μ A.val x ν • Lorentz.CoVector.basis μ ⊗ₜ[ℝ] Lorentz.Vector.basis ν =
  ∑ x_1,
    ∑ y,
      ∂_ (Lorentz.CoVector.indexEquiv (ComponentIdx.prod (e.symm (x_1, y))).1)
          (fun x => ((basis ![Color.up]).repr (Tensorial.toTensor (A.val x))) (ComponentIdx.prod (e.symm (x_1, y))).2)
          x •
        Tensorial.toTensor.symm ((basis (Fin.append ![Color.down] ![Color.up])) (e.symm (x_1, y))) Fintype.sum_prod_typed:ℕA:ElectromagneticPotential dhA:Differentiable ℝ A.valx:SpaceTime de:ComponentIdx (Fin.append ![Color.down] ![Color.up]) ≃ (Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d) := ComponentIdx.prod.trans (Lorentz.CoVector.indexEquiv.prodCongr Lorentz.Vector.indexEquiv)⊢ ∑ μ, ∑ ν, ∂_ μ A.val x ν • Lorentz.CoVector.basis μ ⊗ₜ[ℝ] Lorentz.Vector.basis ν =
  ∑ x_1,
    ∑ y,
      ∂_ (Lorentz.CoVector.indexEquiv (ComponentIdx.prod (e.symm (x_1, y))).1)
          (fun x => ((basis ![Color.up]).repr (Tensorial.toTensor (A.val x))) (ComponentIdx.prod (e.symm (x_1, y))).2)
          x •
        Tensorial.toTensor.symm ((basis (Fin.append ![Color.down] ![Color.up])) (e.symm (x_1, y)))d:ℕA:ElectromagneticPotential dhA:Differentiable ℝ A.valx:SpaceTime de:ComponentIdx (Fin.append ![Color.down] ![Color.up]) ≃ (Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d) := ComponentIdx.prod.trans (Lorentz.CoVector.indexEquiv.prodCongr Lorentz.Vector.indexEquiv)⊢ ∑ μ, ∑ ν, ∂_ μ A.val x ν • Lorentz.CoVector.basis μ ⊗ₜ[ℝ] Lorentz.Vector.basis ν =
  ∑ x_1,
    ∑ y,
      ∂_ (Lorentz.CoVector.indexEquiv (ComponentIdx.prod (e.symm (x_1, y))).1)
          (fun x => ((basis ![Color.up]).repr (Tensorial.toTensor (A.val x))) (ComponentIdx.prod (e.symm (x_1, y))).2)
          x •
        Tensorial.toTensor.symm ((basis (Fin.append ![Color.down] ![Color.up])) (e.symm (x_1, y)))]d:ℕA:ElectromagneticPotential dhA:Differentiable ℝ A.valx:SpaceTime de:ComponentIdx (Fin.append ![Color.down] ![Color.up]) ≃ (Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d) := ComponentIdx.prod.trans (Lorentz.CoVector.indexEquiv.prodCongr Lorentz.Vector.indexEquiv)⊢ ∑ μ, ∑ ν, ∂_ μ A.val x ν • Lorentz.CoVector.basis μ ⊗ₜ[ℝ] Lorentz.Vector.basis ν =
  ∑ x_1,
    ∑ y,
      ∂_ (Lorentz.CoVector.indexEquiv (ComponentIdx.prod (e.symm (x_1, y))).1)
          (fun x => ((basis ![Color.up]).repr (Tensorial.toTensor (A.val x))) (ComponentIdx.prod (e.symm (x_1, y))).2)
          x •
        Tensorial.toTensor.symm ((basis (Fin.append ![Color.down] ![Color.up])) (e.symm (x_1, y)))
  /- Getting rid of the sums -/
  refine Finset.sum_congr rfl (fun μ _ => Finset.sum_congr rfl (fun ν _ => ?_))d:ℕA:ElectromagneticPotential dhA:Differentiable ℝ A.valx:SpaceTime de:ComponentIdx (Fin.append ![Color.down] ![Color.up]) ≃ (Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d) := ComponentIdx.prod.trans (Lorentz.CoVector.indexEquiv.prodCongr Lorentz.Vector.indexEquiv)μ:Fin 1 ⊕ Fin dx✝¹:μ ∈ Finset.univν:Fin 1 ⊕ Fin dx✝:ν ∈ Finset.univ⊢ ∂_ μ A.val x ν • Lorentz.CoVector.basis μ ⊗ₜ[ℝ] Lorentz.Vector.basis ν =
  ∂_ (Lorentz.CoVector.indexEquiv (ComponentIdx.prod (e.symm (μ, ν))).1)
      (fun x => ((basis ![Color.up]).repr (Tensorial.toTensor (A.val x))) (ComponentIdx.prod (e.symm (μ, ν))).2) x •
    Tensorial.toTensor.symm ((basis (Fin.append ![Color.down] ![Color.up])) (e.symm (μ, ν)))
  congre_ad:ℕA:ElectromagneticPotential dhA:Differentiable ℝ A.valx:SpaceTime de:ComponentIdx (Fin.append ![Color.down] ![Color.up]) ≃ (Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d) := ComponentIdx.prod.trans (Lorentz.CoVector.indexEquiv.prodCongr Lorentz.Vector.indexEquiv)μ:Fin 1 ⊕ Fin dx✝¹:μ ∈ Finset.univν:Fin 1 ⊕ Fin dx✝:ν ∈ Finset.univ⊢ ∂_ μ A.val x ν =
  ∂_ (Lorentz.CoVector.indexEquiv (ComponentIdx.prod (e.symm (μ, ν))).1)
    (fun x => ((basis ![Color.up]).repr (Tensorial.toTensor (A.val x))) (ComponentIdx.prod (e.symm (μ, ν))).2) xe_ad:ℕA:ElectromagneticPotential dhA:Differentiable ℝ A.valx:SpaceTime de:ComponentIdx (Fin.append ![Color.down] ![Color.up]) ≃ (Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d) := ComponentIdx.prod.trans (Lorentz.CoVector.indexEquiv.prodCongr Lorentz.Vector.indexEquiv)μ:Fin 1 ⊕ Fin dx✝¹:μ ∈ Finset.univν:Fin 1 ⊕ Fin dx✝:ν ∈ Finset.univ⊢ Lorentz.CoVector.basis μ ⊗ₜ[ℝ] Lorentz.Vector.basis ν =
  Tensorial.toTensor.symm ((basis (Fin.append ![Color.down] ![Color.up])) (e.symm (μ, ν)))
  /- The coefficients. -/
  ·e_ad:ℕA:ElectromagneticPotential dhA:Differentiable ℝ A.valx:SpaceTime de:ComponentIdx (Fin.append ![Color.down] ![Color.up]) ≃ (Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d) := ComponentIdx.prod.trans (Lorentz.CoVector.indexEquiv.prodCongr Lorentz.Vector.indexEquiv)μ:Fin 1 ⊕ Fin dx✝¹:μ ∈ Finset.univν:Fin 1 ⊕ Fin dx✝:ν ∈ Finset.univ⊢ ∂_ μ A.val x ν =
  ∂_ (Lorentz.CoVector.indexEquiv (ComponentIdx.prod (e.symm (μ, ν))).1)
    (fun x => ((basis ![Color.up]).repr (Tensorial.toTensor (A.val x))) (ComponentIdx.prod (e.symm (μ, ν))).2) x simp [e]e_ad:ℕA:ElectromagneticPotential dhA:Differentiable ℝ A.valx:SpaceTime de:ComponentIdx (Fin.append ![Color.down] ![Color.up]) ≃ (Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d) := ComponentIdx.prod.trans (Lorentz.CoVector.indexEquiv.prodCongr Lorentz.Vector.indexEquiv)μ:Fin 1 ⊕ Fin dx✝¹:μ ∈ Finset.univν:Fin 1 ⊕ Fin dx✝:ν ∈ Finset.univ⊢ ∂_ μ A.val x ν =
  ∂_ μ (fun x => ((basis ![Color.up]).repr (Tensorial.toTensor (A.val x))) (Lorentz.Vector.indexEquiv.symm ν)) x
    rw [deriv_apply_eq _ _ _ (byd:ℕA:ElectromagneticPotential dhA:Differentiable ℝ A.valx:SpaceTime de:ComponentIdx (Fin.append ![Color.down] ![Color.up]) ≃ (Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d) := ComponentIdx.prod.trans (Lorentz.CoVector.indexEquiv.prodCongr Lorentz.Vector.indexEquiv)μ:Fin 1 ⊕ Fin dx✝¹:μ ∈ Finset.univν:Fin 1 ⊕ Fin dx✝:ν ∈ Finset.univ⊢ Differentiable ℝ A.vale_ad:ℕA:ElectromagneticPotential dhA:Differentiable ℝ A.valx:SpaceTime de:ComponentIdx (Fin.append ![Color.down] ![Color.up]) ≃ (Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d) := ComponentIdx.prod.trans (Lorentz.CoVector.indexEquiv.prodCongr Lorentz.Vector.indexEquiv)μ:Fin 1 ⊕ Fin dx✝¹:μ ∈ Finset.univν:Fin 1 ⊕ Fin dx✝:ν ∈ Finset.univ⊢ (fderiv ℝ (fun x => A.val x ν) x) (Lorentz.Vector.basis μ) =
  ∂_ μ (fun x => ((basis ![Color.up]).repr (Tensorial.toTensor (A.val x))) (Lorentz.Vector.indexEquiv.symm ν)) x fun_propAll goals completed! 🐙e_ad:ℕA:ElectromagneticPotential dhA:Differentiable ℝ A.valx:SpaceTime de:ComponentIdx (Fin.append ![Color.down] ![Color.up]) ≃ (Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d) := ComponentIdx.prod.trans (Lorentz.CoVector.indexEquiv.prodCongr Lorentz.Vector.indexEquiv)μ:Fin 1 ⊕ Fin dx✝¹:μ ∈ Finset.univν:Fin 1 ⊕ Fin dx✝:ν ∈ Finset.univ⊢ (fderiv ℝ (fun x => A.val x ν) x) (Lorentz.Vector.basis μ) =
  ∂_ μ (fun x => ((basis ![Color.up]).repr (Tensorial.toTensor (A.val x))) (Lorentz.Vector.indexEquiv.symm ν)) x)]e_ad:ℕA:ElectromagneticPotential dhA:Differentiable ℝ A.valx:SpaceTime de:ComponentIdx (Fin.append ![Color.down] ![Color.up]) ≃ (Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d) := ComponentIdx.prod.trans (Lorentz.CoVector.indexEquiv.prodCongr Lorentz.Vector.indexEquiv)μ:Fin 1 ⊕ Fin dx✝¹:μ ∈ Finset.univν:Fin 1 ⊕ Fin dx✝:ν ∈ Finset.univ⊢ (fderiv ℝ (fun x => A.val x ν) x) (Lorentz.Vector.basis μ) =
  ∂_ μ (fun x => ((basis ![Color.up]).repr (Tensorial.toTensor (A.val x))) (Lorentz.Vector.indexEquiv.symm ν)) x
    congre_a.e_fd:ℕA:ElectromagneticPotential dhA:Differentiable ℝ A.valx:SpaceTime de:ComponentIdx (Fin.append ![Color.down] ![Color.up]) ≃ (Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d) := ComponentIdx.prod.trans (Lorentz.CoVector.indexEquiv.prodCongr Lorentz.Vector.indexEquiv)μ:Fin 1 ⊕ Fin dx✝¹:μ ∈ Finset.univν:Fin 1 ⊕ Fin dx✝:ν ∈ Finset.univ⊢ (fun x => A.val x ν) = fun x =>
  ((basis ![Color.up]).repr (Tensorial.toTensor (A.val x))) (Lorentz.Vector.indexEquiv.symm ν)
    simp [Lorentz.Vector.tensor_basis_repr_toTensor_apply]All goals completed! 🐙
  /- The basis elements. -/
  ·e_ad:ℕA:ElectromagneticPotential dhA:Differentiable ℝ A.valx:SpaceTime de:ComponentIdx (Fin.append ![Color.down] ![Color.up]) ≃ (Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d) := ComponentIdx.prod.trans (Lorentz.CoVector.indexEquiv.prodCongr Lorentz.Vector.indexEquiv)μ:Fin 1 ⊕ Fin dx✝¹:μ ∈ Finset.univν:Fin 1 ⊕ Fin dx✝:ν ∈ Finset.univ⊢ Lorentz.CoVector.basis μ ⊗ₜ[ℝ] Lorentz.Vector.basis ν =
  Tensorial.toTensor.symm ((basis (Fin.append ![Color.down] ![Color.up])) (e.symm (μ, ν))) change _ = ((Tensor.basis (S := realLorentzTensor d) (Fin.append ![Color.down] ![Color.up])).map
      (Tensorial.toTensor (M := (Lorentz.CoVector d) ⊗[ℝ] (Lorentz.Vector d))).symm) (e.symm (μ, ν))e_ad:ℕA:ElectromagneticPotential dhA:Differentiable ℝ A.valx:SpaceTime de:ComponentIdx (Fin.append ![Color.down] ![Color.up]) ≃ (Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d) := ComponentIdx.prod.trans (Lorentz.CoVector.indexEquiv.prodCongr Lorentz.Vector.indexEquiv)μ:Fin 1 ⊕ Fin dx✝¹:μ ∈ Finset.univν:Fin 1 ⊕ Fin dx✝:ν ∈ Finset.univ⊢ Lorentz.CoVector.basis μ ⊗ₜ[ℝ] Lorentz.Vector.basis ν =
  ((basis (Fin.append ![Color.down] ![Color.up])).map Tensorial.toTensor.symm) (e.symm (μ, ν))
    rw [Tensorial.basis_map_prod,e_ad:ℕA:ElectromagneticPotential dhA:Differentiable ℝ A.valx:SpaceTime de:ComponentIdx (Fin.append ![Color.down] ![Color.up]) ≃ (Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d) := ComponentIdx.prod.trans (Lorentz.CoVector.indexEquiv.prodCongr Lorentz.Vector.indexEquiv)μ:Fin 1 ⊕ Fin dx✝¹:μ ∈ Finset.univν:Fin 1 ⊕ Fin dx✝:ν ∈ Finset.univ⊢ Lorentz.CoVector.basis μ ⊗ₜ[ℝ] Lorentz.Vector.basis ν =
  ((((basis ![Color.down]).map Tensorial.toTensor.symm).tensorProduct
          ((basis ![Color.up]).map Tensorial.toTensor.symm)).reindex
      ComponentIdx.prod.symm)
    (e.symm (μ, ν))e_ad:ℕA:ElectromagneticPotential dhA:Differentiable ℝ A.valx:SpaceTime de:ComponentIdx (Fin.append ![Color.down] ![Color.up]) ≃ (Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d) := ComponentIdx.prod.trans (Lorentz.CoVector.indexEquiv.prodCongr Lorentz.Vector.indexEquiv)μ:Fin 1 ⊕ Fin dx✝¹:μ ∈ Finset.univν:Fin 1 ⊕ Fin dx✝:ν ∈ Finset.univ⊢ Tensorial.toTensor.symm ((basis ![Color.down]) (Lorentz.CoVector.indexEquiv.symm μ)) ⊗ₜ[ℝ]
    Tensorial.toTensor.symm ((basis ![Color.up]) (Lorentz.Vector.indexEquiv.symm ν)) =
  ((((basis ![Color.down]).map Tensorial.toTensor.symm).tensorProduct
          ((basis ![Color.up]).map Tensorial.toTensor.symm)).reindex
      ComponentIdx.prod.symm)
    (e.symm (μ, ν)) ← Lorentz.Vector.toTensor_symm_basis,e_ad:ℕA:ElectromagneticPotential dhA:Differentiable ℝ A.valx:SpaceTime de:ComponentIdx (Fin.append ![Color.down] ![Color.up]) ≃ (Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d) := ComponentIdx.prod.trans (Lorentz.CoVector.indexEquiv.prodCongr Lorentz.Vector.indexEquiv)μ:Fin 1 ⊕ Fin dx✝¹:μ ∈ Finset.univν:Fin 1 ⊕ Fin dx✝:ν ∈ Finset.univ⊢ Lorentz.CoVector.basis μ ⊗ₜ[ℝ] Tensorial.toTensor.symm ((basis ![Color.up]) (Lorentz.Vector.indexEquiv.symm ν)) =
  ((((basis ![Color.down]).map Tensorial.toTensor.symm).tensorProduct
          ((basis ![Color.up]).map Tensorial.toTensor.symm)).reindex
      ComponentIdx.prod.symm)
    (e.symm (μ, ν))e_ad:ℕA:ElectromagneticPotential dhA:Differentiable ℝ A.valx:SpaceTime de:ComponentIdx (Fin.append ![Color.down] ![Color.up]) ≃ (Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d) := ComponentIdx.prod.trans (Lorentz.CoVector.indexEquiv.prodCongr Lorentz.Vector.indexEquiv)μ:Fin 1 ⊕ Fin dx✝¹:μ ∈ Finset.univν:Fin 1 ⊕ Fin dx✝:ν ∈ Finset.univ⊢ Tensorial.toTensor.symm ((basis ![Color.down]) (Lorentz.CoVector.indexEquiv.symm μ)) ⊗ₜ[ℝ]
    Tensorial.toTensor.symm ((basis ![Color.up]) (Lorentz.Vector.indexEquiv.symm ν)) =
  ((((basis ![Color.down]).map Tensorial.toTensor.symm).tensorProduct
          ((basis ![Color.up]).map Tensorial.toTensor.symm)).reindex
      ComponentIdx.prod.symm)
    (e.symm (μ, ν))
      ← Lorentz.CoVector.toTensor_symm_basise_ad:ℕA:ElectromagneticPotential dhA:Differentiable ℝ A.valx:SpaceTime de:ComponentIdx (Fin.append ![Color.down] ![Color.up]) ≃ (Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d) := ComponentIdx.prod.trans (Lorentz.CoVector.indexEquiv.prodCongr Lorentz.Vector.indexEquiv)μ:Fin 1 ⊕ Fin dx✝¹:μ ∈ Finset.univν:Fin 1 ⊕ Fin dx✝:ν ∈ Finset.univ⊢ Tensorial.toTensor.symm ((basis ![Color.down]) (Lorentz.CoVector.indexEquiv.symm μ)) ⊗ₜ[ℝ]
    Tensorial.toTensor.symm ((basis ![Color.up]) (Lorentz.Vector.indexEquiv.symm ν)) =
  ((((basis ![Color.down]).map Tensorial.toTensor.symm).tensorProduct
          ((basis ![Color.up]).map Tensorial.toTensor.symm)).reindex
      ComponentIdx.prod.symm)
    (e.symm (μ, ν))e_ad:ℕA:ElectromagneticPotential dhA:Differentiable ℝ A.valx:SpaceTime de:ComponentIdx (Fin.append ![Color.down] ![Color.up]) ≃ (Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d) := ComponentIdx.prod.trans (Lorentz.CoVector.indexEquiv.prodCongr Lorentz.Vector.indexEquiv)μ:Fin 1 ⊕ Fin dx✝¹:μ ∈ Finset.univν:Fin 1 ⊕ Fin dx✝:ν ∈ Finset.univ⊢ Tensorial.toTensor.symm ((basis ![Color.down]) (Lorentz.CoVector.indexEquiv.symm μ)) ⊗ₜ[ℝ]
    Tensorial.toTensor.symm ((basis ![Color.up]) (Lorentz.Vector.indexEquiv.symm ν)) =
  ((((basis ![Color.down]).map Tensorial.toTensor.symm).tensorProduct
          ((basis ![Color.up]).map Tensorial.toTensor.symm)).reindex
      ComponentIdx.prod.symm)
    (e.symm (μ, ν))]e_ad:ℕA:ElectromagneticPotential dhA:Differentiable ℝ A.valx:SpaceTime de:ComponentIdx (Fin.append ![Color.down] ![Color.up]) ≃ (Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d) := ComponentIdx.prod.trans (Lorentz.CoVector.indexEquiv.prodCongr Lorentz.Vector.indexEquiv)μ:Fin 1 ⊕ Fin dx✝¹:μ ∈ Finset.univν:Fin 1 ⊕ Fin dx✝:ν ∈ Finset.univ⊢ Tensorial.toTensor.symm ((basis ![Color.down]) (Lorentz.CoVector.indexEquiv.symm μ)) ⊗ₜ[ℝ]
    Tensorial.toTensor.symm ((basis ![Color.up]) (Lorentz.Vector.indexEquiv.symm ν)) =
  ((((basis ![Color.down]).map Tensorial.toTensor.symm).tensorProduct
          ((basis ![Color.up]).map Tensorial.toTensor.symm)).reindex
      ComponentIdx.prod.symm)
    (e.symm (μ, ν))
    simp [e]All goals completed! 🐙

B.1. Equivariance of the derivative tensor

We show that the derivative tensor is equivariant under the action of the Lorentz group. That is, ∂_μ (fun x => Λ • A (Λ⁻¹ • x)) = Λ • (∂_μ A (Λ⁻¹ • x)), or in words: applying the Lorentz transformation to the potential and then taking the derivative is the same as taking the derivative and then applying the Lorentz transformation to the resulting tensor.


lemma deriv_equivariant {d} {x : SpaceTime d} (A : ElectromagneticPotential d)
    (Λ : LorentzGroup d)
    (hf : Differentiable ℝ A) : deriv (Λ • A) x = Λ • (deriv A (Λ⁻¹ • x)) := byd:ℕx:SpaceTime dA:ElectromagneticPotential dΛ:↑(LorentzGroup d)hf:Differentiable ℝ A.val⊢ (Λ • A).deriv x = Λ • A.deriv (Λ⁻¹ • x)
  rw [deriv_eq_tensorDeriv,d:ℕx:SpaceTime dA:ElectromagneticPotential dΛ:↑(LorentzGroup d)hf:Differentiable ℝ A.val⊢ tensorDeriv (Λ • A).val x = Λ • A.deriv (Λ⁻¹ • x)hAd:ℕx:SpaceTime dA:ElectromagneticPotential dΛ:↑(LorentzGroup d)hf:Differentiable ℝ A.val⊢ Differentiable ℝ (Λ • A).valhfd:ℕx:SpaceTime dA:ElectromagneticPotential dΛ:↑(LorentzGroup d)hf:Differentiable ℝ A.val⊢ Differentiable ℝ A.valhAd:ℕx:SpaceTime dA:ElectromagneticPotential dΛ:↑(LorentzGroup d)hf:Differentiable ℝ A.val⊢ Differentiable ℝ A.valhAd:ℕx:SpaceTime dA:ElectromagneticPotential dΛ:↑(LorentzGroup d)hf:Differentiable ℝ A.val⊢ Differentiable ℝ (Λ • A).val deriv_eq_tensorDeriv,d:ℕx:SpaceTime dA:ElectromagneticPotential dΛ:↑(LorentzGroup d)hf:Differentiable ℝ A.val⊢ tensorDeriv (Λ • A).val x = Λ • tensorDeriv A.val (Λ⁻¹ • x)hAd:ℕx:SpaceTime dA:ElectromagneticPotential dΛ:↑(LorentzGroup d)hf:Differentiable ℝ A.val⊢ Differentiable ℝ A.valhAd:ℕx:SpaceTime dA:ElectromagneticPotential dΛ:↑(LorentzGroup d)hf:Differentiable ℝ A.val⊢ Differentiable ℝ (Λ • A).valhfd:ℕx:SpaceTime dA:ElectromagneticPotential dΛ:↑(LorentzGroup d)hf:Differentiable ℝ A.val⊢ Differentiable ℝ A.valhAd:ℕx:SpaceTime dA:ElectromagneticPotential dΛ:↑(LorentzGroup d)hf:Differentiable ℝ A.val⊢ Differentiable ℝ A.valhAd:ℕx:SpaceTime dA:ElectromagneticPotential dΛ:↑(LorentzGroup d)hf:Differentiable ℝ A.val⊢ Differentiable ℝ (Λ • A).val action_val,d:ℕx:SpaceTime dA:ElectromagneticPotential dΛ:↑(LorentzGroup d)hf:Differentiable ℝ A.val⊢ tensorDeriv (fun x => Λ • A.val (Λ⁻¹ • x)) x = Λ • tensorDeriv A.val (Λ⁻¹ • x)hAd:ℕx:SpaceTime dA:ElectromagneticPotential dΛ:↑(LorentzGroup d)hf:Differentiable ℝ A.val⊢ Differentiable ℝ A.valhAd:ℕx:SpaceTime dA:ElectromagneticPotential dΛ:↑(LorentzGroup d)hf:Differentiable ℝ A.val⊢ Differentiable ℝ (Λ • A).valhfd:ℕx:SpaceTime dA:ElectromagneticPotential dΛ:↑(LorentzGroup d)hf:Differentiable ℝ A.val⊢ Differentiable ℝ A.valhAd:ℕx:SpaceTime dA:ElectromagneticPotential dΛ:↑(LorentzGroup d)hf:Differentiable ℝ A.val⊢ Differentiable ℝ A.valhAd:ℕx:SpaceTime dA:ElectromagneticPotential dΛ:↑(LorentzGroup d)hf:Differentiable ℝ A.val⊢ Differentiable ℝ (Λ • A).val tensorDeriv_equivariantd:ℕx:SpaceTime dA:ElectromagneticPotential dΛ:↑(LorentzGroup d)hf:Differentiable ℝ A.val⊢ Λ • tensorDeriv A.val (Λ⁻¹ • x) = Λ • tensorDeriv A.val (Λ⁻¹ • x)hfd:ℕx:SpaceTime dA:ElectromagneticPotential dΛ:↑(LorentzGroup d)hf:Differentiable ℝ A.val⊢ Differentiable ℝ A.valhAd:ℕx:SpaceTime dA:ElectromagneticPotential dΛ:↑(LorentzGroup d)hf:Differentiable ℝ A.val⊢ Differentiable ℝ A.valhAd:ℕx:SpaceTime dA:ElectromagneticPotential dΛ:↑(LorentzGroup d)hf:Differentiable ℝ A.val⊢ Differentiable ℝ (Λ • A).valhfd:ℕx:SpaceTime dA:ElectromagneticPotential dΛ:↑(LorentzGroup d)hf:Differentiable ℝ A.val⊢ Differentiable ℝ A.valhAd:ℕx:SpaceTime dA:ElectromagneticPotential dΛ:↑(LorentzGroup d)hf:Differentiable ℝ A.val⊢ Differentiable ℝ A.valhAd:ℕx:SpaceTime dA:ElectromagneticPotential dΛ:↑(LorentzGroup d)hf:Differentiable ℝ A.val⊢ Differentiable ℝ (Λ • A).val]hfd:ℕx:SpaceTime dA:ElectromagneticPotential dΛ:↑(LorentzGroup d)hf:Differentiable ℝ A.val⊢ Differentiable ℝ A.valhAd:ℕx:SpaceTime dA:ElectromagneticPotential dΛ:↑(LorentzGroup d)hf:Differentiable ℝ A.val⊢ Differentiable ℝ A.valhAd:ℕx:SpaceTime dA:ElectromagneticPotential dΛ:↑(LorentzGroup d)hf:Differentiable ℝ A.val⊢ Differentiable ℝ (Λ • A).val
  all_goals fun_propAll goals completed! 🐙

B.2. The elements of the derivative tensor in terms of the basis

We show that in the standard basis, the elements of the derivative tensor are just equal to ∂_ μ A x ν.

Evaluation of the tensor components of ∂_ μ A x ν.


lemma tensorDeriv_eval_eq {d} {A : ElectromagneticPotential d} (hA : Differentiable ℝ A)
    (x : SpaceTime d) (μ ν : Fin 1 ⊕ Fin d) :
    toField {tensorDeriv A.val x | [μ] [ν]}ᵀ = ∂_ μ A x ν := byd:ℕA:ElectromagneticPotential dhA:Differentiable ℝ A.valx:SpaceTime dμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d⊢ toField ((evalT 0 ν) ((evalT 0 μ) (toTensor (tensorDeriv A.val x)))) = ∂_ μ A.val x ν
  trans (Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis).repr (deriv A x) (μ, ν)d:ℕA:ElectromagneticPotential dhA:Differentiable ℝ A.valx:SpaceTime dμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d⊢ toField ((evalT 0 ν) ((evalT 0 μ) (toTensor (tensorDeriv A.val x)))) =
  ((Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis).repr (A.deriv x)) (μ, ν)d:ℕA:ElectromagneticPotential dhA:Differentiable ℝ A.valx:SpaceTime dμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d⊢ ((Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis).repr (A.deriv x)) (μ, ν) = ∂_ μ A.val x ν; swapd:ℕA:ElectromagneticPotential dhA:Differentiable ℝ A.valx:SpaceTime dμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d⊢ ((Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis).repr (A.deriv x)) (μ, ν) = ∂_ μ A.val x νd:ℕA:ElectromagneticPotential dhA:Differentiable ℝ A.valx:SpaceTime dμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d⊢ toField ((evalT 0 ν) ((evalT 0 μ) (toTensor (tensorDeriv A.val x)))) =
  ((Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis).repr (A.deriv x)) (μ, ν)
  ·d:ℕA:ElectromagneticPotential dhA:Differentiable ℝ A.valx:SpaceTime dμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d⊢ ((Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis).repr (A.deriv x)) (μ, ν) = ∂_ μ A.val x ν simp [deriv, Basis.tensorProduct_repr_tmul_apply, Finsupp.single_apply]All goals completed! 🐙
  rw [deriv_eq_tensorDeriv _ hAd:ℕA:ElectromagneticPotential dhA:Differentiable ℝ A.valx:SpaceTime dμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d⊢ toField ((evalT 0 ν) ((evalT 0 μ) (toTensor (tensorDeriv A.val x)))) =
  ((Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis).repr (tensorDeriv A.val x)) (μ, ν)d:ℕA:ElectromagneticPotential dhA:Differentiable ℝ A.valx:SpaceTime dμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d⊢ toField ((evalT 0 ν) ((evalT 0 μ) (toTensor (tensorDeriv A.val x)))) =
  ((Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis).repr (tensorDeriv A.val x)) (μ, ν)]d:ℕA:ElectromagneticPotential dhA:Differentiable ℝ A.valx:SpaceTime dμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d⊢ toField ((evalT 0 ν) ((evalT 0 μ) (toTensor (tensorDeriv A.val x)))) =
  ((Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis).repr (tensorDeriv A.val x)) (μ, ν)
  generalize (tensorDeriv A.val x) = td:ℕA:ElectromagneticPotential dhA:Differentiable ℝ A.valx:SpaceTime dμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin dt:Lorentz.CoVector d ⊗[ℝ] Lorentz.Vector d⊢ toField ((evalT 0 ν) ((evalT 0 μ) (toTensor t))) =
  ((Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis).repr t) (μ, ν)
  obtain ⟨t, rfl⟩ := toTensor.symm.surjective td:ℕA:ElectromagneticPotential dhA:Differentiable ℝ A.valx:SpaceTime dμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin dt:(realLorentzTensor d).Tensor (Fin.append ![Color.down] ![Color.up])⊢ toField ((evalT 0 ν) ((evalT 0 μ) (toTensor (toTensor.symm t)))) =
  ((Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis).repr (toTensor.symm t)) (μ, ν)
  induction' t using Tensor.induction_on_basis with b a t h t1 t2 h1 h2hd:ℕA:ElectromagneticPotential dhA:Differentiable ℝ A.valx:SpaceTime dμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin db:ComponentIdx (Fin.append ![Color.down] ![Color.up])⊢ toField ((evalT 0 ν) ((evalT 0 μ) (toTensor (toTensor.symm ((basis (Fin.append ![Color.down] ![Color.up])) b))))) =
  ((Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis).repr
      (toTensor.symm ((basis (Fin.append ![Color.down] ![Color.up])) b)))
    (μ, ν)hzerod:ℕA:ElectromagneticPotential dhA:Differentiable ℝ A.valx:SpaceTime dμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d⊢ toField ((evalT 0 ν) ((evalT 0 μ) (toTensor (toTensor.symm 0)))) =
  ((Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis).repr (toTensor.symm 0)) (μ, ν)hsmuld:ℕA:ElectromagneticPotential dhA:Differentiable ℝ A.valx:SpaceTime dμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin da:ℝt:(realLorentzTensor d).Tensor (Fin.append ![Color.down] ![Color.up])h:toField ((evalT 0 ν) ((evalT 0 μ) (toTensor (toTensor.symm t)))) =
  ((Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis).repr (toTensor.symm t)) (μ, ν)⊢ toField ((evalT 0 ν) ((evalT 0 μ) (toTensor (toTensor.symm (a • t))))) =
  ((Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis).repr (toTensor.symm (a • t))) (μ, ν)haddd:ℕA:ElectromagneticPotential dhA:Differentiable ℝ A.valx:SpaceTime dμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin dt1:(realLorentzTensor d).Tensor (Fin.append ![Color.down] ![Color.up])t2:(realLorentzTensor d).Tensor (Fin.append ![Color.down] ![Color.up])h1:toField ((evalT 0 ν) ((evalT 0 μ) (toTensor (toTensor.symm t1)))) =
  ((Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis).repr (toTensor.symm t1)) (μ, ν)h2:toField ((evalT 0 ν) ((evalT 0 μ) (toTensor (toTensor.symm t2)))) =
  ((Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis).repr (toTensor.symm t2)) (μ, ν)⊢ toField ((evalT 0 ν) ((evalT 0 μ) (toTensor (toTensor.symm (t1 + t2))))) =
  ((Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis).repr (toTensor.symm (t1 + t2))) (μ, ν)
  ·hd:ℕA:ElectromagneticPotential dhA:Differentiable ℝ A.valx:SpaceTime dμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin db:ComponentIdx (Fin.append ![Color.down] ![Color.up])⊢ toField ((evalT 0 ν) ((evalT 0 μ) (toTensor (toTensor.symm ((basis (Fin.append ![Color.down] ![Color.up])) b))))) =
  ((Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis).repr
      (toTensor.symm ((basis (Fin.append ![Color.down] ![Color.up])) b)))
    (μ, ν) simp only [LinearEquiv.apply_symm_apply, basis_apply, evalT_pure, Pure.evalP, map_smul,
      toField_pure, smul_eq_mul, mul_one, Pure.evalPCoeff]hd:ℕA:ElectromagneticPotential dhA:Differentiable ℝ A.valx:SpaceTime dμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin db:ComponentIdx (Fin.append ![Color.down] ![Color.up])⊢ ((match Fin.append ![Color.down] ![Color.up] 0 with
          | Color.up => Lorentz.contrBasis d
          | Color.down => Lorentz.coBasis d).repr
        (Pure.basisVector (Fin.append ![Color.down] ![Color.up]) b 0))
      μ *
    ((match (Fin.append ![Color.down] ![Color.up] ∘ Fin.succAbove 0) 0 with
          | Color.up => Lorentz.contrBasis d
          | Color.down => Lorentz.coBasis d).repr
        ((Pure.basisVector (Fin.append ![Color.down] ![Color.up]) b).drop 0 0))
      ν =
  ((Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis).repr
      (toTensor.symm (Pure.basisVector (Fin.append ![Color.down] ![Color.up]) b).toTensor))
    (μ, ν)
    change _ * (Lorentz.contrBasis d).repr (Lorentz.contrBasis d (b 1)) ν = _hd:ℕA:ElectromagneticPotential dhA:Differentiable ℝ A.valx:SpaceTime dμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin db:ComponentIdx (Fin.append ![Color.down] ![Color.up])⊢ ((match Fin.append ![Color.down] ![Color.up] 0 with
          | Color.up => Lorentz.contrBasis d
          | Color.down => Lorentz.coBasis d).repr
        (Pure.basisVector (Fin.append ![Color.down] ![Color.up]) b 0))
      μ *
    ((Lorentz.contrBasis d).repr ((Lorentz.contrBasis d) (b 1))) ν =
  ((Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis).repr
      (toTensor.symm (Pure.basisVector (Fin.append ![Color.down] ![Color.up]) b).toTensor))
    (μ, ν)
    /- Transforming the basis -/
    let e : ComponentIdx (Fin.append ![Color.down] ![Color.up])
      ≃ (Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d) := ComponentIdx.prod.trans <|
      Lorentz.CoVector.indexEquiv.prodCongr Lorentz.Vector.indexEquivhd:ℕA:ElectromagneticPotential dhA:Differentiable ℝ A.valx:SpaceTime dμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin db:ComponentIdx (Fin.append ![Color.down] ![Color.up])e:ComponentIdx (Fin.append ![Color.down] ![Color.up]) ≃ (Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d) := ComponentIdx.prod.trans (Lorentz.CoVector.indexEquiv.prodCongr Lorentz.Vector.indexEquiv)⊢ ((match Fin.append ![Color.down] ![Color.up] 0 with
          | Color.up => Lorentz.contrBasis d
          | Color.down => Lorentz.coBasis d).repr
        (Pure.basisVector (Fin.append ![Color.down] ![Color.up]) b 0))
      μ *
    ((Lorentz.contrBasis d).repr ((Lorentz.contrBasis d) (b 1))) ν =
  ((Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis).repr
      (toTensor.symm (Pure.basisVector (Fin.append ![Color.down] ![Color.up]) b).toTensor))
    (μ, ν)
    have h1 : Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis =
        (((Tensor.basis (Fin.append ![Color.down] ![Color.up]))).map toTensor.symm).reindex e := byd:ℕA:ElectromagneticPotential dhA:Differentiable ℝ A.valx:SpaceTime dμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d⊢ toField ((evalT 0 ν) ((evalT 0 μ) (toTensor (tensorDeriv A.val x)))) = ∂_ μ A.val x νhd:ℕA:ElectromagneticPotential dhA:Differentiable ℝ A.valx:SpaceTime dμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin db:ComponentIdx (Fin.append ![Color.down] ![Color.up])e:ComponentIdx (Fin.append ![Color.down] ![Color.up]) ≃ (Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d) := ComponentIdx.prod.trans (Lorentz.CoVector.indexEquiv.prodCongr Lorentz.Vector.indexEquiv)h1:Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis =
  ((basis (Fin.append ![Color.down] ![Color.up])).map toTensor.symm).reindex e⊢ ((match Fin.append ![Color.down] ![Color.up] 0 with
          | Color.up => Lorentz.contrBasis d
          | Color.down => Lorentz.coBasis d).repr
        (Pure.basisVector (Fin.append ![Color.down] ![Color.up]) b 0))
      μ *
    ((Lorentz.contrBasis d).repr ((Lorentz.contrBasis d) (b 1))) ν =
  ((Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis).repr
      (toTensor.symm (Pure.basisVector (Fin.append ![Color.down] ![Color.up]) b).toTensor))
    (μ, ν)
      ext ⟨i, j⟩d:ℕA:ElectromagneticPotential dhA:Differentiable ℝ A.valx:SpaceTime dμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin db:ComponentIdx (Fin.append ![Color.down] ![Color.up])e:ComponentIdx (Fin.append ![Color.down] ![Color.up]) ≃ (Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d) := ComponentIdx.prod.trans (Lorentz.CoVector.indexEquiv.prodCongr Lorentz.Vector.indexEquiv)i:Fin 1 ⊕ Fin dj:Fin 1 ⊕ Fin d⊢ (Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis) (i, j) =
  (((basis (Fin.append ![Color.down] ![Color.up])).map toTensor.symm).reindex e) (i, j)hd:ℕA:ElectromagneticPotential dhA:Differentiable ℝ A.valx:SpaceTime dμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin db:ComponentIdx (Fin.append ![Color.down] ![Color.up])e:ComponentIdx (Fin.append ![Color.down] ![Color.up]) ≃ (Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d) := ComponentIdx.prod.trans (Lorentz.CoVector.indexEquiv.prodCongr Lorentz.Vector.indexEquiv)h1:Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis =
  ((basis (Fin.append ![Color.down] ![Color.up])).map toTensor.symm).reindex e⊢ ((match Fin.append ![Color.down] ![Color.up] 0 with
          | Color.up => Lorentz.contrBasis d
          | Color.down => Lorentz.coBasis d).repr
        (Pure.basisVector (Fin.append ![Color.down] ![Color.up]) b 0))
      μ *
    ((Lorentz.contrBasis d).repr ((Lorentz.contrBasis d) (b 1))) ν =
  ((Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis).repr
      (toTensor.symm (Pure.basisVector (Fin.append ![Color.down] ![Color.up]) b).toTensor))
    (μ, ν)
      simp_rw [d:ℕA:ElectromagneticPotential dhA:Differentiable ℝ A.valx:SpaceTime dμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin db:ComponentIdx (Fin.append ![Color.down] ![Color.up])e:ComponentIdx (Fin.append ![Color.down] ![Color.up]) ≃ (Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d) := ComponentIdx.prod.trans (Lorentz.CoVector.indexEquiv.prodCongr Lorentz.Vector.indexEquiv)i:Fin 1 ⊕ Fin dj:Fin 1 ⊕ Fin d⊢ (Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis) (i, j) =
  (((basis (Fin.append ![Color.down] ![Color.up])).map toTensor.symm).reindex e) (i, j)hd:ℕA:ElectromagneticPotential dhA:Differentiable ℝ A.valx:SpaceTime dμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin db:ComponentIdx (Fin.append ![Color.down] ![Color.up])e:ComponentIdx (Fin.append ![Color.down] ![Color.up]) ≃ (Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d) := ComponentIdx.prod.trans (Lorentz.CoVector.indexEquiv.prodCongr Lorentz.Vector.indexEquiv)h1:Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis =
  ((basis (Fin.append ![Color.down] ![Color.up])).map toTensor.symm).reindex e⊢ ((match Fin.append ![Color.down] ![Color.up] 0 with
          | Color.up => Lorentz.contrBasis d
          | Color.down => Lorentz.coBasis d).repr
        (Pure.basisVector (Fin.append ![Color.down] ![Color.up]) b 0))
      μ *
    ((Lorentz.contrBasis d).repr ((Lorentz.contrBasis d) (b 1))) ν =
  ((Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis).repr
      (toTensor.symm (Pure.basisVector (Fin.append ![Color.down] ![Color.up]) b).toTensor))
    (μ, ν)Tensorial.basis_map_prod,d:ℕA:ElectromagneticPotential dhA:Differentiable ℝ A.valx:SpaceTime dμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin db:ComponentIdx (Fin.append ![Color.down] ![Color.up])e:ComponentIdx (Fin.append ![Color.down] ![Color.up]) ≃ (Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d) := ComponentIdx.prod.trans (Lorentz.CoVector.indexEquiv.prodCongr Lorentz.Vector.indexEquiv)i:Fin 1 ⊕ Fin dj:Fin 1 ⊕ Fin d⊢ (Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis) (i, j) =
  (((((basis ![Color.down]).map toTensor.symm).tensorProduct ((basis ![Color.up]).map toTensor.symm)).reindex
          ComponentIdx.prod.symm).reindex
      e)
    (i, j)hd:ℕA:ElectromagneticPotential dhA:Differentiable ℝ A.valx:SpaceTime dμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin db:ComponentIdx (Fin.append ![Color.down] ![Color.up])e:ComponentIdx (Fin.append ![Color.down] ![Color.up]) ≃ (Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d) := ComponentIdx.prod.trans (Lorentz.CoVector.indexEquiv.prodCongr Lorentz.Vector.indexEquiv)h1:Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis =
  ((basis (Fin.append ![Color.down] ![Color.up])).map toTensor.symm).reindex e⊢ ((match Fin.append ![Color.down] ![Color.up] 0 with
          | Color.up => Lorentz.contrBasis d
          | Color.down => Lorentz.coBasis d).repr
        (Pure.basisVector (Fin.append ![Color.down] ![Color.up]) b 0))
      μ *
    ((Lorentz.contrBasis d).repr ((Lorentz.contrBasis d) (b 1))) ν =
  ((Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis).repr
      (toTensor.symm (Pure.basisVector (Fin.append ![Color.down] ![Color.up]) b).toTensor))
    (μ, ν) Basis.tensorProduct_apply,d:ℕA:ElectromagneticPotential dhA:Differentiable ℝ A.valx:SpaceTime dμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin db:ComponentIdx (Fin.append ![Color.down] ![Color.up])e:ComponentIdx (Fin.append ![Color.down] ![Color.up]) ≃ (Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d) := ComponentIdx.prod.trans (Lorentz.CoVector.indexEquiv.prodCongr Lorentz.Vector.indexEquiv)i:Fin 1 ⊕ Fin dj:Fin 1 ⊕ Fin d⊢ Lorentz.CoVector.basis i ⊗ₜ[ℝ] Lorentz.Vector.basis j =
  (((((basis ![Color.down]).map toTensor.symm).tensorProduct ((basis ![Color.up]).map toTensor.symm)).reindex
          ComponentIdx.prod.symm).reindex
      e)
    (i, j)hd:ℕA:ElectromagneticPotential dhA:Differentiable ℝ A.valx:SpaceTime dμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin db:ComponentIdx (Fin.append ![Color.down] ![Color.up])e:ComponentIdx (Fin.append ![Color.down] ![Color.up]) ≃ (Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d) := ComponentIdx.prod.trans (Lorentz.CoVector.indexEquiv.prodCongr Lorentz.Vector.indexEquiv)h1:Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis =
  ((basis (Fin.append ![Color.down] ![Color.up])).map toTensor.symm).reindex e⊢ ((match Fin.append ![Color.down] ![Color.up] 0 with
          | Color.up => Lorentz.contrBasis d
          | Color.down => Lorentz.coBasis d).repr
        (Pure.basisVector (Fin.append ![Color.down] ![Color.up]) b 0))
      μ *
    ((Lorentz.contrBasis d).repr ((Lorentz.contrBasis d) (b 1))) ν =
  ((Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis).repr
      (toTensor.symm (Pure.basisVector (Fin.append ![Color.down] ![Color.up]) b).toTensor))
    (μ, ν)
        ← Lorentz.Vector.toTensor_symm_basis,d:ℕA:ElectromagneticPotential dhA:Differentiable ℝ A.valx:SpaceTime dμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin db:ComponentIdx (Fin.append ![Color.down] ![Color.up])e:ComponentIdx (Fin.append ![Color.down] ![Color.up]) ≃ (Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d) := ComponentIdx.prod.trans (Lorentz.CoVector.indexEquiv.prodCongr Lorentz.Vector.indexEquiv)i:Fin 1 ⊕ Fin dj:Fin 1 ⊕ Fin d⊢ Lorentz.CoVector.basis i ⊗ₜ[ℝ] toTensor.symm ((basis ![Color.up]) (Lorentz.Vector.indexEquiv.symm j)) =
  (((((basis ![Color.down]).map toTensor.symm).tensorProduct ((basis ![Color.up]).map toTensor.symm)).reindex
          ComponentIdx.prod.symm).reindex
      e)
    (i, j)hd:ℕA:ElectromagneticPotential dhA:Differentiable ℝ A.valx:SpaceTime dμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin db:ComponentIdx (Fin.append ![Color.down] ![Color.up])e:ComponentIdx (Fin.append ![Color.down] ![Color.up]) ≃ (Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d) := ComponentIdx.prod.trans (Lorentz.CoVector.indexEquiv.prodCongr Lorentz.Vector.indexEquiv)h1:Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis =
  ((basis (Fin.append ![Color.down] ![Color.up])).map toTensor.symm).reindex e⊢ ((match Fin.append ![Color.down] ![Color.up] 0 with
          | Color.up => Lorentz.contrBasis d
          | Color.down => Lorentz.coBasis d).repr
        (Pure.basisVector (Fin.append ![Color.down] ![Color.up]) b 0))
      μ *
    ((Lorentz.contrBasis d).repr ((Lorentz.contrBasis d) (b 1))) ν =
  ((Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis).repr
      (toTensor.symm (Pure.basisVector (Fin.append ![Color.down] ![Color.up]) b).toTensor))
    (μ, ν) ← Lorentz.CoVector.toTensor_symm_basis,d:ℕA:ElectromagneticPotential dhA:Differentiable ℝ A.valx:SpaceTime dμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin db:ComponentIdx (Fin.append ![Color.down] ![Color.up])e:ComponentIdx (Fin.append ![Color.down] ![Color.up]) ≃ (Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d) := ComponentIdx.prod.trans (Lorentz.CoVector.indexEquiv.prodCongr Lorentz.Vector.indexEquiv)i:Fin 1 ⊕ Fin dj:Fin 1 ⊕ Fin d⊢ toTensor.symm ((basis ![Color.down]) (Lorentz.CoVector.indexEquiv.symm i)) ⊗ₜ[ℝ]
    toTensor.symm ((basis ![Color.up]) (Lorentz.Vector.indexEquiv.symm j)) =
  (((((basis ![Color.down]).map toTensor.symm).tensorProduct ((basis ![Color.up]).map toTensor.symm)).reindex
          ComponentIdx.prod.symm).reindex
      e)
    (i, j)hd:ℕA:ElectromagneticPotential dhA:Differentiable ℝ A.valx:SpaceTime dμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin db:ComponentIdx (Fin.append ![Color.down] ![Color.up])e:ComponentIdx (Fin.append ![Color.down] ![Color.up]) ≃ (Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d) := ComponentIdx.prod.trans (Lorentz.CoVector.indexEquiv.prodCongr Lorentz.Vector.indexEquiv)h1:Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis =
  ((basis (Fin.append ![Color.down] ![Color.up])).map toTensor.symm).reindex e⊢ ((match Fin.append ![Color.down] ![Color.up] 0 with
          | Color.up => Lorentz.contrBasis d
          | Color.down => Lorentz.coBasis d).repr
        (Pure.basisVector (Fin.append ![Color.down] ![Color.up]) b 0))
      μ *
    ((Lorentz.contrBasis d).repr ((Lorentz.contrBasis d) (b 1))) ν =
  ((Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis).repr
      (toTensor.symm (Pure.basisVector (Fin.append ![Color.down] ![Color.up]) b).toTensor))
    (μ, ν) ed:ℕA:ElectromagneticPotential dhA:Differentiable ℝ A.valx:SpaceTime dμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin db:ComponentIdx (Fin.append ![Color.down] ![Color.up])e:ComponentIdx (Fin.append ![Color.down] ![Color.up]) ≃ (Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d) := ComponentIdx.prod.trans (Lorentz.CoVector.indexEquiv.prodCongr Lorentz.Vector.indexEquiv)i:Fin 1 ⊕ Fin dj:Fin 1 ⊕ Fin d⊢ toTensor.symm ((basis ![Color.down]) (Lorentz.CoVector.indexEquiv.symm i)) ⊗ₜ[ℝ]
    toTensor.symm ((basis ![Color.up]) (Lorentz.Vector.indexEquiv.symm j)) =
  (((((basis ![Color.down]).map toTensor.symm).tensorProduct ((basis ![Color.up]).map toTensor.symm)).reindex
          ComponentIdx.prod.symm).reindex
      (ComponentIdx.prod.trans (Lorentz.CoVector.indexEquiv.prodCongr Lorentz.Vector.indexEquiv)))
    (i, j)hd:ℕA:ElectromagneticPotential dhA:Differentiable ℝ A.valx:SpaceTime dμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin db:ComponentIdx (Fin.append ![Color.down] ![Color.up])e:ComponentIdx (Fin.append ![Color.down] ![Color.up]) ≃ (Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d) := ComponentIdx.prod.trans (Lorentz.CoVector.indexEquiv.prodCongr Lorentz.Vector.indexEquiv)h1:Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis =
  ((basis (Fin.append ![Color.down] ![Color.up])).map toTensor.symm).reindex e⊢ ((match Fin.append ![Color.down] ![Color.up] 0 with
          | Color.up => Lorentz.contrBasis d
          | Color.down => Lorentz.coBasis d).repr
        (Pure.basisVector (Fin.append ![Color.down] ![Color.up]) b 0))
      μ *
    ((Lorentz.contrBasis d).repr ((Lorentz.contrBasis d) (b 1))) ν =
  ((Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis).repr
      (toTensor.symm (Pure.basisVector (Fin.append ![Color.down] ![Color.up]) b).toTensor))
    (μ, ν)]
      simphd:ℕA:ElectromagneticPotential dhA:Differentiable ℝ A.valx:SpaceTime dμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin db:ComponentIdx (Fin.append ![Color.down] ![Color.up])e:ComponentIdx (Fin.append ![Color.down] ![Color.up]) ≃ (Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d) := ComponentIdx.prod.trans (Lorentz.CoVector.indexEquiv.prodCongr Lorentz.Vector.indexEquiv)h1:Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis =
  ((basis (Fin.append ![Color.down] ![Color.up])).map toTensor.symm).reindex e⊢ ((match Fin.append ![Color.down] ![Color.up] 0 with
          | Color.up => Lorentz.contrBasis d
          | Color.down => Lorentz.coBasis d).repr
        (Pure.basisVector (Fin.append ![Color.down] ![Color.up]) b 0))
      μ *
    ((Lorentz.contrBasis d).repr ((Lorentz.contrBasis d) (b 1))) ν =
  ((Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis).repr
      (toTensor.symm (Pure.basisVector (Fin.append ![Color.down] ![Color.up]) b).toTensor))
    (μ, ν)hd:ℕA:ElectromagneticPotential dhA:Differentiable ℝ A.valx:SpaceTime dμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin db:ComponentIdx (Fin.append ![Color.down] ![Color.up])e:ComponentIdx (Fin.append ![Color.down] ![Color.up]) ≃ (Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d) := ComponentIdx.prod.trans (Lorentz.CoVector.indexEquiv.prodCongr Lorentz.Vector.indexEquiv)h1:Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis =
  ((basis (Fin.append ![Color.down] ![Color.up])).map toTensor.symm).reindex e⊢ ((match Fin.append ![Color.down] ![Color.up] 0 with
          | Color.up => Lorentz.contrBasis d
          | Color.down => Lorentz.coBasis d).repr
        (Pure.basisVector (Fin.append ![Color.down] ![Color.up]) b 0))
      μ *
    ((Lorentz.contrBasis d).repr ((Lorentz.contrBasis d) (b 1))) ν =
  ((Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis).repr
      (toTensor.symm (Pure.basisVector (Fin.append ![Color.down] ![Color.up]) b).toTensor))
    (μ, ν)
    simp [Pure.basisVector, h1, Finsupp.single_apply]hd:ℕA:ElectromagneticPotential dhA:Differentiable ℝ A.valx:SpaceTime dμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin db:ComponentIdx (Fin.append ![Color.down] ![Color.up])e:ComponentIdx (Fin.append ![Color.down] ![Color.up]) ≃ (Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d) := ComponentIdx.prod.trans (Lorentz.CoVector.indexEquiv.prodCongr Lorentz.Vector.indexEquiv)h1:Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis =
  ((basis (Fin.append ![Color.down] ![Color.up])).map toTensor.symm).reindex e⊢ (if b 1 = ν then if b 0 = μ then 1 else 0 else 0) = if b = e.symm (μ, ν) then 1 else 0
    by_cases hμ : b 0 = μposd:ℕA:ElectromagneticPotential dhA:Differentiable ℝ A.valx:SpaceTime dμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin db:ComponentIdx (Fin.append ![Color.down] ![Color.up])e:ComponentIdx (Fin.append ![Color.down] ![Color.up]) ≃ (Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d) := ComponentIdx.prod.trans (Lorentz.CoVector.indexEquiv.prodCongr Lorentz.Vector.indexEquiv)h1:Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis =
  ((basis (Fin.append ![Color.down] ![Color.up])).map toTensor.symm).reindex ehμ:b 0 = μ⊢ (if b 1 = ν then if b 0 = μ then 1 else 0 else 0) = if b = e.symm (μ, ν) then 1 else 0negd:ℕA:ElectromagneticPotential dhA:Differentiable ℝ A.valx:SpaceTime dμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin db:ComponentIdx (Fin.append ![Color.down] ![Color.up])e:ComponentIdx (Fin.append ![Color.down] ![Color.up]) ≃ (Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d) := ComponentIdx.prod.trans (Lorentz.CoVector.indexEquiv.prodCongr Lorentz.Vector.indexEquiv)h1:Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis =
  ((basis (Fin.append ![Color.down] ![Color.up])).map toTensor.symm).reindex ehμ:¬b 0 = μ⊢ (if b 1 = ν then if b 0 = μ then 1 else 0 else 0) = if b = e.symm (μ, ν) then 1 else 0 <;>posd:ℕA:ElectromagneticPotential dhA:Differentiable ℝ A.valx:SpaceTime dμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin db:ComponentIdx (Fin.append ![Color.down] ![Color.up])e:ComponentIdx (Fin.append ![Color.down] ![Color.up]) ≃ (Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d) := ComponentIdx.prod.trans (Lorentz.CoVector.indexEquiv.prodCongr Lorentz.Vector.indexEquiv)h1:Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis =
  ((basis (Fin.append ![Color.down] ![Color.up])).map toTensor.symm).reindex ehμ:b 0 = μ⊢ (if b 1 = ν then if b 0 = μ then 1 else 0 else 0) = if b = e.symm (μ, ν) then 1 else 0negd:ℕA:ElectromagneticPotential dhA:Differentiable ℝ A.valx:SpaceTime dμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin db:ComponentIdx (Fin.append ![Color.down] ![Color.up])e:ComponentIdx (Fin.append ![Color.down] ![Color.up]) ≃ (Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d) := ComponentIdx.prod.trans (Lorentz.CoVector.indexEquiv.prodCongr Lorentz.Vector.indexEquiv)h1:Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis =
  ((basis (Fin.append ![Color.down] ![Color.up])).map toTensor.symm).reindex ehμ:¬b 0 = μ⊢ (if b 1 = ν then if b 0 = μ then 1 else 0 else 0) = if b = e.symm (μ, ν) then 1 else 0 by_cases hν : b 1 = νposd:ℕA:ElectromagneticPotential dhA:Differentiable ℝ A.valx:SpaceTime dμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin db:ComponentIdx (Fin.append ![Color.down] ![Color.up])e:ComponentIdx (Fin.append ![Color.down] ![Color.up]) ≃ (Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d) := ComponentIdx.prod.trans (Lorentz.CoVector.indexEquiv.prodCongr Lorentz.Vector.indexEquiv)h1:Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis =
  ((basis (Fin.append ![Color.down] ![Color.up])).map toTensor.symm).reindex ehμ:¬b 0 = μhν:b 1 = ν⊢ (if b 1 = ν then if b 0 = μ then 1 else 0 else 0) = if b = e.symm (μ, ν) then 1 else 0negd:ℕA:ElectromagneticPotential dhA:Differentiable ℝ A.valx:SpaceTime dμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin db:ComponentIdx (Fin.append ![Color.down] ![Color.up])e:ComponentIdx (Fin.append ![Color.down] ![Color.up]) ≃ (Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d) := ComponentIdx.prod.trans (Lorentz.CoVector.indexEquiv.prodCongr Lorentz.Vector.indexEquiv)h1:Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis =
  ((basis (Fin.append ![Color.down] ![Color.up])).map toTensor.symm).reindex ehμ:¬b 0 = μhν:¬b 1 = ν⊢ (if b 1 = ν then if b 0 = μ then 1 else 0 else 0) = if b = e.symm (μ, ν) then 1 else 0 <;>posd:ℕA:ElectromagneticPotential dhA:Differentiable ℝ A.valx:SpaceTime dμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin db:ComponentIdx (Fin.append ![Color.down] ![Color.up])e:ComponentIdx (Fin.append ![Color.down] ![Color.up]) ≃ (Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d) := ComponentIdx.prod.trans (Lorentz.CoVector.indexEquiv.prodCongr Lorentz.Vector.indexEquiv)h1:Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis =
  ((basis (Fin.append ![Color.down] ![Color.up])).map toTensor.symm).reindex ehμ:b 0 = μhν:b 1 = ν⊢ (if b 1 = ν then if b 0 = μ then 1 else 0 else 0) = if b = e.symm (μ, ν) then 1 else 0negd:ℕA:ElectromagneticPotential dhA:Differentiable ℝ A.valx:SpaceTime dμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin db:ComponentIdx (Fin.append ![Color.down] ![Color.up])e:ComponentIdx (Fin.append ![Color.down] ![Color.up]) ≃ (Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d) := ComponentIdx.prod.trans (Lorentz.CoVector.indexEquiv.prodCongr Lorentz.Vector.indexEquiv)h1:Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis =
  ((basis (Fin.append ![Color.down] ![Color.up])).map toTensor.symm).reindex ehμ:b 0 = μhν:¬b 1 = ν⊢ (if b 1 = ν then if b 0 = μ then 1 else 0 else 0) = if b = e.symm (μ, ν) then 1 else 0posd:ℕA:ElectromagneticPotential dhA:Differentiable ℝ A.valx:SpaceTime dμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin db:ComponentIdx (Fin.append ![Color.down] ![Color.up])e:ComponentIdx (Fin.append ![Color.down] ![Color.up]) ≃ (Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d) := ComponentIdx.prod.trans (Lorentz.CoVector.indexEquiv.prodCongr Lorentz.Vector.indexEquiv)h1:Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis =
  ((basis (Fin.append ![Color.down] ![Color.up])).map toTensor.symm).reindex ehμ:¬b 0 = μhν:b 1 = ν⊢ (if b 1 = ν then if b 0 = μ then 1 else 0 else 0) = if b = e.symm (μ, ν) then 1 else 0negd:ℕA:ElectromagneticPotential dhA:Differentiable ℝ A.valx:SpaceTime dμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin db:ComponentIdx (Fin.append ![Color.down] ![Color.up])e:ComponentIdx (Fin.append ![Color.down] ![Color.up]) ≃ (Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d) := ComponentIdx.prod.trans (Lorentz.CoVector.indexEquiv.prodCongr Lorentz.Vector.indexEquiv)h1:Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis =
  ((basis (Fin.append ![Color.down] ![Color.up])).map toTensor.symm).reindex ehμ:¬b 0 = μhν:¬b 1 = ν⊢ (if b 1 = ν then if b 0 = μ then 1 else 0 else 0) = if b = e.symm (μ, ν) then 1 else 0
    simp_all [Equiv.eq_symm_apply, show e b = (b 0, b 1) from rfl]All goals completed! 🐙
  ·hzerod:ℕA:ElectromagneticPotential dhA:Differentiable ℝ A.valx:SpaceTime dμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d⊢ toField ((evalT 0 ν) ((evalT 0 μ) (toTensor (toTensor.symm 0)))) =
  ((Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis).repr (toTensor.symm 0)) (μ, ν) simp only [map_zero, Finsupp.coe_zero, Pi.zero_apply]All goals completed! 🐙
  ·hsmuld:ℕA:ElectromagneticPotential dhA:Differentiable ℝ A.valx:SpaceTime dμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin da:ℝt:(realLorentzTensor d).Tensor (Fin.append ![Color.down] ![Color.up])h:toField ((evalT 0 ν) ((evalT 0 μ) (toTensor (toTensor.symm t)))) =
  ((Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis).repr (toTensor.symm t)) (μ, ν)⊢ toField ((evalT 0 ν) ((evalT 0 μ) (toTensor (toTensor.symm (a • t))))) =
  ((Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis).repr (toTensor.symm (a • t))) (μ, ν) simp only [map_smul, h, smul_eq_mul, Finsupp.coe_smul, Pi.smul_apply]All goals completed! 🐙
  ·haddd:ℕA:ElectromagneticPotential dhA:Differentiable ℝ A.valx:SpaceTime dμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin dt1:(realLorentzTensor d).Tensor (Fin.append ![Color.down] ![Color.up])t2:(realLorentzTensor d).Tensor (Fin.append ![Color.down] ![Color.up])h1:toField ((evalT 0 ν) ((evalT 0 μ) (toTensor (toTensor.symm t1)))) =
  ((Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis).repr (toTensor.symm t1)) (μ, ν)h2:toField ((evalT 0 ν) ((evalT 0 μ) (toTensor (toTensor.symm t2)))) =
  ((Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis).repr (toTensor.symm t2)) (μ, ν)⊢ toField ((evalT 0 ν) ((evalT 0 μ) (toTensor (toTensor.symm (t1 + t2))))) =
  ((Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis).repr (toTensor.symm (t1 + t2))) (μ, ν) simp only [map_add, h1, h2, Finsupp.coe_add, Pi.add_apply]All goals completed! 🐙

@[simp]
lemma deriv_basis_repr_apply {d} {μν : (Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)}
    (A : ElectromagneticPotential d)
    (x : SpaceTime d) :
    (Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis).repr (deriv A x) μν =
    ∂_ μν.1 A x μν.2 := byd:ℕμν:(Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)A:ElectromagneticPotential dx:SpaceTime d⊢ ((Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis).repr (A.deriv x)) μν = ∂_ μν.1 A.val x μν.2
  rcases μν with ⟨μ, ν⟩d:ℕA:ElectromagneticPotential dx:SpaceTime dμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d⊢ ((Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis).repr (A.deriv x)) (μ, ν) = ∂_ (μ, ν).1 A.val x (μ, ν).2
  simp [deriv, Basis.tensorProduct_repr_tmul_apply, Finsupp.single_apply]All goals completed! 🐙



lemma toTensor_deriv_basis_repr_apply {d} (A : ElectromagneticPotential d)
    (x : SpaceTime d) (b : ComponentIdx (S := realLorentzTensor d)
      (Fin.append ![Color.down] ![Color.up])) :
    (Tensor.basis _).repr (Tensorial.toTensor (deriv A x)) b =
    ∂_ (b 0) A x (b 1) := byd:ℕA:ElectromagneticPotential dx:SpaceTime db:ComponentIdx (Fin.append ![Color.down] ![Color.up])⊢ ((basis (Fin.append ![Color.down] ![Color.up])).repr (toTensor (A.deriv x))) b = ∂_ (b 0) A.val x (b 1)
  rw [Tensorial.basis_toTensor_apply,d:ℕA:ElectromagneticPotential dx:SpaceTime db:ComponentIdx (Fin.append ![Color.down] ![Color.up])⊢ (((basis (Fin.append ![Color.down] ![Color.up])).map toTensor.symm).repr (A.deriv x)) b = ∂_ (b 0) A.val x (b 1)d:ℕA:ElectromagneticPotential dx:SpaceTime db:ComponentIdx (Fin.append ![Color.down] ![Color.up])⊢ (((((basis ![Color.down]).map toTensor.symm).tensorProduct ((basis ![Color.up]).map toTensor.symm)).reindex
          ComponentIdx.prod.symm).repr
      (A.deriv x))
    b =
  ∂_ (b 0) A.val x (b 1) Tensorial.basis_map_prodd:ℕA:ElectromagneticPotential dx:SpaceTime db:ComponentIdx (Fin.append ![Color.down] ![Color.up])⊢ (((((basis ![Color.down]).map toTensor.symm).tensorProduct ((basis ![Color.up]).map toTensor.symm)).reindex
          ComponentIdx.prod.symm).repr
      (A.deriv x))
    b =
  ∂_ (b 0) A.val x (b 1)d:ℕA:ElectromagneticPotential dx:SpaceTime db:ComponentIdx (Fin.append ![Color.down] ![Color.up])⊢ (((((basis ![Color.down]).map toTensor.symm).tensorProduct ((basis ![Color.up]).map toTensor.symm)).reindex
          ComponentIdx.prod.symm).repr
      (A.deriv x))
    b =
  ∂_ (b 0) A.val x (b 1)]d:ℕA:ElectromagneticPotential dx:SpaceTime db:ComponentIdx (Fin.append ![Color.down] ![Color.up])⊢ (((((basis ![Color.down]).map toTensor.symm).tensorProduct ((basis ![Color.up]).map toTensor.symm)).reindex
          ComponentIdx.prod.symm).repr
      (A.deriv x))
    b =
  ∂_ (b 0) A.val x (b 1)
  simp only [Nat.reduceSucc, Nat.reduceAdd, Basis.repr_reindex, Finsupp.mapDomain_equiv_apply,
    Equiv.symm_symm, Fin.isValue]d:ℕA:ElectromagneticPotential dx:SpaceTime db:ComponentIdx (Fin.append ![Color.down] ![Color.up])⊢ ((((basis ![Color.down]).map toTensor.symm).tensorProduct ((basis ![Color.up]).map toTensor.symm)).repr (A.deriv x))
    (ComponentIdx.prod b) =
  ∂_ (b 0) A.val x (b 1)
  rw [Lorentz.Vector.tensor_basis_map_eq_basis_reindex,d:ℕA:ElectromagneticPotential dx:SpaceTime db:ComponentIdx (Fin.append ![Color.down] ![Color.up])⊢ ((((basis ![Color.down]).map toTensor.symm).tensorProduct
          (Lorentz.Vector.basis.reindex Lorentz.Vector.indexEquiv.symm)).repr
      (A.deriv x))
    (ComponentIdx.prod b) =
  ∂_ (b 0) A.val x (b 1)d:ℕA:ElectromagneticPotential dx:SpaceTime db:ComponentIdx (Fin.append ![Color.down] ![Color.up])⊢ (((Lorentz.CoVector.basis.reindex Lorentz.CoVector.indexEquiv.symm).tensorProduct
          (Lorentz.Vector.basis.reindex Lorentz.Vector.indexEquiv.symm)).repr
      (A.deriv x))
    (ComponentIdx.prod b) =
  ∂_ (b 0) A.val x (b 1)
    Lorentz.CoVector.tensor_basis_map_eq_basis_reindexd:ℕA:ElectromagneticPotential dx:SpaceTime db:ComponentIdx (Fin.append ![Color.down] ![Color.up])⊢ (((Lorentz.CoVector.basis.reindex Lorentz.CoVector.indexEquiv.symm).tensorProduct
          (Lorentz.Vector.basis.reindex Lorentz.Vector.indexEquiv.symm)).repr
      (A.deriv x))
    (ComponentIdx.prod b) =
  ∂_ (b 0) A.val x (b 1)d:ℕA:ElectromagneticPotential dx:SpaceTime db:ComponentIdx (Fin.append ![Color.down] ![Color.up])⊢ (((Lorentz.CoVector.basis.reindex Lorentz.CoVector.indexEquiv.symm).tensorProduct
          (Lorentz.Vector.basis.reindex Lorentz.Vector.indexEquiv.symm)).repr
      (A.deriv x))
    (ComponentIdx.prod b) =
  ∂_ (b 0) A.val x (b 1)]d:ℕA:ElectromagneticPotential dx:SpaceTime db:ComponentIdx (Fin.append ![Color.down] ![Color.up])⊢ (((Lorentz.CoVector.basis.reindex Lorentz.CoVector.indexEquiv.symm).tensorProduct
          (Lorentz.Vector.basis.reindex Lorentz.Vector.indexEquiv.symm)).repr
      (A.deriv x))
    (ComponentIdx.prod b) =
  ∂_ (b 0) A.val x (b 1)
  have hb : (((Lorentz.CoVector.basis (d := d)).reindex
      Lorentz.CoVector.indexEquiv.symm).tensorProduct
      (Lorentz.Vector.basis.reindex Lorentz.Vector.indexEquiv.symm)) =
      ((Lorentz.CoVector.basis (d := d)).tensorProduct (Lorentz.Vector.basis (d := d))).reindex
      (Lorentz.CoVector.indexEquiv.symm.prodCongr Lorentz.Vector.indexEquiv.symm) := byd:ℕA:ElectromagneticPotential dx:SpaceTime db:ComponentIdx (Fin.append ![Color.down] ![Color.up])⊢ ((basis (Fin.append ![Color.down] ![Color.up])).repr (toTensor (A.deriv x))) b = ∂_ (b 0) A.val x (b 1)d:ℕA:ElectromagneticPotential dx:SpaceTime db:ComponentIdx (Fin.append ![Color.down] ![Color.up])hb:(Lorentz.CoVector.basis.reindex Lorentz.CoVector.indexEquiv.symm).tensorProduct
    (Lorentz.Vector.basis.reindex Lorentz.Vector.indexEquiv.symm) =
  (Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis).reindex
    (Lorentz.CoVector.indexEquiv.symm.prodCongr Lorentz.Vector.indexEquiv.symm)⊢ (((Lorentz.CoVector.basis.reindex Lorentz.CoVector.indexEquiv.symm).tensorProduct
          (Lorentz.Vector.basis.reindex Lorentz.Vector.indexEquiv.symm)).repr
      (A.deriv x))
    (ComponentIdx.prod b) =
  ∂_ (b 0) A.val x (b 1)
    ext ⟨i, j⟩d:ℕA:ElectromagneticPotential dx:SpaceTime db:ComponentIdx (Fin.append ![Color.down] ![Color.up])i:ComponentIdx ![Color.down]j:ComponentIdx ![Color.up]⊢ ((Lorentz.CoVector.basis.reindex Lorentz.CoVector.indexEquiv.symm).tensorProduct
      (Lorentz.Vector.basis.reindex Lorentz.Vector.indexEquiv.symm))
    (i, j) =
  ((Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis).reindex
      (Lorentz.CoVector.indexEquiv.symm.prodCongr Lorentz.Vector.indexEquiv.symm))
    (i, j)d:ℕA:ElectromagneticPotential dx:SpaceTime db:ComponentIdx (Fin.append ![Color.down] ![Color.up])hb:(Lorentz.CoVector.basis.reindex Lorentz.CoVector.indexEquiv.symm).tensorProduct
    (Lorentz.Vector.basis.reindex Lorentz.Vector.indexEquiv.symm) =
  (Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis).reindex
    (Lorentz.CoVector.indexEquiv.symm.prodCongr Lorentz.Vector.indexEquiv.symm)⊢ (((Lorentz.CoVector.basis.reindex Lorentz.CoVector.indexEquiv.symm).tensorProduct
          (Lorentz.Vector.basis.reindex Lorentz.Vector.indexEquiv.symm)).repr
      (A.deriv x))
    (ComponentIdx.prod b) =
  ∂_ (b 0) A.val x (b 1)
    simpd:ℕA:ElectromagneticPotential dx:SpaceTime db:ComponentIdx (Fin.append ![Color.down] ![Color.up])hb:(Lorentz.CoVector.basis.reindex Lorentz.CoVector.indexEquiv.symm).tensorProduct
    (Lorentz.Vector.basis.reindex Lorentz.Vector.indexEquiv.symm) =
  (Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis).reindex
    (Lorentz.CoVector.indexEquiv.symm.prodCongr Lorentz.Vector.indexEquiv.symm)⊢ (((Lorentz.CoVector.basis.reindex Lorentz.CoVector.indexEquiv.symm).tensorProduct
          (Lorentz.Vector.basis.reindex Lorentz.Vector.indexEquiv.symm)).repr
      (A.deriv x))
    (ComponentIdx.prod b) =
  ∂_ (b 0) A.val x (b 1)d:ℕA:ElectromagneticPotential dx:SpaceTime db:ComponentIdx (Fin.append ![Color.down] ![Color.up])hb:(Lorentz.CoVector.basis.reindex Lorentz.CoVector.indexEquiv.symm).tensorProduct
    (Lorentz.Vector.basis.reindex Lorentz.Vector.indexEquiv.symm) =
  (Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis).reindex
    (Lorentz.CoVector.indexEquiv.symm.prodCongr Lorentz.Vector.indexEquiv.symm)⊢ (((Lorentz.CoVector.basis.reindex Lorentz.CoVector.indexEquiv.symm).tensorProduct
          (Lorentz.Vector.basis.reindex Lorentz.Vector.indexEquiv.symm)).repr
      (A.deriv x))
    (ComponentIdx.prod b) =
  ∂_ (b 0) A.val x (b 1)
  rw [hb,d:ℕA:ElectromagneticPotential dx:SpaceTime db:ComponentIdx (Fin.append ![Color.down] ![Color.up])hb:(Lorentz.CoVector.basis.reindex Lorentz.CoVector.indexEquiv.symm).tensorProduct
    (Lorentz.Vector.basis.reindex Lorentz.Vector.indexEquiv.symm) =
  (Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis).reindex
    (Lorentz.CoVector.indexEquiv.symm.prodCongr Lorentz.Vector.indexEquiv.symm)⊢ (((Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis).reindex
          (Lorentz.CoVector.indexEquiv.symm.prodCongr Lorentz.Vector.indexEquiv.symm)).repr
      (A.deriv x))
    (ComponentIdx.prod b) =
  ∂_ (b 0) A.val x (b 1)d:ℕA:ElectromagneticPotential dx:SpaceTime db:ComponentIdx (Fin.append ![Color.down] ![Color.up])hb:(Lorentz.CoVector.basis.reindex Lorentz.CoVector.indexEquiv.symm).tensorProduct
    (Lorentz.Vector.basis.reindex Lorentz.Vector.indexEquiv.symm) =
  (Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis).reindex
    (Lorentz.CoVector.indexEquiv.symm.prodCongr Lorentz.Vector.indexEquiv.symm)⊢ ∂_ ((Lorentz.CoVector.indexEquiv.symm.prodCongr Lorentz.Vector.indexEquiv.symm).symm (ComponentIdx.prod b)).1 A.val x
    ((Lorentz.CoVector.indexEquiv.symm.prodCongr Lorentz.Vector.indexEquiv.symm).symm (ComponentIdx.prod b)).2 =
  ∂_ (b 0) A.val x (b 1) Module.Basis.repr_reindex_apply,d:ℕA:ElectromagneticPotential dx:SpaceTime db:ComponentIdx (Fin.append ![Color.down] ![Color.up])hb:(Lorentz.CoVector.basis.reindex Lorentz.CoVector.indexEquiv.symm).tensorProduct
    (Lorentz.Vector.basis.reindex Lorentz.Vector.indexEquiv.symm) =
  (Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis).reindex
    (Lorentz.CoVector.indexEquiv.symm.prodCongr Lorentz.Vector.indexEquiv.symm)⊢ ((Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis).repr (A.deriv x))
    ((Lorentz.CoVector.indexEquiv.symm.prodCongr Lorentz.Vector.indexEquiv.symm).symm (ComponentIdx.prod b)) =
  ∂_ (b 0) A.val x (b 1)d:ℕA:ElectromagneticPotential dx:SpaceTime db:ComponentIdx (Fin.append ![Color.down] ![Color.up])hb:(Lorentz.CoVector.basis.reindex Lorentz.CoVector.indexEquiv.symm).tensorProduct
    (Lorentz.Vector.basis.reindex Lorentz.Vector.indexEquiv.symm) =
  (Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis).reindex
    (Lorentz.CoVector.indexEquiv.symm.prodCongr Lorentz.Vector.indexEquiv.symm)⊢ ∂_ ((Lorentz.CoVector.indexEquiv.symm.prodCongr Lorentz.Vector.indexEquiv.symm).symm (ComponentIdx.prod b)).1 A.val x
    ((Lorentz.CoVector.indexEquiv.symm.prodCongr Lorentz.Vector.indexEquiv.symm).symm (ComponentIdx.prod b)).2 =
  ∂_ (b 0) A.val x (b 1) deriv_basis_repr_applyd:ℕA:ElectromagneticPotential dx:SpaceTime db:ComponentIdx (Fin.append ![Color.down] ![Color.up])hb:(Lorentz.CoVector.basis.reindex Lorentz.CoVector.indexEquiv.symm).tensorProduct
    (Lorentz.Vector.basis.reindex Lorentz.Vector.indexEquiv.symm) =
  (Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis).reindex
    (Lorentz.CoVector.indexEquiv.symm.prodCongr Lorentz.Vector.indexEquiv.symm)⊢ ∂_ ((Lorentz.CoVector.indexEquiv.symm.prodCongr Lorentz.Vector.indexEquiv.symm).symm (ComponentIdx.prod b)).1 A.val x
    ((Lorentz.CoVector.indexEquiv.symm.prodCongr Lorentz.Vector.indexEquiv.symm).symm (ComponentIdx.prod b)).2 =
  ∂_ (b 0) A.val x (b 1)d:ℕA:ElectromagneticPotential dx:SpaceTime db:ComponentIdx (Fin.append ![Color.down] ![Color.up])hb:(Lorentz.CoVector.basis.reindex Lorentz.CoVector.indexEquiv.symm).tensorProduct
    (Lorentz.Vector.basis.reindex Lorentz.Vector.indexEquiv.symm) =
  (Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis).reindex
    (Lorentz.CoVector.indexEquiv.symm.prodCongr Lorentz.Vector.indexEquiv.symm)⊢ ∂_ ((Lorentz.CoVector.indexEquiv.symm.prodCongr Lorentz.Vector.indexEquiv.symm).symm (ComponentIdx.prod b)).1 A.val x
    ((Lorentz.CoVector.indexEquiv.symm.prodCongr Lorentz.Vector.indexEquiv.symm).symm (ComponentIdx.prod b)).2 =
  ∂_ (b 0) A.val x (b 1)]d:ℕA:ElectromagneticPotential dx:SpaceTime db:ComponentIdx (Fin.append ![Color.down] ![Color.up])hb:(Lorentz.CoVector.basis.reindex Lorentz.CoVector.indexEquiv.symm).tensorProduct
    (Lorentz.Vector.basis.reindex Lorentz.Vector.indexEquiv.symm) =
  (Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis).reindex
    (Lorentz.CoVector.indexEquiv.symm.prodCongr Lorentz.Vector.indexEquiv.symm)⊢ ∂_ ((Lorentz.CoVector.indexEquiv.symm.prodCongr Lorentz.Vector.indexEquiv.symm).symm (ComponentIdx.prod b)).1 A.val x
    ((Lorentz.CoVector.indexEquiv.symm.prodCongr Lorentz.Vector.indexEquiv.symm).symm (ComponentIdx.prod b)).2 =
  ∂_ (b 0) A.val x (b 1)
  rflAll goals completed! 🐙