Merge pull request #417 from HEPLean/bump

feat: Boosts of Lorentz vectors

PhysLean.lean

@@ -200,6 +200,7 @@ import PhysLean.Relativity.Lorentz.RealTensor.Metrics.Basic
 import PhysLean.Relativity.Lorentz.RealTensor.Metrics.Pre
 import PhysLean.Relativity.Lorentz.RealTensor.Units.Pre
 import PhysLean.Relativity.Lorentz.RealTensor.Vector.Basic
+import PhysLean.Relativity.Lorentz.RealTensor.Vector.Boosts
 import PhysLean.Relativity.Lorentz.RealTensor.Vector.Causality
 import PhysLean.Relativity.Lorentz.RealTensor.Vector.Pre.Basic
 import PhysLean.Relativity.Lorentz.RealTensor.Vector.Pre.Contraction

PhysLean/Electromagnetism/MaxwellEquations.lean

@@ -4,7 +4,6 @@ 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

PhysLean/Particles/StandardModel/HiggsBoson/Basic.lean

@@ -4,10 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
 import PhysLean.Relativity.SpaceTime.Basic
-import Mathlib.Tactic.Polyrith
 import Mathlib.Geometry.Manifold.VectorBundle.SmoothSection
 import Mathlib.Geometry.Manifold.Instances.Real
-import PhysLean.Meta.Informal.Basic
 /-!
 
 # The Higgs field

PhysLean/Particles/StandardModel/HiggsBoson/GaugeAction.lean

@@ -4,10 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
 import PhysLean.Particles.StandardModel.HiggsBoson.Basic
-import Mathlib.RepresentationTheory.Basic
 import PhysLean.Particles.StandardModel.Basic
 import PhysLean.Particles.StandardModel.Representations
-import Mathlib.Analysis.InnerProductSpace.Adjoint
 /-!
 
 # The action of the gauge group on the Higgs field

PhysLean/Relativity/Lorentz/Group/Boosts/Basic.lean

@@ -1,5 +1,5 @@
 /-
-Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
+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
 -/
@@ -21,15 +21,30 @@ namespace LorentzGroup
 variable {d : ℕ}
 variable (Λ : LorentzGroup d)
 
+/-- The Lorentz factor (aka gamma factor or Lorentz term). -/
+def γ (β : ℝ) : ℝ := 1 / Real.sqrt (1 - β^2)
+
+lemma γ_sq (β : ℝ) (hβ : |β| < 1) : (γ β)^2 = 1 / (1 - β^2) := by
+  simp only [γ, one_div, inv_pow, _root_.inv_inj]
+  refine Real.sq_sqrt ?_
+  simp only [sub_nonneg, sq_le_one_iff_abs_le_one]
+  exact le_of_lt hβ
+
+@[simp]
+lemma γ_zero : γ 0 = 1 := by simp [γ]
+
+@[simp]
+lemma γ_neg (β : ℝ) : γ (-β) = γ β := by simp [γ]
+
 /-- The Lorentz boost with in the space direction `i` with speed `β` with
   `|β| < 1`. -/
 def boost (i : Fin d) (β : ℝ) (hβ : |β| < 1) : LorentzGroup d :=
-  ⟨let γ := 1 / Real.sqrt (1 - β^2)
+  ⟨
   fun j k =>
-    if k = Sum.inl 0 ∧ j = Sum.inl 0 then γ
-    else if k = Sum.inl 0 ∧ j = Sum.inr i then - γ * β
-    else if k = Sum.inr i ∧ j = Sum.inl 0 then - γ * β
-    else if k = Sum.inr i ∧ j = Sum.inr i then γ else
+    if k = Sum.inl 0 ∧ j = Sum.inl 0 then γ β
+    else if k = Sum.inl 0 ∧ j = Sum.inr i then - γ β * β
+    else if k = Sum.inr i ∧ j = Sum.inl 0 then - γ β * β
+    else if k = Sum.inr i ∧ j = Sum.inr i then γ β else
     if j = k then 1 else 0, h⟩
 where
   h := by
@@ -66,13 +81,12 @@ where
       simp only [Fin.isValue, ↓reduceIte, minkowskiMatrix.inl_0_inl_0, one_mul, true_and,
         reduceCtorEq, false_and]
       rw [Finset.sum_eq_single i]
