Physlib.Electromagnetism.Distributional.Basic

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.SpaceAndTime.TimeAndSpace.ConstantTimeDist
public import Physlib.Mathematics.VariationalCalculus.HasVarAdjDeriv
public import Physlib.SpaceAndTime.Space.DistOfFunction
public import Physlib.SpaceAndTime.SpaceTime.TimeSlice

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 distribution from spacetime to contravariant Lorentz vectors.

ii. Key results

DistElectromagneticPotential : the type of electromagnetic potentials as distributions.

iii. Table of contents

A. The electromagnetic potential as a distribution

A.1. Constructors

A.2. The derivative of the electromagnetic potential as a distribution

A.3. The derivative 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 as a distribution

attribute [-simp] Fintype.sum_sum_typeattribute [-simp] Nat.succ_eq_add_one

A.1. Constructors

              @[simp]
lemma ofStaticScalarPotentialFunction_of_isDistBounded {d} (c : SpeedOfLight)
    (φ : Space d → ℝ) (hφ : Space.IsDistBounded φ) :
    ofStaticScalarPotentialFunction c φ =
      ofStaticScalarPotential c (Space.distOfFunction φ hφ) := byd:ℕc:SpeedOfLightφ:Space d → ℝhφ:Space.IsDistBounded φ⊢ ofStaticScalarPotentialFunction c φ = (ofStaticScalarPotential c) (Space.distOfFunction φ hφ)
  classical
  simp [ofStaticScalarPotentialFunction, hφ]All goals completed! 🐙@[simp]
lemma ofStaticScalarPotentialFunction_eq_zero_of_not_isDistBounded {d}
    (c : SpeedOfLight) (φ : Space d → ℝ) (hφ : ¬ Space.IsDistBounded φ) :
    ofStaticScalarPotentialFunction c φ = 0 := byd:ℕc:SpeedOfLightφ:Space d → ℝhφ:¬Space.IsDistBounded φ⊢ ofStaticScalarPotentialFunction c φ = 0
  classical
  simp [ofStaticScalarPotentialFunction, hφ]All goals completed! 🐙TODO "Add a constructor for DistElectromagneticPotential from electric and
  magnetic fields."

A.2. The derivative of the electromagnetic potential as a distribution



