Physlib.Electromagnetism.Kinematics.ScalarPotential

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

The Scalar 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 scalar potential, and prove lemmas about it.

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

ii. Key results

ElectromagneticPotential.scalarPotential : The scalar potential from an electromagnetic potential.

iii. Table of contents

A. Definition of the Scalar Potential

B. Relation to constructors

C. Smoothness of the Scalar Potential

D. Differentiability of the Scalar Potential

iv. References

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

A. Definition of the Scalar Potential

B. Relation to constructors

              @[simp]
lemma ofScalarPotential_scalarPotential {d} (c : SpeedOfLight)
    (φ : Time → Space d → ℝ) : (ofScalarPotential c φ).scalarPotential c = φ := byd:ℕc:SpeedOfLightφ:Time → Space d → ℝ⊢ scalarPotential c (ofScalarPotential c φ) = φ
  simp only [scalarPotential, ofScalarPotential, Fin.isValue]d:ℕc:SpeedOfLightφ:Time → Space d → ℝ⊢ ((timeSlice c) fun x => c.val * ((timeSlice c).symm φ x / c.val)) = φ
  field_simpd:ℕc:SpeedOfLightφ:Time → Space d → ℝ⊢ ((timeSlice c) fun x => (timeSlice c).symm φ x) = φ
  simpAll goals completed! 🐙@[simp]
lemma ofStaticScalarPotential_scalarPotential {d} (c : SpeedOfLight)
    (φ : Space d → ℝ) : (ofStaticScalarPotential c φ).scalarPotential c = fun _ => φ := byd:ℕc:SpeedOfLightφ:Space d → ℝ⊢ scalarPotential c (ofStaticScalarPotential c φ) = fun x => φ
  simp [ofStaticScalarPotential]All goals completed! 🐙@[simp]
lemma ofVectorPotential_scalarPotential {d} (c : SpeedOfLight)
    (A : Time → Space d → EuclideanSpace ℝ (Fin d)) :
    (ofVectorPotential c A).scalarPotential = 0 := byd:ℕc:SpeedOfLightA:Time → Space d → EuclideanSpace ℝ (Fin d)⊢ scalarPotential 1 (ofVectorPotential c A) = 0
  simp only [scalarPotential, SpeedOfLight.val_one, ofVectorPotential, Fin.isValue, mul_zero]d:ℕc:SpeedOfLightA:Time → Space d → EuclideanSpace ℝ (Fin d)⊢ (timeSlice fun x => 0) = 0
  rflAll goals completed! 🐙@[simp]
lemma ofStaticVectorPotential_scalarPotential {d} (c : SpeedOfLight)
    (A : Space d → EuclideanSpace ℝ (Fin d)) :
    (ofStaticVectorPotential c A).scalarPotential = 0 := byd:ℕc:SpeedOfLightA:Space d → EuclideanSpace ℝ (Fin d)⊢ scalarPotential 1 (ofStaticVectorPotential c A) = 0
  simp [ofStaticVectorPotential]All goals completed! 🐙@[simp]
lemma ofPotentials_scalarPotential {d} (c : SpeedOfLight) (φ : Time → Space d → ℝ)
    (A : Time → Space d → EuclideanSpace ℝ (Fin d)) :
    (ofPotentials c φ A).scalarPotential c = φ := byd:ℕc:SpeedOfLightφ:Time → Space d → ℝA:Time → Space d → EuclideanSpace ℝ (Fin d)⊢ scalarPotential c (ofPotentials c φ A) = φ
  simp only [scalarPotential, ofPotentials, Fin.isValue]d:ℕc:SpeedOfLightφ:Time → Space d → ℝA:Time → Space d → EuclideanSpace ℝ (Fin d)⊢ ((timeSlice c) fun x => c.val * ((timeSlice c).symm φ x / c.val)) = φ
  field_simpd:ℕc:SpeedOfLightφ:Time → Space d → ℝA:Time → Space d → EuclideanSpace ℝ (Fin d)⊢ ((timeSlice c) fun x => (timeSlice c).symm φ x) = φ
  simpAll goals completed! 🐙@[simp]
