Physlib.Electromagnetism.Kinematics.VectorPotential

Imports

/-
Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
module

public import Physlib.Electromagnetism.Kinematics.EMPotential
public import Mathlib.Algebra.Order.Archimedean.Real.Hom

The vector Potential

i. Overview

The electromagnetic potential is given by A = (1/c φ, \vec A) where φ is the scalar potential and \vec A is the vector potential.

In this module we define the vector potential, and prove lemmas about it.

Since A is relativistic it is a function of SpaceTime d, whilst the vector potential is non-relativistic and is therefore a function of Time and Space d.

ii. Key results

ElectromagneticPotential.vectorPotential : The vector potential from an electromagnetic potential.

iii. Table of contents

A. Definition of the Vector Potential

B. Smoothness of the vector potential

C. Differentiablity of the vector potential

iv. References

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

A. Definition of the Vector Potential

B. Relation to constructors

              @[simp]
lemma ofScalarPotential_vectorPotential {d} (c : SpeedOfLight)
    (φ : Time → Space d → ℝ) : (ofScalarPotential c φ).vectorPotential c = 0 := byd:ℕc:SpeedOfLightφ:Time → Space d → ℝ⊢ vectorPotential c (ofScalarPotential c φ) = 0
  simp only [vectorPotential, ofScalarPotential]d:ℕc:SpeedOfLightφ:Time → Space d → ℝ⊢ ((timeSlice c) fun x => WithLp.toLp 2 fun val => 0) = 0
  rflAll goals completed! 🐙@[simp]
lemma ofStaticScalarPotential_vectorPotential {d} (c : SpeedOfLight)
    (φ : Space d → ℝ) : (ofStaticScalarPotential c φ).vectorPotential c = 0 := byd:ℕc:SpeedOfLightφ:Space d → ℝ⊢ vectorPotential c (ofStaticScalarPotential c φ) = 0
  simp [ofStaticScalarPotential]All goals completed! 🐙@[simp]
lemma ofVectorPotential_vectorPotential {d} (c : SpeedOfLight)
    (A : Time → Space d → EuclideanSpace ℝ (Fin d)) :
    (ofVectorPotential c A).vectorPotential c = A := byd:ℕc:SpeedOfLightA:Time → Space d → EuclideanSpace ℝ (Fin d)⊢ vectorPotential c (ofVectorPotential c A) = A
  ext id:ℕc:SpeedOfLightA:Time → Space d → EuclideanSpace ℝ (Fin d)i:Timex✝:Space di✝:Fin d⊢ (vectorPotential c (ofVectorPotential c A) i x✝).ofLp i✝ = (A i x✝).ofLp i✝
  simp [vectorPotential, ofVectorPotential]All goals completed! 🐙@[simp]
lemma ofStaticVectorPotential_vectorPotential {d} (c : SpeedOfLight)
    (A : Space d → EuclideanSpace ℝ (Fin d)) :
    (ofStaticVectorPotential c A).vectorPotential c = fun _ => A := byd:ℕc:SpeedOfLightA:Space d → EuclideanSpace ℝ (Fin d)⊢ vectorPotential c (ofStaticVectorPotential c A) = fun x => A
  simp [ofStaticVectorPotential]All goals completed! 🐙@[simp]
lemma ofPotentials_vectorPotential {d} (c : SpeedOfLight) (φ : Time → Space d → ℝ)
    (A : Time → Space d → EuclideanSpace ℝ (Fin d)) :
    (ofPotentials c φ A).vectorPotential c = A := byd:ℕc:SpeedOfLightφ:Time → Space d → ℝA:Time → Space d → EuclideanSpace ℝ (Fin d)⊢ vectorPotential c (ofPotentials c φ A) = A
  ext id:ℕc:SpeedOfLightφ:Time → Space d → ℝA:Time → Space d → EuclideanSpace ℝ (Fin d)i:Timex✝:Space di✝:Fin d⊢ (vectorPotential c (ofPotentials c φ A) i x✝).ofLp i✝ = (A i x✝).ofLp i✝
  simp [vectorPotential, ofPotentials]All goals completed! 🐙@[simp]
lemma ofStaticPotentials_vectorPotential {d} (c : SpeedOfLight) (φ : Space d → ℝ)
    (A : Space d → EuclideanSpace ℝ (Fin d)) :
    (ofStaticPotentials c φ A).vectorPotential c = fun _ => A := byd:ℕc:SpeedOfLightφ:Space d → ℝA:Space d → EuclideanSpace ℝ (Fin d)⊢ vectorPotential c (ofStaticPotentials c φ A) = fun x => A
  simp [ofStaticPotentials_eq_ofPotentials]All goals completed! 🐙

B.1. ofElectromagneticField


