Physlib.Electromagnetism.Distributional.MagneticField

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

The Magnetic Field

i. Overview

In general dimensions we define the magnetic field matrix from the spatial components of the field strength matrix. This is an antisymmetric matrix. We define it in this module for distributions.

ii. Key results

DistElectromagneticPotential.magneticFieldMatrix : The magnetic field matrix from the electromagnetic potential in general spatial dimensions.

iii. Table of contents

A. Magnetic field matrix for distributions

A.1. Magnetic field matrix in terms of vector potentials

A.2. The magnetic field matrix in terms of the field strength

A.3. Magnetic field matrix in 1d

iv. References

@[expose] public section

A. Magnetic field matrix for distributions

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

A.1. Magnetic field matrix in terms of vector potentials

              lemma magneticFieldMatrix_eq_vectorPotential {c : SpeedOfLight}
    (A : DistElectromagneticPotential d)
    (ε : 𝓢(Time × Space d, ℝ)) :
    A.magneticFieldMatrix c ε = ∑ i, ∑ j,
    (Space.distSpaceDeriv j (A.vectorPotential c) ε i -
      Space.distSpaceDeriv i (A.vectorPotential c) ε j) •
    EuclideanSpace.basisFun (Fin d) ℝ i ⊗ₜ[ℝ] EuclideanSpace.basisFun (Fin d) ℝ j := byd:ℕc:SpeedOfLightA:DistElectromagneticPotential dε:𝓢(Time × Space d, ℝ)⊢ ((magneticFieldMatrix c) A) ε =
  ∑ i,
    ∑ j,
      ((((Space.distSpaceDeriv j) ((vectorPotential c) A)) ε).ofLp i -
          (((Space.distSpaceDeriv i) ((vectorPotential c) A)) ε).ofLp j) •
        (EuclideanSpace.basisFun (Fin d) ℝ) i ⊗ₜ[ℝ] (EuclideanSpace.basisFun (Fin d) ℝ) j
  simp only [magneticFieldMatrix, LinearMap.coe_mk, AddHom.coe_mk, ContinuousLinearMap.coe_comp,
    ContinuousLinearMap.coe_mk', Function.comp_apply, distTimeSlice_apply, fieldStrength_eq_basis,
    Fintype.sum_sum_type, Finset.univ_unique, Fin.default_eq_zero, Fin.isValue,
    Finset.sum_singleton, inl_0_inl_0, one_mul, inr_i_inr_i, neg_mul, sub_neg_eq_add, sub_self,
    zero_smul, zero_add, map_add, map_sum, map_smul, map_tmul, ContinuousLinearMap.coe_coe,
    Lorentz.Vector.spatialCLM_basis_sum_inl, Lorentz.Vector.spatialCLM_basis_sum_inr,
    EuclideanSpace.basisFun_apply, zero_tmul, smul_zero, Finset.sum_const_zero, tmul_zero]d:ℕc:SpeedOfLightA:DistElectromagneticPotential dε:𝓢(Time × Space d, ℝ)⊢ ∑ x,
    ∑ x_1,
      (-((distDeriv (Sum.inr x)) A) ((compCLMOfContinuousLinearEquiv ℝ (toTimeAndSpace c)) ε) (Sum.inr x_1) +
          ((distDeriv (Sum.inr x_1)) A) ((compCLMOfContinuousLinearEquiv ℝ (toTimeAndSpace c)) ε) (Sum.inr x)) •
        EuclideanSpace.single x 1 ⊗ₜ[ℝ] EuclideanSpace.single x_1 1 =
  ∑ x,
    ∑ x_1,
      ((((Space.distSpaceDeriv x_1) ((vectorPotential c) A)) ε).ofLp x -
          (((Space.distSpaceDeriv x) ((vectorPotential c) A)) ε).ofLp x_1) •
        EuclideanSpace.single x 1 ⊗ₜ[ℝ] EuclideanSpace.single x_1 1
  simp [← distTimeSlice_apply, distTimeSlice_distDeriv_inr, vectorPotential,
  Space.distSpaceDeriv_apply_CLM, Lorentz.Vector.spatialCLM, neg_add_eq_sub]All goals completed! 🐙lemma magneticFieldMatrix_basis_repr_eq_vector_potential {c : SpeedOfLight}
    (A : DistElectromagneticPotential d)
    (ε : 𝓢(Time × Space d, ℝ)) (i j : Fin d) :
    ((PiLp.basisFun 2 ℝ (Fin d)).tensorProduct (PiLp.basisFun 2 ℝ (Fin d))).repr
        (A.magneticFieldMatrix c ε) (i, j) =
      Space.distSpaceDeriv j (A.vectorPotential c) ε i -
      Space.distSpaceDeriv i (A.vectorPotential c) ε j := byd:ℕc:SpeedOfLightA:DistElectromagneticPotential dε:𝓢(Time × Space d, ℝ)i:Fin dj:Fin d⊢ (((PiLp.basisFun 2 ℝ (Fin d)).tensorProduct (PiLp.basisFun 2 ℝ (Fin d))).repr (((magneticFieldMatrix c) A) ε)) (i, j) =
  (((Space.distSpaceDeriv j) ((vectorPotential c) A)) ε).ofLp i -
    (((Space.distSpaceDeriv i) ((vectorPotential c) A)) ε).ofLp j
  simp [magneticFieldMatrix_eq_vectorPotential]All goals completed! 🐙lemma magneticFieldMatrix_distSpaceDeriv_basis_repr_eq_vector_potential {c : SpeedOfLight}
    (A : DistElectromagneticPotential d)
    (ε : 𝓢(Time × Space d, ℝ)) (i j k : Fin d) :
    ((PiLp.basisFun 2 ℝ (Fin d)).tensorProduct (PiLp.basisFun 2 ℝ (Fin d))).repr
    (Space.distSpaceDeriv k (A.magneticFieldMatrix c) ε) (i, j) =
    Space.distSpaceDeriv k (Space.distSpaceDeriv j (A.vectorPotential c)) ε i -
    Space.distSpaceDeriv k (Space.distSpaceDeriv i (A.vectorPotential c)) ε j := byd:ℕc:SpeedOfLightA:DistElectromagneticPotential dε:𝓢(Time × Space d, ℝ)i:Fin dj:Fin dk:Fin d⊢ (((PiLp.basisFun 2 ℝ (Fin d)).tensorProduct (PiLp.basisFun 2 ℝ (Fin d))).repr
      (((Space.distSpaceDeriv k) ((magneticFieldMatrix c) A)) ε))
    (i, j) =
  (((Space.distSpaceDeriv k) ((Space.distSpaceDeriv j) ((vectorPotential c) A))) ε).ofLp i -
    (((Space.distSpaceDeriv k) ((Space.distSpaceDeriv i) ((vectorPotential c) A))) ε).ofLp j
  simp [Space.distSpaceDeriv_apply', magneticFieldMatrix_basis_repr_eq_vector_potential]d:ℕc:SpeedOfLightA:DistElectromagneticPotential dε:𝓢(Time × Space d, ℝ)i:Fin dj:Fin dk:Fin d⊢ -(((vectorPotential c) A)
            ((SchwartzMap.evalCLM ℝ (Time × Space d) ℝ (0, Space.basis i))
              ((fderivCLM ℝ (Time × Space d) ℝ)
                ((SchwartzMap.evalCLM ℝ (Time × Space d) ℝ (0, Space.basis k))
                  ((fderivCLM ℝ (Time × Space d) ℝ) ε))))).ofLp
        j +
    (((vectorPotential c) A)
          ((SchwartzMap.evalCLM ℝ (Time × Space d) ℝ (0, Space.basis j))
            ((fderivCLM ℝ (Time × Space d) ℝ)
              ((SchwartzMap.evalCLM ℝ (Time × Space d) ℝ (0, Space.basis k))
                ((fderivCLM ℝ (Time × Space d) ℝ) ε))))).ofLp
      i =
  (((vectorPotential c) A)
          ((SchwartzMap.evalCLM ℝ (Time × Space d) ℝ (0, Space.basis j))
            ((fderivCLM ℝ (Time × Space d) ℝ)
              ((SchwartzMap.evalCLM ℝ (Time × Space d) ℝ (0, Space.basis k))
                ((fderivCLM ℝ (Time × Space d) ℝ) ε))))).ofLp
      i -
    (((vectorPotential c) A)
          ((SchwartzMap.evalCLM ℝ (Time × Space d) ℝ (0, Space.basis i))
            ((fderivCLM ℝ (Time × Space d) ℝ)
              ((SchwartzMap.evalCLM ℝ (Time × Space d) ℝ (0, Space.basis k))
                ((fderivCLM ℝ (Time × Space d) ℝ) ε))))).ofLp
      j
  ringAll goals completed! 🐙

