perf(PauliMatrices): evaluate Levi-Civita components as a product of signs

Physlib/Mathematics/LeviCivita/Basic.lean

@@ -7,6 +7,7 @@ module
 
 public import Physlib.Mathematics.KroneckerDelta.Basic
 public import Mathlib.LinearAlgebra.Matrix.Permutation
+public import Mathlib.GroupTheory.Perm.Fin
 /-!
 
 # The Levi-Civita symbol in general dimension
@@ -32,13 +33,16 @@ permutation via `Matrix.det_permutation`.
 - `leviCivitaSymbol_comp_swap` : antisymmetry under transposition of two indices.
 - `leviCivitaSymbol_swap_comp` : antisymmetry under transposition of two index values.
 - `leviCivitaSymbol_eq_zero_iff` : the symbol vanishes exactly on repeated indices.
+- `leviCivitaSymbol_eq_prod_prod_Ioi` : on `Fin n` the symbol is the product over pairs
+  `i < j` of the sign of `g j - g i`.
 
 ## iii. Table of contents
 
 - A. Definition
 - B. Value on permutations
 - C. Antisymmetry
 - D. Vanishing on repeated indices
+- E. Closed form on `Fin n`
 
 ## iv. References
 
@@ -150,3 +154,33 @@ lemma leviCivitaSymbol_eq_zero_iff {g : ι → ι} :
     ⟨Equiv.ofBijective g (Finite.injective_iff_bijective.mp hinj), rfl⟩
   rw [leviCivitaSymbol_perm] at h
   exact Units.ne_zero (Equiv.Perm.sign σ) h
+
+/-!
+
+## E. Closed form on `Fin n`
+
+-/
+
+/-- On `Fin n` the Levi-Civita symbol is the product over pairs `i < j` of the sign of
+`g j - g i`. Unlike the determinant defining `leviCivitaSymbol`, this product is cheap to
+evaluate, e.g. by `decide`. -/
+lemma leviCivitaSymbol_eq_prod_prod_Ioi {n : ℕ} (g : Fin n → Fin n) :
+    leviCivitaSymbol g =
+      ∏ i, ∏ j ∈ Finset.Ioi i, (if g i < g j then 1 else if g i = g j then 0 else -1) := by
+  by_cases hg : Function.Injective g
+  · obtain ⟨σ, rfl⟩ : ∃ σ : Equiv.Perm (Fin n), ⇑σ = g :=
+      ⟨Equiv.ofBijective g (Finite.injective_iff_bijective.mp hg), rfl⟩
+    rw [leviCivitaSymbol_perm, Equiv.Perm.sign_eq_prod_prod_Ioi]
+    simp only [Units.coe_prod]
+    refine Finset.prod_congr rfl fun i _ => Finset.prod_congr rfl fun j hj => ?_
+    have hij : σ i ≠ σ j := σ.injective.ne (Finset.mem_Ioi.mp hj).ne
+    split_ifs <;> simp
+  · rw [leviCivitaSymbol_eq_zero_of_not_injective hg]
+    simp only [Function.Injective, not_forall] at hg
+    obtain ⟨i, j, hgij, hij⟩ := hg
+    symm
+    rcases lt_or_gt_of_ne hij with h | h
+    · exact Finset.prod_eq_zero (Finset.mem_univ i)
+        (Finset.prod_eq_zero (Finset.mem_Ioi.mpr h) (by simp [hgij]))
+    · exact Finset.prod_eq_zero (Finset.mem_univ j)
+        (Finset.prod_eq_zero (Finset.mem_Ioi.mpr h) (by simp [hgij]))

Physlib/Relativity/PauliMatrices/Relations.lean

@@ -166,10 +166,10 @@ lemma leviCivita_mul_pauliDual :
     ({ε4ℂ | μ ν ρ κ ⊗ σ^^^ | τ(κ) α β =
       ε4ℂ | μ ν ρ κ ⊗ σ_^^ | κ α β}ᵀ : Prop) := by
   conv_lhs =>
-    simp only [leviCivita_eq_ofRat, toTensor_dualLorentz_eq_ofRat]
+    simp only [leviCivita_eq_ofRat_prod, toTensor_dualLorentz_eq_ofRat]
     rw [prodT_ofRat_ofRat, contrT_ofRat]
   conv_rhs =>
-    simp only [leviCivita_eq_ofRat, pauliCo_eq_ofRat]
+    simp only [leviCivita_eq_ofRat_prod, pauliCo_eq_ofRat]
     rw [prodT_ofRat_ofRat, contrT_ofRat]
   apply (Tensor.basis _).repr.injective
   ext b