lemma vectorPotential_inner_radial_eq_zero_ofElectromagneticField
    {c : SpeedOfLight} {E B : Time → Space 3 → EuclideanSpace ℝ (Fin 3)}
    {t : Time} {x : Space 3} {a : ℝ} (hB : Continuous ↿B) :
    ⟪(ofElectromagneticField c E B).vectorPotential c t (a • x), Space.basis.repr x⟫_ℝ = 0 := byc:SpeedOfLightE:Time → Space → EuclideanSpace ℝ (Fin 3)B:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacea:ℝhB:Continuous ↿B⊢ ⟪vectorPotential c (ofElectromagneticField c E B) t (a • x), Space.basis.repr x⟫_ℝ = 0
  rw [real_inner_commc:SpeedOfLightE:Time → Space → EuclideanSpace ℝ (Fin 3)B:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacea:ℝhB:Continuous ↿B⊢ ⟪Space.basis.repr x, vectorPotential c (ofElectromagneticField c E B) t (a • x)⟫_ℝ = 0c:SpeedOfLightE:Time → Space → EuclideanSpace ℝ (Fin 3)B:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacea:ℝhB:Continuous ↿B⊢ ⟪Space.basis.repr x, vectorPotential c (ofElectromagneticField c E B) t (a • x)⟫_ℝ = 0]c:SpeedOfLightE:Time → Space → EuclideanSpace ℝ (Fin 3)B:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacea:ℝhB:Continuous ↿B⊢ ⟪Space.basis.repr x, vectorPotential c (ofElectromagneticField c E B) t (a • x)⟫_ℝ = 0
  rw [PiLp.inner_applyc:SpeedOfLightE:Time → Space → EuclideanSpace ℝ (Fin 3)B:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacea:ℝhB:Continuous ↿B⊢ ∑ i, ⟪(Space.basis.repr x).ofLp i, (vectorPotential c (ofElectromagneticField c E B) t (a • x)).ofLp i⟫_ℝ = 0c:SpeedOfLightE:Time → Space → EuclideanSpace ℝ (Fin 3)B:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacea:ℝhB:Continuous ↿B⊢ ∑ i, ⟪(Space.basis.repr x).ofLp i, (vectorPotential c (ofElectromagneticField c E B) t (a • x)).ofLp i⟫_ℝ = 0]c:SpeedOfLightE:Time → Space → EuclideanSpace ℝ (Fin 3)B:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacea:ℝhB:Continuous ↿B⊢ ∑ i, ⟪(Space.basis.repr x).ofLp i, (vectorPotential c (ofElectromagneticField c E B) t (a • x)).ofLp i⟫_ℝ = 0
  have h1 (a b : ℝ) : ⟪a, b⟫_ℝ = b * a:= byc:SpeedOfLightE:Time → Space → EuclideanSpace ℝ (Fin 3)B:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacea:ℝhB:Continuous ↿B⊢ ⟪vectorPotential c (ofElectromagneticField c E B) t (a • x), Space.basis.repr x⟫_ℝ = 0c:SpeedOfLightE:Time → Space → EuclideanSpace ℝ (Fin 3)B:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacea:ℝhB:Continuous ↿Bh1:∀ (a b : ℝ), ⟪a, b⟫_ℝ = b * a⊢ ∑ i, ⟪(Space.basis.repr x).ofLp i, (vectorPotential c (ofElectromagneticField c E B) t (a • x)).ofLp i⟫_ℝ = 0 rflc:SpeedOfLightE:Time → Space → EuclideanSpace ℝ (Fin 3)B:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacea:ℝhB:Continuous ↿Bh1:∀ (a b : ℝ), ⟪a, b⟫_ℝ = b * a⊢ ∑ i, ⟪(Space.basis.repr x).ofLp i, (vectorPotential c (ofElectromagneticField c E B) t (a • x)).ofLp i⟫_ℝ = 0c:SpeedOfLightE:Time → Space → EuclideanSpace ℝ (Fin 3)B:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacea:ℝhB:Continuous ↿Bh1:∀ (a b : ℝ), ⟪a, b⟫_ℝ = b * a⊢ ∑ i, ⟪(Space.basis.repr x).ofLp i, (vectorPotential c (ofElectromagneticField c E B) t (a • x)).ofLp i⟫_ℝ = 0
  simp only [Space.basis_repr_apply, ofElectromagneticField_vectorPotential_apply_eq_expand hB,
    Fin.isValue, Space.smul_apply, h1, Fin.sum_univ_three, zero_add, Fin.reduceAdd]c:SpeedOfLightE:Time → Space → EuclideanSpace ℝ (Fin 3)B:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacea:ℝhB:Continuous ↿Bh1:∀ (a b : ℝ), ⟪a, b⟫_ℝ = b * a⊢ ((a * x.val 3 2 * ∫ (u : ℝ) in 0..1, u * (B t (u • a • x)).ofLp 1) -
          a * x.val 3 1 * ∫ (u : ℝ) in 0..1, u * (B t (u • a • x)).ofLp 2) *
        x.val 3 0 +
      ((a * x.val 3 0 * ∫ (u : ℝ) in 0..1, u * (B t (u • a • x)).ofLp 2) -
          a * x.val 3 2 * ∫ (u : ℝ) in 0..1, u * (B t (u • a • x)).ofLp 0) *
        x.val 3 1 +
    ((a * x.val 3 1 * ∫ (u : ℝ) in 0..1, u * (B t (u • a • x)).ofLp 0) -
        a * x.val 3 0 * ∫ (u : ℝ) in 0..1, u * (B t (u • a • x)).ofLp 1) *
      x.val 3 2 =
  0
  ringAll goals completed! 🐙


