Merge pull request #410 from HEPLean/Derivatives

feat: Maxwell's equation

PhysLean.lean

@@ -6,6 +6,7 @@ import PhysLean.Cosmology.Basic
 import PhysLean.Electromagnetism.Basic
 import PhysLean.Electromagnetism.FieldStrength.Basic
 import PhysLean.Electromagnetism.FieldStrength.Derivative
+import PhysLean.Electromagnetism.MaxwellEquations
 import PhysLean.Mathematics.Fin
 import PhysLean.Mathematics.Fin.Involutions
 import PhysLean.Mathematics.LinearMaps

PhysLean/Electromagnetism/Basic.lean

@@ -27,4 +27,5 @@ open realLorentzTensor
 
 /-- The vector potential of an electromagnetic field-/
 abbrev VectorPotential (d : ℕ := 3) := SpaceTime d → ℝT[d, .up]
+
 end Electromagnetism

PhysLean/Electromagnetism/FieldStrength/Derivative.lean

@@ -22,10 +22,14 @@ open IndexNotation
 
 -/
 
+open TensorSpecies.TensorBasis in
 private lemma finsupp_single_prodEquiv (b : (j : Fin (Nat.succ 0 + (Nat.succ 0).succ)) →
       Fin (realLorentzTensor.repDim
-        ((Sum.elim ![Color.up] ![Color.up, Color.up] ∘ ⇑finSumFinEquiv.symm) j))) :
-      (Finsupp.single (TensorSpecies.TensorBasis.prodEquiv b).1 (1 : ℝ)) =
+        ((Sum.elim (fun (i : Fin 1) => realLorentzTensor.τ (![Color.up] i))
+          ![Color.up, Color.up] ∘ ⇑finSumFinEquiv.symm) j))) :
+      (Finsupp.single (fun i => Fin.cast
+        (by simp : realLorentzTensor.repDim (realLorentzTensor.τ (![Color.up] i)) =
+        realLorentzTensor.repDim (![Color.up] i)) ((prodEquiv b).1 i)) (1 : ℝ)) =
       (Finsupp.single (fun | 0 => b 0) 1) := by
   congr
   funext x