lemma ofStaticPotentials_scalarPotential {d} (c : SpeedOfLight) (φ : Space d → ℝ)
    (A : Space d → EuclideanSpace ℝ (Fin d)) :
    (ofStaticPotentials c φ A).scalarPotential c = fun _ => φ := byd:ℕc:SpeedOfLightφ:Space d → ℝA:Space d → EuclideanSpace ℝ (Fin d)⊢ scalarPotential c (ofStaticPotentials c φ A) = fun x => φ
  simp [ofStaticPotentials_eq_ofPotentials]All goals completed! 🐙

C. Smoothness of the Scalar Potential

We prove various lemmas about the smoothness of the scalar potential.

              

lemma scalarPotential_contDiff {n} {d} (c : SpeedOfLight) (A : ElectromagneticPotential d)
    (hA : ContDiff ℝ n A) : ContDiff ℝ n ↿(A.scalarPotential c) := byn:WithTop ℕ∞d:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:ContDiff ℝ n A.val⊢ ContDiff ℝ n ↿(scalarPotential c A)
  simp [scalarPotential]n:WithTop ℕ∞d:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:ContDiff ℝ n A.val⊢ ContDiff ℝ n ↿((timeSlice c) fun x => c.val * A.val x (Sum.inl 0))
  apply timeSlice_contDiffn:WithTop ℕ∞d:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:ContDiff ℝ n A.val⊢ ContDiff ℝ n fun x => c.val * A.val x (Sum.inl 0)
  have h1 : ∀ i, ContDiff ℝ n (fun x => A x i) := byn:WithTop ℕ∞d:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:ContDiff ℝ n A.val⊢ ContDiff ℝ n ↿(scalarPotential 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⊢ ContDiff ℝ n fun x => c.val * A.val x (Sum.inl 0)
    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⊢ ContDiff ℝ n fun x => c.val * A.val x (Sum.inl 0)]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⊢ ContDiff ℝ n fun x => c.val * A.val x (Sum.inl 0)
    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⊢ ContDiff ℝ n fun x => c.val * A.val x (Sum.inl 0)n:WithTop ℕ∞d:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:ContDiff ℝ n A.valh1:∀ (i : Fin 1 ⊕ Fin d), ContDiff ℝ n fun x => A.val x i⊢ ContDiff ℝ n fun x => c.val * A.val x (Sum.inl 0)
  apply ContDiff.mulhfn:WithTop ℕ∞d:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:ContDiff ℝ n A.valh1:∀ (i : Fin 1 ⊕ Fin d), ContDiff ℝ n fun x => A.val x i⊢ ContDiff ℝ n fun x => c.valhgn:WithTop ℕ∞d:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:ContDiff ℝ n A.valh1:∀ (i : Fin 1 ⊕ Fin d), ContDiff ℝ n fun x => A.val x i⊢ ContDiff ℝ n fun x => A.val x (Sum.inl 0)
  ·hfn:WithTop ℕ∞d:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:ContDiff ℝ n A.valh1:∀ (i : Fin 1 ⊕ Fin d), ContDiff ℝ n fun x => A.val x i⊢ ContDiff ℝ n fun x => c.val fun_propAll goals completed! 🐙
  exact h1 (Sum.inl 0)All goals completed! 🐙@[fun_prop]