@[simp]
lemma time_deriv_vectorPotential_inner_radial_eq_zero_ofElectromagneticField
    {c : SpeedOfLight} {E B : Time → Space 3 → EuclideanSpace ℝ (Fin 3)}
    {t : Time} {x : Space 3} {a : ℝ} (hB : ContDiff ℝ 1 ↿B) :
    ⟪∂ₜ ((ofElectromagneticField c E B).vectorPotential c · (a • x)) t,
      Space.basis.repr x⟫_ℝ = 0 := byc:SpeedOfLightE:Time → Space → EuclideanSpace ℝ (Fin 3)B:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacea:ℝhB:ContDiff ℝ 1 ↿B⊢ ⟪∂ₜ (fun x_1 => vectorPotential c (ofElectromagneticField c E B) x_1 (a • x)) t, Space.basis.repr x⟫_ℝ = 0
  trans ∂ₜ (fun t => ⟪(ofElectromagneticField c E B).vectorPotential c t (a • x),
    Space.basis.repr x⟫_ℝ) tc:SpeedOfLightE:Time → Space → EuclideanSpace ℝ (Fin 3)B:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacea:ℝhB:ContDiff ℝ 1 ↿B⊢ ⟪∂ₜ (fun x_1 => vectorPotential c (ofElectromagneticField c E B) x_1 (a • x)) t, Space.basis.repr x⟫_ℝ =
  ∂ₜ (fun t => ⟪vectorPotential c (ofElectromagneticField c E B) t (a • x), Space.basis.repr x⟫_ℝ) tc:SpeedOfLightE:Time → Space → EuclideanSpace ℝ (Fin 3)B:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacea:ℝhB:ContDiff ℝ 1 ↿B⊢ ∂ₜ (fun t => ⟪vectorPotential c (ofElectromagneticField c E B) t (a • x), Space.basis.repr x⟫_ℝ) t = 0
  ·c:SpeedOfLightE:Time → Space → EuclideanSpace ℝ (Fin 3)B:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacea:ℝhB:ContDiff ℝ 1 ↿B⊢ ⟪∂ₜ (fun x_1 => vectorPotential c (ofElectromagneticField c E B) x_1 (a • x)) t, Space.basis.repr x⟫_ℝ =
  ∂ₜ (fun t => ⟪vectorPotential c (ofElectromagneticField c E B) t (a • x), Space.basis.repr x⟫_ℝ) t rw [Time.deriv,c:SpeedOfLightE:Time → Space → EuclideanSpace ℝ (Fin 3)B:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacea:ℝhB:ContDiff ℝ 1 ↿B⊢ ⟪(fderiv ℝ (fun x_1 => vectorPotential c (ofElectromagneticField c E B) x_1 (a • x)) t) 1, Space.basis.repr x⟫_ℝ =
  ∂ₜ (fun t => ⟪vectorPotential c (ofElectromagneticField c E B) t (a • x), Space.basis.repr x⟫_ℝ) tc:SpeedOfLightE:Time → Space → EuclideanSpace ℝ (Fin 3)B:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacea:ℝhB:ContDiff ℝ 1 ↿B⊢ ⟪(fderiv ℝ (fun x_1 => vectorPotential c (ofElectromagneticField c E B) x_1 (a • x)) t) 1, Space.basis.repr x⟫_ℝ =
  (fderiv ℝ (fun t => ⟪vectorPotential c (ofElectromagneticField c E B) t (a • x), Space.basis.repr x⟫_ℝ) t) 1 Time.derivc:SpeedOfLightE:Time → Space → EuclideanSpace ℝ (Fin 3)B:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacea:ℝhB:ContDiff ℝ 1 ↿B⊢ ⟪(fderiv ℝ (fun x_1 => vectorPotential c (ofElectromagneticField c E B) x_1 (a • x)) t) 1, Space.basis.repr x⟫_ℝ =
  (fderiv ℝ (fun t => ⟪vectorPotential c (ofElectromagneticField c E B) t (a • x), Space.basis.repr x⟫_ℝ) t) 1c:SpeedOfLightE:Time → Space → EuclideanSpace ℝ (Fin 3)B:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacea:ℝhB:ContDiff ℝ 1 ↿B⊢ ⟪(fderiv ℝ (fun x_1 => vectorPotential c (ofElectromagneticField c E B) x_1 (a • x)) t) 1, Space.basis.repr x⟫_ℝ =
  (fderiv ℝ (fun t => ⟪vectorPotential c (ofElectromagneticField c E B) t (a • x), Space.basis.repr x⟫_ℝ) t) 1]c:SpeedOfLightE:Time → Space → EuclideanSpace ℝ (Fin 3)B:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacea:ℝhB:ContDiff ℝ 1 ↿B⊢ ⟪(fderiv ℝ (fun x_1 => vectorPotential c (ofElectromagneticField c E B) x_1 (a • x)) t) 1, Space.basis.repr x⟫_ℝ =
  (fderiv ℝ (fun t => ⟪vectorPotential c (ofElectromagneticField c E B) t (a • x), Space.basis.repr x⟫_ℝ) t) 1
    rw [fderiv_inner_applyc:SpeedOfLightE:Time → Space → EuclideanSpace ℝ (Fin 3)B:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacea:ℝhB:ContDiff ℝ 1 ↿B⊢ ⟪(fderiv ℝ (fun x_1 => vectorPotential c (ofElectromagneticField c E B) x_1 (a • x)) t) 1, Space.basis.repr x⟫_ℝ =
  ⟪vectorPotential c (ofElectromagneticField c E B) t (a • x), (fderiv ℝ (fun t => Space.basis.repr x) t) 1⟫_ℝ +
    ⟪(fderiv ℝ (fun t => vectorPotential c (ofElectromagneticField c E B) t (a • x)) t) 1, Space.basis.repr x⟫_ℝhfc:SpeedOfLightE:Time → Space → EuclideanSpace ℝ (Fin 3)B:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacea:ℝhB:ContDiff ℝ 1 ↿B⊢ DifferentiableAt ℝ (fun t => vectorPotential c (ofElectromagneticField c E B) t (a • x)) thgc:SpeedOfLightE:Time → Space → EuclideanSpace ℝ (Fin 3)B:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacea:ℝhB:ContDiff ℝ 1 ↿B⊢ DifferentiableAt ℝ (fun t => Space.basis.repr x) tc:SpeedOfLightE:Time → Space → EuclideanSpace ℝ (Fin 3)B:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacea:ℝhB:ContDiff ℝ 1 ↿B⊢ ⟪(fderiv ℝ (fun x_1 => vectorPotential c (ofElectromagneticField c E B) x_1 (a • x)) t) 1, Space.basis.repr x⟫_ℝ =
  ⟪vectorPotential c (ofElectromagneticField c E B) t (a • x), (fderiv ℝ (fun t => Space.basis.repr x) t) 1⟫_ℝ +
    ⟪(fderiv ℝ (fun t => vectorPotential c (ofElectromagneticField c E B) t (a • x)) t) 1, Space.basis.repr x⟫_ℝhfc:SpeedOfLightE:Time → Space → EuclideanSpace ℝ (Fin 3)B:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacea:ℝhB:ContDiff ℝ 1 ↿B⊢ DifferentiableAt ℝ (fun t => vectorPotential c (ofElectromagneticField c E B) t (a • x)) thgc:SpeedOfLightE:Time → Space → EuclideanSpace ℝ (Fin 3)B:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacea:ℝhB:ContDiff ℝ 1 ↿B⊢ DifferentiableAt ℝ (fun t => Space.basis.repr x) t]c:SpeedOfLightE:Time → Space → EuclideanSpace ℝ (Fin 3)B:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacea:ℝhB:ContDiff ℝ 1 ↿B⊢ ⟪(fderiv ℝ (fun x_1 => vectorPotential c (ofElectromagneticField c E B) x_1 (a • x)) t) 1, Space.basis.repr x⟫_ℝ =
  ⟪vectorPotential c (ofElectromagneticField c E B) t (a • x), (fderiv ℝ (fun t => Space.basis.repr x) t) 1⟫_ℝ +
    ⟪(fderiv ℝ (fun t => vectorPotential c (ofElectromagneticField c E B) t (a • x)) t) 1, Space.basis.repr x⟫_ℝhfc:SpeedOfLightE:Time → Space → EuclideanSpace ℝ (Fin 3)B:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacea:ℝhB:ContDiff ℝ 1 ↿B⊢ DifferentiableAt ℝ (fun t => vectorPotential c (ofElectromagneticField c E B) t (a • x)) thgc:SpeedOfLightE:Time → Space → EuclideanSpace ℝ (Fin 3)B:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacea:ℝhB:ContDiff ℝ 1 ↿B⊢ DifferentiableAt ℝ (fun t => Space.basis.repr x) t
    simp only [fderiv_fun_const, Pi.zero_apply, _root_.zero_apply, inner_zero_right,
      zero_add]hfc:SpeedOfLightE:Time → Space → EuclideanSpace ℝ (Fin 3)B:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacea:ℝhB:ContDiff ℝ 1 ↿B⊢ DifferentiableAt ℝ (fun t => vectorPotential c (ofElectromagneticField c E B) t (a • x)) thgc:SpeedOfLightE:Time → Space → EuclideanSpace ℝ (Fin 3)B:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacea:ℝhB:ContDiff ℝ 1 ↿B⊢ DifferentiableAt ℝ (fun t => Space.basis.repr x) t
    apply Differentiable.differentiableAthfc:SpeedOfLightE:Time → Space → EuclideanSpace ℝ (Fin 3)B:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacea:ℝhB:ContDiff ℝ 1 ↿B⊢ Differentiable ℝ fun t => vectorPotential c (ofElectromagneticField c E B) t (a • x)hgc:SpeedOfLightE:Time → Space → EuclideanSpace ℝ (Fin 3)B:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacea:ℝhB:ContDiff ℝ 1 ↿B⊢ DifferentiableAt ℝ (fun t => Space.basis.repr x) t
    fun_prophgc:SpeedOfLightE:Time → Space → EuclideanSpace ℝ (Fin 3)B:Time → Space → EuclideanSpace ℝ (Fin 3)t:Timex:Spacea:ℝhB:ContDiff ℝ 1 ↿B⊢ DifferentiableAt ℝ (fun t => Space.basis.repr x) t
    fun_propAll goals completed! 🐙
  conv_lhs =>
    enter [1, t]c:SpeedOfLightE:Time → Space → EuclideanSpace ℝ (Fin 3)B:Time → Space → EuclideanSpace ℝ (Fin 3)t✝:Timex:Spacea:ℝhB:ContDiff ℝ 1 ↿Bt:Time| ⟪vectorPotential c (ofElectromagneticField c E B) t (a • x), Space.basis.repr x⟫_ℝ
    rw [vectorPotential_inner_radial_eq_zero_ofElectromagneticField (byc:SpeedOfLightE:Time → Space → EuclideanSpace ℝ (Fin 3)B:Time → Space → EuclideanSpace ℝ (Fin 3)t✝:Timex:Spacea:ℝhB:ContDiff ℝ 1 ↿Bt:Time⊢ Continuous ↿B fun_propAll goals completed! 🐙)]
  simpAll goals completed! 🐙

