feat: Action on EM potential

PhysLean/Electromagnetism/Dynamics/IsExtrema.lean

@@ -179,12 +179,12 @@ lemma isExtrema_lorentzGroup_apply_iff {𝓕 : FreeSpace}
     (A : ElectromagneticPotential d)
     (hA : ContDiff ℝ ∞ A) (J : LorentzCurrentDensity d) (hJ : ContDiff ℝ ∞ J)
     (Λ : LorentzGroup d) :
-    IsExtrema 𝓕 ⟨fun x => Λ • A (Λ⁻¹ • x)⟩ (fun x => Λ • J (Λ⁻¹ • x)) ↔
+    IsExtrema 𝓕 (Λ • A) (fun x => Λ • J (Λ⁻¹ • x)) ↔
     IsExtrema 𝓕 A J := by
   rw [isExtrema_iff_tensors]
   conv_lhs =>
     enter [x, 1, 1, 2, 2, 2]
-    change tensorDeriv (fun x => toFieldStrength ⟨fun x => Λ • A (Λ⁻¹ • x)⟩ x) x
+    change tensorDeriv (fun x => toFieldStrength (Λ • A) x) x
     enter [1,x]
     rw [toFieldStrength_equivariant _ _ (hA.differentiable (by simp))]
   conv_lhs =>

PhysLean/Electromagnetism/Dynamics/KineticTerm.lean

@@ -104,7 +104,7 @@ We show that the kinetic energy is Lorentz invariant.
 lemma kineticTerm_equivariant {d} {𝓕 : FreeSpace} (A : ElectromagneticPotential d)
     (Λ : LorentzGroup d)
     (hf : Differentiable ℝ A) (x : SpaceTime d) :
-    kineticTerm 𝓕 ⟨fun x => Λ • A (Λ⁻¹ • x)⟩ x = kineticTerm 𝓕 A (Λ⁻¹ • x) := by
+    kineticTerm 𝓕 (Λ • A) x = kineticTerm 𝓕 A (Λ⁻¹ • x) := by
   rw [kineticTerm, kineticTerm]
   conv_lhs =>
     enter [2]

PhysLean/Electromagnetism/Kinematics/Boosts.lean