lemma scalarPotential_contDiff_space {n} {d} (c : SpeedOfLight)
    (A : ElectromagneticPotential d)
    (hA : ContDiff ℝ n A) (t : Time) : ContDiff ℝ n (A.scalarPotential c t) := byn:WithTop ℕ∞d:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:ContDiff ℝ n A.valt:Time⊢ ContDiff ℝ n (scalarPotential c A t)
  change ContDiff ℝ n (↿(A.scalarPotential c) ∘ fun x => (t, x))n:WithTop ℕ∞d:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:ContDiff ℝ n A.valt:Time⊢ ContDiff ℝ n (↿(scalarPotential c A) ∘ fun x => (t, x))
  refine ContDiff.comp ?_ ?_refine_1n:WithTop ℕ∞d:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:ContDiff ℝ n A.valt:Time⊢ ContDiff ℝ n ↿(scalarPotential c A)refine_2n:WithTop ℕ∞d:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:ContDiff ℝ n A.valt:Time⊢ ContDiff ℝ n fun x => (t, x)
  ·refine_1n:WithTop ℕ∞d:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:ContDiff ℝ n A.valt:Time⊢ ContDiff ℝ n ↿(scalarPotential c A) exact scalarPotential_contDiff c A hAAll goals completed! 🐙
  ·refine_2n:WithTop ℕ∞d:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:ContDiff ℝ n A.valt:Time⊢ ContDiff ℝ n fun x => (t, x) fun_propAll goals completed! 🐙@[fun_prop]
