Merge pull request #416 from HEPLean/bump

feat: Add ordinary Lorentz boosts

.github/ISSUE_TEMPLATE/Bump.yml

@@ -30,7 +30,7 @@ body:
     label: Scripts
     description: Please check off these items as you complete them
     options:
-      - label: Ensure `lake exe hepLen_style_lint` runs without errors.
+      - label: Ensure `lake exe hepLean_style_lint` runs without errors.
       - label: Ensure `lake exe TODO_to_yml mkFile` runs without errors.
       - label: Ensure `lake exe stats mkHTML` runs without errors.
       - label: Ensure `lake exe informal mkFile mkDot mkHTML` runs without errors.

PhysLean.lean

@@ -180,7 +180,8 @@ import PhysLean.Relativity.Lorentz.ComplexVector.Modules
 import PhysLean.Relativity.Lorentz.ComplexVector.Two
 import PhysLean.Relativity.Lorentz.ComplexVector.Unit
 import PhysLean.Relativity.Lorentz.Group.Basic
-import PhysLean.Relativity.Lorentz.Group.Boosts
+import PhysLean.Relativity.Lorentz.Group.Boosts.Basic
+import PhysLean.Relativity.Lorentz.Group.Boosts.Generalized
 import PhysLean.Relativity.Lorentz.Group.Orthochronous
 import PhysLean.Relativity.Lorentz.Group.Proper
 import PhysLean.Relativity.Lorentz.Group.Restricted

PhysLean/Electromagnetism/MaxwellEquations.lean

@@ -48,18 +48,18 @@ def GaussLawElectric (E : ElectricField) : Prop :=
 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, ∇× B x = μ₀ • (J x + ε₀ • ∂ₜ E x)