A.2. The magnetic field matrix in terms of the field strength

lemma magneticFieldMatrix_basis_repr_eq_fieldStrength {c : SpeedOfLight}
    (A : DistElectromagneticPotential d)
    (ε : 𝓢(Time × Space d, ℝ)) (i j : Fin d) :
    ((PiLp.basisFun 2 ℝ (Fin d)).tensorProduct (PiLp.basisFun 2 ℝ (Fin d))).repr
        (A.magneticFieldMatrix c ε) (i, j) =
      (Lorentz.Vector.basis.tensorProduct Lorentz.Vector.basis).repr
        (distTimeSlice c A.fieldStrength ε) (Sum.inr i, Sum.inr j) := byd:ℕc:SpeedOfLightA:DistElectromagneticPotential dε:𝓢(Time × Space d, ℝ)i:Fin dj:Fin d⊢ (((PiLp.basisFun 2 ℝ (Fin d)).tensorProduct (PiLp.basisFun 2 ℝ (Fin d))).repr (((magneticFieldMatrix c) A) ε)) (i, j) =
  ((Vector.basis.tensorProduct Vector.basis).repr (((distTimeSlice c) (fieldStrength A)) ε)) (Sum.inr i, Sum.inr j)
  simp only [magneticFieldMatrix_eq_vectorPotential, EuclideanSpace.basisFun_apply, map_sum,
    map_smul, Finsupp.coe_finsetSum, Finsupp.coe_smul, Finset.sum_apply, Pi.smul_apply,
    Basis.tensorProduct_repr_tmul_apply, PiLp.basisFun_repr, PiLp.single_apply,
    smul_eq_mul, mul_ite, mul_one, mul_zero, Finset.sum_ite_irrel, Finset.sum_ite_eq,
    Finset.mem_univ, ↓reduceIte, Finset.sum_const_zero, distTimeSlice_apply,
    fieldStrength_basis_repr_eq_single, inr_i_inr_i, neg_mul, one_mul, sub_neg_eq_add]d:ℕc:SpeedOfLightA:DistElectromagneticPotential dε:𝓢(Time × Space d, ℝ)i:Fin dj:Fin d⊢ (((Space.distSpaceDeriv j) ((vectorPotential c) A)) ε).ofLp i -
    (((Space.distSpaceDeriv i) ((vectorPotential c) A)) ε).ofLp j =
  -((distDeriv (Sum.inr i)) A) ((compCLMOfContinuousLinearEquiv ℝ (toTimeAndSpace c)) ε) (Sum.inr j) +
    ((distDeriv (Sum.inr j)) A) ((compCLMOfContinuousLinearEquiv ℝ (toTimeAndSpace c)) ε) (Sum.inr i)
  simp only [vectorPotential, Vector.spatialCLM, LinearMap.coe_mk, AddHom.coe_mk,
    Space.distSpaceDeriv_apply_CLM, ContinuousLinearMap.coe_comp, ContinuousLinearMap.coe_mk',
    Function.comp_apply, ← distTimeSlice_apply, distTimeSlice_distDeriv_inr]d:ℕc:SpeedOfLightA:DistElectromagneticPotential dε:𝓢(Time × Space d, ℝ)i:Fin dj:Fin d⊢ ((Space.distSpaceDeriv j) ((distTimeSlice c) A)) ε (Sum.inr i) -
    ((Space.distSpaceDeriv i) ((distTimeSlice c) A)) ε (Sum.inr j) =
  -((Space.distSpaceDeriv i) ((distTimeSlice c) A)) ε (Sum.inr j) +
    ((Space.distSpaceDeriv j) ((distTimeSlice c) A)) ε (Sum.inr i)
  ringAll goals completed! 🐙

A.3. Magnetic field matrix in 1d

@[simp]
lemma magneticFieldMatrix_one_dim_eq_zero {c : SpeedOfLight}
    (A : DistElectromagneticPotential 1) :
    A.magneticFieldMatrix c = 0 := byc:SpeedOfLightA:DistElectromagneticPotential 1⊢ (magneticFieldMatrix c) A = 0
  ext εc:SpeedOfLightA:DistElectromagneticPotential 1ε:𝓢(Time × Space 1, ℝ)⊢ ((magneticFieldMatrix c) A) ε = 0 ε
  simp [magneticFieldMatrix_eq_vectorPotential]All goals completed! 🐙