Physlib.Electromagnetism.Distributional.ElectricField

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.Distributional.VectorPotential
public import Physlib.Electromagnetism.Distributional.ScalarPotential
public import Physlib.Electromagnetism.Distributional.FieldStrength
public import Physlib.Electromagnetism.Basic

The Electric Field

i. Overview

The electric field is defined in terms of the electromagnetic potential A as E = - ∇ φ - ∂ₜ \vec A.

In this module we define the electric field, and prove lemmas about it.

ii. Key results

DistElectromagneticPotential.electricField : The electric field for electromagnetic potentials which are distributions.

iii. Table of contents

A. Electric field for distributions

iv. References

@[expose] public section

A. Electric field for distributions

              attribute [-simp] Fintype.sum_sum_typeattribute [-simp] Nat.succ_eq_add_onelemma electricField_eq_fieldStrength {d} {c : SpeedOfLight}
    (A : DistElectromagneticPotential d) (ε : 𝓢(Time × Space d, ℝ))
    (i : Fin d) : A.electricField c ε i = - c * (Vector.basis.tensorProduct Vector.basis).repr
      (distTimeSlice c (A.fieldStrength) ε) (Sum.inl 0, Sum.inr i) := byd:ℕc:SpeedOfLightA:DistElectromagneticPotential dε:𝓢(Time × Space d, ℝ)i:Fin d⊢ (((electricField c) A) ε).ofLp i =
  -c.val *
    ((Vector.basis.tensorProduct Vector.basis).repr (((distTimeSlice c) (fieldStrength A)) ε)) (Sum.inl 0, Sum.inr i)
  simp only [distTimeSlice_apply, Fin.isValue, fieldStrength_basis_repr_eq_single, inl_0_inl_0,
    one_mul, inr_i_inr_i, neg_mul, sub_neg_eq_add]d:ℕc:SpeedOfLightA:DistElectromagneticPotential dε:𝓢(Time × Space d, ℝ)i:Fin d⊢ (((electricField c) A) ε).ofLp i =
  -(c.val *
      (((distDeriv (Sum.inl 0)) A) ((compCLMOfContinuousLinearEquiv ℝ (toTimeAndSpace c)) ε) (Sum.inr i) +
        ((distDeriv (Sum.inr i)) A) ((compCLMOfContinuousLinearEquiv ℝ (toTimeAndSpace c)) ε) (Sum.inl 0)))
  simp only [electricField, scalarPotential, Vector.temporalCLM, Fin.isValue, map_smul,
    ContinuousLinearMap.comp_smulₛₗ, Real.ringHom_apply, LinearMap.coe_mk, AddHom.coe_mk,
    vectorPotential, Vector.spatialCLM, Space.distTimeDeriv_apply_CLM, FunLike.coe_sub,
    ContinuousLinearMap.coe_comp, ContinuousLinearMap.coe_mk', Pi.sub_apply,
    _root_.neg_apply, FunLike.coe_smul, Pi.smul_apply,
    Function.comp_apply, PiLp.sub_apply, PiLp.neg_apply, PiLp.smul_apply, Space.distSpaceGrad_apply,
    Space.distSpaceDeriv_apply_CLM, LinearMap.coe_toContinuousLinearMap', smul_eq_mul,
    ← distTimeSlice_apply, distTimeSlice_distDeriv_inl, one_div, Vector.apply_smul,
    distTimeSlice_distDeriv_inr]d:ℕc:SpeedOfLightA:DistElectromagneticPotential dε:𝓢(Time × Space d, ℝ)i:Fin d⊢ -(c.val * ((Space.distSpaceDeriv i) ((distTimeSlice c) A)) ε (Sum.inl 0)) -
    (Space.distTimeDeriv ((distTimeSlice c) A)) ε (Sum.inr i) =
  -(c.val *
      (c.val⁻¹ * (Space.distTimeDeriv ((distTimeSlice c) A)) ε (Sum.inr i) +
        ((Space.distSpaceDeriv i) ((distTimeSlice c) A)) ε (Sum.inl 0)))
  field_simpd:ℕc:SpeedOfLightA:DistElectromagneticPotential dε:𝓢(Time × Space d, ℝ)i:Fin d⊢ -(c.val * ((Space.distSpaceDeriv i) ((distTimeSlice c) A)) ε (Sum.inl 0)) -
    (Space.distTimeDeriv ((distTimeSlice c) A)) ε (Sum.inr i) =
  -((Space.distTimeDeriv ((distTimeSlice c) A)) ε (Sum.inr i) +
      c.val * ((Space.distSpaceDeriv i) ((distTimeSlice c) A)) ε (Sum.inl 0))
  ringAll goals completed! 🐙