@@ -34,7 +38,8 @@ private lemma finsupp_single_prodEquiv (b : (j : Fin (Nat.succ 0 + (Nat.succ 0).
 
 private lemma mapTobasis_prodEquiv (b : (j : Fin (Nat.succ 0 + (Nat.succ 0).succ)) →
     Fin (realLorentzTensor.repDim
-      ((Sum.elim ![Color.up] ![Color.up, Color.up] ∘ ⇑finSumFinEquiv.symm) j))) :
+      ((Sum.elim (fun (i : Fin 1) => realLorentzTensor.τ (![Color.up] i))
+        ![Color.up, Color.up] ∘ ⇑finSumFinEquiv.symm) j))) :
     (fun y => mapToBasis (↑(toElectricMagneticField.symm EM)) y
       (TensorSpecies.TensorBasis.prodEquiv b).2)
     = (fun y => mapToBasis ((toElectricMagneticField.symm EM).1) y
@@ -45,18 +50,20 @@ private lemma mapTobasis_prodEquiv (b : (j : Fin (Nat.succ 0 + (Nat.succ 0).succ
   fin_cases x
   · rfl
   · rfl
+
 lemma derivative_fromElectricMagneticField_repr_diag (EM : ElectricField × MagneticField)
     (hdiff :Differentiable ℝ (mapToBasis (toElectricMagneticField.symm EM).1))
     (y : SpaceTime) (j : ℕ) (hj : j < 4) :
     (realLorentzTensor.tensorBasis _).repr (∂ (fromElectricMagneticField EM).1 y)
     (fun | 0 => μ | 1 => ⟨j, hj⟩ | 2 => ⟨j, hj⟩) = 0 := by
-  simp only [Nat.succ_eq_add_one, Nat.reduceAdd, C_eq_color, Function.comp_apply, Fin.isValue]
+  simp only [Nat.reduceAdd, C_eq_color, Function.comp_apply, Fin.isValue]
   have h_diff : DifferentiableAt ℝ (mapToBasis (toElectricMagneticField.symm EM).1)
       (Finsupp.equivFunOnFinite ((realLorentzTensor.tensorBasis _).repr y)) := by
       exact hdiff (Finsupp.equivFunOnFinite ((realLorentzTensor.tensorBasis ![Color.up]).repr y))
   conv_lhs => erw [derivative_repr _ _ _ h_diff]
-  simp only [Nat.succ_eq_add_one, Nat.reduceAdd, C_eq_color, Fin.isValue]
-  rw [finsupp_single_prodEquiv, mapTobasis_prodEquiv]
+  simp only [Nat.reduceAdd, C_eq_color, Fin.isValue]
+  rw [finsupp_single_prodEquiv]
+  rw [mapTobasis_prodEquiv]
   trans SpaceTime.deriv μ (fun y => 0) y
   rw [SpaceTime.deriv_eq_deriv_on_coord]
   congr 1
@@ -74,7 +81,7 @@ lemma derivative_fromElectricMagneticField_repr_diag (EM : ElectricField × Magn
   · simp
 
 lemma derivative_fromElectricMagneticField_repr_zero_row (EM : ElectricField × MagneticField)
-    (hdiff :Differentiable ℝ (mapToBasis (toElectricMagneticField.symm EM).1))
+    (hdiff : Differentiable ℝ (mapToBasis (toElectricMagneticField.symm EM).1))
     (y : SpaceTime) (j : ℕ) (hj : j + 1 < 4) :
     (realLorentzTensor.tensorBasis _).repr (∂ (fromElectricMagneticField EM).1 y)
     (fun | 0 => μ| 1 => ⟨0, by simp⟩ | 2 => ⟨j + 1, hj⟩) =
@@ -133,7 +140,7 @@ lemma derivative_fromElectricMagneticField_repr_zero_col (EM : ElectricField ×
     simp
 
 lemma derivative_fromElectricMagneticField_repr_one_two (EM : ElectricField × MagneticField)
-    (hdiff :Differentiable ℝ (mapToBasis (toElectricMagneticField.symm EM).1))
+    (hdiff : Differentiable ℝ (mapToBasis (toElectricMagneticField.symm EM).1))
     (y : SpaceTime) :
     (realLorentzTensor.tensorBasis _).repr (∂ (fromElectricMagneticField EM).1 y)
     (fun | 0 => μ | 1 => ⟨1, by simp⟩ | 2 => ⟨2, by simp⟩) =

PhysLean/Electromagnetism/MaxwellEquations.lean

@@ -0,0 +1,65 @@
+/-
+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
+-/
+import PhysLean.Electromagnetism.Basic
+import PhysLean.Relativity.SpaceTime.Basic
+/-!
+
+# Maxwell's equations
+
+-/
+
+namespace Electromagnetism
+
+/-- An electromagnetic system consists of charge density, a current density,
+  the speed ofl light and the electric permittivity. -/
+structure EMSystem where
+  /-- The charge density. -/
+  ρ : SpaceTime → ℝ
+  /-- The current density. -/
+  J : SpaceTime → EuclideanSpace ℝ (Fin 3)
+  /-- The speed of light. -/
+  c : ℝ
+  /-- The permittivity. -/
+  ε₀ : ℝ
+
+namespace EMSystem
+variable (𝓔 : EMSystem)
+open SpaceTime
+
+/-- The permeability. -/
+noncomputable def μ₀ : ℝ := 1/(𝓔.c^2 * 𝓔.ε₀)
+
+/-- Coulomb's constant. -/
+noncomputable def coulombConstant : ℝ := 1/(4 * Real.pi * 𝓔.ε₀)
+
+local notation "ε₀" => 𝓔.ε₀
+local notation "μ₀" => 𝓔.μ₀
+local notation "J" => 𝓔.J
+local notation "ρ" => 𝓔.ρ
+
+/-- Gauss's law for the Electric field. -/
+def GaussLawElectric (E : ElectricField) : Prop :=
+  ∀ x : SpaceTime, ε₀ * (∇⬝ E) x = ρ x
+
+/-- Gauss's law for the Magnetic field. -/
+def GaussLawMagnetic (B : MagneticField) : Prop :=
+  ∀ x : SpaceTime, (∇⬝ B) x = 0
+
+/-- Faraday's law. -/
+def FaradayLaw (E : ElectricField) (B : MagneticField) : Prop :=
+  ∀ x : SpaceTime, ∇× B x = μ₀ • (J x + ε₀ • ∂ₜ E x)
+
+/-- Ampère's law. -/
+def AmpereLaw (E : ElectricField) (B : MagneticField) : Prop :=
+  ∀ x : SpaceTime, ∇× E x = - ∂ₜ B x
+
+/-- Maxwell's equations. -/
+def MaxwellEquations (E : ElectricField) (B : MagneticField) : Prop :=
+  𝓔.GaussLawElectric E ∧ GaussLawMagnetic B ∧
+  𝓔.FaradayLaw E B ∧ AmpereLaw E B
+
+end EMSystem
+end Electromagnetism

PhysLean/Relativity/Lorentz/RealTensor/Derivative.lean

@@ -33,7 +33,8 @@ noncomputable def mapToBasis {d n m : ℕ} {cm : Fin m → (realLorentzTensor d)
     `ℝT(d, cm) → ℝT(d, (Sum.elim cm cn) ∘ finSumFinEquiv.symm)`. -/
 noncomputable def derivative {d n m : ℕ} {cm : Fin m → (realLorentzTensor d).C}
     {cn : Fin n → (realLorentzTensor d).C} (f : ℝT(d, cm) → ℝT(d, cn)) :
-    ℝT(d, cm) → ℝT(d, (Sum.elim cm cn) ∘ finSumFinEquiv.symm) := fun y =>
+    ℝT(d, cm) → ℝT(d, (Sum.elim (fun i => (realLorentzTensor d).τ (cm i)) cn) ∘
+      finSumFinEquiv.symm) := fun y =>
       ((realLorentzTensor d).tensorBasis _).repr.toEquiv.symm <|
       Finsupp.equivFunOnFinite.symm <| fun b =>
   /- The `b` componenet of the derivative of `f` evaluated at `y` is: -/
@@ -42,7 +43,7 @@ noncomputable def derivative {d n m : ℕ} {cm : Fin m → (realLorentzTensor d)
   /- evaluated at the point `y` in `ℝT(d, cm)` -/
     (Finsupp.equivFunOnFinite (((realLorentzTensor d).tensorBasis cm).repr y))
   /- In the direction of `(prodEquiv b).1` -/
-    (Finsupp.single (prodEquiv b).1 (1 : ℝ))
+    (Finsupp.single (fun i => Fin.cast (by simp) ((prodEquiv b).1 i)) (1 : ℝ))
   /- The `(prodEquiv b).2` component of that derivative. -/
     (prodEquiv b).2
 
@@ -54,13 +55,14 @@ lemma derivative_repr {d n m : ℕ} {cm : Fin m → (realLorentzTensor d).C}
     {cn : Fin n → (realLorentzTensor d).C} (f : ℝT(d, cm) → ℝT(d, cn))
     (y : ℝT(d, cm))
     (b : (j : Fin (m + n)) →
-      Fin ((realLorentzTensor d).repDim (((cm ⊕ᵥ cn) ∘ ⇑finSumFinEquiv.symm) j)))
+      Fin ((realLorentzTensor d).repDim
+      ((((fun i => (realLorentzTensor d).τ (cm i)) ⊕ᵥ cn) ∘ ⇑finSumFinEquiv.symm) j)))
     (h1 : DifferentiableAt ℝ (mapToBasis f)
       (Finsupp.equivFunOnFinite (((realLorentzTensor d).tensorBasis cm).repr y))) :
     ((realLorentzTensor d).tensorBasis _).repr (∂ f y) b =
     fderiv ℝ (fun y => mapToBasis f y (prodEquiv b).2)
       (((realLorentzTensor d).tensorBasis cm).repr y)
-      (Finsupp.single (prodEquiv b).1 (1 : ℝ)) := by
+      (Finsupp.single (fun i => Fin.cast (by simp) ((prodEquiv b).1 i)) (1 : ℝ)) := by
   simp [derivative]
   rw [fderiv_pi]
   · simp
@@ -68,4 +70,7 @@ lemma derivative_repr {d n m : ℕ} {cm : Fin m → (realLorentzTensor d).C}
   · rw [← differentiableAt_pi]
     exact h1
 
+TODO "Prove that the derivative obeys the correct equivariant with respect to the
+  Lorentz group."
+
 end realLorentzTensor

PhysLean/Relativity/SpaceTime/Basic.lean

@@ -76,16 +76,23 @@ lemma coord_on_repr {d : ℕ} (μ : Fin (1 + d))
 -/
 
 /-- The derivative of a function `SpaceTime d → ℝ` along the `μ` coordinte. -/
-noncomputable def deriv {d : ℕ} (μ : Fin (1 + d)) (f : SpaceTime d → ℝ) : SpaceTime d → ℝ :=
+noncomputable def deriv {M : Type} [AddCommGroup M] [Module ℝ M] [TopologicalSpace M]
+    {d : ℕ} (μ : Fin (1 + d)) (f : SpaceTime d → M) : SpaceTime d → M :=
   fun y => fderiv ℝ f y ((realLorentzTensor d).tensorBasis _ (fun x => Fin.cast (by simp) μ))
 
+@[inherit_doc deriv]
+scoped notation "∂_" => deriv
+
+/-- The derivative with respect to time. -/
+scoped notation "∂ₜ" => deriv 0
+
 lemma deriv_eq {d : ℕ} (μ : Fin (1 + d)) (f : SpaceTime d → ℝ) (y : SpaceTime d) :
     SpaceTime.deriv μ f y =
     fderiv ℝ f y ((realLorentzTensor d).tensorBasis _ (fun x => Fin.cast (by simp) μ)) := by
   rfl
 
 @[simp]
-lemma deriv_zero {d : ℕ} (μ : Fin (1 + d)) : SpaceTime.deriv μ (fun _ => 0) = 0 := by
+lemma deriv_zero {d : ℕ} (μ : Fin (1 + d)) : SpaceTime.deriv μ (fun _ => (0 : ℝ)) = 0 := by
   ext y
   rw [SpaceTime.deriv_eq]
   simp
@@ -209,11 +216,25 @@ lemma deriv_coord_eq_if {d : ℕ} (μ ν : Fin (1 + d)) (y : SpaceTime d) :
   · rw [if_neg h]
     exact SpaceTime.deriv_coord_diff μ ν h y
 
-/-- The gradiant of a function `SpaceTime d → EuclideanSpace (Fin d) ℝ`. -/
-noncomputable def spaceGrad {d : ℕ} (f : SpaceTime d → EuclideanSpace (Fin d) ℝ) :
+/-- The divergence of a function `SpaceTime d → EuclideanSpace ℝ (Fin d)`. -/
+noncomputable def spaceDiv {d : ℕ} (f : SpaceTime d → EuclideanSpace ℝ (Fin d)) :
     SpaceTime d → ℝ :=
   ∑ j, SpaceTime.deriv (finSumFinEquiv (Sum.inr j)) (fun y => f y j)
 
+@[inherit_doc spaceDiv]
+scoped[SpaceTime] notation "∇⬝" E => spaceDiv E
+
+/-- The curl of a function `SpaceTime → EuclideanSpace ℝ (Fin 3)`. -/
+def spaceCurl (f : SpaceTime → EuclideanSpace ℝ (Fin 3)) :
+    SpaceTime → EuclideanSpace ℝ (Fin 3) := fun x j =>
+  match j with
+  | 0 => deriv 1 (fun y => f y 2) x - deriv 2 (fun y => f y 1) x
+  | 1 => deriv 2 (fun y => f y 0) x - deriv 0 (fun y => f y 2) x
+  | 2 => deriv 0 (fun y => f y 1) x - deriv 1 (fun y => f y 0) x
+
+@[inherit_doc spaceCurl]
+scoped[SpaceTime] notation "∇×" => spaceCurl
+
 end SpaceTime
 
 end