B. Smoothness of the vector potential

We prove various lemmas about the smoothness of the vector potential from the smoothness of the electromagnetic potential.

              

@[fun_prop]
lemma vectorPotential_contDiff {n} {d} {c : SpeedOfLight} (A : ElectromagneticPotential d)
    (hA : ContDiff ℝ n A) : ContDiff ℝ n ↿(A.vectorPotential c) := byn:WithTop ℕ∞d:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:ContDiff ℝ n A.val⊢ ContDiff ℝ n ↿(vectorPotential c A)
  simp [vectorPotential]n:WithTop ℕ∞d:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:ContDiff ℝ n A.val⊢ ContDiff ℝ n ↿((timeSlice c) fun x => WithLp.toLp 2 fun i => A.val x (Sum.inr i))
  apply timeSlice_contDiffn:WithTop ℕ∞d:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:ContDiff ℝ n A.val⊢ ContDiff ℝ n fun x => WithLp.toLp 2 fun i => A.val x (Sum.inr i)
  refine contDiff_euclidean.mpr ?_n:WithTop ℕ∞d:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:ContDiff ℝ n A.val⊢ ∀ (i : Fin d), ContDiff ℝ n fun x => (WithLp.toLp 2 fun i => A.val x (Sum.inr i)).ofLp i
  have h1 : ∀ i, ContDiff ℝ n (fun x => A x i) := byn:WithTop ℕ∞d:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:ContDiff ℝ n A.val⊢ ContDiff ℝ n ↿(vectorPotential c A)n:WithTop ℕ∞d:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:ContDiff ℝ n A.valh1:∀ (i : Fin 1 ⊕ Fin d), ContDiff ℝ n fun x => A.val x i⊢ ∀ (i : Fin d), ContDiff ℝ n fun x => (WithLp.toLp 2 fun i => A.val x (Sum.inr i)).ofLp i
    rw [SpaceTime.contDiff_vectorn:WithTop ℕ∞d:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:ContDiff ℝ n A.val⊢ ContDiff ℝ n A.valn:WithTop ℕ∞d:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:ContDiff ℝ n A.val⊢ ContDiff ℝ n A.valn:WithTop ℕ∞d:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:ContDiff ℝ n A.valh1:∀ (i : Fin 1 ⊕ Fin d), ContDiff ℝ n fun x => A.val x i⊢ ∀ (i : Fin d), ContDiff ℝ n fun x => (WithLp.toLp 2 fun i => A.val x (Sum.inr i)).ofLp i]n:WithTop ℕ∞d:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:ContDiff ℝ n A.val⊢ ContDiff ℝ n A.valn:WithTop ℕ∞d:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:ContDiff ℝ n A.valh1:∀ (i : Fin 1 ⊕ Fin d), ContDiff ℝ n fun x => A.val x i⊢ ∀ (i : Fin d), ContDiff ℝ n fun x => (WithLp.toLp 2 fun i => A.val x (Sum.inr i)).ofLp i
    exact hAn:WithTop ℕ∞d:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:ContDiff ℝ n A.valh1:∀ (i : Fin 1 ⊕ Fin d), ContDiff ℝ n fun x => A.val x i⊢ ∀ (i : Fin d), ContDiff ℝ n fun x => (WithLp.toLp 2 fun i => A.val x (Sum.inr i)).ofLp in:WithTop ℕ∞d:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:ContDiff ℝ n A.valh1:∀ (i : Fin 1 ⊕ Fin d), ContDiff ℝ n fun x => A.val x i⊢ ∀ (i : Fin d), ContDiff ℝ n fun x => (WithLp.toLp 2 fun i => A.val x (Sum.inr i)).ofLp i
  exact fun i => h1 (Sum.inr i)All goals completed! 🐙@[fun_prop]
