Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

feat: Contractions and involutions #272

Merged
merged 8 commits into from
Jan 6, 2025
Merged

feat: Contractions and involutions #272

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
8 commits
Select commit Hold shift + click to select a range
7d1f15e
feat: Contractions and involutions
jstoobysmith Jan 3, 2025
eadb354
feat: equivalence between involutions and contractions
jstoobysmith Jan 4, 2025
840d16a
feat: number of full contractions
jstoobysmith Jan 4, 2025
1ab0c6f
feat: Cardinality of involutions and refactor
jstoobysmith Jan 5, 2025
9184f60
feat: Update free simp
jstoobysmith Jan 5, 2025
7026d8c
refactor: free simps
jstoobysmith Jan 5, 2025
408a676
refactor: style lint
jstoobysmith Jan 5, 2025
83908c6
refactor: Lint and update involutions of Fin n
jstoobysmith Jan 6, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 2 additions & 0 deletions HepLean.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -100,6 +100,7 @@ import HepLean.Lorentz.Weyl.Modules
import HepLean.Lorentz.Weyl.Two
import HepLean.Lorentz.Weyl.Unit
import HepLean.Mathematics.Fin
import HepLean.Mathematics.Fin.Involutions
import HepLean.Mathematics.LinearMaps
import HepLean.Mathematics.List
import HepLean.Mathematics.PiTensorProduct
Expand All @@ -114,6 +115,7 @@ import HepLean.Meta.Notes.NoteFile
import HepLean.Meta.Notes.ToHTML
import HepLean.Meta.TransverseTactics
import HepLean.PerturbationTheory.Contractions.Basic
import HepLean.PerturbationTheory.Contractions.Card
import HepLean.PerturbationTheory.Contractions.Involutions
import HepLean.PerturbationTheory.FeynmanDiagrams.Basic
import HepLean.PerturbationTheory.FeynmanDiagrams.Instances.ComplexScalar
Expand Down
2 changes: 1 addition & 1 deletion HepLean/Lorentz/ComplexTensor/PauliMatrices/Basis.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -485,7 +485,7 @@ lemma pauliMatrix_contr_down_3 :
rw [contrBasisVectorMul_pos _]
conv =>
lhs; rhs; rhs; lhs;
rw [contrBasisVectorMul_pos _]
rw [contrBasisVectorMul_pos _]
conv =>
lhs
simp only [_root_.zero_smul, one_smul, _root_.smul_zero, _root_.add_zero, _root_.zero_add]
Expand Down
12 changes: 6 additions & 6 deletions HepLean/Mathematics/Fin.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -101,7 +101,7 @@ lemma succAbove_succAbove_predAboveI (i : Fin n.succ.succ) (j : Fin n.succ) (x :
· rw [Fin.succAbove_of_castSucc_lt _ _]
exact hx1
· rw [Fin.lt_def] at h1 hx1 ⊢
simp_all
simp_all only [Nat.succ_eq_add_one, Fin.coe_castSucc]
omega
· exact Nat.lt_trans hx1 h1
· simp only [not_lt] at hx1
Expand All @@ -115,7 +115,7 @@ lemma succAbove_succAbove_predAboveI (i : Fin n.succ.succ) (j : Fin n.succ) (x :
· rfl
· exact hx1
· rw [Fin.lt_def] at hx2 ⊢
simp_all
simp_all only [Nat.succ_eq_add_one, Fin.coe_castSucc, Fin.val_succ]
omega
· simp only [Nat.succ_eq_add_one, not_lt] at hx2
rw [Fin.succAbove_of_le_castSucc _ _ hx2]
Expand All @@ -135,12 +135,12 @@ lemma succAbove_succAbove_predAboveI (i : Fin n.succ.succ) (j : Fin n.succ) (x :
· nth_rewrite 2 [Fin.succAbove_of_le_castSucc _ _]
· rw [Fin.succAbove_of_le_castSucc _ _]
rw [Fin.le_def] at hx1 ⊢
simp_all
simp_all only [Nat.succ_eq_add_one, Fin.coe_castSucc, Fin.val_succ, add_le_add_iff_right]
· rw [Fin.le_def] at h1 hx1 ⊢
simp_all
simp_all only [Nat.succ_eq_add_one, Fin.coe_castSucc]
omega
· rw [Fin.le_def] at hx1 h1 ⊢
simp_all
simp_all only [Nat.succ_eq_add_one, Fin.coe_castSucc, Fin.val_succ]
omega
· simp only [Nat.succ_eq_add_one, not_le] at hx1
rw [Fin.lt_def] at hx1
Expand All @@ -151,7 +151,7 @@ lemma succAbove_succAbove_predAboveI (i : Fin n.succ.succ) (j : Fin n.succ) (x :
nth_rewrite 2 [Fin.succAbove_of_castSucc_lt _ _]
· rw [Fin.succAbove_of_castSucc_lt _ _]
rw [Fin.lt_def] at hx2 ⊢
simp_all
simp_all only [Nat.succ_eq_add_one, Fin.coe_castSucc, Fin.val_succ]
omega
· rw [Fin.lt_def] at hx2 ⊢
simp_all
Expand Down
Loading
Loading