-      · simp
+      · simp only [Fin.isValue, and_true, ↓reduceIte]
         by_cases hk : k = Sum.inl 0
         · subst hk
           simp only [Fin.isValue, ↓reduceIte, one_apply_eq]
           ring_nf
-          field_simp [hb1, hb2]
-          ring
+          field_simp [γ, hb1, hb2]
         · simp only [Fin.isValue, hk, ↓reduceIte]
           by_cases hk' : k = Sum.inr i
           · simp only [hk', ↓reduceIte, Fin.isValue, ne_eq, reduceCtorEq, not_false_eq_true,
@@ -109,8 +123,7 @@ where
             simp only [Fin.isValue, reduceCtorEq, ↓reduceIte, neg_mul, one_mul, neg_neg, and_true,
               and_self, one_apply_eq]
             ring_nf
-            field_simp [hb1, hb2]
-            ring
+            field_simp [γ, hb1, hb2]
           · rw [one_apply]
             simp only [Fin.isValue, reduceCtorEq, ↓reduceIte, Sum.inr.injEq, hk, and_true, and_self,
               neg_mul, one_mul, neg_neg, zero_add]
@@ -174,7 +187,7 @@ lemma boost_zero_eq_id (i : Fin d) : boost i 0 (by simp) = 1 := by
   simp only [boost, Fin.isValue, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow, sub_zero,
     Real.sqrt_one, one_ne_zero, div_self, mul_zero, lorentzGroupIsGroup_one_coe]
   match j, k with
-  | Sum.inl 0, Sum.inl 0 => rfl
+  | Sum.inl 0, Sum.inl 0 => simp [γ]
   | Sum.inl 0, Sum.inr k =>
     simp
   | Sum.inr i, Sum.inl 0 =>
@@ -228,6 +241,55 @@ lemma boost_inverse (i : Fin d) {β : ℝ} (hβ : |β| < 1) :
         rw [if_neg (fun a => h2 (Eq.symm a))]
         simp
 
+@[simp]
+lemma boost_inl_0_inl_0 (i : Fin d) {β : ℝ} (hβ : |β| < 1) :
+    (boost i β hβ).1 (Sum.inl 0) (Sum.inl 0) = γ β := by
+  simp [boost]
+
+@[simp]
+lemma boost_inr_self_inr_self (i : Fin d) {β : ℝ} (hβ : |β| < 1) :
+    (boost i β hβ).1 (Sum.inr i) (Sum.inr i) = γ β := by
+  simp [boost]
+
+@[simp]
+lemma boost_inl_0_inr_self (i : Fin d) {β : ℝ} (hβ : |β| < 1) :
+    (boost i β hβ).1 (Sum.inl 0) (Sum.inr i) = - γ β * β := by
+  simp [boost]
+
+@[simp]
+lemma boost_inr_self_inl_0 (i : Fin d) {β : ℝ} (hβ : |β| < 1) :
+    (boost i β hβ).1 (Sum.inr i) (Sum.inl 0) = - γ β * β := by
+  simp [boost]
+
+lemma boost_inl_0_inr_other {i j : Fin d} {β : ℝ} (hβ : |β| < 1) (hij : j ≠ i) :
+    (boost i β hβ).1 (Sum.inl 0) (Sum.inr j) = 0 := by
+  simp [boost, hij]
+
+lemma boost_inr_other_inl_0 {i j : Fin d} {β : ℝ} (hβ : |β| < 1) (hij : j ≠ i) :
+    (boost i β hβ).1 (Sum.inr j) (Sum.inl 0) = 0 := by
+  simp [boost, hij]
+
+lemma boost_inr_self_inr_other {i j : Fin d} {β : ℝ} (hβ : |β| < 1) (hij : j ≠ i) :
+    (boost i β hβ).1 (Sum.inr i) (Sum.inr j) = 0 := by
+  simp only [boost, Fin.isValue, neg_mul, reduceCtorEq, and_self, ↓reduceIte, and_true,
+    Sum.inr.injEq, hij, ite_eq_right_iff, one_ne_zero, imp_false]
+  exact id (Ne.symm hij)
+
+lemma boost_inr_other_inr_self {i j : Fin d} {β : ℝ} (hβ : |β| < 1) (hij : j ≠ i) :
+    (boost i β hβ).1 (Sum.inr j) (Sum.inr i) = 0 := by
+  simp [boost, hij]
+
+lemma boost_inr_other_inr {i j k : Fin d} {β : ℝ} (hβ : |β| < 1) (hij : j ≠ i) :
+    (boost i β hβ).1 (Sum.inr j) (Sum.inr k) = if j = k then 1 else 0:= by
+  simp [boost, hij]
+
+lemma boost_inr_inr_other {i j k : Fin d} {β : ℝ} (hβ : |β| < 1) (hij : j ≠ i) :
+    (boost i β hβ).1 (Sum.inr k) (Sum.inr j) = if j = k then 1 else 0:= by
+  rw [← boost_transpose_eq_self]
+  simp only [transpose, transpose_apply]
+  rw [boost_inr_other_inr]
+  exact hij
+
 end LorentzGroup
 
 end

PhysLean/Relativity/Lorentz/RealTensor/Vector/Basic.lean

@@ -31,6 +31,10 @@ abbrev Vector (d : ℕ := 3) := ℝT[d, .up]
 
 namespace Vector
 
+set_option quotPrecheck false in
+/-- The actoin of the Lorentz group on a Lorentz vector. -/
+scoped infixl:60 "•" => ((realLorentzTensor _).F.obj (OverColor.mk ![Color.up])).ρ
+
 /-- The equivalence between the type of indices of a Lorentz vector and
   `Fin 1 ⊕ Fin d`. -/
 def indexEquiv {d : ℕ} :
@@ -72,6 +76,19 @@ lemma toCoord_injective {d : ℕ} : Function.Injective (@toCoord d) := by
 
 instance : CoeFun (Vector d) (fun _ => Fin 1 ⊕ Fin d → ℝ) := ⟨toCoord⟩
 
+lemma toCoord_tprod {d : ℕ} (p : (i : Fin 1) →
+    ↑((realLorentzTensor d).FD.obj { as := ![Color.up] i }).V) (i : Fin 1 ⊕ Fin d) :
+    toCoord (PiTensorProduct.tprod ℝ p) i =
+      ((Lorentz.contrBasisFin d).repr (p 0))
+      (indexEquiv.symm i 0) := by
+  rw [toCoord_apply]
+  simp only [Nat.succ_eq_add_one, Nat.reduceAdd, C_eq_color, OverColor.mk_left, Functor.id_obj,
+    OverColor.mk_hom, Equiv.piCongrLeft'_apply, Finsupp.equivFunOnFinite_apply, Fin.isValue]
+  erw [TensorSpecies.TensorBasis.tensorBasis_repr_tprod]
+  simp only [Finset.univ_unique, Fin.default_eq_zero, Fin.isValue, C_eq_color,
+    Finset.prod_singleton, cons_val_zero]
+  rfl
+
 lemma tensorNode_repr_apply {d : ℕ} (p : Vector d)
     (b : (j : Fin (Nat.succ 0)) → Fin ((realLorentzTensor d).repDim (![Color.up] j))) :
     ((realLorentzTensor d).tensorBasis _).repr p b =
@@ -155,10 +172,10 @@ lemma innerProduct_zero_right {d : ℕ} (p : Vector d) :
 
 @[simp]
 lemma innerProduct_invariant {d : ℕ} (p q : Vector d) (Λ : LorentzGroup d) :
-    ⟪((realLorentzTensor d).F.obj _).ρ Λ p, ((realLorentzTensor d).F.obj _).ρ Λ q⟫ₘ = ⟪p, q⟫ₘ := by
+    ⟪Λ • p, Λ • q⟫ₘ = ⟪p, q⟫ₘ := by
   rw [innerProduct]
   have h1 (q : Vector d) :
-    (tensorNode ((((realLorentzTensor d).F.obj (OverColor.mk ![Color.up])).ρ Λ) q)).tensor
+    (tensorNode (Λ • q)).tensor
     = (action Λ (tensorNode q)).tensor := by simp [action_tensor]
   rw [field]
   rw [contr_tensor_eq <| prod_tensor_eq_snd <| h1 q]
@@ -253,6 +270,62 @@ instance : ChartedSpace (Vector d) (Vector d) := chartedSpaceSelf (Vector d)
 
 end smoothness
 
+/-!
+
+## The Lorentz action
+
+-/
+
+lemma action_apply_eq_sum (i : Fin 1 ⊕ Fin d) (Λ : LorentzGroup d) (p : Vector d) :
+    (Λ • p) i = ∑ j, Λ.1 i j * p j := by
+  revert p
+  refine fun p ↦
+    PiTensorProduct.induction_on' p ?_ (by
+    intro a b hx hy
+    simp at hx hy ⊢
+    rw [hx, hy]
+    simp [mul_add, Finset.sum_add_distrib]
+    ring)
+  intro r p
+  simp only [C_eq_color, TensorSpecies.F_def, Nat.succ_eq_add_one, Nat.reduceAdd, OverColor.mk_left,
+    Functor.id_obj, OverColor.mk_hom, PiTensorProduct.tprodCoeff_eq_smul_tprod, _root_.map_smul,
+    Pi.smul_apply, smul_eq_mul]
+  erw [OverColor.lift.objObj'_ρ_tprod]
+  conv_rhs =>
+    enter [2, x]
+    rw [← mul_assoc, mul_comm _ r, mul_assoc]
+  rw [← Finset.mul_sum]
+  congr
+  simp_all only [Nat.succ_eq_add_one, OverColor.mk_left, _root_.zero_add, Functor.id_obj,
+    C_eq_color, OverColor.mk_hom]
+  erw [toCoord_tprod]
+  change ((contrBasisFin d).repr (Λ *ᵥ _)) _ = _
+  rw [contrBasisFin_repr_apply]
+  rw [ContrMod.mulVec_val]
+  rw [mulVec_eq_sum]
+  simp only [Fin.isValue, op_smul_eq_smul, Nat.succ_eq_add_one, Nat.reduceAdd, Finset.sum_apply,
+    Pi.smul_apply, transpose_apply, smul_eq_mul]
+  congr
+  funext j
+  rw [mul_comm]
+  congr
+  · match i with
+    | Sum.inl 0 => rfl
+    | Sum.inr i => simp [finSumFinEquiv, indexEquiv]
+  · erw [toCoord_tprod]
+    rw [contrBasisFin_repr_apply]
+    congr
+    match j with
+    | Sum.inl 0 => rfl
+    | Sum.inr j => simp [finSumFinEquiv, indexEquiv]
+
+lemma action_toCoord_eq_mulVec {d} (Λ : LorentzGroup d) (p : Vector d) :
+    toCoord (Λ • p) = Λ.1 *ᵥ (toCoord p) := by
+  funext i
+  rw [action_apply_eq_sum, mulVec_eq_sum]
+  simp only [op_smul_eq_smul, Finset.sum_apply, Pi.smul_apply, transpose_apply, smul_eq_mul,
+    mul_comm]
+
 end Vector
 
 end Lorentz

PhysLean/Relativity/Lorentz/RealTensor/Vector/Boosts.lean

@@ -0,0 +1,87 @@
+/-
+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.Relativity.Lorentz.RealTensor.Vector.Basic
+import PhysLean.Relativity.Lorentz.Group.Boosts.Basic
+/-!
+
+## Boosts of Lorentz vectors
+
+These recover what one would describe as the ordinary Lorentz transformations
+of Lorentz vectors.
+
+-/
+
+namespace Lorentz
+open realLorentzTensor
+open LorentzGroup
+variable {d : ℕ}
+
+namespace Vector
+
+lemma boost_time_eq (i : Fin d) (β : ℝ) (hβ : |β| < 1) (p : Vector d) :
+    (boost i β hβ • p) (Sum.inl 0) = γ β * (p (Sum.inl 0) - β * p (Sum.inr i)) := by
+  rw [action_apply_eq_sum]
+  simp [Fin.isValue, Fintype.sum_sum_type, Finset.univ_unique, Fin.default_eq_zero,
+    Finset.sum_singleton]
+  rw [Finset.sum_eq_single i]
+  · simp
+    ring
+  · intro b _ hbi
+    rw [boost_inl_0_inr_other]
+    · simp
+    · exact hbi
+  · simp
+
+lemma boost_inr_self_eq (i : Fin d) (β : ℝ) (hβ : |β| < 1) (p : Vector d) :
+    (boost i β hβ • p) (Sum.inr i) = γ β * (p (Sum.inr i) - β * p (Sum.inl 0)) := by
+  rw [action_apply_eq_sum]
+  simp only [Fintype.sum_sum_type, Finset.univ_unique, Fin.default_eq_zero, Fin.isValue,
+    Finset.sum_singleton, boost_inr_self_inl_0, neg_mul]
+  rw [Finset.sum_eq_single i]
+  · simp only [Fin.isValue, boost_inr_self_inr_self]
+    ring
+  · intro b _ hbi
+    rw [boost_inr_self_inr_other]
+    · simp
+    · exact hbi
+  · simp
+
+lemma boost_inr_other_eq (i j : Fin d) (hji : j ≠ i) (β : ℝ) (hβ : |β| < 1) (p : Vector d) :
+    (boost i β hβ • p) (Sum.inr j) = p (Sum.inr j) := by
+  rw [action_apply_eq_sum]
+  simp only [Fintype.sum_sum_type, Finset.univ_unique, Fin.default_eq_zero, Fin.isValue,
+    Finset.sum_singleton]
+  rw [boost_inr_other_inl_0 hβ hji]
+  rw [Finset.sum_eq_single j]
+  · rw [boost_inr_other_inr hβ hji]
+    simp
+  · intro b _ hbj
+    rw [boost_inr_other_inr hβ hji]
+    rw [if_neg ((Ne.symm hbj))]
+    simp
+  · simp
+
+lemma boost_toCoord_eq (i : Fin d) (β : ℝ) (hβ : |β| < 1) (p : Vector d) :
+    toCoord (boost i β hβ • p) = fun j =>
+      match j with
+      | Sum.inl 0 => γ β * (p (Sum.inl 0) - β * p (Sum.inr i))
+      | Sum.inr j =>
+        if j = i then γ β * (p (Sum.inr i) - β * p (Sum.inl 0))
+        else p (Sum.inr j) := by
+  ext j
+  match j with
+  | Sum.inl 0 => rw [boost_time_eq]
+  | Sum.inr j =>
+    by_cases hj : j = i
+    · subst hj
+      rw [boost_inr_self_eq]
+      simp
+    · rw [boost_inr_other_eq _ _ hj]
+      simp [hj]
+
+end Vector
+
+end Lorentz

PhysLean/Relativity/Lorentz/RealTensor/Vector/Pre/Basic.lean

@@ -53,6 +53,9 @@ lemma contrBasisFin_toFin1dℝ {d : ℕ} (i : Fin (1 + d)) :
     (contrBasisFin d i).toFin1dℝ = Pi.single (finSumFinEquiv.symm i) 1 := by
   simp only [contrBasisFin, Basis.reindex_apply, contrBasis_toFin1dℝ, Basis.coe_ofEquivFun]
 
+lemma contrBasisFin_repr_apply {d : ℕ} (p : Contr d) (i : Fin (1 + d)) :
+    (contrBasisFin d).repr p i = p.val (finSumFinEquiv.symm i) := by rfl
+
 /-- The representation of contravariant Lorentz vectors forms a topological space, induced
   by its equivalence to `Fin 1 ⊕ Fin d → ℝ`. -/
 instance : TopologicalSpace (Contr d) := TopologicalSpace.induced

PhysLean/Relativity/Lorentz/RealTensor/Vector/Pre/Modules.lean

@@ -144,6 +144,11 @@ lemma mulVec_toFin1dℝ (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) (v
     (M *ᵥ v).toFin1dℝ = M *ᵥ v.toFin1dℝ := by
   rfl
 
+@[simp]
+lemma mulVec_val (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) (v : ContrMod d) :
+    (M *ᵥ v).val = M *ᵥ v.val := by
+  rfl
+
 lemma mulVec_sub (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) (v w : ContrMod d) :
     M *ᵥ (v - w) = M *ᵥ v - M *ᵥ w := by
   simp only [mulVec, LinearMap.map_sub]

lakefile.toml

@@ -98,11 +98,6 @@ name = "redundent_imports"
 supportInterpreter = true
 srcDir = "scripts/MetaPrograms"
 
-[[lean_exe]]
-name = "Spelling"
-supportInterpreter = true
-srcDir = "scripts/MetaPrograms"
-
 # -- Optional inclusion of openAI_doc_check. Needs `llm` above.
 #[[lean_exe]]
 #name = "openAI_doc_check"