lemma vectorPotential_contDiff_of_smooth {n : ℕ} {d} {c : SpeedOfLight}
    (A : ElectromagneticPotential d) (hA : ContDiff ℝ ∞ A) :
    ContDiff ℝ n ↿(A.vectorPotential c) := byn:ℕd:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.val⊢ ContDiff ℝ ↑n ↿(vectorPotential c A)
  apply vectorPotential_contDiffn:ℕd:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.val⊢ ContDiff ℝ (↑n) A.val
  exact hA.of_le (ENat.LEInfty.out)All goals completed! 🐙lemma vectorPotential_apply_contDiff {n} {d} {c : SpeedOfLight} (A : ElectromagneticPotential d)
    (hA : ContDiff ℝ n A) (i : Fin d) : ContDiff ℝ n ↿(fun t x => A.vectorPotential c t x i) := byn:ℕ∞ωd:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:ContDiff ℝ n A.vali:Fin d⊢ ContDiff ℝ n ↿fun t x => (vectorPotential c A t x).ofLp i
  change ContDiff ℝ n (EuclideanSpace.proj i ∘ ↿(A.vectorPotential c))n:ℕ∞ωd:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:ContDiff ℝ n A.vali:Fin d⊢ ContDiff ℝ n (⇑(EuclideanSpace.proj i) ∘ ↿(vectorPotential c A))
  refine ContDiff.comp ?_ ?_refine_1n:ℕ∞ωd:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:ContDiff ℝ n A.vali:Fin d⊢ ContDiff ℝ n ⇑(EuclideanSpace.proj i)refine_2n:ℕ∞ωd:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:ContDiff ℝ n A.vali:Fin d⊢ ContDiff ℝ n ↿(vectorPotential c A)
  ·refine_1n:ℕ∞ωd:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:ContDiff ℝ n A.vali:Fin d⊢ ContDiff ℝ n ⇑(EuclideanSpace.proj i) exact ContinuousLinearMap.contDiff (𝕜 := ℝ) (n := n) (EuclideanSpace.proj i)All goals completed! 🐙
  ·refine_2n:ℕ∞ωd:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:ContDiff ℝ n A.vali:Fin d⊢ ContDiff ℝ n ↿(vectorPotential c A) exact vectorPotential_contDiff A hAAll goals completed! 🐙lemma vectorPotential_comp_contDiff {n} {d} {c : SpeedOfLight} (A : ElectromagneticPotential d)
    (hA : ContDiff ℝ n A) (i : Fin d) : ContDiff ℝ n ↿(fun t x => A.vectorPotential c t x i) := byn:ℕ∞ωd:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:ContDiff ℝ n A.vali:Fin d⊢ ContDiff ℝ n ↿fun t x => (vectorPotential c A t x).ofLp i
  change ContDiff ℝ n (EuclideanSpace.proj i ∘ ↿(A.vectorPotential c))n:ℕ∞ωd:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:ContDiff ℝ n A.vali:Fin d⊢ ContDiff ℝ n (⇑(EuclideanSpace.proj i) ∘ ↿(vectorPotential c A))
  refine ContDiff.comp ?_ ?_refine_1n:ℕ∞ωd:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:ContDiff ℝ n A.vali:Fin d⊢ ContDiff ℝ n ⇑(EuclideanSpace.proj i)refine_2n:ℕ∞ωd:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:ContDiff ℝ n A.vali:Fin d⊢ ContDiff ℝ n ↿(vectorPotential c A)
  ·refine_1n:ℕ∞ωd:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:ContDiff ℝ n A.vali:Fin d⊢ ContDiff ℝ n ⇑(EuclideanSpace.proj i) exact ContinuousLinearMap.contDiff (𝕜 := ℝ) (n := n) (EuclideanSpace.proj i)All goals completed! 🐙
  ·refine_2n:ℕ∞ωd:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:ContDiff ℝ n A.vali:Fin d⊢ ContDiff ℝ n ↿(vectorPotential c A) exact vectorPotential_contDiff A hAAll goals completed! 🐙lemma vectorPotential_contDiff_space {n} {d} {c : SpeedOfLight} (A : ElectromagneticPotential d)
    (hA : ContDiff ℝ n A) (t : Time) : ContDiff ℝ n (A.vectorPotential c t) := byn:ℕ∞ωd:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:ContDiff ℝ n A.valt:Time⊢ ContDiff ℝ n (vectorPotential c A t)
  change ContDiff ℝ n (↿(A.vectorPotential c) ∘ fun x => (t, x))n:ℕ∞ωd:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:ContDiff ℝ n A.valt:Time⊢ ContDiff ℝ n (↿(vectorPotential c A) ∘ fun x => (t, x))
  refine ContDiff.comp ?_ ?_refine_1n:ℕ∞ωd:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:ContDiff ℝ n A.valt:Time⊢ ContDiff ℝ n ↿(vectorPotential c A)refine_2n:ℕ∞ωd:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:ContDiff ℝ n A.valt:Time⊢ ContDiff ℝ n fun x => (t, x)
  ·refine_1n:ℕ∞ωd:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:ContDiff ℝ n A.valt:Time⊢ ContDiff ℝ n ↿(vectorPotential c A) exact vectorPotential_contDiff A hAAll goals completed! 🐙
  ·refine_2n:ℕ∞ωd:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:ContDiff ℝ n A.valt:Time⊢ ContDiff ℝ n fun x => (t, x) fun_propAll goals completed! 🐙lemma vectorPotential_apply_contDiff_space {n} {d} {c : SpeedOfLight}
    (A : ElectromagneticPotential d)
    (hA : ContDiff ℝ n A) (t : Time) (i : Fin d) :
    ContDiff ℝ n (fun x => A.vectorPotential c t x i) := byn:ℕ∞ωd:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:ContDiff ℝ n A.valt:Timei:Fin d⊢ ContDiff ℝ n fun x => (vectorPotential c A t x).ofLp i
  change ContDiff ℝ n (EuclideanSpace.proj i ∘ (↿(A.vectorPotential c) ∘ fun x => (t, x)))n:ℕ∞ωd:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:ContDiff ℝ n A.valt:Timei:Fin d⊢ ContDiff ℝ n (⇑(EuclideanSpace.proj i) ∘ ↿(vectorPotential c A) ∘ fun x => (t, x))
  refine ContDiff.comp ?_ ?_refine_1n:ℕ∞ωd:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:ContDiff ℝ n A.valt:Timei:Fin d⊢ ContDiff ℝ n ⇑(EuclideanSpace.proj i)refine_2n:ℕ∞ωd:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:ContDiff ℝ n A.valt:Timei:Fin d⊢ ContDiff ℝ n (↿(vectorPotential c A) ∘ fun x => (t, x))
  ·refine_1n:ℕ∞ωd:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:ContDiff ℝ n A.valt:Timei:Fin d⊢ ContDiff ℝ n ⇑(EuclideanSpace.proj i) exact ContinuousLinearMap.contDiff (𝕜 := ℝ) (n := n) (EuclideanSpace.proj i)All goals completed! 🐙
  ·refine_2n:ℕ∞ωd:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:ContDiff ℝ n A.valt:Timei:Fin d⊢ ContDiff ℝ n (↿(vectorPotential c A) ∘ fun x => (t, x)) exact vectorPotential_contDiff_space A hA tAll goals completed! 🐙lemma vectorPotential_contDiff_time {n} {d} {c : SpeedOfLight} (A : ElectromagneticPotential d)
    (hA : ContDiff ℝ n A) (x : Space d) : ContDiff ℝ n (A.vectorPotential c · x) := byn:ℕ∞ωd:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:ContDiff ℝ n A.valx:Space d⊢ ContDiff ℝ n fun x_1 => vectorPotential c A x_1 x
  change ContDiff ℝ n (↿(A.vectorPotential c) ∘ fun t => (t, x))n:ℕ∞ωd:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:ContDiff ℝ n A.valx:Space d⊢ ContDiff ℝ n (↿(vectorPotential c A) ∘ fun t => (t, x))
  refine ContDiff.comp ?_ ?_refine_1n:ℕ∞ωd:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:ContDiff ℝ n A.valx:Space d⊢ ContDiff ℝ n ↿(vectorPotential c A)refine_2n:ℕ∞ωd:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:ContDiff ℝ n A.valx:Space d⊢ ContDiff ℝ n fun t => (t, x)
  ·refine_1n:ℕ∞ωd:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:ContDiff ℝ n A.valx:Space d⊢ ContDiff ℝ n ↿(vectorPotential c A) exact vectorPotential_contDiff A hAAll goals completed! 🐙
  ·refine_2n:ℕ∞ωd:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:ContDiff ℝ n A.valx:Space d⊢ ContDiff ℝ n fun t => (t, x) fun_propAll goals completed! 🐙