lemma distTensorDeriv_eq_sum_sum {d} (A : DistElectromagneticPotential d)
    (ε : 𝓢(SpaceTime d, ℝ)) :
    distTensorDeriv A ε =∑ μ, ∑ ν, (SpaceTime.distDeriv μ A ε ν) •
      Lorentz.CoVector.basis μ ⊗ₜ[ℝ] Lorentz.Vector.basis ν := byd:ℕA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)⊢ (distTensorDeriv A) ε = ∑ μ, ∑ ν, ((distDeriv μ) A) ε ν • Lorentz.CoVector.basis μ ⊗ₜ[ℝ] Lorentz.Vector.basis ν
  simp [distTensorDeriv_apply]d:ℕA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)⊢ ∑ μ, Lorentz.CoVector.basis μ ⊗ₜ[ℝ] ((distDeriv μ) A) ε =
  ∑ μ, ∑ ν, ((distDeriv μ) A) ε ν • Lorentz.CoVector.basis μ ⊗ₜ[ℝ] Lorentz.Vector.basis ν
  congre_fd:ℕA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)⊢ (fun μ => Lorentz.CoVector.basis μ ⊗ₜ[ℝ] ((distDeriv μ) A) ε) = fun μ =>
  ∑ ν, ((distDeriv μ) A) ε ν • Lorentz.CoVector.basis μ ⊗ₜ[ℝ] Lorentz.Vector.basis ν
  funext μe_fd:ℕA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)μ:Fin 1 ⊕ Fin d⊢ Lorentz.CoVector.basis μ ⊗ₜ[ℝ] ((distDeriv μ) A) ε =
  ∑ ν, ((distDeriv μ) A) ε ν • Lorentz.CoVector.basis μ ⊗ₜ[ℝ] Lorentz.Vector.basis ν
  conv_lhs => rw [← Lorentz.Vector.basis.sum_repr (SpaceTime.distDeriv μ A ε)]d:ℕA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)μ:Fin 1 ⊕ Fin d| Lorentz.CoVector.basis μ ⊗ₜ[ℝ] ∑ i, (Lorentz.Vector.basis.repr (((distDeriv μ) A) ε)) i • Lorentz.Vector.basis i
  rw [tmul_sume_fd:ℕA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)μ:Fin 1 ⊕ Fin d⊢ ∑ a, Lorentz.CoVector.basis μ ⊗ₜ[ℝ] ((Lorentz.Vector.basis.repr (((distDeriv μ) A) ε)) a • Lorentz.Vector.basis a) =
  ∑ ν, ((distDeriv μ) A) ε ν • Lorentz.CoVector.basis μ ⊗ₜ[ℝ] Lorentz.Vector.basis νe_fd:ℕA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)μ:Fin 1 ⊕ Fin d⊢ ∑ a, Lorentz.CoVector.basis μ ⊗ₜ[ℝ] ((Lorentz.Vector.basis.repr (((distDeriv μ) A) ε)) a • Lorentz.Vector.basis a) =
  ∑ ν, ((distDeriv μ) A) ε ν • Lorentz.CoVector.basis μ ⊗ₜ[ℝ] Lorentz.Vector.basis ν]e_fd:ℕA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)μ:Fin 1 ⊕ Fin d⊢ ∑ a, Lorentz.CoVector.basis μ ⊗ₜ[ℝ] ((Lorentz.Vector.basis.repr (((distDeriv μ) A) ε)) a • Lorentz.Vector.basis a) =
  ∑ ν, ((distDeriv μ) A) ε ν • Lorentz.CoVector.basis μ ⊗ₜ[ℝ] Lorentz.Vector.basis ν
  congre_f.e_fd:ℕA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)μ:Fin 1 ⊕ Fin d⊢ (fun a =>
    Lorentz.CoVector.basis μ ⊗ₜ[ℝ] ((Lorentz.Vector.basis.repr (((distDeriv μ) A) ε)) a • Lorentz.Vector.basis a)) =
  fun ν => ((distDeriv μ) A) ε ν • Lorentz.CoVector.basis μ ⊗ₜ[ℝ] Lorentz.Vector.basis ν
  funext νe_f.e_fd:ℕA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)μ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d⊢ Lorentz.CoVector.basis μ ⊗ₜ[ℝ] ((Lorentz.Vector.basis.repr (((distDeriv μ) A) ε)) ν • Lorentz.Vector.basis ν) =
  ((distDeriv μ) A) ε ν • Lorentz.CoVector.basis μ ⊗ₜ[ℝ] Lorentz.Vector.basis ν
  simpe_f.e_fd:ℕA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)μ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d⊢ (Lorentz.Vector.basis.repr (((distDeriv μ) A) ε)) ν • Lorentz.CoVector.basis μ ⊗ₜ[ℝ] Lorentz.Vector.basis ν =
  ((distDeriv μ) A) ε ν • Lorentz.CoVector.basis μ ⊗ₜ[ℝ] Lorentz.Vector.basis ν
  rflAll goals completed! 🐙

A.3. The derivative in terms of the basis



