From 049370513d1367e127ae36fe6717da0069d04bc4 Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Wed, 26 Jun 2024 14:04:18 -0400 Subject: [PATCH 1/5] refactor: Create Mathematics folder --- HepLean.lean | 4 ++-- HepLean/AnomalyCancellation/Basic.lean | 2 +- HepLean/{AnomalyCancellation => Mathematics}/LinearMaps.lean | 0 HepLean/{GroupTheory => Mathematics}/SO3/Basic.lean | 0 HepLean/SpaceTime/LorentzGroup/Rotations.lean | 2 +- 5 files changed, 4 insertions(+), 4 deletions(-) rename HepLean/{AnomalyCancellation => Mathematics}/LinearMaps.lean (100%) rename HepLean/{GroupTheory => Mathematics}/SO3/Basic.lean (100%) diff --git a/HepLean.lean b/HepLean.lean index ee22052..5cbd5d9 100644 --- a/HepLean.lean +++ b/HepLean.lean @@ -1,6 +1,5 @@ import HepLean.AnomalyCancellation.Basic import HepLean.AnomalyCancellation.GroupActions -import HepLean.AnomalyCancellation.LinearMaps import HepLean.AnomalyCancellation.MSSMNu.B3 import HepLean.AnomalyCancellation.MSSMNu.Basic import HepLean.AnomalyCancellation.MSSMNu.HyperCharge @@ -59,7 +58,8 @@ import HepLean.FlavorPhysics.CKMMatrix.Relations import HepLean.FlavorPhysics.CKMMatrix.Rows import HepLean.FlavorPhysics.CKMMatrix.StandardParameterization.Basic import HepLean.FlavorPhysics.CKMMatrix.StandardParameterization.StandardParameters -import HepLean.GroupTheory.SO3.Basic +import HepLean.Mathematics.SO3.Basic +import HepLean.Mathematics.LinearMaps import HepLean.SpaceTime.AsSelfAdjointMatrix import HepLean.SpaceTime.Basic import HepLean.SpaceTime.CliffordAlgebra diff --git a/HepLean/AnomalyCancellation/Basic.lean b/HepLean/AnomalyCancellation/Basic.lean index 9014d50..c44b98f 100644 --- a/HepLean/AnomalyCancellation/Basic.lean +++ b/HepLean/AnomalyCancellation/Basic.lean @@ -3,7 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved. Released under Apache 2.0 license. Authors: Joseph Tooby-Smith -/ -import HepLean.AnomalyCancellation.LinearMaps +import HepLean.Mathematics.LinearMaps import Mathlib.Algebra.Module.Basic import Mathlib.LinearAlgebra.FiniteDimensional /-! diff --git a/HepLean/AnomalyCancellation/LinearMaps.lean b/HepLean/Mathematics/LinearMaps.lean similarity index 100% rename from HepLean/AnomalyCancellation/LinearMaps.lean rename to HepLean/Mathematics/LinearMaps.lean diff --git a/HepLean/GroupTheory/SO3/Basic.lean b/HepLean/Mathematics/SO3/Basic.lean similarity index 100% rename from HepLean/GroupTheory/SO3/Basic.lean rename to HepLean/Mathematics/SO3/Basic.lean diff --git a/HepLean/SpaceTime/LorentzGroup/Rotations.lean b/HepLean/SpaceTime/LorentzGroup/Rotations.lean index c4a861d..605d025 100644 --- a/HepLean/SpaceTime/LorentzGroup/Rotations.lean +++ b/HepLean/SpaceTime/LorentzGroup/Rotations.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license. Authors: Joseph Tooby-Smith -/ import HepLean.SpaceTime.LorentzGroup.Basic -import HepLean.GroupTheory.SO3.Basic +import HepLean.Mathematics.SO3.Basic import Mathlib.Topology.Constructions /-! # Rotations From 04df500fae153185d70585c85d6b35b9207d7da3 Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Thu, 27 Jun 2024 07:00:53 -0400 Subject: [PATCH 2/5] feat: Add matrix rank --- HepLean/Mathematics/Matrices/Rank.lean | 85 ++++++++++++++++++++++++++ 1 file changed, 85 insertions(+) create mode 100644 HepLean/Mathematics/Matrices/Rank.lean diff --git a/HepLean/Mathematics/Matrices/Rank.lean b/HepLean/Mathematics/Matrices/Rank.lean new file mode 100644 index 0000000..28e098f --- /dev/null +++ b/HepLean/Mathematics/Matrices/Rank.lean @@ -0,0 +1,85 @@ +/- +Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved. +Released under Apache 2.0 license. +Authors: Joseph Tooby-Smith +-/ +import Mathlib.LinearAlgebra.UnitaryGroup +import Mathlib.Data.Complex.Exponential +import Mathlib.Tactic.Polyrith +import LeanCopilot +/-! + +# Rank of matrices + +This field contains addiational lemmas and results about the rank of matrices beyond +those which appear in Mathlib. + +Our method is to provide a certificate checker for the rank of the matrix. + +## TODO + +- Automate, following the method of `polyrith`, the process of finding the + row-reduced form of a matrix. + +-/ + +namespace Mathematics +variable {n m : ℕ} +open Matrix + +/-- The proposition on a matrix for it to be in row echelon form. -/ +def IsRowEchelonForm (M : Matrix (Fin n) (Fin m) ℚ) : Prop := + ∀ i j, i < j → + match Fin.find (fun k => M i k ≠ 0), Fin.find (fun k => M j k ≠ 0) with + | some i', some j' => i' < j' + | some _, none => true + | none, some _ => false + | none, none => true + +instance (M : Matrix (Fin n) (Fin m) ℚ) : Decidable (IsRowEchelonForm M) := by + refine @Fintype.decidableForallFintype _ _ (fun i => ?_) _ + refine @Fintype.decidableForallFintype _ _ (fun j => ?_) _ + refine @instDecidableForall _ _ (i.decLt j) ?_ + match Fin.find (fun k => M i k ≠ 0), Fin.find (fun k => M j k ≠ 0) with + | some i', some j' => exact i'.decLt j' + | some _, none => exact true.decEq true + | none, some _ => exact false.decEq true + | none, none => exact true.decEq true + +example : IsRowEchelonForm !![1, 2, 3; 0, 1, 3; 0, 0, 1] := by + decide + +example : ¬ IsRowEchelonForm !![1, 2, 3; 0, 1, 3; 0, 2, 1] := by + decide + +/-- `M` is a row echelon form of `N`. -/ +structure RowEchelonFormOf (M : Matrix (Fin n) (Fin m) ℚ) where + rowEchelonForm : Matrix (Fin n) (Fin m) ℚ + transform : Matrix (Fin n) (Fin n) ℚ + transformInv : Matrix (Fin n) (Fin n) ℚ + transform_invert : transform * transformInv = 1 := by norm_num <;> decide + transform_mul : transform * M = rowEchelonForm := by norm_num + rowEchelonForm_isRowEchelonForm : IsRowEchelonForm rowEchelonForm := by decide + +def sageRowEchelonFormQuery (M : Matrix (Fin n) (Fin m) ℚ) : IO Unit := + let M := List.map (fun i => + String.intercalate ", " (List.map (fun j => toString (M i j)) (Fin.list m))) (Fin.list n) + let echelonForm := +"M = Matrix([[" ++ String.intercalate "],[" M ++ "]]) +REF, P = M.echelon_form(transformation=True) +def format(matrix): + rows = [] + for row in matrix.rows(): + rows.append(', '.join(map(str, row))) + return \"!![\" + \"; \".join(rows) + \"]\" +print(f\"rowEchelonForm := {format(REF)}\") +print(f\"transform := {format(P)}\") +print(f\"transformInv := {format(P.inverse())}\")" + IO.println (echelonForm) + +def myTestMatrix : RowEchelonFormOf !![1, 2, 3; 4, 5, 6; 7, 8, 9; 10, 11, 12] where + rowEchelonForm := !![1, 2, 3; 0, 3, 6; 0, 0, 0; 0, 0, 0] + transform := !![0, 0, 3, -2; 0, 0, 10, -7; 1, 0, -3, 2; 0, 1, -2, 1] + transformInv := !![1, 0, 1, 0; 4, -1, 0, 1; 7, -2, 0, 0; 10, -3, 0, 0] + +end Mathematics From f92291885a9b44314b33c61e8ce4672e7f7817a0 Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Thu, 27 Jun 2024 08:43:57 -0400 Subject: [PATCH 3/5] remove matrix.rank file --- HepLean/Mathematics/Matrices/Rank.lean | 85 -------------------------- scripts/check_file_imports.lean | 5 +- 2 files changed, 1 insertion(+), 89 deletions(-) delete mode 100644 HepLean/Mathematics/Matrices/Rank.lean diff --git a/HepLean/Mathematics/Matrices/Rank.lean b/HepLean/Mathematics/Matrices/Rank.lean deleted file mode 100644 index 28e098f..0000000 --- a/HepLean/Mathematics/Matrices/Rank.lean +++ /dev/null @@ -1,85 +0,0 @@ -/- -Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved. -Released under Apache 2.0 license. -Authors: Joseph Tooby-Smith --/ -import Mathlib.LinearAlgebra.UnitaryGroup -import Mathlib.Data.Complex.Exponential -import Mathlib.Tactic.Polyrith -import LeanCopilot -/-! - -# Rank of matrices - -This field contains addiational lemmas and results about the rank of matrices beyond -those which appear in Mathlib. - -Our method is to provide a certificate checker for the rank of the matrix. - -## TODO - -- Automate, following the method of `polyrith`, the process of finding the - row-reduced form of a matrix. - --/ - -namespace Mathematics -variable {n m : ℕ} -open Matrix - -/-- The proposition on a matrix for it to be in row echelon form. -/ -def IsRowEchelonForm (M : Matrix (Fin n) (Fin m) ℚ) : Prop := - ∀ i j, i < j → - match Fin.find (fun k => M i k ≠ 0), Fin.find (fun k => M j k ≠ 0) with - | some i', some j' => i' < j' - | some _, none => true - | none, some _ => false - | none, none => true - -instance (M : Matrix (Fin n) (Fin m) ℚ) : Decidable (IsRowEchelonForm M) := by - refine @Fintype.decidableForallFintype _ _ (fun i => ?_) _ - refine @Fintype.decidableForallFintype _ _ (fun j => ?_) _ - refine @instDecidableForall _ _ (i.decLt j) ?_ - match Fin.find (fun k => M i k ≠ 0), Fin.find (fun k => M j k ≠ 0) with - | some i', some j' => exact i'.decLt j' - | some _, none => exact true.decEq true - | none, some _ => exact false.decEq true - | none, none => exact true.decEq true - -example : IsRowEchelonForm !![1, 2, 3; 0, 1, 3; 0, 0, 1] := by - decide - -example : ¬ IsRowEchelonForm !![1, 2, 3; 0, 1, 3; 0, 2, 1] := by - decide - -/-- `M` is a row echelon form of `N`. -/ -structure RowEchelonFormOf (M : Matrix (Fin n) (Fin m) ℚ) where - rowEchelonForm : Matrix (Fin n) (Fin m) ℚ - transform : Matrix (Fin n) (Fin n) ℚ - transformInv : Matrix (Fin n) (Fin n) ℚ - transform_invert : transform * transformInv = 1 := by norm_num <;> decide - transform_mul : transform * M = rowEchelonForm := by norm_num - rowEchelonForm_isRowEchelonForm : IsRowEchelonForm rowEchelonForm := by decide - -def sageRowEchelonFormQuery (M : Matrix (Fin n) (Fin m) ℚ) : IO Unit := - let M := List.map (fun i => - String.intercalate ", " (List.map (fun j => toString (M i j)) (Fin.list m))) (Fin.list n) - let echelonForm := -"M = Matrix([[" ++ String.intercalate "],[" M ++ "]]) -REF, P = M.echelon_form(transformation=True) -def format(matrix): - rows = [] - for row in matrix.rows(): - rows.append(', '.join(map(str, row))) - return \"!![\" + \"; \".join(rows) + \"]\" -print(f\"rowEchelonForm := {format(REF)}\") -print(f\"transform := {format(P)}\") -print(f\"transformInv := {format(P.inverse())}\")" - IO.println (echelonForm) - -def myTestMatrix : RowEchelonFormOf !![1, 2, 3; 4, 5, 6; 7, 8, 9; 10, 11, 12] where - rowEchelonForm := !![1, 2, 3; 0, 3, 6; 0, 0, 0; 0, 0, 0] - transform := !![0, 0, 3, -2; 0, 0, 10, -7; 1, 0, -3, 2; 0, 1, -2, 1] - transformInv := !![1, 0, 1, 0; 4, -1, 0, 1; 7, -2, 0, 0; 10, -3, 0, 0] - -end Mathematics diff --git a/scripts/check_file_imports.lean b/scripts/check_file_imports.lean index ec21e44..394826c 100644 --- a/scripts/check_file_imports.lean +++ b/scripts/check_file_imports.lean @@ -22,11 +22,9 @@ The functions are adapted from `batteries.scripts.check_imports.lean` authored by Joe Hendrix. - -/ open Lean System Meta - /-- Recursively finds files in directory. -/ partial def addModulesIn (recurse : Bool) (prev : Array Name) (root : Name := .anonymous) (path : FilePath) : IO (Array Name) := do @@ -41,7 +39,6 @@ partial def addModulesIn (recurse : Bool) (prev : Array Name) (root : Name := .a r := r.push (root.mkStr mod) pure r - /-- Compute imports expected by `HepLean.lean` by looking at file structure. -/ def expectedHepLeanImports : IO (Array Name) := do let mut needed := #[] @@ -80,7 +77,7 @@ def checkMissingImports (modData : ModuleData) (reqImports : Array Name) : def main (_ : List String) : IO UInt32 := do initSearchPath (← findSysroot) let mods : Name := `HepLean - let imp : Import := {module := mods} + let imp : Import := {module := mods} let mFile ← findOLean imp.module unless (← mFile.pathExists) do throw <| IO.userError s!"object file '{mFile}' of module {imp.module} does not exist" From fc6db7354bb6c90b161fa014399443fd82cde687 Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Thu, 27 Jun 2024 08:48:09 -0400 Subject: [PATCH 4/5] refactor: Lint --- HepLean.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/HepLean.lean b/HepLean.lean index 5cbd5d9..7940592 100644 --- a/HepLean.lean +++ b/HepLean.lean @@ -58,8 +58,8 @@ import HepLean.FlavorPhysics.CKMMatrix.Relations import HepLean.FlavorPhysics.CKMMatrix.Rows import HepLean.FlavorPhysics.CKMMatrix.StandardParameterization.Basic import HepLean.FlavorPhysics.CKMMatrix.StandardParameterization.StandardParameters -import HepLean.Mathematics.SO3.Basic import HepLean.Mathematics.LinearMaps +import HepLean.Mathematics.SO3.Basic import HepLean.SpaceTime.AsSelfAdjointMatrix import HepLean.SpaceTime.Basic import HepLean.SpaceTime.CliffordAlgebra From 99a915d31583e4538dd2ef0ece6b2cb463da4582 Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Thu, 27 Jun 2024 08:49:13 -0400 Subject: [PATCH 5/5] style: Remove some extra spaces --- HepLean/FlavorPhysics/CKMMatrix/PhaseFreedom.lean | 2 -- 1 file changed, 2 deletions(-) diff --git a/HepLean/FlavorPhysics/CKMMatrix/PhaseFreedom.lean b/HepLean/FlavorPhysics/CKMMatrix/PhaseFreedom.lean index 90dbf32..974f81d 100644 --- a/HepLean/FlavorPhysics/CKMMatrix/PhaseFreedom.lean +++ b/HepLean/FlavorPhysics/CKMMatrix/PhaseFreedom.lean @@ -224,7 +224,6 @@ lemma ubOnePhaseCond_shift_solution {V : CKMMatrix} (h1 : a + f = - arg [V]ub) subst hc ring --- rename lemma fstRowThdColRealCond_holds_up_to_equiv (V : CKMMatrix) : ∃ (U : CKMMatrix), V ≈ U ∧ FstRowThdColRealCond U:= by obtain ⟨τ, hτ⟩ := V.uRow_cross_cRow_eq_tRow @@ -319,7 +318,6 @@ lemma ubOnePhaseCond_hold_up_to_equiv_of_ub_one {V : CKMMatrix} (hb : ¬ ([V]ud ring rw [hcs, hUV, cs_of_ud_us_zero hb] - lemma cd_of_fstRowThdColRealCond {V : CKMMatrix} (hb : [V]ud ≠ 0 ∨ [V]us ≠ 0) (hV : FstRowThdColRealCond V) : [V]cd = (- VtbAbs ⟦V⟧ * VusAbs ⟦V⟧ / (VudAbs ⟦V⟧ ^2 + VusAbs ⟦V⟧ ^2)) +