C. Differentiablity of the vector potential

We prove various lemmas about the differentiablity of the vector potential from the differentiablity of the electromagnetic potential.



lemma vectorPotential_differentiable {d} {c : SpeedOfLight} (A : ElectromagneticPotential d)
    (hA : Differentiable ℝ A) : Differentiable ℝ ↿(A.vectorPotential c) := byd:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:Differentiable ℝ A.val⊢ Differentiable ℝ ↿(vectorPotential c A)
  simp [vectorPotential]d:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:Differentiable ℝ A.val⊢ Differentiable ℝ ↿((timeSlice c) fun x => WithLp.toLp 2 fun i => A.val x (Sum.inr i))
  apply timeSlice_differentiabled:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:Differentiable ℝ A.val⊢ Differentiable ℝ fun x => WithLp.toLp 2 fun i => A.val x (Sum.inr i)
  refine differentiable_euclidean.mpr ?_d:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:Differentiable ℝ A.val⊢ ∀ (i : Fin d), Differentiable ℝ fun x => (WithLp.toLp 2 fun i => A.val x (Sum.inr i)).ofLp i
  have h1 : ∀ i, Differentiable ℝ (fun x => A x i) := byd:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:Differentiable ℝ A.val⊢ Differentiable ℝ ↿(vectorPotential c A)d:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:Differentiable ℝ A.valh1:∀ (i : Fin 1 ⊕ Fin d), Differentiable ℝ fun x => A.val x i⊢ ∀ (i : Fin d), Differentiable ℝ fun x => (WithLp.toLp 2 fun i => A.val x (Sum.inr i)).ofLp i
    rw [SpaceTime.differentiable_vectord:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:Differentiable ℝ A.val⊢ Differentiable ℝ A.vald:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:Differentiable ℝ A.val⊢ Differentiable ℝ A.vald:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:Differentiable ℝ A.valh1:∀ (i : Fin 1 ⊕ Fin d), Differentiable ℝ fun x => A.val x i⊢ ∀ (i : Fin d), Differentiable ℝ fun x => (WithLp.toLp 2 fun i => A.val x (Sum.inr i)).ofLp i]d:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:Differentiable ℝ A.val⊢ Differentiable ℝ A.vald:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:Differentiable ℝ A.valh1:∀ (i : Fin 1 ⊕ Fin d), Differentiable ℝ fun x => A.val x i⊢ ∀ (i : Fin d), Differentiable ℝ fun x => (WithLp.toLp 2 fun i => A.val x (Sum.inr i)).ofLp i
    exact hAd:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:Differentiable ℝ A.valh1:∀ (i : Fin 1 ⊕ Fin d), Differentiable ℝ fun x => A.val x i⊢ ∀ (i : Fin d), Differentiable ℝ fun x => (WithLp.toLp 2 fun i => A.val x (Sum.inr i)).ofLp id:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:Differentiable ℝ A.valh1:∀ (i : Fin 1 ⊕ Fin d), Differentiable ℝ fun x => A.val x i⊢ ∀ (i : Fin d), Differentiable ℝ fun x => (WithLp.toLp 2 fun i => A.val x (Sum.inr i)).ofLp i
  exact fun i => h1 (Sum.inr i)All goals completed! 🐙