@@ -68,7 +68,7 @@ lemma electricField_apply_x_boost_zero {d : ℕ} {c : SpeedOfLight} (β : ℝ) (
     let x' : Space d.succ := ⟨fun
       | 0 => γ β * (x 0 + c * β * t.val)
       | ⟨Nat.succ n, ih⟩ => x ⟨Nat.succ n, ih⟩⟩
-    electricField c ⟨fun x => Λ • A (Λ⁻¹ • x)⟩ t x 0 =
+    electricField c (Λ • A) t x 0 =
     A.electricField c t' x' 0 := by
   dsimp
   rw [electricField_eq_fieldStrengthMatrix, fieldStrengthMatrix_equivariant]
@@ -94,13 +94,7 @@ lemma electricField_apply_x_boost_zero {d : ℕ} {c : SpeedOfLight} (β : ℝ) (
   rfl
   exact hA
   exact hA
-  · simp only
-    apply Differentiable.comp
-    · change Differentiable ℝ (Lorentz.Vector.actionCLM (boost 0 β hβ))
-      exact ContinuousLinearMap.differentiable (Lorentz.Vector.actionCLM (boost 0 β hβ))
-    · apply Differentiable.comp
-      · exact hA
-      · exact ContinuousLinearMap.differentiable (Lorentz.Vector.actionCLM (boost 0 β hβ)⁻¹)
+  · fun_prop
 
 /-!
 
@@ -116,7 +110,7 @@ lemma electricField_apply_x_boost_succ {d : ℕ} {c : SpeedOfLight} (β : ℝ) (
     let x' : Space d.succ := ⟨fun
       | 0 => γ β * (x 0 + c * β * t.val)
       | ⟨Nat.succ n, ih⟩ => x ⟨Nat.succ n, ih⟩⟩
-    electricField c ⟨fun x => Λ • A (Λ⁻¹ • x)⟩ t x i.succ =
+    electricField c (Λ • A) t x i.succ =
     γ β * (A.electricField c t' x' i.succ + c * β * A.magneticFieldMatrix c t' x' (0, i.succ)) := by
   dsimp
   rw [electricField_eq_fieldStrengthMatrix,
@@ -134,13 +128,7 @@ lemma electricField_apply_x_boost_succ {d : ℕ} {c : SpeedOfLight} (β : ℝ) (
   field_simp
   rfl
   exact hA
-  · simp only
-    apply Differentiable.comp
-    · change Differentiable ℝ (Lorentz.Vector.actionCLM (boost 0 β hβ))
-      exact ContinuousLinearMap.differentiable (Lorentz.Vector.actionCLM (boost 0 β hβ))
-    · apply Differentiable.comp
-      · exact hA
-      · exact ContinuousLinearMap.differentiable (Lorentz.Vector.actionCLM (boost 0 β hβ)⁻¹)
+  · fun_prop
 
 /-!
 
@@ -162,7 +150,7 @@ lemma magneticFieldMatrix_apply_x_boost_zero_succ {d : ℕ} {c : SpeedOfLight} (
     let x' : Space d.succ := ⟨fun
       | 0 => γ β * (x 0 + c * β * t.val)
       | ⟨Nat.succ n, ih⟩ => x ⟨Nat.succ n, ih⟩⟩
-    magneticFieldMatrix c ⟨fun x => Λ • A (Λ⁻¹ • x)⟩ t x (0, i.succ) =
+    magneticFieldMatrix c (Λ • A) t x (0, i.succ) =
     γ β * (A.magneticFieldMatrix c t' x' (0, i.succ) + β / c * A.electricField c t' x' i.succ) := by
   dsimp
   rw [magneticFieldMatrix_eq]
@@ -196,7 +184,7 @@ lemma magneticFieldMatrix_apply_x_boost_succ_succ {d : ℕ} {c : SpeedOfLight} (
     let x' : Space d.succ := ⟨fun
       | 0 => γ β * (x 0 + c * β * t.val)
       | ⟨Nat.succ n, ih⟩ => x ⟨Nat.succ n, ih⟩⟩
-    magneticFieldMatrix c ⟨fun x => Λ • A (Λ⁻¹ • x)⟩ t x (i.succ, j.succ) =
+    magneticFieldMatrix c (Λ • A) t x (i.succ, j.succ) =
     A.magneticFieldMatrix c t' x' (i.succ, j.succ) := by
   dsimp
   rw [magneticFieldMatrix_eq]

PhysLean/Electromagnetism/Kinematics/EMPotential.lean

@@ -31,10 +31,11 @@ spacetime to contravariant Lorentz vectors.
 
 - A. The electromagnetic potential
   - A.1. Basic instances on the type of electromagnetic potentials
-  - A.2. The action on the space-time derivatives
+  - A.2. The group action on the ElectromagneticPotential
   - A.3. Differentiability
-  - A.4. Variational adjoint derivative of component
-  - A.5. Variational adjoint derivative of derivatives of the potential
+  - A.4. The action on the space-time derivatives
+  - A.5. Variational adjoint derivative of component
+  - A.6. Variational adjoint derivative of derivatives of the potential
 - B. The derivative tensor of the electromagnetic potential
   - B.1. Equivariance of the derivative tensor
   - B.2. The elements of the derivative tensor in terms of the basis
@@ -82,6 +83,12 @@ open minkowskiMatrix
 attribute [-simp] Fintype.sum_sum_type
 attribute [-simp] Nat.succ_eq_add_one
 
+@[ext]
+lemma eq_of_val_eq (A B : ElectromagneticPotential d) (h : A.val = B.val) : A = B := by
+  cases A; cases B
+  simp at h
+  rw [h]
+
 /-!
 
 ## A.1. Basic instances on the type of electromagnetic potentials
@@ -114,19 +121,63 @@ lemma smul_apply {d} (r : ℝ) (A : ElectromagneticPotential d) (x : SpaceTime d
 
 /-!
 
-### A.2. The action on the space-time derivatives
+## A.2. The group action on the ElectromagneticPotential
+
+-/
+
+noncomputable instance {d} : SMul (LorentzGroup d) (ElectromagneticPotential d) where
+  smul Λ A := ⟨fun x => Λ • A (Λ⁻¹ • x)⟩
+
+lemma action_val {d} (Λ : LorentzGroup d) (A : ElectromagneticPotential d) :
+    (Λ • A).val = fun x => Λ • A (Λ⁻¹ • x) := rfl
+
+noncomputable instance {d} : MulAction (LorentzGroup d) (ElectromagneticPotential d) where
+  mul_smul Λ₁ Λ₂ A := by
+    ext i
+    simp [action_val, mul_smul]
+  one_smul A := by
+    ext i
+    simp [action_val, one_smul]
+
+/-!
+
+### A.3. Differentiability
+
+We show that the components of field strength tensor are differentiable if the potential is.
+-/
+
+@[fun_prop]
+lemma differentiable_component {d : ℕ}
+    (A : ElectromagneticPotential d) (hA : Differentiable ℝ A) (μ : Fin 1 ⊕ Fin d) :
+    Differentiable ℝ (fun x => A x μ) := by
+  revert μ
+  rw [SpaceTime.differentiable_vector]
+  exact hA
+
+
+@[fun_prop]
+lemma differentiable_action {d} (Λ : LorentzGroup d) (A : ElectromagneticPotential d)
+    (hA : Differentiable ℝ A) : Differentiable ℝ (fun x => Λ • A (Λ⁻¹ • x)) := by
+  apply Differentiable.comp
+  · exact ContinuousLinearMap.differentiable (Lorentz.Vector.actionCLM Λ)
+  · apply Differentiable.comp
+    · exact hA
+    · exact ContinuousLinearMap.differentiable (Lorentz.Vector.actionCLM Λ⁻¹)
+
+/-!
+
+### A.4. The action on the space-time derivatives
 
 Given a ElectromagneticPotential `A^μ`, we can consider its derivative `∂_μ A^ν`.
 Under a Lorentz transformation `Λ`, this transforms as
-`∂_ μ (fun x => Λ • A (Λ⁻¹ • x))`, we write an expression for this in terms of the tensor.
+`∂_ μ (Λ • A)`, we write an expression for this in terms of the tensor.
 `∂_ ρ A (Λ⁻¹ • x) κ`.
 
 -/
 
 lemma spaceTime_deriv_action_eq_sum {d} {μ ν : Fin 1 ⊕ Fin d} {x : SpaceTime d}
     (Λ : LorentzGroup d) (A : ElectromagneticPotential d) (hA : Differentiable ℝ A) :
-    ∂_ μ (fun x => Λ • A (Λ⁻¹ • x)) x ν =
-    ∑ κ, ∑ ρ, (Λ.1 ν κ * Λ⁻¹.1 ρ μ) * ∂_ ρ A (Λ⁻¹ • x) κ := by
+    ∂_ μ (Λ • A) x ν = ∑ κ, ∑ ρ, (Λ.1 ν κ * Λ⁻¹.1 ρ μ) * ∂_ ρ A (Λ⁻¹ • x) κ := by
   calc _
     _ = ((Λ • (∂_ μ (fun x => A (Λ⁻¹ • x)) x)) ν) := by
       have hdif : ∀ i, DifferentiableAt ℝ (fun x => A (Λ⁻¹ • x) i) x := by
@@ -140,14 +191,8 @@ lemma spaceTime_deriv_action_eq_sum {d} {μ ν : Fin 1 ⊕ Fin d} {x : SpaceTime
           exact ContinuousLinearMap.differentiable (Lorentz.Vector.actionCLM Λ⁻¹)
       trans ∂_ μ (fun x => (Λ • A (Λ⁻¹ • x)) ν) x
       · rw [SpaceTime.deriv_eq, SpaceTime.deriv_eq, SpaceTime.fderiv_vector]
-        intro ν
-        conv =>
-          enter [2, x]; rw [← Lorentz.Vector.actionCLM_apply, ← Lorentz.Vector.actionCLM_apply]
-        apply Differentiable.comp
-        · exact ContinuousLinearMap.differentiable (Lorentz.Vector.actionCLM Λ)
-        · apply Differentiable.comp
-          · exact hA
-          · exact ContinuousLinearMap.differentiable (Lorentz.Vector.actionCLM Λ⁻¹)
+        simp only [action_val]
+        fun_prop
       conv_lhs =>
         enter [2, x]
         rw [Lorentz.Vector.smul_eq_sum]
@@ -185,22 +230,7 @@ lemma spaceTime_deriv_action_eq_sum {d} {μ ν : Fin 1 ⊕ Fin d} {x : SpaceTime
 
 /-!
 
-### A.3. Differentiability
-
-We show that the components of field strength tensor are differentiable if the potential is.
--/
-
-@[fun_prop]
-lemma differentiable_component {d : ℕ}
-    (A : ElectromagneticPotential d) (hA : Differentiable ℝ A) (μ : Fin 1 ⊕ Fin d) :
-    Differentiable ℝ (fun x => A x μ) := by
-  revert μ
-  rw [SpaceTime.differentiable_vector]
-  exact hA
-
-/-!
-
-### A.4. Variational adjoint derivative of component
+### A.5. Variational adjoint derivative of component
 
 We find the variational adjoint derivative of the components of the potential.
 This will be used to find e.g. the variational derivative of the kinetic term,
@@ -232,7 +262,7 @@ lemma hasVarAdjDerivAt_component {d : ℕ} (μ : Fin 1 ⊕ Fin d) (A : SpaceTime
 
 /-!
 
-### A.5. Variational adjoint derivative of derivatives of the potential
+### A.6. Variational adjoint derivative of derivatives of the potential
 
 We find the variational adjoint derivative of the derivatives of the components of the potential.
 This will again be used to find the variational derivative of the kinetic term,
@@ -281,7 +311,7 @@ as taking the derivative and then applying the Lorentz transformation to the res
 -/
 lemma deriv_equivariant {d} {x : SpaceTime d} (A : ElectromagneticPotential d)
     (Λ : LorentzGroup d)
-    (hf : Differentiable ℝ A) : deriv ⟨fun x => Λ • A (Λ⁻¹ • x)⟩ x = Λ • (deriv A (Λ⁻¹ • x)) := by
+    (hf : Differentiable ℝ A) : deriv (Λ • A) x = Λ • (deriv A (Λ⁻¹ • x)) := by
     calc _
       _ = ∑ μ, ∑ ν, ∑ κ, ∑ ρ, (Λ.1 ν κ * (Λ⁻¹.1 ρ μ • ∂_ ρ A (Λ⁻¹ • x) κ)) •
           (Lorentz.CoVector.basis μ) ⊗ₜ[ℝ]

PhysLean/Electromagnetism/Kinematics/FieldStrength.lean

@@ -369,16 +369,15 @@ as taking the field strength and then transforming the resulting tensor.
 
 lemma toFieldStrength_equivariant {d} (A : ElectromagneticPotential d) (Λ : LorentzGroup d)
     (hf : Differentiable ℝ A) (x : SpaceTime d) :
-    toFieldStrength ⟨fun x => Λ • A (Λ⁻¹ • x)⟩ x =
-      Λ • toFieldStrength A (Λ⁻¹ • x) := by
+    toFieldStrength (Λ • A) x = Λ • toFieldStrength A (Λ⁻¹ • x) := by
   rw [toFieldStrength, deriv_equivariant A Λ hf, ← actionT_contrMetric Λ, toFieldStrength]
   simp only [Tensorial.toTensor_smul, prodT_equivariant, contrT_equivariant, map_neg,
     permT_equivariant, map_add, ← Tensorial.smul_toTensor_symm, smul_add, smul_neg]
 
 lemma fieldStrengthMatrix_equivariant {d} (A : ElectromagneticPotential d)
     (Λ : LorentzGroup d) (hf : Differentiable ℝ A) (x : SpaceTime d)
     (μ : (Fin 1 ⊕ Fin d)) (ν : Fin 1 ⊕ Fin d) :
-    fieldStrengthMatrix ⟨fun x => Λ • A (Λ⁻¹ • x)⟩ x (μ, ν) =
+    fieldStrengthMatrix (Λ • A) x (μ, ν) =
     ∑ κ, ∑ ρ, (Λ.1 μ κ * Λ.1 ν ρ) * A.fieldStrengthMatrix (Λ⁻¹ • x) (κ, ρ) := by
   rw [fieldStrengthMatrix, toFieldStrength_equivariant A Λ hf x]
   conv_rhs =>