@[simp]
lemma distTensorDeriv_basis_repr_apply {d} {μν : (Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)}
    (A : DistElectromagneticPotential d)
    (ε : 𝓢(SpaceTime d, ℝ)) :
    (Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis).repr (distTensorDeriv A ε) μν =
    distDeriv μν.1 A ε μν.2 := byd:ℕμν:(Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)A:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)⊢ ((Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis).repr ((distTensorDeriv A) ε)) μν =
  ((distDeriv μν.1) A) ε μν.2
  match μν with
  | (μ, ν) =>d:ℕμν:(Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)A:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)μ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d⊢ ((Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis).repr ((distTensorDeriv A) ε)) (μ, ν) =
  ((distDeriv (μ, ν).1) A) ε (μ, ν).2
  rw [distTensorDeriv_eq_sum_sumd:ℕμν:(Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)A:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)μ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d⊢ ((Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis).repr
      (∑ μ, ∑ ν, ((distDeriv μ) A) ε ν • Lorentz.CoVector.basis μ ⊗ₜ[ℝ] Lorentz.Vector.basis ν))
    (μ, ν) =
  ((distDeriv (μ, ν).1) A) ε (μ, ν).2d:ℕμν:(Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)A:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)μ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d⊢ ((Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis).repr
      (∑ μ, ∑ ν, ((distDeriv μ) A) ε ν • Lorentz.CoVector.basis μ ⊗ₜ[ℝ] Lorentz.Vector.basis ν))
    (μ, ν) =
  ((distDeriv (μ, ν).1) A) ε (μ, ν).2]d:ℕμν:(Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)A:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)μ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d⊢ ((Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis).repr
      (∑ μ, ∑ ν, ((distDeriv μ) A) ε ν • Lorentz.CoVector.basis μ ⊗ₜ[ℝ] Lorentz.Vector.basis ν))
    (μ, ν) =
  ((distDeriv (μ, ν).1) A) ε (μ, ν).2
  simp only [map_sum, map_smul, Finsupp.coe_finsetSum, Finsupp.coe_smul, Finset.sum_apply,
    Pi.smul_apply, Basis.tensorProduct_repr_tmul_apply, Basis.repr_self, smul_eq_mul]d:ℕμν:(Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)A:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)μ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d⊢ ∑ x, ∑ x_1, ((distDeriv x) A) ε x_1 * ((Finsupp.single x_1 1) ν * (Finsupp.single x 1) μ) = ((distDeriv μ) A) ε ν
  rw [Finset.sum_eq_single μ,d:ℕμν:(Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)A:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)μ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d⊢ ∑ x, ((distDeriv μ) A) ε x * ((Finsupp.single x 1) ν * (Finsupp.single μ 1) μ) = ((distDeriv μ) A) ε νh₀d:ℕμν:(Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)A:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)μ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d⊢ ∀ b ∈ Finset.univ, b ≠ μ → ∑ x, ((distDeriv b) A) ε x * ((Finsupp.single x 1) ν * (Finsupp.single b 1) μ) = 0h₁d:ℕμν:(Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)A:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)μ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d⊢ μ ∉ Finset.univ → ∑ x, ((distDeriv μ) A) ε x * ((Finsupp.single x 1) ν * (Finsupp.single μ 1) μ) = 0d:ℕμν:(Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)A:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)μ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d⊢ ((distDeriv μ) A) ε ν * ((Finsupp.single ν 1) ν * (Finsupp.single μ 1) μ) = ((distDeriv μ) A) ε νh₀d:ℕμν:(Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)A:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)μ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d⊢ ∀ b ∈ Finset.univ, b ≠ ν → ((distDeriv μ) A) ε b * ((Finsupp.single b 1) ν * (Finsupp.single μ 1) μ) = 0h₁d:ℕμν:(Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)A:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)μ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d⊢ ν ∉ Finset.univ → ((distDeriv μ) A) ε ν * ((Finsupp.single ν 1) ν * (Finsupp.single μ 1) μ) = 0h₀d:ℕμν:(Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)A:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)μ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d⊢ ∀ b ∈ Finset.univ, b ≠ μ → ∑ x, ((distDeriv b) A) ε x * ((Finsupp.single x 1) ν * (Finsupp.single b 1) μ) = 0h₁d:ℕμν:(Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)A:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)μ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d⊢ μ ∉ Finset.univ → ∑ x, ((distDeriv μ) A) ε x * ((Finsupp.single x 1) ν * (Finsupp.single μ 1) μ) = 0 Finset.sum_eq_single νd:ℕμν:(Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)A:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)μ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d⊢ ((distDeriv μ) A) ε ν * ((Finsupp.single ν 1) ν * (Finsupp.single μ 1) μ) = ((distDeriv μ) A) ε νh₀d:ℕμν:(Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)A:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)μ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d⊢ ∀ b ∈ Finset.univ, b ≠ ν → ((distDeriv μ) A) ε b * ((Finsupp.single b 1) ν * (Finsupp.single μ 1) μ) = 0h₁d:ℕμν:(Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)A:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)μ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d⊢ ν ∉ Finset.univ → ((distDeriv μ) A) ε ν * ((Finsupp.single ν 1) ν * (Finsupp.single μ 1) μ) = 0h₀d:ℕμν:(Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)A:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)μ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d⊢ ∀ b ∈ Finset.univ, b ≠ μ → ∑ x, ((distDeriv b) A) ε x * ((Finsupp.single x 1) ν * (Finsupp.single b 1) μ) = 0h₁d:ℕμν:(Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)A:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)μ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d⊢ μ ∉ Finset.univ → ∑ x, ((distDeriv μ) A) ε x * ((Finsupp.single x 1) ν * (Finsupp.single μ 1) μ) = 0d:ℕμν:(Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)A:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)μ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d⊢ ((distDeriv μ) A) ε ν * ((Finsupp.single ν 1) ν * (Finsupp.single μ 1) μ) = ((distDeriv μ) A) ε νh₀d:ℕμν:(Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)A:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)μ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d⊢ ∀ b ∈ Finset.univ, b ≠ ν → ((distDeriv μ) A) ε b * ((Finsupp.single b 1) ν * (Finsupp.single μ 1) μ) = 0h₁d:ℕμν:(Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)A:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)μ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d⊢ ν ∉ Finset.univ → ((distDeriv μ) A) ε ν * ((Finsupp.single ν 1) ν * (Finsupp.single μ 1) μ) = 0h₀d:ℕμν:(Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)A:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)μ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d⊢ ∀ b ∈ Finset.univ, b ≠ μ → ∑ x, ((distDeriv b) A) ε x * ((Finsupp.single x 1) ν * (Finsupp.single b 1) μ) = 0h₁d:ℕμν:(Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)A:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)μ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d⊢ μ ∉ Finset.univ → ∑ x, ((distDeriv μ) A) ε x * ((Finsupp.single x 1) ν * (Finsupp.single μ 1) μ) = 0]d:ℕμν:(Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)A:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)μ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d⊢ ((distDeriv μ) A) ε ν * ((Finsupp.single ν 1) ν * (Finsupp.single μ 1) μ) = ((distDeriv μ) A) ε νh₀d:ℕμν:(Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)A:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)μ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d⊢ ∀ b ∈ Finset.univ, b ≠ ν → ((distDeriv μ) A) ε b * ((Finsupp.single b 1) ν * (Finsupp.single μ 1) μ) = 0h₁d:ℕμν:(Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)A:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)μ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d⊢ ν ∉ Finset.univ → ((distDeriv μ) A) ε ν * ((Finsupp.single ν 1) ν * (Finsupp.single μ 1) μ) = 0h₀d:ℕμν:(Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)A:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)μ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d⊢ ∀ b ∈ Finset.univ, b ≠ μ → ∑ x, ((distDeriv b) A) ε x * ((Finsupp.single x 1) ν * (Finsupp.single b 1) μ) = 0h₁d:ℕμν:(Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)A:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)μ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d⊢ μ ∉ Finset.univ → ∑ x, ((distDeriv μ) A) ε x * ((Finsupp.single x 1) ν * (Finsupp.single μ 1) μ) = 0
  ·d:ℕμν:(Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)A:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)μ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d⊢ ((distDeriv μ) A) ε ν * ((Finsupp.single ν 1) ν * (Finsupp.single μ 1) μ) = ((distDeriv μ) A) ε ν simpAll goals completed! 🐙
  ·h₀d:ℕμν:(Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)A:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)μ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d⊢ ∀ b ∈ Finset.univ, b ≠ ν → ((distDeriv μ) A) ε b * ((Finsupp.single b 1) ν * (Finsupp.single μ 1) μ) = 0 intro μ' _ hh₀d:ℕμν:(Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)A:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)μ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin dμ':Fin 1 ⊕ Fin da✝:μ' ∈ Finset.univh:μ' ≠ ν⊢ ((distDeriv μ) A) ε μ' * ((Finsupp.single μ' 1) ν * (Finsupp.single μ 1) μ) = 0
    simp [h]All goals completed! 🐙
  ·h₁d:ℕμν:(Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)A:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)μ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d⊢ ν ∉ Finset.univ → ((distDeriv μ) A) ε ν * ((Finsupp.single ν 1) ν * (Finsupp.single μ 1) μ) = 0 simpAll goals completed! 🐙
  ·h₀d:ℕμν:(Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)A:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)μ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d⊢ ∀ b ∈ Finset.univ, b ≠ μ → ∑ x, ((distDeriv b) A) ε x * ((Finsupp.single x 1) ν * (Finsupp.single b 1) μ) = 0 intro ν' _ hh₀d:ℕμν:(Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)A:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)μ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin dν':Fin 1 ⊕ Fin da✝:ν' ∈ Finset.univh:ν' ≠ μ⊢ ∑ x, ((distDeriv ν') A) ε x * ((Finsupp.single x 1) ν * (Finsupp.single ν' 1) μ) = 0
    simp [h]All goals completed! 🐙
  ·h₁d:ℕμν:(Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)A:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)μ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d⊢ μ ∉ Finset.univ → ∑ x, ((distDeriv μ) A) ε x * ((Finsupp.single x 1) ν * (Finsupp.single μ 1) μ) = 0 simpAll goals completed! 🐙