lemma scalarPotential_contDiff_space_of_smooth {n : ℕ} {d} (c : SpeedOfLight)
    (A : ElectromagneticPotential d)
    (hA : ContDiff ℝ ∞ A) (t : Time) : ContDiff ℝ n (A.scalarPotential c t) := byn:ℕd:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valt:Time⊢ ContDiff ℝ (↑n) (scalarPotential c A t)
  apply scalarPotential_contDiff_spacen:ℕd:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valt:Time⊢ ContDiff ℝ (↑n) A.val
  exact hA.of_le (ENat.LEInfty.out)All goals completed! 🐙lemma scalarPotential_contDiff_time {n} {d} (c : SpeedOfLight) (A : ElectromagneticPotential d)
    (hA : ContDiff ℝ n A) (x : Space d) : ContDiff ℝ n (A.scalarPotential c · x) := byn:ℕ∞ωd:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:ContDiff ℝ n A.valx:Space d⊢ ContDiff ℝ n fun x_1 => scalarPotential c A x_1 x
  change ContDiff ℝ n (↿(A.scalarPotential c) ∘ fun t => (t, x))n:ℕ∞ωd:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:ContDiff ℝ n A.valx:Space d⊢ ContDiff ℝ n (↿(scalarPotential c A) ∘ fun t => (t, x))
  refine ContDiff.comp ?_ ?_refine_1n:ℕ∞ωd:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:ContDiff ℝ n A.valx:Space d⊢ ContDiff ℝ n ↿(scalarPotential 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 ↿(scalarPotential c A) exact scalarPotential_contDiff c 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! 🐙

d. Differentiability of the Scalar Potential

We prove various lemmas about the differentiability of the scalar potential.

              

lemma scalarPotential_differentiable {d} (c : SpeedOfLight) (A : ElectromagneticPotential d)
    (hA : Differentiable ℝ A) : Differentiable ℝ ↿(A.scalarPotential c) := byd:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:Differentiable ℝ A.val⊢ Differentiable ℝ ↿(scalarPotential c A)
  simp [scalarPotential]d:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:Differentiable ℝ A.val⊢ Differentiable ℝ ↿((timeSlice c) fun x => c.val * A.val x (Sum.inl 0))
  apply timeSlice_differentiabled:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:Differentiable ℝ A.val⊢ Differentiable ℝ fun x => c.val * A.val x (Sum.inl 0)
  have h1 : ∀ i, Differentiable ℝ (fun x => A x i) := byd:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:Differentiable ℝ A.val⊢ Differentiable ℝ ↿(scalarPotential c A)d:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:Differentiable ℝ A.valh1:∀ (i : Fin 1 ⊕ Fin d), Differentiable ℝ fun x => A.val x i⊢ Differentiable ℝ fun x => c.val * A.val x (Sum.inl 0)
    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⊢ Differentiable ℝ fun x => c.val * A.val x (Sum.inl 0)]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⊢ Differentiable ℝ fun x => c.val * A.val x (Sum.inl 0)
    exact hAd:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:Differentiable ℝ A.valh1:∀ (i : Fin 1 ⊕ Fin d), Differentiable ℝ fun x => A.val x i⊢ Differentiable ℝ fun x => c.val * A.val x (Sum.inl 0)d:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:Differentiable ℝ A.valh1:∀ (i : Fin 1 ⊕ Fin d), Differentiable ℝ fun x => A.val x i⊢ Differentiable ℝ fun x => c.val * A.val x (Sum.inl 0)
  apply Differentiable.mulhad:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:Differentiable ℝ A.valh1:∀ (i : Fin 1 ⊕ Fin d), Differentiable ℝ fun x => A.val x i⊢ Differentiable ℝ fun x => c.valhbd:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:Differentiable ℝ A.valh1:∀ (i : Fin 1 ⊕ Fin d), Differentiable ℝ fun x => A.val x i⊢ Differentiable ℝ fun x => A.val x (Sum.inl 0)
  ·had:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:Differentiable ℝ A.valh1:∀ (i : Fin 1 ⊕ Fin d), Differentiable ℝ fun x => A.val x i⊢ Differentiable ℝ fun x => c.val fun_propAll goals completed! 🐙
  exact h1 (Sum.inl 0)All goals completed! 🐙lemma scalarPotential_differentiable_space {d} (c : SpeedOfLight) (A : ElectromagneticPotential d)
    (hA : Differentiable ℝ A) (t : Time) : Differentiable ℝ (A.scalarPotential c t) := byd:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:Differentiable ℝ A.valt:Time⊢ Differentiable ℝ (scalarPotential c A t)
  change Differentiable ℝ (↿(A.scalarPotential c) ∘ fun x => (t, x))d:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:Differentiable ℝ A.valt:Time⊢ Differentiable ℝ (↿(scalarPotential c A) ∘ fun x => (t, x))
  refine Differentiable.comp ?_ ?_refine_1d:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:Differentiable ℝ A.valt:Time⊢ Differentiable ℝ ↿(scalarPotential c A)refine_2d:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:Differentiable ℝ A.valt:Time⊢ Differentiable ℝ fun x => (t, x)
  ·refine_1d:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:Differentiable ℝ A.valt:Time⊢ Differentiable ℝ ↿(scalarPotential c A) exact scalarPotential_differentiable c A hAAll goals completed! 🐙
  ·refine_2d:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:Differentiable ℝ A.valt:Time⊢ Differentiable ℝ fun x => (t, x) fun_propAll goals completed! 🐙lemma scalarPotential_differentiable_time {d} (c : SpeedOfLight) (A : ElectromagneticPotential d)
    (hA : Differentiable ℝ A) (x : Space d) : Differentiable ℝ (A.scalarPotential c · x) := byd:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:Differentiable ℝ A.valx:Space d⊢ Differentiable ℝ fun x_1 => scalarPotential c A x_1 x
  change Differentiable ℝ (↿(A.scalarPotential c) ∘ fun t => (t, x))d:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:Differentiable ℝ A.valx:Space d⊢ Differentiable ℝ (↿(scalarPotential c A) ∘ fun t => (t, x))
  refine Differentiable.comp ?_ ?_refine_1d:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:Differentiable ℝ A.valx:Space d⊢ Differentiable ℝ ↿(scalarPotential 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 ℝ ↿(scalarPotential c A) exact scalarPotential_differentiable c A hAAll goals completed! 🐙
  ·refine_2d:ℕc:SpeedOfLightA:ElectromagneticPotential dhA:Differentiable ℝ A.valx:Space d⊢ Differentiable ℝ fun t => (t, x) fun_propAll goals completed! 🐙