+
+/-- Faraday's law. -/
+def FaradayLaw (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
+  FaradayLaw E B ∧ 𝓔.AmpereLaw E B
 
 end EMSystem
 end Electromagnetism

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

@@ -0,0 +1,233 @@
+/-
+Copyright (c) 2024 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.Pre.NormOne
+import PhysLean.Relativity.Lorentz.Group.Proper
+/-!
+# Boosts in the Lorentz group
+
+-/
+
+noncomputable section
+
+open Matrix
+open Complex
+open ComplexConjugate
+
+namespace LorentzGroup
+
+variable {d : ℕ}
+variable (Λ : LorentzGroup d)
+
+/-- 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 j = k then 1 else 0, h⟩
+where
+  h := by
+    rw [mem_iff_dual_mul_self]
+    ext j k
+    rw [Matrix.mul_apply]
+    conv_lhs =>
+      enter [2, x]
+      rw [minkowskiMatrix.dual_apply]
+    simp only [Fintype.sum_sum_type, Finset.univ_unique, Fin.default_eq_zero, Fin.isValue,
+      Finset.sum_singleton]
+    rw [minkowskiMatrix.inl_0_inl_0]
+    simp only [Fin.isValue, and_true, one_div, reduceCtorEq, and_false, ↓reduceIte, neg_mul,
+      mul_ite, mul_neg, mul_one, mul_zero, ite_mul, zero_mul, Sum.inr.injEq]
+    conv_lhs =>
+      enter [2, 2, x]
+      rw [minkowskiMatrix.inr_i_inr_i]
+    simp only [Fin.isValue, mul_neg, mul_one, neg_mul, neg_neg]
+    have hb1 : √(1 - β ^ 2) ^ 2 = 1 - β ^ 2 := by
+      refine Real.sq_sqrt ?_
+      simp only [sub_nonneg, sq_le_one_iff_abs_le_one]
+      exact le_of_lt hβ
+    have hb2 : 1 - β ^ 2 ≠ 0 := by
+      simp only [ne_eq, sub_ne_zero]
+      by_contra h
+      have hl : 1 ^ 2 = β ^ 2 := by
+        rw [← h]
+        simp
+      rw [sq_eq_sq_iff_abs_eq_abs] at hl
+      rw [← hl] at hβ
+      simp at hβ
+    by_cases hj : j = Sum.inl 0
+    · subst hj
+      simp only [Fin.isValue, ↓reduceIte, minkowskiMatrix.inl_0_inl_0, one_mul, true_and,
+        reduceCtorEq, false_and]
+      rw [Finset.sum_eq_single i]
+      · simp
+        by_cases hk : k = Sum.inl 0
+        · subst hk
+          simp only [Fin.isValue, ↓reduceIte, one_apply_eq]
+          ring_nf
+          field_simp [hb1, hb2]
+          ring
+        · 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,
+            one_apply_ne]
+            ring
+          · simp only [hk', ↓reduceIte, Fin.isValue]
+            rw [one_apply_ne fun a => hk (id (Eq.symm a))]
+            rw [if_neg (by exact fun a => hk (id (Eq.symm a)))]
+            rw [if_neg (by exact fun a => hk' (id (Eq.symm a)))]
+            simp
+      · intro b _ hb
+        simp [hb]
+      · simp
+    · match j with
+      | Sum.inl 0 => simp at hj
+      | Sum.inr j =>
+      rw [minkowskiMatrix.inr_i_inr_i, Finset.sum_eq_single j]
+      · by_cases hj' : j = i
+        · subst hj'
+          conv_lhs =>
+            enter [1, 1, 2]
+            simp only [Fin.isValue]
+          conv_lhs =>
+            enter [2, 1, 1, 2]
+            simp only [Fin.isValue]
+          match k with
+          | Sum.inl 0 =>
+            simp only [Fin.isValue, ↓reduceIte, reduceCtorEq, neg_mul, one_mul, neg_neg, and_self,
+              and_true, ne_eq, not_false_eq_true, one_apply_ne]
+            ring
+          | Sum.inr k =>
+          by_cases hk : k = j
+          · subst hk
+            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
+          · 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]
+            rw [if_neg (fun a => hk (id (Eq.symm a))), if_neg (fun a => hk (id (Eq.symm a)))]
+        · conv_lhs =>
+            enter [1, 1, 2]
+            simp only [Fin.isValue]
+          conv_lhs =>
+            enter [2, 1, 1, 2]
+            simp only [Fin.isValue]
+          rw [one_apply]
+          simp [hj']
+      · intro b _ hb
+        simp only [Fin.isValue, one_div, neg_mul, reduceCtorEq, and_self, ↓reduceIte,
+          Sum.inr.injEq, false_and, and_false, hb, mul_ite, one_mul, mul_zero, mul_neg, ite_mul,
+          zero_mul, mul_one]
+        match k with
+        | Sum.inl 0 =>
+          simp only [Fin.isValue, true_and, neg_neg, reduceCtorEq, false_and, ↓reduceIte,
+            ite_eq_right_iff, neg_eq_zero, mul_eq_zero, inv_eq_zero, or_self_left, and_imp]
+          intro h1 h2
+          subst h1 h2
+          simp at hb
+        | Sum.inr k =>
+        simp only [Fin.isValue, reduceCtorEq, false_and, ↓reduceIte, Sum.inr.injEq, neg_neg]
+        by_cases hb' : b = i
+        · simp only [hb', and_true]
+          subst hb'
+          simp [Ne.symm hb]
+        · simp [hb']
+      · simp
+
+@[simp]
+lemma boost_transpose_eq_self (i : Fin d) {β : ℝ} (hβ : |β| < 1) :
+    transpose (boost i β hβ) = boost i β hβ := by
+  ext j k
+  simp [transpose, boost]
+  match j, k with
+  | Sum.inl 0, Sum.inl 0 => rfl
+  | Sum.inl 0, Sum.inr k =>
+    simp
+  | Sum.inr i, Sum.inl 0 =>
+    simp
+  | Sum.inr j, Sum.inr k =>
+    simp only [Fin.isValue, reduceCtorEq, and_self, ↓reduceIte, Sum.inr.injEq, false_and, and_false]
+    conv_lhs =>
+      enter [1]
+      rw [and_comm]
+    conv_lhs =>
+      enter [3, 1]
+      rw [eq_comm]
+
+@[simp]
+lemma boost_transpose_matrix_eq_self (i : Fin d) {β : ℝ} (hβ : |β| < 1) :
+    Matrix.transpose (boost i β hβ).1 = (boost i β hβ).1 := by
+  rw [← transpose_val, boost_transpose_eq_self]
+
+@[simp]
+lemma boost_zero_eq_id (i : Fin d) : boost i 0 (by simp) = 1 := by
+  ext j k
+  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.inr k =>
+    simp
+  | Sum.inr i, Sum.inl 0 =>
+    simp
+  | Sum.inr j, Sum.inr k =>
+    rw [one_apply]
+    simp only [Fin.isValue, reduceCtorEq, and_self, ↓reduceIte, Sum.inr.injEq, false_and, and_false,
+      ite_eq_right_iff, and_imp]
+    intro h1 h2
+    subst h1 h2
+    simp
+
+lemma boost_inverse (i : Fin d) {β : ℝ} (hβ : |β| < 1) :
+    (boost i β hβ)⁻¹ = boost i (-β) (by simpa using hβ) := by
+  rw [lorentzGroupIsGroup_inv]
+  ext j k
+  simp only
+  rw [minkowskiMatrix.dual_apply]
+  match j, k with
+  | Sum.inl 0, Sum.inl 0 =>
+    rw [minkowskiMatrix.inl_0_inl_0]
+    simp [boost]
+  | Sum.inl 0, Sum.inr k =>
+    rw [minkowskiMatrix.inl_0_inl_0, minkowskiMatrix.inr_i_inr_i]
+    simp only [boost, Fin.isValue, one_div, neg_mul, reduceCtorEq, and_false, ↓reduceIte,
+      Sum.inr.injEq, true_and, and_self, false_and, mul_ite, mul_neg, one_mul, mul_zero, mul_one,
+      even_two, Even.neg_pow, neg_neg, and_true]
+    split
+    · simp
+    · simp
+  | Sum.inr j, Sum.inl 0 =>
+    rw [minkowskiMatrix.inl_0_inl_0, minkowskiMatrix.inr_i_inr_i]
+    simp [boost]
+  | Sum.inr j, Sum.inr k =>
+    rw [minkowskiMatrix.inr_i_inr_i, minkowskiMatrix.inr_i_inr_i]
+    simp only [boost, Fin.isValue, one_div, neg_mul, reduceCtorEq, and_self, ↓reduceIte,
+      Sum.inr.injEq, false_and, and_false, mul_ite, one_mul, mul_one, mul_zero, mul_neg, even_two,
+      Even.neg_pow, neg_neg]
+    split
+    · simp
+      rw [if_pos]
+      simp_all
+    · rename_i h
+      conv_rhs =>
+        rw [if_neg (fun a => h (And.symm a))]
+      split
+      · rename_i h2
+        rw [if_pos (Eq.symm h2)]
+        simp
+      · rename_i h2
+        rw [if_neg (fun a => h2 (Eq.symm a))]
+        simp
+
+end LorentzGroup
+
+end

lakefile.toml

@@ -98,6 +98,10 @@ 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]]