lemma toTensor_distTensorDeriv_basis_repr_apply {d} (A : DistElectromagneticPotential d)
    (ε : 𝓢(SpaceTime d, ℝ)) (b : ComponentIdx (S := realLorentzTensor d)
      (Fin.append ![Color.down] ![Color.up])) :
    (Tensor.basis _).repr (Tensorial.toTensor (distTensorDeriv A ε)) b =
    distDeriv (b 0) A ε (b 1) := byd:ℕA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)b:ComponentIdx (Fin.append ![Color.down] ![Color.up])⊢ ((basis (Fin.append ![Color.down] ![Color.up])).repr (Tensorial.toTensor ((distTensorDeriv A) ε))) b =
  ((distDeriv (b 0)) A) ε (b 1)
  rw [Tensorial.basis_toTensor_applyd:ℕA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)b:ComponentIdx (Fin.append ![Color.down] ![Color.up])⊢ (((basis (Fin.append ![Color.down] ![Color.up])).map Tensorial.toTensor.symm).repr ((distTensorDeriv A) ε)) b =
  ((distDeriv (b 0)) A) ε (b 1)d:ℕA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)b:ComponentIdx (Fin.append ![Color.down] ![Color.up])⊢ (((basis (Fin.append ![Color.down] ![Color.up])).map Tensorial.toTensor.symm).repr ((distTensorDeriv A) ε)) b =
  ((distDeriv (b 0)) A) ε (b 1)]d:ℕA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)b:ComponentIdx (Fin.append ![Color.down] ![Color.up])⊢ (((basis (Fin.append ![Color.down] ![Color.up])).map Tensorial.toTensor.symm).repr ((distTensorDeriv A) ε)) b =
  ((distDeriv (b 0)) A) ε (b 1)
  rw [Tensorial.basis_map_prodd:ℕA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)b:ComponentIdx (Fin.append ![Color.down] ![Color.up])⊢ (((((basis ![Color.down]).map Tensorial.toTensor.symm).tensorProduct
              ((basis ![Color.up]).map Tensorial.toTensor.symm)).reindex
          ComponentIdx.prod.symm).repr
      ((distTensorDeriv A) ε))
    b =
  ((distDeriv (b 0)) A) ε (b 1)d:ℕA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)b:ComponentIdx (Fin.append ![Color.down] ![Color.up])⊢ (((((basis ![Color.down]).map Tensorial.toTensor.symm).tensorProduct
              ((basis ![Color.up]).map Tensorial.toTensor.symm)).reindex
          ComponentIdx.prod.symm).repr
      ((distTensorDeriv A) ε))
    b =
  ((distDeriv (b 0)) A) ε (b 1)]d:ℕA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)b:ComponentIdx (Fin.append ![Color.down] ![Color.up])⊢ (((((basis ![Color.down]).map Tensorial.toTensor.symm).tensorProduct
              ((basis ![Color.up]).map Tensorial.toTensor.symm)).reindex
          ComponentIdx.prod.symm).repr
      ((distTensorDeriv A) ε))
    b =
  ((distDeriv (b 0)) A) ε (b 1)
  simp only [Nat.reduceSucc, Nat.reduceAdd, Basis.repr_reindex, Finsupp.mapDomain_equiv_apply,
    Equiv.symm_symm, Fin.isValue]d:ℕA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)b:ComponentIdx (Fin.append ![Color.down] ![Color.up])⊢ ((((basis ![Color.down]).map Tensorial.toTensor.symm).tensorProduct
          ((basis ![Color.up]).map Tensorial.toTensor.symm)).repr
      ((distTensorDeriv A) ε))
    (ComponentIdx.prod b) =
  ((distDeriv (b 0)) A) ε (b 1)
  rw [Lorentz.Vector.tensor_basis_map_eq_basis_reindex,d:ℕA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)b:ComponentIdx (Fin.append ![Color.down] ![Color.up])⊢ ((((basis ![Color.down]).map Tensorial.toTensor.symm).tensorProduct
          (Lorentz.Vector.basis.reindex Lorentz.Vector.indexEquiv.symm)).repr
      ((distTensorDeriv A) ε))
    (ComponentIdx.prod b) =
  ((distDeriv (b 0)) A) ε (b 1)d:ℕA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)b: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
      ((distTensorDeriv A) ε))
    (ComponentIdx.prod b) =
  ((distDeriv (b 0)) A) ε (b 1)
    Lorentz.CoVector.tensor_basis_map_eq_basis_reindexd:ℕA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)b: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
      ((distTensorDeriv A) ε))
    (ComponentIdx.prod b) =
  ((distDeriv (b 0)) A) ε (b 1)d:ℕA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)b: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
      ((distTensorDeriv A) ε))
    (ComponentIdx.prod b) =
  ((distDeriv (b 0)) A) ε (b 1)]d:ℕA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)b: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
      ((distTensorDeriv A) ε))
    (ComponentIdx.prod b) =
  ((distDeriv (b 0)) A) ε (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:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)b:ComponentIdx (Fin.append ![Color.down] ![Color.up])⊢ ((basis (Fin.append ![Color.down] ![Color.up])).repr (Tensorial.toTensor ((distTensorDeriv A) ε))) b =
  ((distDeriv (b 0)) A) ε (b 1)d:ℕA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)b: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
      ((distTensorDeriv A) ε))
    (ComponentIdx.prod b) =
  ((distDeriv (b 0)) A) ε (b 1)
    ext bd:ℕA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)b✝:ComponentIdx (Fin.append ![Color.down] ![Color.up])b:ComponentIdx ![Color.down] × ComponentIdx ![Color.up]⊢ ((Lorentz.CoVector.basis.reindex Lorentz.CoVector.indexEquiv.symm).tensorProduct
      (Lorentz.Vector.basis.reindex Lorentz.Vector.indexEquiv.symm))
    b =
  ((Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis).reindex
      (Lorentz.CoVector.indexEquiv.symm.prodCongr Lorentz.Vector.indexEquiv.symm))
    bd:ℕA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)b: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
      ((distTensorDeriv A) ε))
    (ComponentIdx.prod b) =
  ((distDeriv (b 0)) A) ε (b 1)
    match b with
    | ⟨i, j⟩ =>d:ℕA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)b✝:ComponentIdx (Fin.append ![Color.down] ![Color.up])b:ComponentIdx ![Color.down] × ComponentIdx ![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:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)b: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
      ((distTensorDeriv A) ε))
    (ComponentIdx.prod b) =
  ((distDeriv (b 0)) A) ε (b 1)
    simpd:ℕA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)b: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
      ((distTensorDeriv A) ε))
    (ComponentIdx.prod b) =
  ((distDeriv (b 0)) A) ε (b 1)d:ℕA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)b: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
      ((distTensorDeriv A) ε))
    (ComponentIdx.prod b) =
  ((distDeriv (b 0)) A) ε (b 1)
  rw [hbd:ℕA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)b: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
      ((distTensorDeriv A) ε))
    (ComponentIdx.prod b) =
  ((distDeriv (b 0)) A) ε (b 1)d:ℕA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)b: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
      ((distTensorDeriv A) ε))
    (ComponentIdx.prod b) =
  ((distDeriv (b 0)) A) ε (b 1)]d:ℕA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)b: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
      ((distTensorDeriv A) ε))
    (ComponentIdx.prod b) =
  ((distDeriv (b 0)) A) ε (b 1)
  rw [Module.Basis.repr_reindex_apply,d:ℕA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)b: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 ((distTensorDeriv A) ε))
    ((Lorentz.CoVector.indexEquiv.symm.prodCongr Lorentz.Vector.indexEquiv.symm).symm (ComponentIdx.prod b)) =
  ((distDeriv (b 0)) A) ε (b 1)d:ℕA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)b: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)⊢ ((distDeriv ((Lorentz.CoVector.indexEquiv.symm.prodCongr Lorentz.Vector.indexEquiv.symm).symm (ComponentIdx.prod b)).1)
      A)
    ε ((Lorentz.CoVector.indexEquiv.symm.prodCongr Lorentz.Vector.indexEquiv.symm).symm (ComponentIdx.prod b)).2 =
  ((distDeriv (b 0)) A) ε (b 1) distTensorDeriv_basis_repr_applyd:ℕA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)b: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)⊢ ((distDeriv ((Lorentz.CoVector.indexEquiv.symm.prodCongr Lorentz.Vector.indexEquiv.symm).symm (ComponentIdx.prod b)).1)
      A)
    ε ((Lorentz.CoVector.indexEquiv.symm.prodCongr Lorentz.Vector.indexEquiv.symm).symm (ComponentIdx.prod b)).2 =
  ((distDeriv (b 0)) A) ε (b 1)d:ℕA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)b: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)⊢ ((distDeriv ((Lorentz.CoVector.indexEquiv.symm.prodCongr Lorentz.Vector.indexEquiv.symm).symm (ComponentIdx.prod b)).1)
      A)
    ε ((Lorentz.CoVector.indexEquiv.symm.prodCongr Lorentz.Vector.indexEquiv.symm).symm (ComponentIdx.prod b)).2 =
  ((distDeriv (b 0)) A) ε (b 1)]d:ℕA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)b: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)⊢ ((distDeriv ((Lorentz.CoVector.indexEquiv.symm.prodCongr Lorentz.Vector.indexEquiv.symm).symm (ComponentIdx.prod b)).1)
      A)
    ε ((Lorentz.CoVector.indexEquiv.symm.prodCongr Lorentz.Vector.indexEquiv.symm).symm (ComponentIdx.prod b)).2 =
  ((distDeriv (b 0)) A) ε (b 1)
  rflAll goals completed! 🐙