lemma vectorPotential_differentiable_time {d} {c : SpeedOfLight} (A : ElectromagneticPotential d)
    (hA : Differentiable ℝ A) (x : Space d) : Differentiable ℝ (A.vectorPotential c · x) := byd:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:Differentiable ℝ A.valx:Space d⊢ Differentiable ℝ fun x_1 => vectorPotential c A x_1 x
  change Differentiable ℝ (↿(A.vectorPotential c) ∘ fun t => (t, x))d:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:Differentiable ℝ A.valx:Space d⊢ Differentiable ℝ (↿(vectorPotential c A) ∘ fun t => (t, x))
  refine Differentiable.comp ?_ ?_refine_1d:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:Differentiable ℝ A.valx:Space d⊢ Differentiable ℝ ↿(vectorPotential c A)refine_2d:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:Differentiable ℝ A.valx:Space d⊢ Differentiable ℝ fun t => (t, x)
  ·refine_1d:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:Differentiable ℝ A.valx:Space d⊢ Differentiable ℝ ↿(vectorPotential c A) exact vectorPotential_differentiable A hAAll goals completed! 🐙
  ·refine_2d:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:Differentiable ℝ A.valx:Space d⊢ Differentiable ℝ fun t => (t, x) fun_propAll goals completed! 🐙