@@ -192,15 +192,15 @@ lemma pauliContr_mul_pauliContrDown_mul_pauliContr : ({
   conv_rhs =>
     rw [leviCivita_mul_pauliDual]
     simp only [contrMetric_eq_ofRat, toTensor_eq_ofRat, prodT_ofRat_ofRat]
-    simp only [leviCivita_eq_ofRat, pauliCo_eq_ofRat]
+    simp only [leviCivita_eq_ofRat_prod, pauliCo_eq_ofRat]
     rw [prodT_ofRat_ofRat, contrT_ofRat, permT_ofRat]
   apply (Tensor.basis _).repr.injective
   ext b
   rw [ofRat_basis_repr_apply, permT_basis_repr_symm_apply]
   simp only [map_add, Finsupp.coe_add, Pi.add_apply]
   simp only [permT_basis_repr_symm_apply, map_neg, Finsupp.coe_neg, Pi.neg_apply,
     map_smul, Finsupp.coe_smul, Pi.smul_apply, smul_eq_mul, ofRat_basis_repr_apply]
-  rw [Physlib.RatComplexNum.I_mul_toComplexNum]
+  conv_rhs => arg 2; rw [Physlib.RatComplexNum.I_mul_toComplexNum]
   apply Physlib.RatComplexNum.toComplexNum_eq_add_neg_add_add_iff.mpr
   decide +revert +kernel
 
@@ -219,15 +219,15 @@ lemma pauliContrDown_mul_pauliContr_mul_pauliContrDown : ({
       prodT_ofRat_ofRat, contrT_ofRat]
   conv_rhs =>
     simp only [contrMetric_eq_ofRat, toTensor_dualWeyl_eq_ofRat, prodT_ofRat_ofRat]
-    simp only [leviCivita_eq_ofRat, toTensor_dualAll_eq_ofRat]
+    simp only [leviCivita_eq_ofRat_prod, toTensor_dualAll_eq_ofRat]
     rw [prodT_ofRat_ofRat, contrT_ofRat, permT_ofRat]
   apply (Tensor.basis _).repr.injective
   ext b
   rw [ofRat_basis_repr_apply, permT_basis_repr_symm_apply]
   simp only [map_add, Finsupp.coe_add, Pi.add_apply]
   simp only [permT_basis_repr_symm_apply, map_neg, Finsupp.coe_neg, Pi.neg_apply,
     map_smul, Finsupp.coe_smul, Pi.smul_apply, smul_eq_mul, ofRat_basis_repr_apply]
-  rw [Physlib.RatComplexNum.neg_I_mul_toComplexNum]
+  conv_rhs => arg 2; rw [Physlib.RatComplexNum.neg_I_mul_toComplexNum]
   apply Physlib.RatComplexNum.toComplexNum_eq_add_neg_add_add_iff.mpr
   decide +revert +kernel
 

Physlib/Relativity/Tensors/LeviCivita/Complex.lean

@@ -101,4 +101,21 @@ lemma leviCivita_eq_ofRat : ε4ℂ = ofRat (fun
     (b (IsReindexing.inv id leviCivita_isReindexing i))).trans
     (congrArg (fun x => (b x).val) (hinv i))
 
+/-- The components of the complex Levi-Civita tensor as the product over pairs `i < j` of the
+sign of `b j - b i`, from `leviCivitaSymbol_eq_prod_prod_Ioi`. Unlike the determinant appearing
+in `leviCivita_eq_ofRat`, these components are cheap to evaluate, e.g. by `decide`. -/
+lemma leviCivita_eq_ofRat_prod : ε4ℂ = ofRat (fun
+    b : ComponentIdx (S := complexLorentzTensor) ![Color.up, Color.up, Color.up, Color.up] =>
+    ⟨((∏ i : Fin 4, ∏ j ∈ Finset.Ioi i,
+      (if (Fin.cast (by fin_cases i <;> rfl) (b i) : Fin 4) <
+          (Fin.cast (by fin_cases j <;> rfl) (b j) : Fin 4) then 1
+        else if (Fin.cast (by fin_cases i <;> rfl) (b i) : Fin 4) =
+          (Fin.cast (by fin_cases j <;> rfl) (b j) : Fin 4) then 0 else -1) : ℤ) : ℚ), 0⟩) := by
+  rw [leviCivita_eq_ofRat]
+  refine congrArg ofRat (funext fun b => ?_)
+  have h := leviCivitaSymbol_eq_prod_prod_Ioi
+    (fun i : Fin 4 => (Fin.cast (by fin_cases i <;> rfl) (b i) : Fin 4))
+  rw [← h]
+  rfl
+
 end complexLorentzTensor