Merge pull request #267 from HEPLean/WickContract

Static Wick's theorem
This commit is contained in:
Joseph Tooby-Smith 2024-12-19 16:02:57 +00:00 committed by GitHub
commit 2cc79d0770
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
25 changed files with 3594 additions and 1834 deletions

View file

@ -117,15 +117,20 @@ import HepLean.Meta.TransverseTactics
import HepLean.PerturbationTheory.FeynmanDiagrams.Basic
import HepLean.PerturbationTheory.FeynmanDiagrams.Instances.ComplexScalar
import HepLean.PerturbationTheory.FeynmanDiagrams.Instances.Phi4
import HepLean.PerturbationTheory.FeynmanDiagrams.Light
import HepLean.PerturbationTheory.FeynmanDiagrams.Momentum
import HepLean.PerturbationTheory.Wick.Algebra
import HepLean.PerturbationTheory.Wick.Contract
import HepLean.PerturbationTheory.Wick.MomentumSpace
import HepLean.PerturbationTheory.Wick.PositionSpace
import HepLean.PerturbationTheory.Wick.Species
import HepLean.PerturbationTheory.Wick.String
import HepLean.PerturbationTheory.Wick.Theorem
import HepLean.PerturbationTheory.Wick.Contraction
import HepLean.PerturbationTheory.Wick.CreateAnnilateSection
import HepLean.PerturbationTheory.Wick.KoszulOrder
import HepLean.PerturbationTheory.Wick.OfList
import HepLean.PerturbationTheory.Wick.OperatorMap
import HepLean.PerturbationTheory.Wick.Signs.Grade
import HepLean.PerturbationTheory.Wick.Signs.InsertSign
import HepLean.PerturbationTheory.Wick.Signs.KoszulSign
import HepLean.PerturbationTheory.Wick.Signs.KoszulSignInsert
import HepLean.PerturbationTheory.Wick.Signs.StaticWickCoef
import HepLean.PerturbationTheory.Wick.Signs.SuperCommuteCoef
import HepLean.PerturbationTheory.Wick.StaticTheorem
import HepLean.PerturbationTheory.Wick.SuperCommute
import HepLean.SpaceTime.Basic
import HepLean.SpaceTime.CliffordAlgebra
import HepLean.StandardModel.Basic

View file

@ -240,7 +240,8 @@ lemma toLorentzGroup_fst_col (M : SL(2, )) :
| Sum.inr 2 => ((- ‖M.1 0 0‖ ^ 2 - ‖M.1 0 1‖ ^ 2 + ‖M.1 1 0‖ ^ 2 + ‖M.1 1 1‖ ^ 2) / 2)
change (fun μ => (toLorentzGroup M).1 μ (Sum.inl 0)) = k
have h1 : toSelfAdjointMap M (PauliMatrix.σSAL (Sum.inl 0)) = ∑ μ, k μ • PauliMatrix.σSAL μ := by
simp [Fin.sum_univ_three]
simp only [Fin.isValue, Fintype.sum_sum_type, Finset.univ_unique, Fin.default_eq_zero,
Finset.sum_singleton, Fin.sum_univ_three]
rw [toSelfAdjointMap_apply_σSAL_inl]
abel
rw [toSelfAdjointMap_basis] at h1

View file

@ -174,6 +174,7 @@ def finExtractOne {n : } (i : Fin n.succ) : Fin n.succ ≃ Fin 1 ⊕ Fin n :=
(Equiv.sumAssoc (Fin 1) (Fin i) (Fin (n - i))).trans <|
Equiv.sumCongr (Equiv.refl (Fin 1)) (finSumFinEquiv.trans (finCongr (by omega)))
@[simp]
lemma finExtractOne_apply_eq {n : } (i : Fin n.succ) :
finExtractOne i i = Sum.inl 0 := by
simp only [Nat.succ_eq_add_one, finExtractOne, Equiv.trans_apply, finCongr_apply,
@ -239,12 +240,20 @@ lemma finExtractOne_symm_inl_apply {n : } (i : Fin n.succ) :
(finExtractOne i).symm (Sum.inl 0) = i := by
rfl
lemma finExtractOne_apply_neq {n : } (i j : Fin n.succ.succ) (hij : i ≠ j) :
finExtractOne i j = Sum.inr (predAboveI i j) := by
symm
apply (Equiv.symm_apply_eq _).mp ?_
simp only [Nat.succ_eq_add_one, finExtractOne_symm_inr_apply]
exact succsAbove_predAboveI hij
/-- Given an equivalence `Fin n.succ.succ ≃ Fin n.succ.succ`, and an `i : Fin n.succ.succ`,
the map `Fin n.succ → Fin n.succ` obtained by dropping `i` and it's image. -/
def finExtractOnPermHom (i : Fin n.succ.succ) (σ : Fin n.succ.succ ≃ Fin n.succ.succ) :
Fin n.succ → Fin n.succ := fun x => predAboveI (σ i) (σ ((finExtractOne i).symm (Sum.inr x)))
def finExtractOnPermHom {m : } (i : Fin n.succ.succ) (σ : Fin n.succ.succ ≃ Fin m.succ.succ) :
Fin n.succ → Fin m.succ := fun x => predAboveI (σ i) (σ ((finExtractOne i).symm (Sum.inr x)))
lemma finExtractOnPermHom_inv (i : Fin n.succ.succ) (σ : Fin n.succ.succ ≃ Fin n.succ.succ) :
lemma finExtractOnPermHom_inv {m : } (i : Fin n.succ.succ)
(σ : Fin n.succ.succ ≃ Fin m.succ.succ) :
(finExtractOnPermHom (σ i) σ.symm) ∘ (finExtractOnPermHom i σ) = id := by
funext x
simp only [Nat.succ_eq_add_one, Function.comp_apply, finExtractOnPermHom, Equiv.symm_apply_apply,
@ -270,8 +279,8 @@ lemma finExtractOnPermHom_inv (i : Fin n.succ.succ) (σ : Fin n.succ.succ ≃ Fi
/-- Given an equivalence `Fin n.succ.succ ≃ Fin n.succ.succ`, and an `i : Fin n.succ.succ`,
the equivalence `Fin n.succ ≃ Fin n.succ` obtained by dropping `i` and it's image. -/
def finExtractOnePerm (i : Fin n.succ.succ) (σ : Fin n.succ.succ ≃ Fin n.succ.succ) :
Fin n.succ ≃ Fin n.succ where
def finExtractOnePerm {m : } (i : Fin n.succ.succ) (σ : Fin n.succ.succ ≃ Fin m.succ.succ) :
Fin n.succ ≃ Fin m.succ where
toFun x := finExtractOnPermHom i σ x
invFun x := finExtractOnPermHom (σ i) σ.symm x
left_inv x := by
@ -279,6 +288,17 @@ def finExtractOnePerm (i : Fin n.succ.succ) (σ : Fin n.succ.succ ≃ Fin n.succ
right_inv x := by
simpa using congrFun (finExtractOnPermHom_inv (σ i) σ.symm) x
lemma finExtractOnePerm_equiv {n m : } (e : Fin n.succ.succ ≃ Fin m.succ.succ)
(i : Fin n.succ.succ) :
e ∘ i.succAbove = (e i).succAbove ∘ finExtractOnePerm i e := by
simp only [Nat.succ_eq_add_one, finExtractOnePerm, Equiv.coe_fn_mk]
funext x
simp only [Function.comp_apply, finExtractOnPermHom, Nat.succ_eq_add_one,
finExtractOne_symm_inr_apply]
rw [succsAbove_predAboveI]
simp only [Nat.succ_eq_add_one, ne_eq, EmbeddingLike.apply_eq_iff_eq]
exact Fin.ne_succAbove i x
@[simp]
lemma finExtractOnePerm_apply (i : Fin n.succ.succ) (σ : Fin n.succ.succ ≃ Fin n.succ.succ)
(x : Fin n.succ) : finExtractOnePerm i σ x = predAboveI (σ i)
@ -376,6 +396,11 @@ def equivCons {n m : } (e : Fin n ≃ Fin m) : Fin n.succ ≃ Fin m.succ wher
subst hj
simp
@[simp]
lemma equivCons_zero {n m : } (e : Fin n ≃ Fin m) :
equivCons e 0 = 0 := by
simp [equivCons]
@[simp]
lemma equivCons_trans {n m k : } (e : Fin n ≃ Fin m) (f : Fin m ≃ Fin k) :
Fin.equivCons (e.trans f) = (Fin.equivCons e).trans (Fin.equivCons f) := by
@ -409,4 +434,15 @@ lemma equivCons_symm_succ {n m : } (e : Fin n ≃ Fin m) (i : ) (hi : i +
rw [Fin.cons_succ]
simp
@[simp]
lemma equivCons_succ {n m : } (e : Fin n ≃ Fin m) (i : ) (hi : i + 1 < n.succ) :
(Fin.equivCons e) ⟨i + 1, hi⟩ = (e ⟨i, Nat.succ_lt_succ_iff.mp hi⟩).succ := by
simp only [Nat.succ_eq_add_one, equivCons, Equiv.toFun_as_coe, Equiv.invFun_as_coe,
Equiv.coe_fn_symm_mk]
have hi : ⟨i + 1, hi⟩ = Fin.succ ⟨i, Nat.succ_lt_succ_iff.mp hi⟩ := by rfl
simp only [Equiv.coe_fn_mk]
rw [hi]
rw [Fin.cons_succ]
rfl
end HepLean.Fin

View file

@ -3,9 +3,6 @@ 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 Mathlib.LinearAlgebra.PiTensorProduct
import Mathlib.Tactic.Polyrith
import Mathlib.Tactic.Linarith
import HepLean.Mathematics.Fin
/-!
# List lemmas
@ -17,96 +14,602 @@ open Fin
open HepLean
variable {n : Nat}
/-- The equivalence between `Fin (a :: l).length` and `Fin (List.orderedInsert r a l).length`
mapping `0` in the former to the location of `a` in the latter. -/
def insertEquiv {α : Type} (r : αα → Prop) [DecidableRel r] (a : α) : (l : List α) →
Fin (a :: l).length ≃ Fin (List.orderedInsert r a l).length
| [] => Equiv.refl _
| b :: l => by
if r a b then
exact (Fin.castOrderIso (List.orderedInsert_length r (b :: l) a).symm).toEquiv
else
let e := insertEquiv (r := r) a l
let e2 : Fin (a :: b :: l).length ≃ Fin (b :: a :: l).length :=
Equiv.swap ⟨0, Nat.zero_lt_succ (b :: l).length⟩ ⟨1, Nat.one_lt_succ_succ l.length⟩
let e3 : Fin (b :: a :: l).length ≃ Fin (b :: List.orderedInsert r a l).length :=
Fin.equivCons e
let e4 : Fin (b :: List.orderedInsert r a l).length ≃
Fin (List.orderedInsert r a (b :: l)).length :=
(Fin.castOrderIso (by
rw [List.orderedInsert_length]
simpa using List.orderedInsert_length r l a)).toEquiv
exact e2.trans (e3.trans e4)
lemma takeWile_eraseIdx {I : Type} (P : I → Prop) [DecidablePred P] :
(l : List I) → (i : ) → (hi : ∀ (i j : Fin l.length), i < j → P (l.get j) → P (l.get i)) →
List.takeWhile P (List.eraseIdx l i) = (List.takeWhile P l).eraseIdx i
| [], _, h => by
rfl
| a :: [], 0, h => by
simp only [List.takeWhile, List.eraseIdx_zero, List.nil_eq]
split
· rfl
· rfl
| a :: [], Nat.succ n, h => by
simp only [Nat.succ_eq_add_one, List.eraseIdx_cons_succ, List.eraseIdx_nil]
rw [List.eraseIdx_of_length_le]
have h1 : (List.takeWhile P [a]).length ≤ [a].length :=
List.Sublist.length_le (List.takeWhile_sublist _)
simp only [List.length_singleton] at h1
omega
| a :: b :: l, 0, h => by
simp only [List.takeWhile, List.eraseIdx_zero]
by_cases hPb : P b
· have hPa : P a := by
simpa using h ⟨0, by simp⟩ ⟨1, by simp⟩ (by simp [Fin.lt_def]) (by simpa using hPb)
simp [hPb, hPa]
· simp only [hPb, decide_False, List.nil_eq]
simp_all only [List.length_cons, List.get_eq_getElem]
split
· rfl
· rfl
| a :: b :: l, Nat.succ n, h => by
simp only [Nat.succ_eq_add_one, List.eraseIdx_cons_succ]
by_cases hPa : P a
· dsimp [List.takeWhile]
simp only [hPa, decide_True, List.eraseIdx_cons_succ, List.cons.injEq, true_and]
rw [takeWile_eraseIdx]
rfl
intro i j hij hP
simpa using h (Fin.succ i) (Fin.succ j) (by simpa using hij) (by simpa using hP)
· simp [hPa]
lemma insertEquiv_congr {α : Type} {r : αα → Prop} [DecidableRel r] (a : α) (l l' : List α)
(h : l = l') : insertEquiv r a l = (Fin.castOrderIso (by simp [h])).toEquiv.trans
((insertEquiv r a l').trans (Fin.castOrderIso (by simp [h])).toEquiv) := by
lemma dropWile_eraseIdx {I : Type} (P : I → Prop) [DecidablePred P] :
(l : List I) → (i : ) → (hi : ∀ (i j : Fin l.length), i < j → P (l.get j) → P (l.get i)) →
List.dropWhile P (List.eraseIdx l i) =
if (List.takeWhile P l).length ≤ i then
(List.dropWhile P l).eraseIdx (i - (List.takeWhile P l).length)
else (List.dropWhile P l)
| [], _, h => by
simp
| a :: [], 0, h => by
simp only [List.dropWhile, nonpos_iff_eq_zero, List.length_eq_zero, List.takeWhile_eq_nil_iff,
List.length_singleton, zero_lt_one, Fin.zero_eta, Fin.isValue, List.get_eq_getElem,
Fin.val_eq_zero, List.getElem_cons_zero, decide_eq_true_eq, forall_const, zero_le,
Nat.sub_eq_zero_of_le, List.eraseIdx_zero, ite_not, List.nil_eq]
simp_all only [List.length_singleton, List.get_eq_getElem, Fin.val_eq_zero,
List.getElem_cons_zero, implies_true, decide_True, decide_False, List.tail_cons, ite_self]
| a :: [], Nat.succ n, h => by
simp only [List.dropWhile, List.eraseIdx_nil, List.takeWhile, Nat.succ_eq_add_one]
rw [List.eraseIdx_of_length_le]
simp_all only [List.length_singleton, List.get_eq_getElem, Fin.val_eq_zero,
List.getElem_cons_zero, implies_true, ite_self]
simp_all only [List.length_singleton, List.get_eq_getElem, Fin.val_eq_zero,
List.getElem_cons_zero, implies_true]
split
next x heq =>
simp_all only [decide_eq_true_eq, List.length_nil, List.length_singleton,
add_tsub_cancel_right, zero_le]
next x heq =>
simp_all only [decide_eq_false_iff_not, List.length_singleton, List.length_nil, tsub_zero,
le_add_iff_nonneg_left, zero_le]
| a :: b :: l, 0, h => by
simp only [List.dropWhile, List.takeWhile, nonpos_iff_eq_zero, List.length_eq_zero, zero_le,
Nat.sub_eq_zero_of_le, List.eraseIdx_zero]
by_cases hPb : P b
· have hPa : P a := by
simpa using h ⟨0, by simp⟩ ⟨1, by simp⟩ (by simp [Fin.lt_def]) (by simpa using hPb)
simp [hPb, hPa]
· simp only [hPb, decide_False, nonpos_iff_eq_zero, List.length_eq_zero]
simp_all only [List.length_cons, List.get_eq_getElem]
simp_all only [decide_False, nonpos_iff_eq_zero, List.length_eq_zero]
split
next h_1 =>
simp_all only [nonpos_iff_eq_zero, List.length_eq_zero]
split
next x heq => simp_all only [List.cons_ne_self]
· rfl
next h_1 =>
simp_all only [nonpos_iff_eq_zero, List.length_eq_zero]
split
next x heq => rfl
next x heq => simp_all only [not_true_eq_false]
| a :: b :: l, Nat.succ n, h => by
simp only [Nat.succ_eq_add_one, List.eraseIdx_cons_succ]
by_cases hPb : P b
· have hPa : P a := by
simpa using h ⟨0, by simp⟩ ⟨1, by simp⟩ (by simp [Fin.lt_def]) (by simpa using hPb)
simp only [List.dropWhile, hPa, decide_True, List.takeWhile, hPb, List.length_cons,
add_le_add_iff_right, Nat.reduceSubDiff]
rw [dropWile_eraseIdx]
simp_all only [List.length_cons, List.get_eq_getElem, decide_True, List.takeWhile_cons_of_pos,
List.dropWhile_cons_of_pos]
intro i j hij hP
simpa using h (Fin.succ i) (Fin.succ j) (by simpa using hij) (by simpa using hP)
· simp only [List.dropWhile, List.takeWhile, hPb, decide_False]
by_cases hPa : P a
· rw [dropWile_eraseIdx]
simp only [hPa, decide_True, hPb, decide_False, Bool.false_eq_true, not_false_eq_true,
List.takeWhile_cons_of_neg, List.length_nil, zero_le, ↓reduceIte, List.dropWhile,
tsub_zero, List.length_singleton, le_add_iff_nonneg_left, add_tsub_cancel_right]
intro i j hij hP
simpa using h (Fin.succ i) (Fin.succ j) (by simpa using hij) (by simpa using hP)
· simp [hPa]
/-- The position `r0` ends up in `r` on adding it via `List.orderedInsert _ r0 r`. -/
def orderedInsertPos {I : Type} (le1 : I → I → Prop) [DecidableRel le1] (r : List I) (r0 : I) :
Fin (List.orderedInsert le1 r0 r).length :=
⟨(List.takeWhile (fun b => decide ¬ le1 r0 b) r).length, by
rw [List.orderedInsert_length]
have h1 : (List.takeWhile (fun b => decide ¬le1 r0 b) r).length ≤ r.length :=
List.Sublist.length_le (List.takeWhile_sublist fun b => decide ¬le1 r0 b)
omega⟩
lemma orderedInsertPos_lt_length {I : Type} (le1 : I → I → Prop) [DecidableRel le1] (r : List I)
(r0 : I) : orderedInsertPos le1 r r0 < (r0 :: r).length := by
simp only [orderedInsertPos, List.length_cons]
have h1 : (List.takeWhile (fun b => decide ¬le1 r0 b) r).length ≤ r.length :=
List.Sublist.length_le (List.takeWhile_sublist fun b => decide ¬le1 r0 b)
omega
@[simp]
lemma orderedInsert_get_orderedInsertPos {I : Type} (le1 : I → I → Prop) [DecidableRel le1]
(r : List I) (r0 : I) :
(List.orderedInsert le1 r0 r)[(orderedInsertPos le1 r r0).val] = r0 := by
simp only [List.orderedInsert_eq_take_drop, decide_not, orderedInsertPos]
rw [List.getElem_append]
simp
@[simp]
lemma orderedInsert_eraseIdx_orderedInsertPos {I : Type} (le1 : I → I → Prop) [DecidableRel le1]
(r : List I) (r0 : I) :
(List.orderedInsert le1 r0 r).eraseIdx ↑(orderedInsertPos le1 r r0) = r := by
simp only [List.orderedInsert_eq_take_drop]
rw [List.eraseIdx_append_of_length_le]
· simp [orderedInsertPos]
· rfl
lemma orderedInsertPos_cons {I : Type} (le1 : I → I → Prop) [DecidableRel le1]
(r : List I) (r0 r1 : I) :
(orderedInsertPos le1 (r1 ::r) r0).val =
if le1 r0 r1 then ⟨0, by simp⟩ else (Fin.succ (orderedInsertPos le1 r r0)) := by
simp only [List.orderedInsert.eq_2, orderedInsertPos, List.takeWhile, decide_not, Fin.zero_eta,
Fin.succ_mk]
by_cases h : le1 r0 r1
· simp [h]
· simp [h]
lemma orderedInsertPos_sigma {I : Type} {f : I → Type}
(le1 : I → I → Prop) [DecidableRel le1] (l : List (Σ i, f i))
(k : I) (a : f k) :
(orderedInsertPos (fun (i j : Σ i, f i) => le1 i.1 j.1) l ⟨k, a⟩).1 =
(orderedInsertPos le1 (List.map (fun (i : Σ i, f i) => i.1) l) k).1 := by
simp only [orderedInsertPos, decide_not]
induction l with
| nil =>
simp
| cons a l ih =>
simp only [List.takeWhile]
obtain ⟨fst, snd⟩ := a
simp_all only
split
next x heq =>
simp_all only [Bool.not_eq_eq_eq_not, Bool.not_true, decide_eq_false_iff_not,
List.length_cons, decide_False, Bool.not_false]
next x heq =>
simp_all only [Bool.not_eq_eq_eq_not, Bool.not_false, decide_eq_true_eq, List.length_nil,
decide_True, Bool.not_true]
lemma orderedInsert_get_lt {I : Type} (le1 : I → I → Prop) [DecidableRel le1]
(r : List I) (r0 : I) (i : )
(hi : i < orderedInsertPos le1 r r0) :
(List.orderedInsert le1 r0 r)[i] = r.get ⟨i, by
simp only [orderedInsertPos] at hi
have h1 : (List.takeWhile (fun b => decide ¬le1 r0 b) r).length ≤ r.length :=
List.Sublist.length_le (List.takeWhile_sublist fun b => decide ¬le1 r0 b)
omega⟩ := by
simp only [orderedInsertPos, decide_not] at hi
simp only [List.orderedInsert_eq_take_drop, decide_not, List.get_eq_getElem]
rw [List.getElem_append]
simp only [hi, ↓reduceDIte]
rw [List.IsPrefix.getElem]
exact List.takeWhile_prefix fun b => !decide (le1 r0 b)
lemma orderedInsertPos_take_orderedInsert {I : Type} (le1 : I → I → Prop) [DecidableRel le1]
(r : List I) (r0 : I) :
(List.take (orderedInsertPos le1 r r0) (List.orderedInsert le1 r0 r)) =
List.takeWhile (fun b => decide ¬le1 r0 b) r := by
simp [orderedInsertPos, List.orderedInsert_eq_take_drop]
lemma orderedInsertPos_take_eq_orderedInsert {I : Type} (le1 : I → I → Prop) [DecidableRel le1]
(r : List I) (r0 : I) :
List.take (orderedInsertPos le1 r r0) r =
List.take (orderedInsertPos le1 r r0) (List.orderedInsert le1 r0 r) := by
refine List.ext_get ?_ ?_
· simp only [List.length_take, Fin.is_le', inf_of_le_left, inf_eq_left]
exact Nat.le_of_lt_succ (orderedInsertPos_lt_length le1 r r0)
· intro n h1 h2
simp only [List.get_eq_getElem, List.getElem_take]
erw [orderedInsert_get_lt le1 r r0 n]
rfl
simp only [List.length_take, lt_inf_iff] at h1
exact h1.1
lemma orderedInsertPos_drop_eq_orderedInsert {I : Type} (le1 : I → I → Prop) [DecidableRel le1]
(r : List I) (r0 : I) :
List.drop (orderedInsertPos le1 r r0) r =
List.drop (orderedInsertPos le1 r r0).succ (List.orderedInsert le1 r0 r) := by
conv_rhs => simp [orderedInsertPos, List.orderedInsert_eq_take_drop]
have hr : r = List.takeWhile (fun b => !decide (le1 r0 b)) r ++
List.dropWhile (fun b => !decide (le1 r0 b)) r := by
exact Eq.symm (List.takeWhile_append_dropWhile (fun b => !decide (le1 r0 b)) r)
conv_lhs =>
rhs
rw [hr]
rw [List.drop_append_eq_append_drop]
simp [orderedInsertPos]
lemma orderedInsertPos_take {I : Type} (le1 : I → I → Prop) [DecidableRel le1]
(r : List I) (r0 : I) :
List.take (orderedInsertPos le1 r r0) r = List.takeWhile (fun b => decide ¬le1 r0 b) r := by
rw [orderedInsertPos_take_eq_orderedInsert]
rw [orderedInsertPos_take_orderedInsert]
lemma orderedInsertPos_drop {I : Type} (le1 : I → I → Prop) [DecidableRel le1]
(r : List I) (r0 : I) :
List.drop (orderedInsertPos le1 r r0) r = List.dropWhile (fun b => decide ¬le1 r0 b) r := by
rw [orderedInsertPos_drop_eq_orderedInsert]
simp [orderedInsertPos, List.orderedInsert_eq_take_drop]
lemma orderedInsertPos_succ_take_orderedInsert {I : Type} (le1 : I → I → Prop) [DecidableRel le1]
(r : List I) (r0 : I) :
(List.take (orderedInsertPos le1 r r0).succ (List.orderedInsert le1 r0 r)) =
List.takeWhile (fun b => decide ¬le1 r0 b) r ++ [r0] := by
simp [orderedInsertPos, List.orderedInsert_eq_take_drop, List.take_append_eq_append_take]
lemma lt_orderedInsertPos_rel {I : Type} (le1 : I → I → Prop) [DecidableRel le1]
(r0 : I) (r : List I) (n : Fin r.length)
(hn : n.val < (orderedInsertPos le1 r r0).val) : ¬ le1 r0 (r.get n) := by
have htake : r.get n ∈ List.take (orderedInsertPos le1 r r0) r := by
rw [@List.mem_take_iff_getElem]
use n
simp only [List.get_eq_getElem, lt_inf_iff, Fin.is_lt, and_true, exists_prop]
exact hn
rw [orderedInsertPos_take] at htake
have htake' := List.mem_takeWhile_imp htake
simpa using htake'
lemma gt_orderedInsertPos_rel {I : Type} (le1 : I → I → Prop) [DecidableRel le1]
[IsTotal I le1] [IsTrans I le1] (r0 : I) (r : List I) (hs : List.Sorted le1 r)
(n : Fin r.length)
(hn : ¬ n.val < (orderedInsertPos le1 r r0).val) : le1 r0 (r.get n) := by
have hrsSorted : List.Sorted le1 (List.orderedInsert le1 r0 r) :=
List.Sorted.orderedInsert r0 r hs
apply List.Sorted.rel_of_mem_take_of_mem_drop (k := (orderedInsertPos le1 r r0).succ) hrsSorted
· rw [orderedInsertPos_succ_take_orderedInsert]
simp
· rw [← orderedInsertPos_drop_eq_orderedInsert]
refine List.mem_drop_iff_getElem.mpr ?hy.a
use n - (orderedInsertPos le1 r r0).val
have hn : ↑n - ↑(orderedInsertPos le1 r r0) + ↑(orderedInsertPos le1 r r0) < r.length := by
omega
use hn
congr
omega
lemma orderedInsert_eraseIdx_lt_orderedInsertPos {I : Type} (le1 : I → I → Prop) [DecidableRel le1]
(r : List I) (r0 : I) (i : )
(hi : i < orderedInsertPos le1 r r0)
(hr : ∀ (i j : Fin r.length), i < j → ¬le1 r0 (r.get j) → ¬le1 r0 (r.get i)) :
(List.orderedInsert le1 r0 r).eraseIdx i = List.orderedInsert le1 r0 (r.eraseIdx i) := by
conv_lhs => simp only [List.orderedInsert_eq_take_drop]
rw [List.eraseIdx_append_of_lt_length]
· simp only [List.orderedInsert_eq_take_drop]
congr 1
· rw [takeWile_eraseIdx]
exact hr
· rw [dropWile_eraseIdx]
simp only [orderedInsertPos, decide_not] at hi
have hi' : ¬ (List.takeWhile (fun b => !decide (le1 r0 b)) r).length ≤ ↑i := by
omega
simp only [decide_not, hi', ↓reduceIte]
exact fun i j a a_1 => hr i j a a_1
· exact hi
lemma orderedInsert_eraseIdx_orderedInsertPos_le {I : Type} (le1 : I → I → Prop) [DecidableRel le1]
(r : List I) (r0 : I) (i : )
(hi : orderedInsertPos le1 r r0 ≤ i)
(hr : ∀ (i j : Fin r.length), i < j → ¬le1 r0 (r.get j) → ¬le1 r0 (r.get i)) :
(List.orderedInsert le1 r0 r).eraseIdx (Nat.succ i) =
List.orderedInsert le1 r0 (r.eraseIdx i) := by
conv_lhs => simp only [List.orderedInsert_eq_take_drop]
rw [List.eraseIdx_append_of_length_le]
· simp only [List.orderedInsert_eq_take_drop]
congr 1
· rw [takeWile_eraseIdx]
rw [List.eraseIdx_of_length_le]
simp only [orderedInsertPos, decide_not] at hi
simp only [decide_not]
omega
exact hr
· simp only [Nat.succ_eq_add_one]
have hn : (i + 1 - (List.takeWhile (fun b => (decide (¬ le1 r0 b))) r).length)
= (i - (List.takeWhile (fun b => decide (¬ le1 r0 b)) r).length) + 1 := by
simp only [orderedInsertPos] at hi
omega
rw [hn]
simp only [List.eraseIdx_cons_succ, List.cons.injEq, true_and]
rw [dropWile_eraseIdx]
rw [if_pos]
· simp only [orderedInsertPos] at hi
omega
· exact hr
· simp only [orderedInsertPos] at hi
omega
/-- The equivalence between `Fin (r0 :: r).length` and `Fin (List.orderedInsert le1 r0 r).length`
according to where the elements map. I.e. `0` is taken to `orderedInsertPos le1 r r0`. -/
def orderedInsertEquiv {I : Type} (le1 : I → I → Prop) [DecidableRel le1] (r : List I) (r0 : I) :
Fin (r0 :: r).length ≃ Fin (List.orderedInsert le1 r0 r).length := by
let e2 : Fin (List.orderedInsert le1 r0 r).length ≃ Fin (r0 :: r).length :=
(Fin.castOrderIso (List.orderedInsert_length le1 r r0)).toEquiv
let e3 : Fin (r0 :: r).length ≃ Fin 1 ⊕ Fin (r).length := finExtractOne 0
let e4 : Fin (r0 :: r).length ≃ Fin 1 ⊕ Fin (r).length :=
finExtractOne ⟨orderedInsertPos le1 r r0, orderedInsertPos_lt_length le1 r r0⟩
exact e3.trans (e4.symm.trans e2.symm)
lemma orderedInsertEquiv_zero {I : Type} (le1 : I → I → Prop) [DecidableRel le1] (r : List I)
(r0 : I) : orderedInsertEquiv le1 r r0 ⟨0, by simp⟩ = orderedInsertPos le1 r r0 := by
simp [orderedInsertEquiv]
lemma orderedInsertEquiv_succ {I : Type} (le1 : I → I → Prop) [DecidableRel le1] (r : List I)
(r0 : I) (n : ) (hn : Nat.succ n < (r0 :: r).length) :
orderedInsertEquiv le1 r r0 ⟨Nat.succ n, hn⟩ =
Fin.cast (List.orderedInsert_length le1 r r0).symm
((Fin.succAbove ⟨(orderedInsertPos le1 r r0), orderedInsertPos_lt_length le1 r r0⟩)
⟨n, Nat.succ_lt_succ_iff.mp hn⟩) := by
simp only [List.length_cons, orderedInsertEquiv, Nat.succ_eq_add_one, OrderIso.toEquiv_symm,
Fin.symm_castOrderIso, Equiv.trans_apply, RelIso.coe_fn_toEquiv, Fin.castOrderIso_apply]
match r with
| [] =>
simp
| r1 :: r =>
erw [finExtractOne_apply_neq]
simp only [List.orderedInsert.eq_2, List.length_cons, orderedInsertPos, decide_not,
Nat.succ_eq_add_one, finExtractOne_symm_inr_apply]
rfl
exact ne_of_beq_false rfl
lemma orderedInsertEquiv_fin_succ {I : Type} (le1 : I → I → Prop) [DecidableRel le1] (r : List I)
(r0 : I) (n : Fin r.length) :
orderedInsertEquiv le1 r r0 n.succ = Fin.cast (List.orderedInsert_length le1 r r0).symm
((Fin.succAbove ⟨(orderedInsertPos le1 r r0), orderedInsertPos_lt_length le1 r r0⟩)
⟨n, n.isLt⟩) := by
simp only [List.length_cons, orderedInsertEquiv, Nat.succ_eq_add_one, OrderIso.toEquiv_symm,
Fin.symm_castOrderIso, Equiv.trans_apply, RelIso.coe_fn_toEquiv, Fin.castOrderIso_apply,
Fin.eta]
match r with
| [] =>
simp
| r1 :: r =>
erw [finExtractOne_apply_neq]
simp only [List.orderedInsert.eq_2, List.length_cons, orderedInsertPos, decide_not,
Nat.succ_eq_add_one, finExtractOne_symm_inr_apply]
rfl
exact ne_of_beq_false rfl
lemma orderedInsertEquiv_congr {α : Type} {r : αα → Prop} [DecidableRel r] (a : α)
(l l' : List α) (h : l = l') :
orderedInsertEquiv r l a = (Fin.castOrderIso (by simp [h])).toEquiv.trans
((orderedInsertEquiv r l' a).trans (Fin.castOrderIso (by simp [h])).toEquiv) := by
subst h
rfl
lemma insertEquiv_cons_pos {α : Type} {r : αα → Prop} [DecidableRel r] (a b : α) (hab : r a b)
(l : List α) : insertEquiv r a (b :: l) =
(Fin.castOrderIso (List.orderedInsert_length r (b :: l) a).symm).toEquiv := by
simp [insertEquiv, hab]
lemma get_eq_orderedInsertEquiv {I : Type} (le1 : I → I → Prop) [DecidableRel le1] (r : List I)
(r0 : I) :
(r0 :: r).get = (List.orderedInsert le1 r0 r).get ∘ (orderedInsertEquiv le1 r r0) := by
funext x
match x with
| ⟨0, h⟩ =>
simp only [List.length_cons, Fin.zero_eta, List.get_eq_getElem, Fin.val_zero,
List.getElem_cons_zero, Function.comp_apply]
erw [orderedInsertEquiv_zero]
simp
| ⟨Nat.succ n, h⟩ =>
simp only [List.length_cons, Nat.succ_eq_add_one, List.get_eq_getElem, List.getElem_cons_succ,
Function.comp_apply]
erw [orderedInsertEquiv_succ]
simp only [Fin.succAbove, Fin.castSucc_mk, Fin.mk_lt_mk, Fin.succ_mk, Fin.coe_cast]
by_cases hn : n < ↑(orderedInsertPos le1 r r0)
· simp [hn, orderedInsert_get_lt]
· simp only [hn, ↓reduceIte]
simp only [List.orderedInsert_eq_take_drop, decide_not]
rw [List.getElem_append]
have hn' : ¬ n + 1 < (List.takeWhile (fun b => !decide (le1 r0 b)) r).length := by
simp only [orderedInsertPos, decide_not, not_lt] at hn
omega
simp only [hn', ↓reduceDIte]
have hnn : n + 1 - (List.takeWhile (fun b => !decide (le1 r0 b)) r).length =
(n - (List.takeWhile (fun b => !decide (le1 r0 b)) r).length) + 1 := by
simp only [orderedInsertPos, decide_not, not_lt] at hn
omega
simp only [hnn, List.getElem_cons_succ]
conv_rhs =>
rw [List.IsSuffix.getElem (List.dropWhile_suffix fun b => !decide (le1 r0 b))]
congr
have hr : r.length = (List.takeWhile (fun b => !decide (le1 r0 b)) r).length +
(List.dropWhile (fun b => !decide (le1 r0 b)) r).length := by
rw [← List.length_append]
congr
exact Eq.symm (List.takeWhile_append_dropWhile (fun b => !decide (le1 r0 b)) r)
simp only [hr, add_tsub_cancel_right]
omega
lemma insertEquiv_cons_neg {α : Type} {r : αα → Prop} [DecidableRel r] (a b : α) (hab : ¬ r a b)
(l : List α) : insertEquiv r a (b :: l) =
let e := insertEquiv r a l
let e2 : Fin (a :: b :: l).length ≃ Fin (b :: a :: l).length :=
Equiv.swap ⟨0, Nat.zero_lt_succ (b :: l).length⟩ ⟨1, Nat.one_lt_succ_succ l.length⟩
let e3 : Fin (b :: a :: l).length ≃ Fin (b :: List.orderedInsert r a l).length :=
Fin.equivCons e
let e4 : Fin (b :: List.orderedInsert r a l).length ≃
Fin (List.orderedInsert r a (b :: l)).length :=
(Fin.castOrderIso (by
rw [List.orderedInsert_length]
simpa using List.orderedInsert_length r l a)).toEquiv
e2.trans (e3.trans e4) := by
simp [insertEquiv, hab]
lemma orderedInsertEquiv_get {I : Type} (le1 : I → I → Prop) [DecidableRel le1] (r : List I)
(r0 : I) :
(r0 :: r).get ∘ (orderedInsertEquiv le1 r r0).symm = (List.orderedInsert le1 r0 r).get := by
rw [get_eq_orderedInsertEquiv le1]
funext x
simp
lemma insertEquiv_get {α : Type} {r : αα → Prop} [DecidableRel r] (a : α) : (l : List α) →
(a :: l).get ∘ (insertEquiv r a l).symm = (List.orderedInsert r a l).get
| [] => by
simp [insertEquiv]
| b :: l => by
by_cases hr : r a b
· rw [insertEquiv_cons_pos a b hr l]
simp_all only [List.orderedInsert.eq_2, List.length_cons, OrderIso.toEquiv_symm,
Fin.symm_castOrderIso, RelIso.coe_fn_toEquiv]
ext x : 1
simp_all only [Function.comp_apply, Fin.castOrderIso_apply, List.get_eq_getElem,
List.length_cons, Fin.coe_cast, ↓reduceIte]
· rw [insertEquiv_cons_neg a b hr l]
trans (b :: List.orderedInsert r a l).get ∘ Fin.cast (by
rw [List.orderedInsert_length]
simp [List.orderedInsert_length])
· simp only [List.orderedInsert.eq_2, List.length_cons, Fin.zero_eta, Fin.mk_one]
ext x
match x with
| ⟨0, h⟩ => rfl
| ⟨Nat.succ x, h⟩ =>
simp only [Nat.succ_eq_add_one, Function.comp_apply, Equiv.symm_trans_apply,
Equiv.symm_swap, OrderIso.toEquiv_symm, Fin.symm_castOrderIso, RelIso.coe_fn_toEquiv,
Fin.castOrderIso_apply, Fin.cast_mk, equivCons_symm_succ, List.get_eq_getElem,
List.length_cons, List.getElem_cons_succ]
have hswap (n : Fin (b :: a :: l).length) :
(a :: b :: l).get (Equiv.swap ⟨0, by simp⟩ ⟨1, by simp⟩ n) = (b :: a :: l).get n := by
match n with
| ⟨0, h⟩ => rfl
| ⟨1, h⟩ => rfl
| ⟨Nat.succ (Nat.succ x), h⟩ => rfl
trans (a :: b :: l).get (Equiv.swap ⟨0, by simp⟩ ⟨1, by simp⟩
((insertEquiv r a l).symm ⟨x, by simpa [List.orderedInsert_length, hr] using h⟩).succ)
· simp
· rw [hswap]
simp only [List.length_cons, List.get_eq_getElem, Fin.val_succ, List.getElem_cons_succ]
change _ = (List.orderedInsert r a l).get _
rw [← insertEquiv_get (r := r) a l]
simp
· simp_all only [List.orderedInsert.eq_2, List.length_cons]
ext x : 1
simp_all only [Function.comp_apply, List.get_eq_getElem, List.length_cons, Fin.coe_cast,
↓reduceIte]
lemma orderedInsert_eraseIdx_orderedInsertEquiv_zero
{I : Type} (le1 : I → I → Prop) [DecidableRel le1] (r : List I) (r0 : I) :
(List.orderedInsert le1 r0 r).eraseIdx (orderedInsertEquiv le1 r r0 ⟨0, by simp⟩) = r := by
simp [orderedInsertEquiv]
lemma orderedInsert_eraseIdx_orderedInsertEquiv_succ
{I : Type} (le1 : I → I → Prop) [DecidableRel le1] (r : List I) (r0 : I) (n : )
(hn : Nat.succ n < (r0 :: r).length)
(hr : ∀ (i j : Fin r.length), i < j → ¬le1 r0 (r.get j) → ¬le1 r0 (r.get i)) :
(List.orderedInsert le1 r0 r).eraseIdx (orderedInsertEquiv le1 r r0 ⟨Nat.succ n, hn⟩) =
(List.orderedInsert le1 r0 (r.eraseIdx n)) := by
induction r with
| nil =>
simp at hn
| cons r1 r ih =>
rw [orderedInsertEquiv_succ]
simp only [List.length_cons, Fin.succAbove,
Fin.castSucc_mk, Fin.mk_lt_mk, Fin.succ_mk, Fin.coe_cast]
by_cases hn' : n < (orderedInsertPos le1 (r1 :: r) r0)
· simp only [hn', ↓reduceIte]
rw [orderedInsert_eraseIdx_lt_orderedInsertPos le1 (r1 :: r) r0 n hn' hr]
· simp only [hn', ↓reduceIte]
rw [orderedInsert_eraseIdx_orderedInsertPos_le le1 (r1 :: r) r0 n _ hr]
omega
lemma orderedInsert_eraseIdx_orderedInsertEquiv_fin_succ
{I : Type} (le1 : I → I → Prop) [DecidableRel le1] (r : List I) (r0 : I) (n : Fin r.length)
(hr : ∀ (i j : Fin r.length), i < j → ¬le1 r0 (r.get j) → ¬le1 r0 (r.get i)) :
(List.orderedInsert le1 r0 r).eraseIdx (orderedInsertEquiv le1 r r0 n.succ) =
(List.orderedInsert le1 r0 (r.eraseIdx n)) := by
have hn : n.succ = ⟨n.val + 1, by omega⟩ := by
rw [Fin.ext_iff]
rfl
rw [hn]
exact orderedInsert_eraseIdx_orderedInsertEquiv_succ le1 r r0 n.val _ hr
lemma orderedInsertEquiv_sigma {I : Type} {f : I → Type}
(le1 : I → I → Prop) [DecidableRel le1] (l : List (Σ i, f i))
(i : I) (a : f i) :
(orderedInsertEquiv (fun i j => le1 i.fst j.fst) l ⟨i, a⟩) =
(Fin.castOrderIso (by simp)).toEquiv.trans
((orderedInsertEquiv le1 (List.map (fun i => i.1) l) i).trans
(Fin.castOrderIso (by simp [List.orderedInsert_length])).toEquiv) := by
ext x
match x with
| ⟨0, h0⟩ =>
simp only [List.length_cons, Fin.zero_eta, Equiv.trans_apply, RelIso.coe_fn_toEquiv,
Fin.castOrderIso_apply, Fin.cast_zero, Fin.coe_cast]
erw [orderedInsertEquiv_zero, orderedInsertEquiv_zero]
simp [orderedInsertPos_sigma]
| ⟨Nat.succ n, h0⟩ =>
simp only [List.length_cons, Nat.succ_eq_add_one, Equiv.trans_apply, RelIso.coe_fn_toEquiv,
Fin.castOrderIso_apply, Fin.cast_mk, Fin.coe_cast]
erw [orderedInsertEquiv_succ, orderedInsertEquiv_succ]
simp only [orderedInsertPos_sigma, Fin.coe_cast]
rw [Fin.succAbove, Fin.succAbove]
simp only [Fin.castSucc_mk, Fin.mk_lt_mk, Fin.succ_mk]
split
· rfl
· rfl
/-- This result is taken from:
https://github.com/leanprover/lean4/blob/master/src/Init/Data/List/Nat/InsertIdx.lean
with simple modification here to make it run.
The file it was taken from is licensed under the Apache License, Version 2.0.
and written by Parikshit Khanna, Jeremy Avigad, Leonardo de Moura,
Floris van Doorn, Mario Carneiro.
Once HepLean is updated to a more recent version of Lean this result will be removed.
-/
theorem length_insertIdx' : ∀ n as, (List.insertIdx n a as).length =
if n ≤ as.length then as.length + 1 else as.length
| 0, _ => by simp
| n + 1, [] => by rfl
| n + 1, a :: as => by
simp only [List.insertIdx_succ_cons, List.length_cons, length_insertIdx',
Nat.add_le_add_iff_right]
split <;> rfl
/-- This result is taken from:
https://github.com/leanprover/lean4/blob/master/src/Init/Data/List/Nat/InsertIdx.lean
with simple modification here to make it run.
The file it was taken from is licensed under the Apache License, Version 2.0.
and written by Parikshit Khanna, Jeremy Avigad, Leonardo de Moura,
Floris van Doorn, Mario Carneiro.
Once HepLean is updated to that version of Lean this result will be removed.
-/
theorem _root_.List.getElem_insertIdx_of_ge {l : List α} {x : α} {n k : Nat} (hn : n + 1 ≤ k)
(hk : k < (List.insertIdx n x l).length) :
(List.insertIdx n x l)[k] =
l[k - 1]'(by simp only [length_insertIdx'] at hk; split at hk <;> omega) := by
induction l generalizing n k with
| nil =>
cases n with
| zero =>
simp only [List.insertIdx_zero, List.length_cons, List.length_nil, zero_add,
Nat.lt_one_iff] at hk
omega
| succ n => simp at hk
| cons _ _ ih =>
cases n with
| zero =>
simp only [List.insertIdx_zero] at hk
cases k with
| zero => omega
| succ k => simp
| succ n =>
cases k with
| zero => simp
| succ k =>
simp only [List.insertIdx_succ_cons, List.getElem_cons_succ]
rw [ih (by omega)]
cases k with
| zero => omega
| succ k => simp
lemma orderedInsert_eq_insertIdx_orderedInsertPos {I : Type} (le1 : I → I → Prop) [DecidableRel le1]
(r : List I) (r0 : I) :
List.orderedInsert le1 r0 r = List.insertIdx (orderedInsertPos le1 r r0).1 r0 r := by
apply List.ext_get
· simp only [List.orderedInsert_length]
rw [List.length_insertIdx]
have h1 := orderedInsertPos_lt_length le1 r r0
simp only [List.length_cons] at h1
omega
intro n h1 h2
obtain ⟨n', hn'⟩ := (orderedInsertEquiv le1 r r0).surjective ⟨n, h1⟩
rw [← hn']
have hn'' : n = ((orderedInsertEquiv le1 r r0) n').val := by rw [hn']
subst hn''
rw [← orderedInsertEquiv_get]
simp only [List.length_cons, Function.comp_apply, Equiv.symm_apply_apply, List.get_eq_getElem]
match n' with
| ⟨0, h0⟩ =>
simp only [List.getElem_cons_zero, orderedInsertEquiv, List.length_cons, Nat.succ_eq_add_one,
OrderIso.toEquiv_symm, Fin.symm_castOrderIso, Fin.zero_eta, Equiv.trans_apply,
finExtractOne_apply_eq, Fin.isValue, finExtractOne_symm_inl_apply, RelIso.coe_fn_toEquiv,
Fin.castOrderIso_apply, Fin.cast_mk, Fin.eta]
rw [List.getElem_insertIdx_self]
exact Nat.le_of_lt_succ (orderedInsertPos_lt_length le1 r r0)
| ⟨Nat.succ n', h0⟩ =>
simp only [Nat.succ_eq_add_one, List.getElem_cons_succ, List.length_cons]
have hr := orderedInsertEquiv_succ le1 r r0 n' h0
trans (List.insertIdx (↑(orderedInsertPos le1 r r0)) r0 r).get
⟨↑((orderedInsertEquiv le1 r r0) ⟨n' +1, h0⟩), h2⟩
swap
· rfl
rw [Fin.ext_iff] at hr
have hx : (⟨↑((orderedInsertEquiv le1 r r0) ⟨n' +1, h0⟩), h2⟩ :
Fin (List.insertIdx (↑(orderedInsertPos le1 r r0)) r0 r).length) =
⟨((⟨↑(orderedInsertPos le1 r r0),
orderedInsertPos_lt_length le1 r r0⟩ : Fin ((r).length + 1))).succAbove
⟨n', Nat.succ_lt_succ_iff.mp h0⟩, by
erw [← hr]
exact h2⟩ := by
rw [Fin.ext_iff]
simp only [List.length_cons]
simpa using hr
rw [hx]
simp only [Fin.succAbove, Fin.castSucc_mk, Fin.mk_lt_mk, Fin.succ_mk, List.get_eq_getElem]
by_cases hn' : n' < ↑(orderedInsertPos le1 r r0)
· simp only [hn', ↓reduceIte]
erw [List.getElem_insertIdx_of_lt]
exact hn'
· simp only [hn', ↓reduceIte]
rw [List.getElem_insertIdx_of_ge]
· rfl
· omega
/-- The equivalence between `Fin l.length ≃ Fin (List.insertionSort r l).length` induced by the
sorting algorithm. -/
@ -114,16 +617,15 @@ def insertionSortEquiv {α : Type} (r : αα → Prop) [DecidableRel r] : (
Fin l.length ≃ Fin (List.insertionSort r l).length
| [] => Equiv.refl _
| a :: l =>
(Fin.equivCons (insertionSortEquiv r l)).trans (insertEquiv r a (List.insertionSort r l))
(Fin.equivCons (insertionSortEquiv r l)).trans (orderedInsertEquiv r (List.insertionSort r l) a)
lemma insertionSortEquiv_get {α : Type} {r : αα → Prop} [DecidableRel r] : (l : List α) →
l.get ∘ (insertionSortEquiv r l).symm = (List.insertionSort r l).get
| [] => by
simp [insertionSortEquiv]
| [] => by rfl
| a :: l => by
rw [insertionSortEquiv]
change ((a :: l).get ∘ ((Fin.equivCons (insertionSortEquiv r l))).symm) ∘
(insertEquiv r a (List.insertionSort r l)).symm = _
(orderedInsertEquiv r (List.insertionSort r l) a).symm = _
have hl : (a :: l).get ∘ ((Fin.equivCons (insertionSortEquiv r l))).symm =
(a :: List.insertionSort r l).get := by
ext x
@ -134,12 +636,103 @@ lemma insertionSortEquiv_get {α : Type} {r : αα → Prop} [DecidableRel
rw [← insertionSortEquiv_get (r := r) l]
rfl
rw [hl]
rw [insertEquiv_get (r := r) a (List.insertionSort r l)]
rw [orderedInsertEquiv_get r (List.insertionSort r l) a]
rfl
lemma insertionSortEquiv_congr {α : Type} {r : αα → Prop} [DecidableRel r] (l l' : List α)
(h : l = l') : insertionSortEquiv r l = (Fin.castOrderIso (by simp [h])).toEquiv.trans
((insertionSortEquiv r l').trans (Fin.castOrderIso (by simp [h])).toEquiv) := by
subst h
rfl
lemma insertionSort_get_comp_insertionSortEquiv {α : Type} {r : αα → Prop} [DecidableRel r]
(l : List α) : (List.insertionSort r l).get ∘ (insertionSortEquiv r l) = l.get := by
rw [← insertionSortEquiv_get]
funext x
simp
lemma insertionSort_eq_ofFn {α : Type} {r : αα → Prop} [DecidableRel r] (l : List α) :
List.insertionSort r l = List.ofFn (l.get ∘ (insertionSortEquiv r l).symm) := by
rw [insertionSortEquiv_get (r := r)]
exact Eq.symm (List.ofFn_get (List.insertionSort r l))
/-- Optional erase of an element in a list. For `none` returns the list, for `some i` returns
the list with the `i`'th element erased. -/
def optionErase {I : Type} (l : List I) (i : Option (Fin l.length)) : List I :=
match i with
| none => l
| some i => List.eraseIdx l i
/-- Optional erase of an element in a list, with addition for `none`. For `none` adds `a` to the
front of the list, for `some i` removes the `i`th element of the list (does not add `a`).
E.g. `optionEraseZ [0, 1, 2] 4 none = [4, 0, 1, 2]` and
`optionEraseZ [0, 1, 2] 4 (some 1) = [0, 2]`. -/
def optionEraseZ {I : Type} (l : List I) (a : I) (i : Option (Fin l.length)) : List I :=
match i with
| none => a :: l
| some i => List.eraseIdx l i
lemma eraseIdx_length {I : Type} (l : List I) (i : Fin l.length) :
(List.eraseIdx l i).length + 1 = l.length := by
simp only [List.length_eraseIdx, Fin.is_lt, ↓reduceIte]
have hi := i.prop
omega
lemma eraseIdx_cons_length {I : Type} (a : I) (l : List I) (i : Fin (a :: l).length) :
(List.eraseIdx (a :: l) i).length= l.length := by
simp [List.length_eraseIdx]
lemma eraseIdx_get {I : Type} (l : List I) (i : Fin l.length) :
(List.eraseIdx l i).get = l.get ∘ (Fin.cast (eraseIdx_length l i)) ∘
(Fin.cast (eraseIdx_length l i).symm i).succAbove := by
ext x
simp only [Function.comp_apply, List.get_eq_getElem, List.eraseIdx, List.getElem_eraseIdx]
simp only [Fin.succAbove, Fin.coe_cast]
by_cases hi: x.castSucc < Fin.cast (by exact Eq.symm (eraseIdx_length l i)) i
· simp only [hi, ↓reduceIte, Fin.coe_castSucc, dite_eq_left_iff, not_lt]
intro h
rw [Fin.lt_def] at hi
simp_all only [Fin.coe_castSucc, Fin.coe_cast]
omega
· simp only [hi, ↓reduceIte, Fin.val_succ]
rw [Fin.lt_def] at hi
simp only [Fin.coe_castSucc, Fin.coe_cast, not_lt] at hi
have hn : ¬ x.val < i.val := by omega
simp [hn]
lemma eraseIdx_insertionSort {I : Type} (le1 : I → I → Prop) [DecidableRel le1]
[IsTotal I le1] [IsTrans I le1] :
(n : ) → (r : List I) → (hn : n < r.length) →
(List.insertionSort le1 r).eraseIdx ↑((HepLean.List.insertionSortEquiv le1 r) ⟨n, hn⟩)
= List.insertionSort le1 (r.eraseIdx n)
| 0, [], _ => by rfl
| 0, (r0 :: r), hn => by
simp only [List.insertionSort, List.insertionSort.eq_2, List.length_cons, insertionSortEquiv,
Nat.succ_eq_add_one, Fin.zero_eta, Equiv.trans_apply, equivCons_zero, List.eraseIdx_zero,
List.tail_cons]
erw [orderedInsertEquiv_zero]
simp
| Nat.succ n, [], hn => by rfl
| Nat.succ n, (r0 :: r), hn => by
simp only [List.insertionSort, List.length_cons, insertionSortEquiv, Nat.succ_eq_add_one,
Equiv.trans_apply, equivCons_succ]
have hOr := orderedInsert_eraseIdx_orderedInsertEquiv_fin_succ le1
(List.insertionSort le1 r) r0 ((insertionSortEquiv le1 r) ⟨n, by simpa using hn⟩)
erw [hOr]
congr
refine eraseIdx_insertionSort le1 n r _
intro i j hij hn
have hx := List.Sorted.rel_get_of_lt (r := le1) (l := (List.insertionSort le1 r))
(List.sorted_insertionSort le1 r) hij
have ht (i j k : I) (hij : le1 i j) (hjk : ¬ le1 k j) : ¬ le1 k i := by
intro hik
have ht := IsTrans.trans (r := le1) k i j hik hij
exact hjk ht
exact ht ((List.insertionSort le1 r).get i) ((List.insertionSort le1 r).get j) r0 hx hn
lemma eraseIdx_insertionSort_fin {I : Type} (le1 : I → I → Prop) [DecidableRel le1]
[IsTotal I le1] [IsTrans I le1] (r : List I) (n : Fin r.length) :
(List.insertionSort le1 r).eraseIdx ↑((HepLean.List.insertionSortEquiv le1 r) n)
= List.insertionSort le1 (r.eraseIdx n) :=
eraseIdx_insertionSort le1 n.val r (Fin.prop n)
end HepLean.List

View file

@ -1,63 +0,0 @@
/-
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 HepLean.PerturbationTheory.Wick.Contract
import HepLean.PerturbationTheory.Wick.Species
/-!
# Feynman diagrams
This file currently contains a lighter implmentation of Feynman digrams than can be found in
`HepLean.PerturbationTheory.FeynmanDiagrams.Basic`. Eventually this will superseed that file.
The implmentation here is done in conjunction with Wicks species etc.
-/
/-! TODO: Remove this namespace-/
namespace LightFeynman
informal_definition FeynmanDiagram where
math :≈ "
Let S be a WickSpecies
A Feynman diagram contains the following data:
- A type of vertices 𝓥 → S.𝓯 ⊕ S.𝓘.
- A type of edges ed : 𝓔 → S.𝓕.
- A type of half-edges 𝓱𝓔 with maps `e : 𝓱𝓔𝓔`, `v : 𝓱𝓔𝓥` and `f : 𝓱𝓔 → S.𝓯`
Subject to the following conditions:
- `𝓱𝓔` is a double cover of `𝓔` through `e`. That is,
for each edge `x : 𝓔` there exists an isomorphism between `i : Fin 2 → e⁻¹ 𝓱𝓔 {x}`.
- These isomorphisms must satisfy `⟦f(i(0))⟧ = ⟦f(i(1))⟧ = ed(e)` and `f(i(0)) = S.ξ (f(i(1)))`.
- For each vertex `ver : 𝓥` there exists an isomorphism between the object (roughly)
`(𝓘Fields v).2` and the pullback of `v` along `ver`."
deps :≈ [``Wick.Species]
informal_definition _root_.Wick.Contract.toFeynmanDiagram where
math :≈ "The Feynman diagram constructed from a complete Wick contraction."
deps :≈ [``Wick.WickContract, ``FeynmanDiagram]
informal_lemma _root_.Wick.Contract.toFeynmanDiagram_surj where
math :≈ "The map from Wick contractions to Feynman diagrams is surjective."
physics :≈ "Every Feynman digram corresponds to some Wick contraction."
deps :≈ [``Wick.WickContract, ``FeynmanDiagram]
informal_definition FeynmanDiagram.toSimpleGraph where
math :≈ "The simple graph underlying a Feynman diagram."
deps :≈ [``FeynmanDiagram]
informal_definition FeynmanDiagram.IsConnected where
math :≈ "A Feynman diagram is connected if its underlying simple graph is connected."
deps :≈ [``FeynmanDiagram]
informal_definition _root_.Wick.Contract.toFeynmanDiagram_isConnected_iff where
math :≈ "The Feynman diagram corresponding to a Wick contraction is connected
if and only if the Wick contraction is connected."
deps :≈ [``Wick.WickContract.IsConnected, ``FeynmanDiagram.IsConnected]
/-! TODO: Define an equivalence relation on Wick contracts related to the their underlying tensors
been equal after permutation. Show that two Wick contractions are equal under this
equivalence relation if and only if they have the same Feynman diagram. First step
is to turn these statements into appropriate informal lemmas and definitions. -/
end LightFeynman

View file

@ -1,693 +0,0 @@
/-
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 HepLean.PerturbationTheory.Wick.Species
import HepLean.Lorentz.RealVector.Basic
import HepLean.Mathematics.Fin
import HepLean.SpaceTime.Basic
import HepLean.Mathematics.SuperAlgebra.Basic
import HepLean.Mathematics.List
import HepLean.Meta.Notes.Basic
import Init.Data.List.Sort.Basic
/-!
# Operator algebra
Currently this file is only for an example of Wick strings, correpsonding to a
theory with two complex scalar fields. The concepts will however generalize.
We will formally define the operator ring, in terms of the fields present in the theory.
## Futher reading
- https://physics.stackexchange.com/questions/258718/ and links therein
- Ryan Thorngren (https://physics.stackexchange.com/users/10336/ryan-thorngren), Fermions,
different species and (anti-)commutation rules, URL (version: 2019-02-20) :
https://physics.stackexchange.com/q/461929
- Tong, https://www.damtp.cam.ac.uk/user/tong/qft/qft.pdf
-/
namespace Wick
note r"
<h2>Operator algebra</h2>
Given a Wick Species $S$, we can define the operator algebra of that theory.
The operator algebra is a super-algebra over the complex numbers, which acts on
the Hilbert space of the theory. A super-algebra is an algebra with a $\mathbb{Z}/2$ grading.
To do pertubation theory in a QFT we need a need some basic properties of the operator algebra,
$A$.
<br><br>
For every field $f ∈ \mathcal{f}$, we have a number of families of operators. For every
space-time point $x ∈ \mathbb{R}^4$, we have the operators $ψ(f, x)$ which we decomponse into
a creation and destruction part, $ψ_c(f, x)$ and $ψ_d(f, x)$ respectively. Thus
$ψ(f, x) = ψ_c(f, x) + ψ_d(f, x)$.
For each momentum $p$ we also have the asymptotic states $φ_c(f, p)$ and $φ_d(f, p)$.
<br><br>
If the field $f$ corresponds to a fermion, then all of these operators are homogeneous elements
in the non-identity part of $A$. Conversely, if the field $f$ corresponds to a boson, then all
of these operators are homogeneous elements in the module of $A$ corresponding to
$0 ∈ \mathbb{Z}/2$.
<br><br>
The super-commutator of any of the operators above is in the center of the algebra. Moreover,
the following super-commutators are zero:
<ul>
<li>$[ψ_c(f, x), ψ_c(g, y)] = 0$</li>
<li>$[ψ_d(f, x), ψ_d(g, y)] = 0$</li>
<li>$[φ_c(f, p), φ_c(g, q)] = 0$</li>
<li>$[φ_d(f, p), φ_d(g, q)] = 0$</li>
<li>$[φ_c(f, p), φ_d(g, q)] = 0$ for $f \neq \xi g$</li>
<li>$[φ_d(f, p), ψ_c(g, y)] = 0$ for $f \neq \xi g$</li>
<li>$[φ_c(f, p), ψ_d(g, y)] = 0$ for $f \neq \xi g$</li>
</ul>
<br>
This basic structure constitutes what we call a Wick Algebra:
"
/-- The abstract notion of a operator algebra containing all the necessary ingrediants
to do perturbation theory.
Warning: The definition here is not complete. -/
@[note_attr]
structure WickAlgebra (S : Species) where
/-- The underlying operator algebra. -/
A : Type
/-- The type `A` is a semiring. -/
[A_semiring : Semiring A]
/-- The type `A` is an algebra. -/
[A_algebra : Algebra A]
/-- Position based field operators. -/
ψ : S.𝓯 → SpaceTime → A
/-- Position based constructive operators. -/
ψc : S.𝓯 → SpaceTime → A
/-- Position based destructive operators. -/
ψd : S.𝓯 → SpaceTime → A
/-- Constructive asymptotic operators. -/
φc : S.𝓯 → Lorentz.Contr 3 → A
/-- Distructive asymptotic operators. -/
φd : S.𝓯 → Lorentz.Contr 3 → A
ψc_ψd : ∀ i x, ψc i x + ψd i x = ψ i x
/- Self comutators. -/
ψc_comm_ψc : ∀ i j x y, ψc i x * ψc j y + (S.commFactor i j) • ψc j y * ψc i x = 0
ψd_comm_ψd : ∀ i j x y, ψd i x * ψd j y + (S.commFactor i j) • ψd j y * ψd i x = 0
φc_comm_φc : ∀ i j x y, φc i x * φc j y + (S.commFactor i j) • φc j y * φc i x = 0
φd_comm_φd : ∀ i j x y, φd i x * φd j y + (S.commFactor i j) • φd j y * φd i x = 0
/- Cross comutators. -/
namespace WickAlgebra
variable {S : Species} (𝓞 : WickAlgebra S)
/-- The type `A` of a Wick algebra is a semi-ring. -/
instance : Semiring 𝓞.A := 𝓞.A_semiring
/-- The type `A` of a Wick algebra is an algebra. -/
instance : Algebra 𝓞.A := 𝓞.A_algebra
end WickAlgebra
namespace Species
variable (S : Species)
note r"
<h2>Order</h2>
Suppose we have a type $I$ with a order $r$, a map $g : I \to \mathbb{Z}/2$,
and a map $f : I \to A$ such that $f(i) \in A_{g(i)}$.
Consider the free algebra generated by $I$, which we will denote $A_I$.
The map $f$ can be extended to a map $T_r : A_I \to A$ such that
a monomial $i_1 \cdots i_n$ gets mapped to $(-1)^{K(σ)}f(i_{σ(1)})...f(i_{σ(n)})$ where $σ$ is the
permutation oredering the $i$'s by $r$ (preserving the order of terms which are equal under $r$),
and $K(σ)$ is the Koszul sign factor. (see e.g. PSE:24157)
<br><br>
There are two types $I$ we are intrested in.
"
/-- Gives a factor of `-1` when inserting `a` into a list `List I` in the ordered position
for each fermion-fermion cross. -/
def koszulSignInsert {I : Type} (r : I → I → Prop) [DecidableRel r] (q : I → Fin 2) (a : I) :
List I →
| [] => 1
| b :: l => if r a b then 1 else
if q a = 1 ∧ q b = 1 then - koszulSignInsert r q a l else koszulSignInsert r q a l
/-- When inserting a boson the `koszulSignInsert` is always `1`. -/
lemma koszulSignInsert_boson {I : Type} (r : I → I → Prop) [DecidableRel r] (q : I → Fin 2) (a : I)
(ha : q a = 0) : (l : List I) → koszulSignInsert r q a l = 1
| [] => by
simp [koszulSignInsert]
| b :: l => by
simp only [koszulSignInsert, Fin.isValue, ite_eq_left_iff]
intro _
simp only [ha, Fin.isValue, zero_ne_one, false_and, ↓reduceIte]
exact koszulSignInsert_boson r q a ha l
/-- Gives a factor of `- 1` for every fermion-fermion (`q` is `1`) crossing that occurs when sorting
a list of based on `r`. -/
def koszulSign {I : Type} (r : I → I → Prop) [DecidableRel r] (q : I → Fin 2) :
List I →
| [] => 1
| a :: l => koszulSignInsert r q a l * koszulSign r q l
@[simp]
lemma koszulSign_freeMonoid_of {I : Type} (r : I → I → Prop) [DecidableRel r] (q : I → Fin 2)
(i : I) : koszulSign r q (FreeMonoid.of i) = 1 := by
change koszulSign r q [i] = 1
simp only [koszulSign, mul_one]
rfl
noncomputable section
/-- Given a relation `r` on `I` sorts elements of `MonoidAlgebra (FreeMonoid I)` by `r` giving it
a signed dependent on `q`. -/
def koszulOrderMonoidAlgebra {I : Type} (r : I → I → Prop) [DecidableRel r] (q : I → Fin 2) :
MonoidAlgebra (FreeMonoid I) →ₗ[] MonoidAlgebra (FreeMonoid I) :=
Finsupp.lift (MonoidAlgebra (FreeMonoid I)) (List I)
(fun i => Finsupp.lsingle (R := ) (List.insertionSort r i) (koszulSign r q i))
lemma koszulOrderMonoidAlgebra_ofList {I : Type} (r : I → I → Prop) [DecidableRel r]
(q : I → Fin 2) (i : List I) :
koszulOrderMonoidAlgebra r q (MonoidAlgebra.of (FreeMonoid I) i) =
(koszulSign r q i) • (MonoidAlgebra.of (FreeMonoid I) (List.insertionSort r i)) := by
simp only [koszulOrderMonoidAlgebra, Finsupp.lsingle_apply, MonoidAlgebra.of_apply,
MonoidAlgebra.smul_single', mul_one]
rw [MonoidAlgebra.ext_iff]
intro x
erw [Finsupp.lift_apply]
simp only [MonoidAlgebra.smul_single', zero_mul, Finsupp.single_zero, Finsupp.sum_single_index,
one_mul]
@[simp]
lemma koszulOrderMonoidAlgebra_single {I : Type} (r : I → I → Prop) [DecidableRel r] (q : I → Fin 2)
(l : FreeMonoid I) (x : ) :
koszulOrderMonoidAlgebra r q (MonoidAlgebra.single l x)
= (koszulSign r q l) • (MonoidAlgebra.single (List.insertionSort r l) x) := by
simp only [koszulOrderMonoidAlgebra, Finsupp.lsingle_apply, MonoidAlgebra.smul_single']
rw [MonoidAlgebra.ext_iff]
intro x'
erw [Finsupp.lift_apply]
simp only [MonoidAlgebra.smul_single', zero_mul, Finsupp.single_zero, Finsupp.sum_single_index,
one_mul, MonoidAlgebra.single]
congr 2
rw [NonUnitalNormedCommRing.mul_comm]
/-- Given a relation `r` on `I` sorts elements of `FreeAlgebra I` by `r` giving it
a signed dependent on `q`. -/
def koszulOrder {I : Type} (r : I → I → Prop) [DecidableRel r] (q : I → Fin 2) :
FreeAlgebra I →ₗ[] FreeAlgebra I :=
FreeAlgebra.equivMonoidAlgebraFreeMonoid.symm.toAlgHom.toLinearMap
∘ₗ koszulOrderMonoidAlgebra r q
∘ₗ FreeAlgebra.equivMonoidAlgebraFreeMonoid.toAlgHom.toLinearMap
lemma koszulOrder_ι {I : Type} (r : I → I → Prop) [DecidableRel r] (q : I → Fin 2) (i : I) :
koszulOrder r q (FreeAlgebra.ι i) = FreeAlgebra.ι i := by
simp only [koszulOrder, AlgEquiv.toAlgHom_eq_coe, AlgEquiv.toAlgHom_toLinearMap,
koszulOrderMonoidAlgebra, Finsupp.lsingle_apply, LinearMap.coe_comp, Function.comp_apply,
AlgEquiv.toLinearMap_apply]
rw [AlgEquiv.symm_apply_eq]
simp only [FreeAlgebra.equivMonoidAlgebraFreeMonoid, MonoidAlgebra.of_apply,
AlgEquiv.ofAlgHom_apply, FreeAlgebra.lift_ι_apply]
rw [@MonoidAlgebra.ext_iff]
intro x
erw [Finsupp.lift_apply]
simp only [MonoidAlgebra.smul_single', List.insertionSort, List.orderedInsert,
koszulSign_freeMonoid_of, mul_one, Finsupp.single_zero, Finsupp.sum_single_index]
rfl
@[simp]
lemma koszulOrder_single {I : Type} (r : I → I → Prop) [DecidableRel r] (q : I → Fin 2)
(l : FreeMonoid I) :
koszulOrder r q (FreeAlgebra.equivMonoidAlgebraFreeMonoid.symm (MonoidAlgebra.single l x))
= FreeAlgebra.equivMonoidAlgebraFreeMonoid.symm
(MonoidAlgebra.single (List.insertionSort r l) (koszulSign r q l * x)) := by
simp [koszulOrder]
end
/-- The indexing set of constructive and destructive position based operators. -/
def ConstDestAlgebra.index : Type := Fin 2 × S.𝓯 × SpaceTime
/-- The free algebra generated by constructive and destructive parts of fields position-based
fields. -/
abbrev ConstDestAlgebra := FreeAlgebra (ConstDestAlgebra.index S)
/-- The indexing set of position based field operators. -/
def FieldAlgebra.index : Type := S.𝓯 × SpaceTime
/-- The free algebra generated by fields. -/
abbrev FieldAlgebra := FreeAlgebra (FieldAlgebra.index S)
namespace ConstDestAlgebra
variable {S} (𝓞 : WickAlgebra S)
/-- The inclusion of constructive and destructive fields into the full operator algebra. -/
def toWickAlgebra : ConstDestAlgebra S →ₐ[] 𝓞.A :=
FreeAlgebra.lift (fun (i, f, x) =>
match i with
| 0 => 𝓞.ψc f x
| 1 => 𝓞.ψd f x)
@[simp]
lemma toWickAlgebra_ι_zero (x : S.𝓯 × SpaceTime) :
toWickAlgebra 𝓞 (FreeAlgebra.ι (0, x)) = 𝓞.ψc x.1 x.2 := by
simp [toWickAlgebra]
@[simp]
lemma toWickAlgebra_ι_one (x : S.𝓯 × SpaceTime) :
toWickAlgebra 𝓞 (FreeAlgebra.ι (1, x)) = 𝓞.ψd x.1 x.2 := by
simp [toWickAlgebra]
/-- The time ordering relation on constructive and destructive operators. -/
def timeOrderRel : index S → index S → Prop := fun x y => x.2.2 0 ≤ y.2.2 0
/-- The normal ordering relation on constructive and destructive operators. -/
def normalOrderRel : index S → index S → Prop := fun x y => x.1 ≤ y.1
/-- The normal ordering relation of constructive and destructive operators is decidable. -/
instance : DecidableRel (@normalOrderRel S) := fun a b => a.1.decLe b.1
noncomputable section
/-- The time ordering relation of constructive and destructive operators is decidable. -/
instance : DecidableRel (@timeOrderRel S) :=
fun a b => Real.decidableLE (a.2.2 0) (b.2.2 0)
/-- The time ordering of constructive and destructive operators. -/
def timeOrder (q : index S → Fin 2) : S.ConstDestAlgebra →ₗ[] S.ConstDestAlgebra :=
koszulOrder timeOrderRel q
/-- The normal ordering of constructive and destructive operators. -/
def normalOrder (q : index S → Fin 2) : S.ConstDestAlgebra →ₗ[] S.ConstDestAlgebra :=
koszulOrder normalOrderRel q
/-- Contraction of constructive and destructive operators, defined as their time
ordering minus their normal ordering. -/
def contract (q : index S → Fin 2) : S.ConstDestAlgebra →ₗ[] S.ConstDestAlgebra :=
timeOrder q - normalOrder q
end
end ConstDestAlgebra
namespace FieldAlgebra
variable {S} (𝓞 : WickAlgebra S)
/-- The inclusion fo the field algebra into the operator algebra. -/
def toWickAlgebra : FieldAlgebra S →ₐ[] 𝓞.A :=
FreeAlgebra.lift (fun i => 𝓞.ψ i.1 i.2)
@[simp]
lemma toWickAlgebra_ι (i : index S) : toWickAlgebra 𝓞 (FreeAlgebra.ι i) = 𝓞.ψ i.1 i.2 := by
simp [toWickAlgebra]
/-- The time ordering relation in the field algebra. -/
def timeOrderRel : index S → index S → Prop := fun x y => x.2 0 ≤ y.2 0
/-- The time ordering relation in the field algebra is decidable. -/
noncomputable instance : DecidableRel (@timeOrderRel S) :=
fun a b => Real.decidableLE (a.2 0) (b.2 0)
/-- The time ordering in the field algebra. -/
noncomputable def timeOrder (q : index S → Fin 2) : S.FieldAlgebra →ₗ[] S.FieldAlgebra :=
koszulOrder timeOrderRel q
/-- Given a list of fields and a map `f` tell us which field is constructive and
which is destructive, a list of constructive and destructive fields. -/
def listToConstDestList : (l : List (index S)) →
(f : Fin l.length → Fin 2) → List (ConstDestAlgebra.index S)
| [], _ => []
| i :: l, f =>
(f ⟨0, Nat.zero_lt_succ l.length⟩, i.1, i.2) :: listToConstDestList l (f ∘ Fin.succ)
@[simp]
lemma listToConstDestList_length (l : List (index S)) (f : Fin l.length → Fin 2) :
(listToConstDestList l f).length = l.length := by
induction l with
| nil => rfl
| cons i l ih =>
simp only [listToConstDestList, List.length_cons, Fin.zero_eta, Prod.mk.eta, add_left_inj]
rw [ih]
lemma listToConstDestList_insertionSortEquiv (l : List (index S))
(f : Fin l.length → Fin 2) :
(HepLean.List.insertionSortEquiv ConstDestAlgebra.timeOrderRel (listToConstDestList l f))
= (Fin.castOrderIso (by simp)).toEquiv.trans
((HepLean.List.insertionSortEquiv timeOrderRel l).trans
(Fin.castOrderIso (by simp)).toEquiv) := by
induction l with
| nil =>
simp [listToConstDestList, HepLean.List.insertionSortEquiv]
| cons i l ih =>
simp only [listToConstDestList, List.length_cons, Fin.zero_eta, List.insertionSort]
conv_lhs => simp [HepLean.List.insertionSortEquiv]
have h1 (l' : List (ConstDestAlgebra.index S)) :
(HepLean.List.insertEquiv ConstDestAlgebra.timeOrderRel (f ⟨0, by simp⟩, i.1, i.2) l') =
(Fin.castOrderIso (by simp)).toEquiv.trans
((HepLean.List.insertEquiv timeOrderRel (i.1, i.2) (l'.unzip).2).trans
(Fin.castOrderIso (by simp [List.orderedInsert_length])).toEquiv) := by
induction l' with
| nil =>
simp only [List.length_cons, Nat.add_zero, Nat.zero_eq, Fin.zero_eta, List.length_singleton,
List.orderedInsert, HepLean.List.insertEquiv, Fin.castOrderIso_refl,
OrderIso.refl_toEquiv, Equiv.trans_refl]
rfl
| cons j l' ih' =>
by_cases hr : ConstDestAlgebra.timeOrderRel (f ⟨0, by simp⟩, i) j
· rw [HepLean.List.insertEquiv_cons_pos]
· erw [HepLean.List.insertEquiv_cons_pos]
· rfl
· exact hr
· exact hr
· rw [HepLean.List.insertEquiv_cons_neg]
· erw [HepLean.List.insertEquiv_cons_neg]
· simp only [List.length_cons, Nat.add_zero, Nat.zero_eq, Fin.zero_eta,
List.orderedInsert, Prod.mk.eta, Fin.mk_one]
erw [ih']
ext x
simp only [Prod.mk.eta, List.length_cons, Nat.add_zero, Nat.zero_eq, Fin.zero_eta,
HepLean.Fin.equivCons_trans, Nat.succ_eq_add_one,
HepLean.Fin.equivCons_castOrderIso, Equiv.trans_apply, RelIso.coe_fn_toEquiv,
Fin.castOrderIso_apply, Fin.cast_trans, Fin.coe_cast]
congr 2
match x with
| ⟨0, h⟩ => rfl
| ⟨1, h⟩ => rfl
| ⟨Nat.succ (Nat.succ x), h⟩ => rfl
· exact hr
· exact hr
erw [h1]
rw [ih]
simp only [HepLean.Fin.equivCons_trans, Nat.succ_eq_add_one,
HepLean.Fin.equivCons_castOrderIso, List.length_cons, Nat.add_zero, Nat.zero_eq,
Fin.zero_eta]
ext x
conv_rhs => simp [HepLean.List.insertionSortEquiv]
simp only [Equiv.trans_apply, RelIso.coe_fn_toEquiv, Fin.castOrderIso_apply, Fin.cast_trans,
Fin.coe_cast]
have h2' (i : ConstDestAlgebra.index S) (l' : List (ConstDestAlgebra.index S)) :
(List.orderedInsert ConstDestAlgebra.timeOrderRel i l').unzip.2 =
List.orderedInsert timeOrderRel i.2 l'.unzip.2 := by
induction l' with
| nil =>
simp [HepLean.List.insertEquiv]
| cons j l' ih' =>
by_cases hij : ConstDestAlgebra.timeOrderRel i j
· rw [List.orderedInsert_of_le]
· erw [List.orderedInsert_of_le]
· simp
· exact hij
· exact hij
· simp only [List.orderedInsert, hij, ↓reduceIte, List.unzip_snd, List.map_cons]
have hn : ¬ timeOrderRel i.2 j.2 := hij
simp only [hn, ↓reduceIte, List.cons.injEq, true_and]
simpa using ih'
have h2 (l' : List (ConstDestAlgebra.index S)) :
(List.insertionSort ConstDestAlgebra.timeOrderRel l').unzip.2 =
List.insertionSort timeOrderRel l'.unzip.2 := by
induction l' with
| nil =>
simp [HepLean.List.insertEquiv]
| cons i l' ih' =>
simp only [List.insertionSort, List.unzip_snd]
simp only [List.unzip_snd] at h2'
rw [h2']
congr
simpa using ih'
rw [HepLean.List.insertEquiv_congr _ _ _ (h2 _)]
simp only [List.length_cons, Equiv.trans_apply, RelIso.coe_fn_toEquiv, Fin.castOrderIso_apply,
Fin.cast_trans, Fin.coe_cast]
have h3 : (List.insertionSort timeOrderRel (listToConstDestList l (f ∘ Fin.succ)).unzip.2) =
List.insertionSort timeOrderRel l := by
congr
have h3' (l : List (index S)) (f : Fin l.length → Fin 2) :
(listToConstDestList l (f)).unzip.2 = l := by
induction l with
| nil => rfl
| cons i l ih' =>
simp only [listToConstDestList, List.length_cons, Fin.zero_eta, Prod.mk.eta,
List.unzip_snd, List.map_cons, List.cons.injEq, true_and]
simpa using ih' (f ∘ Fin.succ)
rw [h3']
rw [HepLean.List.insertEquiv_congr _ _ _ h3]
simp only [List.length_cons, Equiv.trans_apply, RelIso.coe_fn_toEquiv, Fin.castOrderIso_apply,
Fin.cast_trans, Fin.cast_eq_self, Fin.coe_cast]
rfl
lemma listToConstDestList_get (l : List (index S)) (f : Fin l.length → Fin 2) :
(listToConstDestList l f).get = (fun i => (f i, l.get i)) ∘ Fin.cast (by simp) := by
induction l with
| nil =>
funext i
exact Fin.elim0 i
| cons i l ih =>
simp only [listToConstDestList, List.length_cons, Fin.zero_eta, List.get_eq_getElem]
funext x
match x with
| ⟨0, h⟩ => rfl
| ⟨x + 1, h⟩ =>
simp only [List.length_cons, List.get_eq_getElem, Prod.mk.eta, List.getElem_cons_succ,
Function.comp_apply, Fin.cast_mk]
change (listToConstDestList l _).get _ = _
rw [ih]
simp
lemma listToConstDestList_timeOrder (l : List (index S)) (f : Fin l.length → Fin 2) :
List.insertionSort ConstDestAlgebra.timeOrderRel (listToConstDestList l f) =
listToConstDestList (List.insertionSort timeOrderRel l)
(f ∘ (HepLean.List.insertionSortEquiv (timeOrderRel) l).symm) := by
let l1 := List.insertionSort (ConstDestAlgebra.timeOrderRel) (listToConstDestList l f)
let l2 := listToConstDestList (List.insertionSort timeOrderRel l)
(f ∘ (HepLean.List.insertionSortEquiv (timeOrderRel) l).symm)
change l1 = l2
have hlen : l1.length = l2.length := by
simp [l1, l2]
have hget : l1.get = l2.get ∘ Fin.cast hlen := by
rw [← HepLean.List.insertionSortEquiv_get]
rw [listToConstDestList_get]
rw [listToConstDestList_get]
rw [← HepLean.List.insertionSortEquiv_get]
funext i
simp only [List.get_eq_getElem, Function.comp_apply, Fin.coe_cast, Fin.cast_trans]
congr 2
· rw [listToConstDestList_insertionSortEquiv]
simp
· rw [listToConstDestList_insertionSortEquiv]
simp
apply List.ext_get hlen
rw [hget]
simp
lemma listToConstDestList_koszulSignInsert (q : index S → Fin 2) (l : List (index S)) (i : index S)
(f : Fin l.length → Fin 2) (a : Fin 2) :
koszulSignInsert ConstDestAlgebra.timeOrderRel (fun i => q i.2) (a, i)
(listToConstDestList l f) = koszulSignInsert timeOrderRel q i l := by
induction l with
| nil =>
simp [listToConstDestList, koszulSignInsert]
| cons j s ih =>
simp only [koszulSignInsert, List.length_cons, Fin.zero_eta, Prod.mk.eta, Fin.isValue]
by_cases hr : ConstDestAlgebra.timeOrderRel (a, i) (f ⟨0, by simp⟩, j)
· rw [if_pos]
· rw [if_pos]
· exact hr
· exact hr
· rw [if_neg]
· nth_rewrite 2 [if_neg]
· rw [ih (f ∘ Fin.succ)]
· exact hr
· exact hr
lemma listToConstDestList_koszulSign (q : index S → Fin 2) (l : List (index S))
(f : Fin l.length → Fin 2) :
koszulSign ConstDestAlgebra.timeOrderRel (fun i => q i.2) (listToConstDestList l f) =
koszulSign timeOrderRel q l := by
induction l with
| nil => rfl
| cons i l ih =>
simp only [koszulSign, List.length_cons, Fin.zero_eta, Prod.mk.eta]
rw [ih]
simp only [mul_eq_mul_right_iff]
apply Or.inl
exact listToConstDestList_koszulSignInsert q l i _ _
/-- The map from the field algebra to the algebra of constructive and destructive fields. -/
def toConstDestAlgebra : FieldAlgebra S →ₐ[] ConstDestAlgebra S :=
FreeAlgebra.lift (fun i => FreeAlgebra.ι (0, i) + FreeAlgebra.ι (1, i))
@[simp]
lemma toConstDestAlgebra_ι (i : index S) : toConstDestAlgebra (FreeAlgebra.ι i) =
FreeAlgebra.ι (0, i) + FreeAlgebra.ι (1, i) := by
simp [toConstDestAlgebra]
lemma toConstDestAlgebra_single (x : ) : (l : FreeMonoid (index S)) →
toConstDestAlgebra (FreeAlgebra.equivMonoidAlgebraFreeMonoid.symm (MonoidAlgebra.single l x))
= ∑ (f : Fin l.length → Fin 2), FreeAlgebra.equivMonoidAlgebraFreeMonoid.symm
(MonoidAlgebra.single (listToConstDestList l f) x)
| [] => by
simp only [MonoidAlgebra.single, FreeMonoid.length, List.length_nil, Finset.univ_unique,
listToConstDestList, Finset.sum_const, Finset.card_singleton, one_smul]
trans x • 1
· trans toConstDestAlgebra (x • 1)
· congr
simp only [FreeAlgebra.equivMonoidAlgebraFreeMonoid, MonoidAlgebra.of_apply,
FreeMonoid.lift, FreeMonoid.prodAux, FreeMonoid.toList, Equiv.coe_fn_mk,
AlgEquiv.ofAlgHom_symm_apply, MonoidAlgebra.lift_single, MonoidHom.coe_mk, OneHom.coe_mk]
rfl
· simp only [toConstDestAlgebra, Fin.isValue, map_smul, map_one]
· simp only [FreeAlgebra.equivMonoidAlgebraFreeMonoid, MonoidAlgebra.of_apply, FreeMonoid.lift,
FreeMonoid.prodAux, FreeMonoid.toList, Equiv.coe_fn_mk, AlgEquiv.ofAlgHom_symm_apply,
MonoidAlgebra.lift_single, MonoidHom.coe_mk, OneHom.coe_mk]
rfl
| i :: l => by
simp only [MonoidAlgebra.single, FreeMonoid.length, List.length_cons, listToConstDestList,
Fin.zero_eta, Prod.mk.eta]
have h1 : FreeAlgebra.equivMonoidAlgebraFreeMonoid.symm (Finsupp.single (i :: l) x) =
(FreeAlgebra.ι i) *
(FreeAlgebra.equivMonoidAlgebraFreeMonoid.symm (Finsupp.single l x)) := by
simp only [FreeAlgebra.equivMonoidAlgebraFreeMonoid, MonoidAlgebra.of_apply,
AlgEquiv.ofAlgHom_symm_apply, MonoidAlgebra.lift_single, Algebra.mul_smul_comm]
congr
simp only [FreeMonoid.lift, FreeMonoid.prodAux, FreeMonoid.toList, Equiv.coe_fn_mk,
MonoidHom.coe_mk, OneHom.coe_mk]
change List.foldl (fun x1 x2 => x1 * x2)
(FreeAlgebra.ι i) (List.map (FreeAlgebra.ι ) l) = _
match l with
| [] =>
simp only [List.map_nil, List.foldl_nil, ne_eq, FreeAlgebra.ι_ne_zero, not_false_eq_true,
left_eq_mul₀]
rfl
| x :: l =>
simp only [List.map_cons, List.foldl_cons]
change _ = FreeAlgebra.ι i * List.foldl (fun x1 x2 => x1 * x2) _ _
rw [List.foldl_assoc]
rw [h1]
rw [map_mul]
trans ∑ f : Fin (l.length + 1) → Fin 2, (FreeAlgebra.ι ((f 0, i)) : ConstDestAlgebra S) *
(FreeAlgebra.equivMonoidAlgebraFreeMonoid.symm
(Finsupp.single (listToConstDestList l (f ∘ Fin.succ)) x) : ConstDestAlgebra S)
· rw [← (Fin.consEquiv (n := l.length) (fun _ => Fin 2)).sum_comp
(α := FreeAlgebra (ConstDestAlgebra.index S))]
erw [Finset.sum_product]
simp only [toConstDestAlgebra_ι, Fin.isValue, Fin.consEquiv_apply, Fin.cons_zero,
Fin.sum_univ_two]
rw [← Finset.mul_sum, ← Finset.mul_sum]
erw [← toConstDestAlgebra_single]
rw [add_mul]
· congr
funext f
simp only [FreeAlgebra.equivMonoidAlgebraFreeMonoid, MonoidAlgebra.of_apply,
AlgEquiv.ofAlgHom_symm_apply, MonoidAlgebra.lift_single, Algebra.mul_smul_comm]
congr
simp only [FreeMonoid.lift, FreeMonoid.prodAux, FreeMonoid.toList, Equiv.coe_fn_mk,
MonoidHom.coe_mk, OneHom.coe_mk]
match l with
| [] =>
simp only [listToConstDestList]
change FreeAlgebra.ι (f 0, i) * 1 = _
simp only [mul_one]
rfl
| x :: l =>
simp only [listToConstDestList, List.length_cons, Fin.zero_eta, Function.comp_apply,
Fin.succ_zero_eq_one, Prod.mk.eta]
change FreeAlgebra.ι (f 0, i) * List.foldl _ _ _ = List.foldl _ _ _
simp only [List.map_cons, List.foldl_cons]
haveI : Std.Associative fun
(x1 x2 : FreeAlgebra (ConstDestAlgebra.index S)) => x1 * x2 := by
exact Semigroup.to_isAssociative
refine Eq.symm List.foldl_assoc
lemma toWickAlgebra_factor_toConstDestAlgebra :
toWickAlgebra 𝓞 = (ConstDestAlgebra.toWickAlgebra 𝓞).comp toConstDestAlgebra := by
refine FreeAlgebra.hom_ext ?_
funext i
simp only [Function.comp_apply, toWickAlgebra_ι, ConstDestAlgebra.toWickAlgebra, AlgHom.coe_comp,
toConstDestAlgebra_ι, Fin.isValue, map_add, FreeAlgebra.lift_ι_apply]
split
rename_i x i_1 f x_1 heq
simp_all only [Fin.isValue, Prod.mk.injEq]
obtain ⟨left, right⟩ := heq
subst left right
exact Eq.symm (𝓞.ψc_ψd f x_1)
/-- Time ordering fields and then mapping to constructive and destructive fields is the same as
mapping to constructive and destructive fields and then time ordering. -/
lemma timeOrder_comm_toConstDestAlgebra (q : index S → Fin 2) :
(ConstDestAlgebra.timeOrder (fun i => q i.2)).comp toConstDestAlgebra.toLinearMap =
toConstDestAlgebra.toLinearMap.comp (timeOrder q) := by
let e : S.FieldAlgebra ≃ₗ[] MonoidAlgebra (FreeMonoid (index S)) :=
FreeAlgebra.equivMonoidAlgebraFreeMonoid.toLinearEquiv
apply (LinearEquiv.eq_comp_toLinearMap_iff (e₁₂ := e.symm) _ _).mp
apply MonoidAlgebra.lhom_ext'
intro l
apply LinearMap.ext
intro x
simp only [AlgEquiv.toLinearEquiv_symm, AlgEquiv.toLinearEquiv_toLinearMap, LinearMap.coe_comp,
Function.comp_apply, MonoidAlgebra.lsingle_apply, AlgEquiv.toLinearMap_apply,
AlgHom.toLinearMap_apply, toConstDestAlgebra_single, map_sum, timeOrder, koszulOrder_single, e]
simp only [FreeMonoid.length]
let ew := Equiv.piCongrLeft' (fun _ => Fin 2)
(HepLean.List.insertionSortEquiv (timeOrderRel) l)
rw [← ew.sum_comp (α := FreeAlgebra (ConstDestAlgebra.index S))]
congr
funext f
simp only [ConstDestAlgebra.timeOrder, koszulOrder_single, EmbeddingLike.apply_eq_iff_eq]
congr 1
· rw [listToConstDestList_timeOrder]
simp only [ew]
rfl
· simp only [mul_eq_mul_right_iff]
exact Or.inl (listToConstDestList_koszulSign q l f)
/-- The contraction of fields defined as the time order minus normal order once mapped down
to constructive and destructive fields. -/
noncomputable def contract (q : index S → Fin 2) : FieldAlgebra S →ₗ[] ConstDestAlgebra S :=
ConstDestAlgebra.contract (fun i => q i.2) ∘ₗ toConstDestAlgebra.toLinearMap
end FieldAlgebra
end Species
informal_definition asymptoicContract where
math :≈ "Given two `i j : S.𝓯 × SpaceTime`, the super-commutator [φd(i), ψ(j)]."
ref :≈ "See e.g. http://www.dylanjtemples.com:82/solutions/QFT_Solution_I-6.pdf"
informal_definition contractAsymptotic where
math :≈ "Given two `i j : S.𝓯 × SpaceTime`, the super-commutator [ψ(i), φc(j)]."
informal_definition asymptoicContractAsymptotic where
math :≈ "Given two `i j : S.𝓯 × SpaceTime`, the super-commutator
[φd(i), φc(j)]."
informal_lemma contraction_in_center where
math :≈ "The contraction of two fields is in the center of the algebra."
deps :≈ [``WickAlgebra]
informal_lemma contraction_non_dual_is_zero where
math :≈ "The contraction of two fields is zero if the fields are not dual to each other."
deps :≈ [``WickAlgebra]
informal_lemma timeOrder_single where
math :≈ "The time ordering of a single field is the normal ordering of that field."
proof :≈ "Follows from the definitions."
deps :≈ [``WickAlgebra]
informal_lemma timeOrder_pair where
math :≈ "The time ordering of two fields is the normal ordering of the fields plus the
contraction of the fields."
proof :≈ "Follows from the definition of contraction."
deps :≈ [``WickAlgebra]
informal_definition WickMap where
math :≈ "A linear map `vev` from the Wick algebra `A` to the underlying field such that
`vev(...ψd(t)) = 0` and `vev(ψc(t)...) = 0`."
physics :≈ "An abstraction of the notion of a vacuum expectation value, containing
the necessary properties for lots of theorems to hold."
deps :≈ [``WickAlgebra]
informal_lemma normalOrder_wickMap where
math :≈ "Any normal ordering maps to zero under a Wick map."
deps :≈ [``WickMap]
end Wick

View file

@ -1,665 +0,0 @@
/-
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 HepLean.PerturbationTheory.Wick.String
import Mathlib.Algebra.Order.Ring.Nat
import Mathlib.Data.Fintype.Sum
import Mathlib.Logic.Equiv.Fin
import HepLean.Meta.Notes.Basic
/-!
# Wick Contract
## Further reading
- https://www.imperial.ac.uk/media/imperial-college/research-centres-and-groups/theoretical-physics/msc/current/qft/handouts/qftwickstheorem.pdf
-/
namespace Wick
variable {S : Species}
note r"
<h2>Wick Contractions</h2>
"
/-- A Wick contraction for a Wick string is a series of pairs `i` and `j` of indices
to be contracted, subject to ordering and subject to the condition that they can
be contracted. -/
inductive WickContract : {ni : } → {i : Fin ni → S.𝓯} → {n : } → {c : Fin n → S.𝓯} →
{no : } → {o : Fin no → S.𝓯} →
(str : WickString i c o final) →
{k : } → (b1 : Fin k → Fin n) → (b2 : Fin k → Fin n) → Type where
| string {ni : } {i : Fin ni → S.𝓯} {n : } {c : Fin n → S.𝓯}
{no : } {o : Fin no → S.𝓯}
{str : WickString i c o final} : WickContract str Fin.elim0 Fin.elim0
| contr {ni : } {i : Fin ni → S.𝓯} {n : } {c : Fin n → S.𝓯}
{no : } {o : Fin no → S.𝓯} {str : WickString i c o final} {k : }
{b1 : Fin k → Fin n} {b2 : Fin k → Fin n} : (i : Fin n) →
(j : Fin n) → (h : c j = S.ξ (c i)) →
(hilej : i < j) → (hb1 : ∀ r, b1 r < i) → (hb2i : ∀ r, b2 r ≠ i) → (hb2j : ∀ r, b2 r ≠ j) →
(w : WickContract str b1 b2) →
WickContract str (Fin.snoc b1 i) (Fin.snoc b2 j)
namespace WickContract
/-- The number of nodes of a Wick contraction. -/
def size {ni : } {i : Fin ni → S.𝓯} {n : } {c : Fin n → S.𝓯}
{no : } {o : Fin no → S.𝓯} {str : WickString i c o final} {k : } {b1 b2 : Fin k → Fin n} :
WickContract str b1 b2 → := fun
| string => 0
| contr _ _ _ _ _ _ _ w => w.size + 1
/-- The number of nodes in a wick contraction tree is the same as `k`. -/
lemma size_eq_k {ni : } {i : Fin ni → S.𝓯} {n : } {c : Fin n → S.𝓯}
{no : } {o : Fin no → S.𝓯} {str : WickString i c o final} {k : } {b1 b2 : Fin k → Fin n} :
(w : WickContract str b1 b2) → w.size = k := fun
| string => rfl
| contr _ _ _ _ _ _ _ w => by
simpa [size] using w.size_eq_k
/-- The map giving the vertices on the left-hand-side of a contraction. -/
@[nolint unusedArguments]
def boundFst {ni : } {i : Fin ni → S.𝓯} {n : } {c : Fin n → S.𝓯}
{no : } {o : Fin no → S.𝓯} {str : WickString i c o final}
{k : } {b1 b2 : Fin k → Fin n} :
WickContract str b1 b2 → Fin k → Fin n := fun _ => b1
@[simp]
lemma boundFst_contr_castSucc {ni : } {i : Fin ni → S.𝓯} {n : } {c : Fin n → S.𝓯}
{no : } {o : Fin no → S.𝓯} {str : WickString i c o final}
{k : } {b1 b2 : Fin k → Fin n} (i j : Fin n)
(h : c j = S.ξ (c i))
(hilej : i < j)
(hb1 : ∀ r, b1 r < i)
(hb2i : ∀ r, b2 r ≠ i)
(hb2j : ∀ r, b2 r ≠ j)
(w : WickContract str b1 b2) (r : Fin k) :
(contr i j h hilej hb1 hb2i hb2j w).boundFst r.castSucc = w.boundFst r := by
simp only [boundFst, Fin.snoc_castSucc]
@[simp]
lemma boundFst_contr_last {ni : } {i : Fin ni → S.𝓯} {n : } {c : Fin n → S.𝓯}
{no : } {o : Fin no → S.𝓯} {str : WickString i c o final}
{k : } {b1 b2 : Fin k → Fin n} (i j : Fin n)
(h : c j = S.ξ (c i))
(hilej : i < j)
(hb1 : ∀ r, b1 r < i)
(hb2i : ∀ r, b2 r ≠ i)
(hb2j : ∀ r, b2 r ≠ j)
(w : WickContract str b1 b2) :
(contr i j h hilej hb1 hb2i hb2j w).boundFst (Fin.last k) = i := by
simp only [boundFst, Fin.snoc_last]
lemma boundFst_strictMono {ni : } {i : Fin ni → S.𝓯} {n : } {c : Fin n → S.𝓯}
{no : } {o : Fin no → S.𝓯} {str : WickString i c o final}
{k : } {b1 b2 : Fin k → Fin n} : (w : WickContract str b1 b2) → StrictMono w.boundFst := fun
| string => fun k => Fin.elim0 k
| contr i j _ _ hb1 _ _ w => by
intro r s hrs
rcases Fin.eq_castSucc_or_eq_last r with hr | hr
· obtain ⟨r, hr⟩ := hr
subst hr
rcases Fin.eq_castSucc_or_eq_last s with hs | hs
· obtain ⟨s, hs⟩ := hs
subst hs
simp only [boundFst_contr_castSucc]
apply w.boundFst_strictMono _
simpa using hrs
· subst hs
simp only [boundFst_contr_castSucc, boundFst_contr_last]
exact hb1 r
· subst hr
rcases Fin.eq_castSucc_or_eq_last s with hs | hs
· obtain ⟨s, hs⟩ := hs
subst hs
rw [Fin.lt_def] at hrs
simp only [Fin.val_last, Fin.coe_castSucc] at hrs
omega
· subst hs
simp at hrs
/-- The map giving the vertices on the right-hand-side of a contraction. -/
@[nolint unusedArguments]
def boundSnd {ni : } {i : Fin ni → S.𝓯} {n : } {c : Fin n → S.𝓯}
{no : } {o : Fin no → S.𝓯} {str : WickString i c o final}
{k : } {b1 b2 : Fin k → Fin n} :
WickContract str b1 b2 → Fin k → Fin n := fun _ => b2
@[simp]
lemma boundSnd_contr_castSucc {ni : } {i : Fin ni → S.𝓯} {n : } {c : Fin n → S.𝓯}
{no : } {o : Fin no → S.𝓯} {str : WickString i c o final}
{k : } {b1 b2 : Fin k → Fin n} (i j : Fin n)
(h : c j = S.ξ (c i))
(hilej : i < j)
(hb1 : ∀ r, b1 r < i)
(hb2i : ∀ r, b2 r ≠ i)
(hb2j : ∀ r, b2 r ≠ j)
(w : WickContract str b1 b2) (r : Fin k) :
(contr i j h hilej hb1 hb2i hb2j w).boundSnd r.castSucc = w.boundSnd r := by
simp only [boundSnd, Fin.snoc_castSucc]
@[simp]
lemma boundSnd_contr_last {ni : } {i : Fin ni → S.𝓯} {n : } {c : Fin n → S.𝓯}
{no : } {o : Fin no → S.𝓯} {str : WickString i c o final}
{k : } {b1 b2 : Fin k → Fin n} (i j : Fin n)
(h : c j = S.ξ (c i))
(hilej : i < j)
(hb1 : ∀ r, b1 r < i)
(hb2i : ∀ r, b2 r ≠ i)
(hb2j : ∀ r, b2 r ≠ j)
(w : WickContract str b1 b2) :
(contr i j h hilej hb1 hb2i hb2j w).boundSnd (Fin.last k) = j := by
simp only [boundSnd, Fin.snoc_last]
lemma boundSnd_injective {ni : } {i : Fin ni → S.𝓯} {n : } {c : Fin n → S.𝓯}
{no : } {o : Fin no → S.𝓯} {str : WickString i c o final}
{k : } {b1 b2 : Fin k → Fin n} :
(w : WickContract str b1 b2) → Function.Injective w.boundSnd := fun
| string => by
intro i j _
exact Fin.elim0 i
| contr i j hij hilej hi h2i h2j w => by
intro r s hrs
rcases Fin.eq_castSucc_or_eq_last r with hr | hr
· obtain ⟨r, hr⟩ := hr
subst hr
rcases Fin.eq_castSucc_or_eq_last s with hs | hs
· obtain ⟨s, hs⟩ := hs
subst hs
simp only [boundSnd_contr_castSucc] at hrs
simpa using w.boundSnd_injective hrs
· subst hs
simp only [boundSnd_contr_castSucc, boundSnd_contr_last] at hrs
exact False.elim (h2j r hrs)
· subst hr
rcases Fin.eq_castSucc_or_eq_last s with hs | hs
· obtain ⟨s, hs⟩ := hs
subst hs
simp only [boundSnd_contr_last, boundSnd_contr_castSucc] at hrs
exact False.elim (h2j s hrs.symm)
· subst hs
rfl
lemma color_boundSnd_eq_dual_boundFst {ni : } {i : Fin ni → S.𝓯} {n : } {c : Fin n → S.𝓯}
{no : } {o : Fin no → S.𝓯} {str : WickString i c o final}
{k : } {b1 b2 : Fin k → Fin n} :
(w : WickContract str b1 b2) → (i : Fin k) → c (w.boundSnd i) = S.ξ (c (w.boundFst i)) := fun
| string => fun i => Fin.elim0 i
| contr i j hij hilej hi _ _ w => fun r => by
rcases Fin.eq_castSucc_or_eq_last r with hr | hr
· obtain ⟨r, hr⟩ := hr
subst hr
simpa using w.color_boundSnd_eq_dual_boundFst r
· subst hr
simpa using hij
lemma boundFst_lt_boundSnd {ni : } {i : Fin ni → S.𝓯} {n : } {c : Fin n → S.𝓯}
{no : } {o : Fin no → S.𝓯} {str : WickString i c o final}
{k : } {b1 b2 : Fin k → Fin n} : (w : WickContract str b1 b2) → (i : Fin k) →
w.boundFst i < w.boundSnd i := fun
| string => fun i => Fin.elim0 i
| contr i j hij hilej hi _ _ w => fun r => by
rcases Fin.eq_castSucc_or_eq_last r with hr | hr
· obtain ⟨r, hr⟩ := hr
subst hr
simpa using w.boundFst_lt_boundSnd r
· subst hr
simp only [boundFst_contr_last, boundSnd_contr_last]
exact hilej
lemma boundFst_neq_boundSnd {ni : } {i : Fin ni → S.𝓯} {n : } {c : Fin n → S.𝓯}
{no : } {o : Fin no → S.𝓯} {str : WickString i c o final}
{k : } {b1 b2 : Fin k → Fin n} :
(w : WickContract str b1 b2) → (r1 r2 : Fin k) → b1 r1 ≠ b2 r2 := fun
| string => fun i => Fin.elim0 i
| contr i j _ hilej h1 h2i h2j w => fun r s => by
rcases Fin.eq_castSucc_or_eq_last r with hr | hr
<;> rcases Fin.eq_castSucc_or_eq_last s with hs | hs
· obtain ⟨r, hr⟩ := hr
obtain ⟨s, hs⟩ := hs
subst hr hs
simpa using w.boundFst_neq_boundSnd r s
· obtain ⟨r, hr⟩ := hr
subst hr hs
simp only [Fin.snoc_castSucc, Fin.snoc_last, ne_eq]
have hn := h1 r
omega
· obtain ⟨s, hs⟩ := hs
subst hr hs
simp only [Fin.snoc_last, Fin.snoc_castSucc, ne_eq]
exact (h2i s).symm
· subst hr hs
simp only [Fin.snoc_last, ne_eq]
omega
/-- Casts a Wick contraction from `WickContract str b1 b2` to `WickContract str b1' b2'` with a
proof that `b1 = b1'` and `b2 = b2'`, and that they are defined from the same `k = k'`. -/
def castMaps {ni : } {i : Fin ni → S.𝓯} {n : } {c : Fin n → S.𝓯}
{no : } {o : Fin no → S.𝓯} {str : WickString i c o final}
{k k' : } {b1 b2 : Fin k → Fin n} {b1' b2' : Fin k' → Fin n}
(hk : k = k')
(hb1 : b1 = b1' ∘ Fin.cast hk) (hb2 : b2 = b2' ∘ Fin.cast hk) (w : WickContract str b1 b2) :
WickContract str b1' b2' :=
cast (by subst hk; rfl) (hb2 ▸ hb1 ▸ w)
@[simp]
lemma castMaps_rfl {ni : } {i : Fin ni → S.𝓯} {n : } {c : Fin n → S.𝓯}
{no : } {o : Fin no → S.𝓯} {str : WickString i c o final}
{k : } {b1 b2 : Fin k → Fin n} (w : WickContract str b1 b2) :
castMaps rfl rfl rfl w = w := rfl
lemma mem_snoc' {ni : } {i : Fin ni → S.𝓯} {n : } {c : Fin n → S.𝓯}
{no : } {o : Fin no → S.𝓯} {str : WickString i c o final}
{k : } {b1' b2' : Fin k → Fin n} :
(w : WickContract str b1' b2') →
{k' : } → (hk' : k'.succ = k) →
(b1 b2 : Fin k' → Fin n) → (i j : Fin n) → (h : c j = S.ξ (c i)) →
(hilej : i < j) → (hb1 : ∀ r, b1 r < i) → (hb2i : ∀ r, b2 r ≠ i) → (hb2j : ∀ r, b2 r ≠ j) →
(hb1' : Fin.snoc b1 i = b1' ∘ Fin.cast hk') →
(hb2' : Fin.snoc b2 j = b2' ∘ Fin.cast hk') →
∃ (w' : WickContract str b1 b2), w = castMaps hk' hb1' hb2'
(contr i j h hilej hb1 hb2i hb2j w') := fun
| string => fun hk' => by
simp at hk'
| contr i' j' h' hilej' hb1' hb2i' hb2j' w' => by
intro hk b1 b2 i j h hilej hb1 hb2i hb2j hb1' hb2'
rename_i k' k b1' b2' f
have hk2 : k' = k := Nat.succ_inj'.mp hk
subst hk2
simp_all
have hb2'' : b2 = b2' := by
funext k
trans (@Fin.snoc k' (fun _ => Fin n) b2 j) (Fin.castSucc k)
· simp
· rw [hb2']
simp
have hb1'' : b1 = b1' := by
funext k
trans (@Fin.snoc k' (fun _ => Fin n) b1 i) (Fin.castSucc k)
· simp
· rw [hb1']
simp
have hi : i = i' := by
trans (@Fin.snoc k' (fun _ => Fin n) b1 i) (Fin.last k')
· simp
· rw [hb1']
simp
have hj : j = j' := by
trans (@Fin.snoc k' (fun _ => Fin n) b2 j) (Fin.last k')
· simp
· rw [hb2']
simp
subst hb1'' hb2'' hi hj
simp
lemma mem_snoc {ni : } {i : Fin ni → S.𝓯} {n : } {c : Fin n → S.𝓯}
{no : } {o : Fin no → S.𝓯} {str : WickString i c o final}
{k : } {b1 b2 : Fin k → Fin n}
(i j : Fin n) (h : c j = S.ξ (c i)) (hilej : i < j) (hb1 : ∀ r, b1 r < i)
(hb2i : ∀ r, b2 r ≠ i) (hb2j : ∀ r, b2 r ≠ j)
(w : WickContract str (Fin.snoc b1 i) (Fin.snoc b2 j)) :
∃ (w' : WickContract str b1 b2), w = contr i j h hilej hb1 hb2i hb2j w' := by
exact mem_snoc' w rfl b1 b2 i j h hilej hb1 hb2i hb2j rfl rfl
lemma is_subsingleton {ni : } {i : Fin ni → S.𝓯} {n : } {c : Fin n → S.𝓯}
{no : } {o : Fin no → S.𝓯} {str : WickString i c o final}
{k : } {b1 b2 : Fin k → Fin n} :
Subsingleton (WickContract str b1 b2) := Subsingleton.intro fun w1 w2 => by
induction k with
| zero =>
have hb1 : b1 = Fin.elim0 := Subsingleton.elim _ _
have hb2 : b2 = Fin.elim0 := Subsingleton.elim _ _
subst hb1 hb2
match w1, w2 with
| string, string => rfl
| succ k hI =>
match w1, w2 with
| contr i j h hilej hb1 hb2i hb2j w, w2 =>
let ⟨w', hw'⟩ := mem_snoc i j h hilej hb1 hb2i hb2j w2
rw [hw']
apply congrArg (contr i j _ _ _ _ _) (hI w w')
lemma eq_snoc_castSucc {k n : } (b1 : Fin k.succ → Fin n) :
b1 = Fin.snoc (b1 ∘ Fin.castSucc) (b1 (Fin.last k)) := by
funext i
rcases Fin.eq_castSucc_or_eq_last i with h1 | h1
· obtain ⟨i, rfl⟩ := h1
simp
· subst h1
simp
/-- The construction of a Wick contraction from maps `b1 b2 : Fin k → Fin n`, with the former
giving the first index to be contracted, and the latter the second index. These
maps must satisfy a series of conditions. -/
def fromMaps {ni : } {i : Fin ni → S.𝓯} {n : } {c : Fin n → S.𝓯}
{no : } {o : Fin no → S.𝓯} {str : WickString i c o final}
{k : } (b1 b2 : Fin k → Fin n)
(hi : ∀ i, c (b2 i) = S.ξ (c (b1 i)))
(hb1ltb2 : ∀ i, b1 i < b2 i)
(hb1 : StrictMono b1)
(hb1neb2 : ∀ r1 r2, b1 r1 ≠ b2 r2)
(hb2 : Function.Injective b2) :
WickContract str b1 b2 := by
match k with
| 0 =>
refine castMaps ?_ ?_ ?_ string
· rfl
· exact funext (fun i => Fin.elim0 i)
· exact funext (fun i => Fin.elim0 i)
| Nat.succ k =>
refine castMaps rfl (eq_snoc_castSucc b1).symm (eq_snoc_castSucc b2).symm
(contr (b1 (Fin.last k)) (b2 (Fin.last k))
(hi (Fin.last k))
(hb1ltb2 (Fin.last k))
(fun r => hb1 (Fin.castSucc_lt_last r))
(fun r a => hb1neb2 (Fin.last k) r.castSucc a.symm)
(fun r => hb2.eq_iff.mp.mt (Fin.ne_last_of_lt (Fin.castSucc_lt_last r)))
(fromMaps (b1 ∘ Fin.castSucc) (b2 ∘ Fin.castSucc) (fun i => hi (Fin.castSucc i))
(fun i => hb1ltb2 (Fin.castSucc i)) (StrictMono.comp hb1 Fin.strictMono_castSucc)
?_ ?_))
· exact fun r1 r2 => hb1neb2 r1.castSucc r2.castSucc
· exact Function.Injective.comp hb2 (Fin.castSucc_injective k)
/-- Given a Wick contraction with `k.succ` contractions, returns the Wick contraction with
`k` contractions by dropping the last contraction (defined by the first index contracted). -/
def dropLast {ni : } {i : Fin ni → S.𝓯} {n : } {c : Fin n → S.𝓯}
{no : } {o : Fin no → S.𝓯} {str : WickString i c o final}
{k : } {b1 b2 : Fin k.succ → Fin n}
(w : WickContract str b1 b2) : WickContract str (b1 ∘ Fin.castSucc) (b2 ∘ Fin.castSucc) :=
fromMaps (b1 ∘ Fin.castSucc) (b2 ∘ Fin.castSucc)
(fun i => color_boundSnd_eq_dual_boundFst w i.castSucc)
(fun i => boundFst_lt_boundSnd w i.castSucc)
(StrictMono.comp w.boundFst_strictMono Fin.strictMono_castSucc)
(fun r1 r2 => boundFst_neq_boundSnd w r1.castSucc r2.castSucc)
(Function.Injective.comp w.boundSnd_injective (Fin.castSucc_injective k))
lemma eq_from_maps {ni : } {i : Fin ni → S.𝓯} {n : } {c : Fin n → S.𝓯}
{no : } {o : Fin no → S.𝓯} {str : WickString i c o final}
{k : } {b1 b2 : Fin k → Fin n}
(w : WickContract str b1 b2) :
w = fromMaps w.boundFst w.boundSnd w.color_boundSnd_eq_dual_boundFst
w.boundFst_lt_boundSnd w.boundFst_strictMono w.boundFst_neq_boundSnd
w.boundSnd_injective := is_subsingleton.allEq w _
lemma eq_dropLast_contr {ni : } {i : Fin ni → S.𝓯} {n : } {c : Fin n → S.𝓯}
{no : } {o : Fin no → S.𝓯} {str : WickString i c o final}
{k : } {b1 b2 : Fin k.succ → Fin n} (w : WickContract str b1 b2) :
w = castMaps rfl (eq_snoc_castSucc b1).symm (eq_snoc_castSucc b2).symm
(contr (b1 (Fin.last k)) (b2 (Fin.last k))
(w.color_boundSnd_eq_dual_boundFst (Fin.last k))
(w.boundFst_lt_boundSnd (Fin.last k))
(fun r => w.boundFst_strictMono (Fin.castSucc_lt_last r))
(fun r a => w.boundFst_neq_boundSnd (Fin.last k) r.castSucc a.symm)
(fun r => w.boundSnd_injective.eq_iff.mp.mt (Fin.ne_last_of_lt (Fin.castSucc_lt_last r)))
(dropLast w)) := by
rw [eq_from_maps w]
rfl
/-- Wick contractions of a given Wick string with `k` different contractions. -/
def Level {ni : } {i : Fin ni → S.𝓯} {n : } {c : Fin n → S.𝓯}
{no : } {o : Fin no → S.𝓯} (str : WickString i c o final) (k : ) : Type :=
Σ (b1 : Fin k → Fin n) (b2 : Fin k → Fin n), WickContract str b1 b2
/-- There is a finite number of Wick contractions with no contractions. In particular,
this is just the original Wick string. -/
instance levelZeroFintype {ni : } {i : Fin ni → S.𝓯} {n : } {c : Fin n → S.𝓯}
{no : } {o : Fin no → S.𝓯} (str : WickString i c o final) :
Fintype (Level str 0) where
elems := {⟨Fin.elim0, Fin.elim0, WickContract.string⟩}
complete := by
intro x
match x with
| ⟨b1, b2, w⟩ =>
have hb1 : b1 = Fin.elim0 := Subsingleton.elim _ _
have hb2 : b2 = Fin.elim0 := Subsingleton.elim _ _
subst hb1 hb2
simp only [Finset.mem_singleton]
rw [is_subsingleton.allEq w string]
/-- The pairs of additional indices which can be contracted given a Wick contraction. -/
structure ContrPair {ni : } {i : Fin ni → S.𝓯} {n : } {c : Fin n → S.𝓯}
{no : } {o : Fin no → S.𝓯} {str : WickString i c o final}
{k : } {b1 b2 : Fin k → Fin n}
(w : WickContract str b1 b2) where
/-- The first index in the contraction pair. -/
i : Fin n
/-- The second index in the contraction pair. -/
j : Fin n
h : c j = S.ξ (c i)
hilej : i < j
hb1 : ∀ r, b1 r < i
hb2i : ∀ r, b2 r ≠ i
hb2j : ∀ r, b2 r ≠ j
/-- The pairs of additional indices which can be contracted, given an existing wick contraction,
is equivalent to the a subtype of `Fin n × Fin n` defined by certain conditions equivalent
to the conditions appearing in `ContrPair`. -/
def contrPairEquivSubtype {ni : } {i : Fin ni → S.𝓯} {n : } {c : Fin n → S.𝓯}
{no : } {o : Fin no → S.𝓯} {str : WickString i c o final}
{k : } {b1 b2 : Fin k → Fin n} (w : WickContract str b1 b2) :
ContrPair w ≃ {x : Fin n × Fin n // c x.2 = S.ξ (c x.1) ∧ x.1 < x.2 ∧
(∀ r, b1 r < x.1) ∧ (∀ r, b2 r ≠ x.1) ∧ (∀ r, b2 r ≠ x.2)} where
toFun cp := ⟨⟨cp.i, cp.j⟩, ⟨cp.h, cp.hilej, cp.hb1, cp.hb2i, cp.hb2j⟩⟩
invFun x :=
match x with
| ⟨⟨i, j⟩, ⟨h, hilej, hb1, hb2i, hb2j⟩⟩ => ⟨i, j, h, hilej, hb1, hb2i, hb2j⟩
left_inv x := by rfl
right_inv x := by
simp_all only [ne_eq]
obtain ⟨val, property⟩ := x
obtain ⟨fst, snd⟩ := val
obtain ⟨left, right⟩ := property
obtain ⟨left_1, right⟩ := right
obtain ⟨left_2, right⟩ := right
obtain ⟨left_3, right⟩ := right
simp_all only [ne_eq]
lemma heq_eq {ni : } {i : Fin ni → S.𝓯} {n : } {c : Fin n → S.𝓯}
{no : } {o : Fin no → S.𝓯} {str : WickString i c o final}
{k : } {b1 b2 b1' b2' : Fin k → Fin n}
(w : WickContract str b1 b2)
(w' : WickContract str b1' b2') (h1 : b1 = b1') (h2 : b2 = b2') : HEq w w':= by
subst h1 h2
simp only [heq_eq_eq]
exact is_subsingleton.allEq w w'
/-- The equivalence between Wick contractions consisting of `k.succ` contractions and
those with `k` contractions paired with a suitable contraction pair. -/
def levelSuccEquiv {ni : } {i : Fin ni → S.𝓯} {n : } {c : Fin n → S.𝓯}
{no : } {o : Fin no → S.𝓯} (str : WickString i c o final) (k : ) :
Level str k.succ ≃ (w : Level str k) × ContrPair w.2.2 where
toFun w :=
match w with
| ⟨b1, b2, w⟩ =>
⟨⟨b1 ∘ Fin.castSucc, b2 ∘ Fin.castSucc, dropLast w⟩,
⟨b1 (Fin.last k), b2 (Fin.last k),
w.color_boundSnd_eq_dual_boundFst (Fin.last k),
w.boundFst_lt_boundSnd (Fin.last k),
fun r => w.boundFst_strictMono (Fin.castSucc_lt_last r),
fun r a => w.boundFst_neq_boundSnd (Fin.last k) r.castSucc a.symm,
fun r => w.boundSnd_injective.eq_iff.mp.mt (Fin.ne_last_of_lt (Fin.castSucc_lt_last r))⟩⟩
invFun w :=
match w with
| ⟨⟨b1, b2, w⟩, cp⟩ => ⟨Fin.snoc b1 cp.i, Fin.snoc b2 cp.j,
contr cp.i cp.j cp.h cp.hilej cp.hb1 cp.hb2i cp.hb2j w⟩
left_inv w := by
match w with
| ⟨b1, b2, w⟩ =>
simp only [Nat.succ_eq_add_one, Function.comp_apply]
congr
· exact Eq.symm (eq_snoc_castSucc b1)
· funext b2
congr
exact Eq.symm (eq_snoc_castSucc b1)
· exact Eq.symm (eq_snoc_castSucc b2)
· rw [eq_dropLast_contr w]
simp only [castMaps, Nat.succ_eq_add_one, cast_eq, heq_eqRec_iff_heq, heq_eq_eq,
contr.injEq]
rfl
right_inv w := by
match w with
| ⟨⟨b1, b2, w⟩, cp⟩ =>
simp only [Nat.succ_eq_add_one, Fin.snoc_last, Sigma.mk.inj_iff]
apply And.intro
· congr
· exact Fin.snoc_comp_castSucc
· funext b2
congr
exact Fin.snoc_comp_castSucc
· exact Fin.snoc_comp_castSucc
· exact heq_eq _ _ Fin.snoc_comp_castSucc Fin.snoc_comp_castSucc
· congr
· exact Fin.snoc_comp_castSucc
· exact Fin.snoc_comp_castSucc
· exact heq_eq _ _ Fin.snoc_comp_castSucc Fin.snoc_comp_castSucc
· simp
· simp
· simp
/-- The sum of `boundFst` and `boundSnd`, giving on `Sum.inl k` the first index
in the `k`th contraction, and on `Sum.inr k` the second index in the `k`th contraction. -/
def bound {ni : } {i : Fin ni → S.𝓯} {n : } {c : Fin n → S.𝓯}
{no : } {o : Fin no → S.𝓯} {str : WickString i c o final}
{k : } {b1 b2 : Fin k → Fin n}
(w : WickContract str b1 b2) : Fin k ⊕ Fin k → Fin n :=
Sum.elim w.boundFst w.boundSnd
/-- On `Sum.inl k` the map `bound` acts via `boundFst`. -/
@[simp]
lemma bound_inl {ni : } {i : Fin ni → S.𝓯} {n : } {c : Fin n → S.𝓯}
{no : } {o : Fin no → S.𝓯} {str : WickString i c o final}
{k : } {b1 b2 : Fin k → Fin n}
(w : WickContract str b1 b2) (i : Fin k) : w.bound (Sum.inl i) = w.boundFst i := rfl
/-- On `Sum.inr k` the map `bound` acts via `boundSnd`. -/
@[simp]
lemma bound_inr {ni : } {i : Fin ni → S.𝓯} {n : } {c : Fin n → S.𝓯}
{no : } {o : Fin no → S.𝓯} {str : WickString i c o final}
{k : } {b1 b2 : Fin k → Fin n}
(w : WickContract str b1 b2) (i : Fin k) : w.bound (Sum.inr i) = w.boundSnd i := rfl
lemma bound_injection {ni : } {i : Fin ni → S.𝓯} {n : } {c : Fin n → S.𝓯}
{no : } {o : Fin no → S.𝓯} {str : WickString i c o final}
{k : } {b1 b2 : Fin k → Fin n}
(w : WickContract str b1 b2) : Function.Injective w.bound := by
intro x y h
match x, y with
| Sum.inl x, Sum.inl y =>
simp only [bound_inl] at h
simpa using (StrictMono.injective w.boundFst_strictMono).eq_iff.mp h
| Sum.inr x, Sum.inr y =>
simp only [bound_inr] at h
simpa using w.boundSnd_injective h
| Sum.inl x, Sum.inr y =>
simp only [bound_inl, bound_inr] at h
exact False.elim (w.boundFst_neq_boundSnd x y h)
| Sum.inr x, Sum.inl y =>
simp only [bound_inr, bound_inl] at h
exact False.elim (w.boundFst_neq_boundSnd y x h.symm)
lemma bound_le_total {ni : } {i : Fin ni → S.𝓯} {n : } {c : Fin n → S.𝓯}
{no : } {o : Fin no → S.𝓯} {str : WickString i c o final}
{k : } {b1 b2 : Fin k → Fin n}
(w : WickContract str b1 b2) : 2 * k ≤ n := by
refine Fin.nonempty_embedding_iff.mp ⟨w.bound ∘ finSumFinEquiv.symm ∘ Fin.cast (Nat.two_mul k),
?_⟩
apply Function.Injective.comp (Function.Injective.comp _ finSumFinEquiv.symm.injective)
· exact Fin.cast_injective (Nat.two_mul k)
· exact bound_injection w
/-- The list of fields (indexed by `Fin n`) in a Wick contraction which are not bound,
i.e. which do not appear in any contraction. -/
def unboundList {ni : } {i : Fin ni → S.𝓯} {n : } {c : Fin n → S.𝓯}
{no : } {o : Fin no → S.𝓯} {str : WickString i c o final}
{k : } {b1 b2 : Fin k → Fin n}
(w : WickContract str b1 b2) : List (Fin n) :=
List.filter (fun i => decide (∀ r, w.bound r ≠ i)) (List.finRange n)
/-- THe list of field positions which are not contracted has no duplicates. -/
lemma unboundList_nodup {ni : } {i : Fin ni → S.𝓯} {n : } {c : Fin n → S.𝓯}
{no : } {o : Fin no → S.𝓯} {str : WickString i c o final}
{k : } {b1 b2 : Fin k → Fin n}
(w : WickContract str b1 b2) : (w.unboundList).Nodup :=
List.Nodup.filter _ (List.nodup_finRange n)
/-- The length of the `unboundList` is equal to `n - 2 * k`. That is
the total number of fields minus the number of contracted fields. -/
lemma unboundList_length {ni : } {i : Fin ni → S.𝓯} {n : } {c : Fin n → S.𝓯}
{no : } {o : Fin no → S.𝓯} {str : WickString i c o final}
{k : } {b1 b2 : Fin k → Fin n} (w : WickContract str b1 b2) :
w.unboundList.length = n - 2 * k := by
rw [← List.Nodup.dedup w.unboundList_nodup]
rw [← List.card_toFinset, unboundList]
rw [List.toFinset_filter, List.toFinset_finRange]
have hn := Finset.filter_card_add_filter_neg_card_eq_card (s := Finset.univ)
(fun (i : Fin n) => i ∈ Finset.image w.bound Finset.univ)
have hn' :(Finset.filter (fun i => i ∈ Finset.image w.bound Finset.univ) Finset.univ).card =
(Finset.image w.bound Finset.univ).card := by
refine Finset.card_equiv (Equiv.refl _) fun i => ?_
simp
rw [hn'] at hn
rw [Finset.card_image_of_injective] at hn
simp only [Finset.card_univ, Fintype.card_sum, Fintype.card_fin,
Finset.mem_univ, true_and, Sum.exists, bound_inl, bound_inr, not_or, not_exists] at hn
have hn'' : (Finset.filter (fun a => a ∉ Finset.image w.bound Finset.univ) Finset.univ).card =
n - 2 * k := by
omega
rw [← hn'']
congr
funext x
simp only [ne_eq, Sum.forall, bound_inl, bound_inr, Bool.decide_and, Bool.and_eq_true,
decide_eq_true_eq, Finset.mem_image, Finset.mem_univ, true_and, Sum.exists, not_or, not_exists]
exact bound_injection w
lemma unboundList_sorted {ni : } {i : Fin ni → S.𝓯} {n : } {c : Fin n → S.𝓯}
{no : } {o : Fin no → S.𝓯} {str : WickString i c o final}
{k : } {b1 b2 : Fin k → Fin n} (w : WickContract str b1 b2) :
List.Sorted (fun i j => i < j) w.unboundList :=
List.Pairwise.sublist (List.filter_sublist (List.finRange n)) (List.pairwise_lt_finRange n)
/-- The ordered embedding giving the fields which are not bound in a contraction. These
are the fields that will appear in a normal operator in Wick's theorem. -/
def unbound {ni : } {i : Fin ni → S.𝓯} {n : } {c : Fin n → S.𝓯}
{no : } {o : Fin no → S.𝓯} {str : WickString i c o final}
{k : } {b1 b2 : Fin k → Fin n}
(w : WickContract str b1 b2) : Fin (n - 2 * k) ↪o Fin n where
toFun := w.unboundList.get ∘ Fin.cast w.unboundList_length.symm
inj' := by
apply Function.Injective.comp
· rw [← List.nodup_iff_injective_get]
exact w.unboundList_nodup
· exact Fin.cast_injective _
map_rel_iff' := by
refine fun {a b} => StrictMono.le_iff_le ?_
rw [Function.Embedding.coeFn_mk]
apply StrictMono.comp
· exact List.Sorted.get_strictMono w.unboundList_sorted
· exact fun ⦃a b⦄ a => a
informal_lemma level_fintype where
math :≈ "Level is a finite type, as there are only finitely many ways to contract a Wick string."
deps :≈ [``Level]
informal_definition HasEqualTimeContractions where
math :≈ "The condition for a Wick contraction to have two fields contracted
which are of equal time, i.e. come from the same vertex."
deps :≈ [``WickContract]
informal_definition IsConnected where
math :≈ "The condition for a full Wick contraction that for any two vertices
(including external vertices) are connected by contractions."
deps :≈ [``WickContract]
informal_definition HasVacuumContributions where
math :≈ "The condition for a full Wick contraction to have a vacuum contribution."
deps :≈ [``WickContract]
informal_definition IsOneParticleIrreducible where
math :≈ "The condition for a full Wick contraction to be one-particle irreducible."
deps :≈ [``WickContract]
end WickContract
end Wick

View file

@ -0,0 +1,182 @@
/-
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 HepLean.PerturbationTheory.Wick.OperatorMap
/-!
# Koszul signs and ordering for lists and algebras
-/
namespace Wick
noncomputable section
open HepLean.List
/-- Given a list of fields `l`, the type of pairwise-contractions associated with `l`
which have the list `aux` uncontracted. -/
inductive ContractionsAux {I : Type} : (l : List I) → (aux : List I) → Type
| nil : ContractionsAux [] []
| cons {l : List I} {aux : List I} {a : I} (i : Option (Fin aux.length)) :
ContractionsAux l aux → ContractionsAux (a :: l) (optionEraseZ aux a i)
/-- Given a list of fields `l`, the type of pairwise-contractions associated with `l`. -/
def Contractions {I : Type} (l : List I) : Type := Σ aux, ContractionsAux l aux
namespace Contractions
variable {I : Type} {l : List I} (c : Contractions l)
/-- The list of uncontracted fields. -/
def normalize : List I := c.1
lemma contractions_nil (a : Contractions ([] : List I)) : a = ⟨[], ContractionsAux.nil⟩ := by
cases a
rename_i aux c
cases c
rfl
lemma contractions_single {i : I} (a : Contractions [i]) : a =
⟨[i], ContractionsAux.cons none ContractionsAux.nil⟩ := by
cases a
rename_i aux c
cases c
rename_i aux' c'
cases c'
cases aux'
simp only [List.length_nil, optionEraseZ]
rename_i x
exact Fin.elim0 x
/-- For the nil list of fields there is only one contraction. -/
def nilEquiv : Contractions ([] : List I) ≃ Unit where
toFun _ := ()
invFun _ := ⟨[], ContractionsAux.nil⟩
left_inv a := Eq.symm (contractions_nil a)
right_inv _ := rfl
/-- The equivalence between contractions of `a :: l` and contractions of
`Contractions l` paired with an optional element of `Fin (c.normalize).length` specifying
what `a` contracts with if any. -/
def consEquiv {a : I} {l : List I} :
Contractions (a :: l) ≃ (c : Contractions l) × Option (Fin (c.normalize).length) where
toFun c :=
match c with
| ⟨aux, c⟩ =>
match c with
| ContractionsAux.cons (aux := aux') i c => ⟨⟨aux', c⟩, i⟩
invFun ci :=
⟨(optionEraseZ (ci.fst.normalize) a ci.2), ContractionsAux.cons (a := a) ci.2 ci.1.2⟩
left_inv c := by
match c with
| ⟨aux, c⟩ =>
match c with
| ContractionsAux.cons (aux := aux') i c => rfl
right_inv ci := by rfl
/-- The type of contractions is decidable. -/
instance decidable : (l : List I) → DecidableEq (Contractions l)
| [] => fun a b =>
match a, b with
| ⟨_, a⟩, ⟨_, b⟩ =>
match a, b with
| ContractionsAux.nil, ContractionsAux.nil => isTrue rfl
| _ :: l =>
haveI : DecidableEq (Contractions l) := decidable l
haveI : DecidableEq ((c : Contractions l) × Option (Fin (c.normalize).length)) :=
Sigma.instDecidableEqSigma
Equiv.decidableEq consEquiv
/-- The type of contractions is finite. -/
instance fintype : (l : List I) → Fintype (Contractions l)
| [] => {
elems := {⟨[], ContractionsAux.nil⟩}
complete := by
intro a
rw [Finset.mem_singleton]
exact contractions_nil a}
| a :: l =>
haveI : Fintype (Contractions l) := fintype l
haveI : Fintype ((c : Contractions l) × Option (Fin (c.normalize).length)) :=
Sigma.instFintype
Fintype.ofEquiv _ consEquiv.symm
/-- A structure specifying when a type `I` and a map `f :I → Type` corresponds to
the splitting of a fields `φ` into a creation `n` and annihlation part `p`. -/
structure Splitting {I : Type} (f : I → Type) [∀ i, Fintype (f i)]
(le1 : (Σ i, f i) → (Σ i, f i) → Prop) [DecidableRel le1] where
/-- The creation part of the fields. The label `n` corresponds to the fact that
in normal ordering these feilds get pushed to the negative (left) direction. -/
𝓑n : I → (Σ i, f i)
/-- The annhilation part of the fields. The label `p` corresponds to the fact that
in normal ordering these feilds get pushed to the positive (right) direction. -/
𝓑p : I → (Σ i, f i)
/-- The complex coefficent of creation part of a field `i`. This is usually `0` or `1`. -/
𝓧n : I →
/-- The complex coefficent of annhilation part of a field `i`. This is usually `0` or `1`. -/
𝓧p : I →
h𝓑 : ∀ i, ofListLift f [i] 1 = ofList [𝓑n i] (𝓧n i) + ofList [𝓑p i] (𝓧p i)
h𝓑n : ∀ i j, le1 (𝓑n i) j
h𝓑p : ∀ i j, le1 j (𝓑p i)
/-- In the static wick's theorem, the term associated with a contraction `c` containing
the contractions. -/
def toCenterTerm {I : Type} (f : I → Type) [∀ i, Fintype (f i)]
(q : I → Fin 2)
(le1 : (Σ i, f i) → (Σ i, f i) → Prop) [DecidableRel le1]
{A : Type} [Semiring A] [Algebra A]
(F : FreeAlgebra (Σ i, f i) →ₐ[] A) :
{r : List I} → (c : Contractions r) → (S : Splitting f le1) → A
| [], ⟨[], .nil⟩, _ => 1
| _ :: _, ⟨_, .cons (aux := aux') none c⟩, S => toCenterTerm f q le1 F ⟨aux', c⟩ S
| a :: _, ⟨_, .cons (aux := aux') (some n) c⟩, S => toCenterTerm f q le1 F ⟨aux', c⟩ S *
superCommuteCoef q [aux'.get n] (List.take (↑n) aux') •
F (((superCommute fun i => q i.fst) (ofList [S.𝓑p a] (S.𝓧p a))) (ofListLift f [aux'.get n] 1))
lemma toCenterTerm_none {I : Type} (f : I → Type) [∀ i, Fintype (f i)]
(q : I → Fin 2) {r : List I}
(le1 : (Σ i, f i) → (Σ i, f i) → Prop) [DecidableRel le1]
{A : Type} [Semiring A] [Algebra A]
(F : FreeAlgebra (Σ i, f i) →ₐ A)
(S : Splitting f le1) (a : I) (c : Contractions r) :
toCenterTerm (r := a :: r) f q le1 F (Contractions.consEquiv.symm ⟨c, none⟩) S =
toCenterTerm f q le1 F c S := by
rw [consEquiv]
simp only [Equiv.coe_fn_symm_mk]
dsimp [toCenterTerm]
rfl
lemma toCenterTerm_center {I : Type} (f : I → Type) [∀ i, Fintype (f i)]
(q : I → Fin 2)
(le1 : (Σ i, f i) → (Σ i, f i) → Prop) [DecidableRel le1]
{A : Type} [Semiring A] [Algebra A]
(F : FreeAlgebra (Σ i, f i) →ₐ A) [OperatorMap (fun i => q i.1) le1 F] :
{r : List I} → (c : Contractions r) → (S : Splitting f le1) →
(c.toCenterTerm f q le1 F S) ∈ Subalgebra.center A
| [], ⟨[], .nil⟩, _ => by
dsimp [toCenterTerm]
exact Subalgebra.one_mem (Subalgebra.center A)
| _ :: _, ⟨_, .cons (aux := aux') none c⟩, S => by
dsimp [toCenterTerm]
exact toCenterTerm_center f q le1 F ⟨aux', c⟩ S
| a :: _, ⟨_, .cons (aux := aux') (some n) c⟩, S => by
dsimp [toCenterTerm]
refine Subalgebra.mul_mem (Subalgebra.center A) ?hx ?hy
exact toCenterTerm_center f q le1 F ⟨aux', c⟩ S
apply Subalgebra.smul_mem
rw [ofListLift_expand]
rw [map_sum, map_sum]
refine Subalgebra.sum_mem (Subalgebra.center A) ?hy.hx.h
intro x _
simp only [CreateAnnilateSect.toList]
rw [ofList_singleton]
exact OperatorMap.superCommute_ofList_singleton_ι_center (q := fun i => q i.1)
(le1 := le1) F (S.𝓑p a) ⟨aux'[↑n], x.head⟩
end Contractions
end
end Wick

View file

@ -0,0 +1,431 @@
/-
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 HepLean.PerturbationTheory.Wick.Signs.StaticWickCoef
/-!
# Create and annihilate sections (of bundles)
-/
namespace Wick
open HepLean.List
/-- The sections of `Σ i, f i` over a list `l : List I`.
In terms of physics, given some fields `φ₁...φₙ`, the different ways one can associate
each field as a `creation` or an `annilation` operator. E.g. the number of terms
`φ₁⁰φ₂¹...φₙ⁰` `φ₁¹φ₂¹...φₙ⁰` etc. If some fields are exclusively creation or annhilation
operators at this point (e.g. ansymptotic states) this is accounted for. -/
def CreateAnnilateSect {I : Type} (f : I → Type) (l : List I) : Type :=
Π i, f (l.get i)
namespace CreateAnnilateSect
variable {I : Type} {f : I → Type} [∀ i, Fintype (f i)] {l : List I} (a : CreateAnnilateSect f l)
/-- The type `CreateAnnilateSect f l` is finite. -/
instance fintype : Fintype (CreateAnnilateSect f l) := Pi.fintype
/-- The section got by dropping the first element of `l` if it exists. -/
def tail : {l : List I} → (a : CreateAnnilateSect f l) → CreateAnnilateSect f l.tail
| [], a => a
| _ :: _, a => fun i => a (Fin.succ i)
/-- For a list of fields `i :: l` the value of the section at the head `i`. -/
def head {i : I} (a : CreateAnnilateSect f (i :: l)) : f i := a ⟨0, Nat.zero_lt_succ l.length⟩
/-- The list `List (Σ i, f i)` defined by `a`. -/
def toList : {l : List I} → (a : CreateAnnilateSect f l) → List (Σ i, f i)
| [], _ => []
| i :: _, a => ⟨i, a.head⟩ :: toList a.tail
omit [∀ i, Fintype (f i)] in
@[simp]
lemma toList_length : (toList a).length = l.length := by
induction l with
| nil => rfl
| cons i l ih =>
simp only [toList, List.length_cons, Fin.zero_eta]
rw [ih]
omit [∀ i, Fintype (f i)] in
lemma toList_tail : {l : List I} → (a : CreateAnnilateSect f l) → toList a.tail = (toList a).tail
| [], _ => rfl
| i :: l, a => by
simp [toList]
omit [∀ i, Fintype (f i)] in
lemma toList_cons {i : I} (a : CreateAnnilateSect f (i :: l)) :
(toList a) = ⟨i, a.head⟩ :: toList a.tail := by
rfl
omit [∀ i, Fintype (f i)] in
lemma toList_get (a : CreateAnnilateSect f l) :
(toList a).get = (fun i => ⟨l.get i, a i⟩) ∘ Fin.cast (by simp) := by
induction l with
| nil =>
funext i
exact Fin.elim0 i
| cons i l ih =>
simp only [toList_cons, List.get_eq_getElem, Fin.zero_eta, List.getElem_cons_succ,
Function.comp_apply, Fin.cast_mk]
funext x
match x with
| ⟨0, h⟩ => rfl
| ⟨x + 1, h⟩ =>
simp only [List.get_eq_getElem, Prod.mk.eta, List.getElem_cons_succ, Function.comp_apply]
change (toList a.tail).get _ = _
rw [ih]
simp [tail]
omit [∀ i, Fintype (f i)] in
@[simp]
lemma toList_grade (q : I → Fin 2) :
grade (fun i => q i.fst) a.toList = 1 ↔ grade q l = 1 := by
induction l with
| nil =>
simp [toList]
| cons i r ih =>
simp only [grade, Fin.isValue, ite_eq_right_iff, zero_ne_one, imp_false]
have ih' := ih (fun i => a i.succ)
have h1 : grade (fun i => q i.fst) a.tail.toList = grade q r := by
by_cases h : grade q r = 1
· simp_all
· have h0 : grade q r = 0 := by
omega
rw [h0] at ih'
simp only [Fin.isValue, zero_ne_one, iff_false] at ih'
have h0' : grade (fun i => q i.fst) a.tail.toList = 0 := by
simp only [List.tail_cons, tail, Fin.isValue]
omega
rw [h0, h0']
rw [h1]
@[simp]
lemma toList_grade_take {I : Type} {f : I → Type}
(q : I → Fin 2) : (r : List I) → (a : CreateAnnilateSect f r) → (n : ) →
grade (fun i => q i.fst) (List.take n a.toList) = grade q (List.take n r)
| [], _, _ => by
simp [toList]
| i :: r, a, 0 => by
simp
| i :: r, a, Nat.succ n => by
simp only [grade, Fin.isValue]
rw [toList_grade_take q r a.tail n]
/-- The equivalence between `CreateAnnilateSect f l` and
`f (l.get n) × CreateAnnilateSect f (l.eraseIdx n)` obtained by extracting the `n`th field
from `l`. -/
def extractEquiv {I : Type} {f : I → Type} {l : List I}
(n : Fin l.length) : CreateAnnilateSect f l ≃
f (l.get n) × CreateAnnilateSect f (l.eraseIdx n) := by
match l with
| [] => exact Fin.elim0 n
| l0 :: l =>
let e1 : CreateAnnilateSect f ((l0 :: l).eraseIdx n) ≃ Π i, f ((l0 :: l).get (n.succAbove i)) :=
Equiv.piCongr (Fin.castOrderIso (by rw [eraseIdx_cons_length])).toEquiv
fun x => Equiv.cast (congrArg f (by
rw [HepLean.List.eraseIdx_get]
simp only [List.length_cons, Function.comp_apply, List.get_eq_getElem, Fin.coe_cast,
RelIso.coe_fn_toEquiv, Fin.castOrderIso_apply]
congr 1
simp only [Fin.succAbove]
split
next h =>
simp_all only [Fin.coe_castSucc]
split
next h_1 => simp_all only [Fin.coe_castSucc, Fin.coe_cast]
next h_1 =>
simp_all only [not_lt, Fin.val_succ, Fin.coe_cast, self_eq_add_right, one_ne_zero]
simp only [Fin.le_def, List.length_cons, Fin.coe_castSucc, Fin.coe_cast] at h_1
simp only [Fin.lt_def, Fin.coe_castSucc, Fin.coe_cast] at h
omega
next h =>
simp_all only [not_lt, Fin.val_succ]
split
next h_1 =>
simp_all only [Fin.coe_castSucc, Fin.coe_cast, add_right_eq_self, one_ne_zero]
simp only [Fin.lt_def, Fin.coe_castSucc, Fin.coe_cast] at h_1
simp only [Fin.le_def, Fin.coe_cast, Fin.coe_castSucc] at h
omega
next h_1 => simp_all only [not_lt, Fin.val_succ, Fin.coe_cast]))
exact (Fin.insertNthEquiv _ _).symm.trans (Equiv.prodCongr (Equiv.refl _) e1.symm)
lemma extractEquiv_symm_toList_get_same {I : Type} {f : I → Type}
{l : List I} (n : Fin l.length) (a0 : f (l.get n)) (a : CreateAnnilateSect f (l.eraseIdx n)) :
((extractEquiv n).symm (a0, a)).toList[n] = ⟨l[n], a0⟩ := by
match l with
| [] => exact Fin.elim0 n
| l0 :: l =>
trans (((CreateAnnilateSect.extractEquiv n).symm (a0, a)).toList).get (Fin.cast (by simp) n)
· simp only [List.length_cons, List.get_eq_getElem, Fin.coe_cast]
rfl
rw [CreateAnnilateSect.toList_get]
simp only [List.get_eq_getElem, List.length_cons, extractEquiv, RelIso.coe_fn_toEquiv,
Fin.castOrderIso_apply, Equiv.symm_trans_apply, Equiv.symm_symm, Equiv.prodCongr_symm,
Equiv.refl_symm, Equiv.prodCongr_apply, Equiv.coe_refl, Prod.map_apply, id_eq,
Function.comp_apply, Fin.cast_trans, Fin.cast_eq_self, Sigma.mk.inj_iff, heq_eq_eq]
apply And.intro
· rfl
erw [Fin.insertNthEquiv_apply]
simp only [Fin.insertNth_apply_same]
/-- The section obtained by dropping the `n`th field. -/
def eraseIdx (n : Fin l.length) : CreateAnnilateSect f (l.eraseIdx n) :=
(extractEquiv n a).2
omit [∀ i, Fintype (f i)] in
@[simp]
lemma eraseIdx_zero_tail {i : I} {l : List I} (a : CreateAnnilateSect f (i :: l)) :
(eraseIdx a (@OfNat.ofNat (Fin (l.length + 1)) 0 Fin.instOfNat : Fin (l.length + 1))) =
a.tail := by
simp only [List.length_cons, Fin.val_zero, List.eraseIdx_cons_zero, eraseIdx, List.get_eq_getElem,
List.getElem_cons_zero, extractEquiv, Fin.zero_succAbove, Fin.val_succ, List.getElem_cons_succ,
Fin.insertNthEquiv_zero, RelIso.coe_fn_toEquiv, Fin.castOrderIso_apply, Fin.cast_eq_self,
Equiv.cast_refl, Equiv.trans_apply, Equiv.prodCongr_apply, Equiv.coe_refl, Prod.map_snd]
rfl
omit [∀ i, Fintype (f i)] in
lemma eraseIdx_succ_head {i : I} {l : List I} (n : ) (hn : n + 1 < (i :: l).length)
(a : CreateAnnilateSect f (i :: l)) : (eraseIdx a ⟨n + 1, hn⟩).head = a.head := by
rw [eraseIdx, extractEquiv]
simp only [List.length_cons, List.get_eq_getElem, List.getElem_cons_succ, List.eraseIdx_cons_succ,
RelIso.coe_fn_toEquiv, Fin.castOrderIso_apply, Equiv.trans_apply, Equiv.prodCongr_apply,
Equiv.coe_refl, Prod.map_snd]
conv_lhs =>
rhs
rhs
rhs
erw [Fin.insertNthEquiv_symm_apply]
simp only [head, Equiv.piCongr, RelIso.coe_fn_toEquiv, Fin.castOrderIso_apply, Equiv.piCongrRight,
Equiv.cast_symm, Equiv.piCongrLeft, OrderIso.toEquiv_symm, OrderIso.symm_symm,
Equiv.piCongrLeft', List.length_cons, Fin.zero_eta, Equiv.symm_trans_apply, Equiv.symm_symm,
Equiv.coe_fn_mk, Equiv.coe_fn_symm_mk, Pi.map_apply, Fin.cast_zero, Fin.val_zero,
List.getElem_cons_zero, Equiv.cast_apply]
simp only [Fin.succAbove, Fin.castSucc_zero', Fin.removeNth]
refine cast_eq_iff_heq.mpr ?_
congr
simp [Fin.ext_iff]
omit [∀ i, Fintype (f i)] in
lemma eraseIdx_succ_tail {i : I} {l : List I} (n : ) (hn : n + 1 < (i :: l).length)
(a : CreateAnnilateSect f (i :: l)) :
(eraseIdx a ⟨n + 1, hn⟩).tail = eraseIdx a.tail ⟨n, Nat.succ_lt_succ_iff.mp hn⟩ := by
match l with
| [] =>
simp at hn
| r0 :: r =>
rw [eraseIdx, extractEquiv]
simp only [List.length_cons, List.eraseIdx_cons_succ, List.tail_cons, List.get_eq_getElem,
List.getElem_cons_succ, RelIso.coe_fn_toEquiv, Fin.castOrderIso_apply, Equiv.trans_apply,
Equiv.prodCongr_apply, Equiv.coe_refl, Prod.map_snd, Nat.succ_eq_add_one]
conv_lhs =>
rhs
rhs
rhs
erw [Fin.insertNthEquiv_symm_apply]
rw [eraseIdx]
conv_rhs =>
rhs
rw [extractEquiv]
simp only [List.get_eq_getElem, List.length_cons, RelIso.coe_fn_toEquiv, Fin.castOrderIso_apply,
Equiv.trans_apply, Equiv.prodCongr_apply, Equiv.coe_refl, Prod.map_snd]
erw [Fin.insertNthEquiv_symm_apply]
simp only [tail, List.tail_cons, Equiv.piCongr, RelIso.coe_fn_toEquiv, Fin.castOrderIso_apply,
Equiv.piCongrRight, Equiv.cast_symm, Equiv.piCongrLeft, OrderIso.toEquiv_symm,
OrderIso.symm_symm, Equiv.piCongrLeft', Equiv.symm_trans_apply, Equiv.symm_symm,
Equiv.coe_fn_mk, Equiv.coe_fn_symm_mk, Pi.map_apply, Fin.cast_succ_eq, Fin.val_succ,
List.getElem_cons_succ, Equiv.cast_apply, List.get_eq_getElem, List.length_cons, Fin.succ_mk,
Prod.map_apply, id_eq]
funext i
simp only [Pi.map_apply, Equiv.cast_apply]
have hcast {α β : Type} (h : α = β) (a : α) (b : β) : cast h a = b ↔ a = cast (Eq.symm h) b := by
cases h
simp
rw [hcast]
simp only [cast_cast]
refine eq_cast_iff_heq.mpr ?_
simp only [Fin.succAbove, Fin.removeNth]
congr
simp only [List.length_cons, Fin.ext_iff, Fin.val_succ]
split
next h =>
simp_all only [Fin.coe_castSucc, Fin.val_succ, Fin.coe_cast, add_left_inj]
split
next h_1 => simp_all only [Fin.coe_castSucc, Fin.coe_cast]
next h_1 =>
simp_all only [not_lt, Fin.val_succ, Fin.coe_cast, self_eq_add_right, one_ne_zero]
simp only [Fin.lt_def, Fin.coe_castSucc, Fin.val_succ, Fin.coe_cast, add_lt_add_iff_right]
at h
simp only [Fin.le_def, Fin.coe_castSucc, Fin.coe_cast] at h_1
omega
next h =>
simp_all only [not_lt, Fin.val_succ, Fin.coe_cast, add_left_inj]
split
next h_1 =>
simp_all only [Fin.coe_castSucc, Fin.coe_cast, add_right_eq_self, one_ne_zero]
simp only [Fin.le_def, Fin.coe_castSucc, Fin.val_succ, Fin.coe_cast, add_le_add_iff_right]
at h
simp only [Fin.lt_def, Fin.coe_castSucc, Fin.coe_cast] at h_1
omega
next h_1 => simp_all only [not_lt, Fin.val_succ, Fin.coe_cast]
omit [∀ i, Fintype (f i)] in
lemma eraseIdx_toList : {l : List I} → {n : Fin l.length} → (a : CreateAnnilateSect f l) →
(eraseIdx a n).toList = a.toList.eraseIdx n
| [], n, _ => Fin.elim0 n
| r0 :: r, ⟨0, h⟩, a => by
simp [toList_tail]
| r0 :: r, ⟨n + 1, h⟩, a => by
simp only [toList, List.length_cons, List.tail_cons, List.eraseIdx_cons_succ, List.cons.injEq,
Sigma.mk.inj_iff, heq_eq_eq, true_and]
apply And.intro
· rw [eraseIdx_succ_head]
· conv_rhs => rw [← eraseIdx_toList (l := r) (n := ⟨n, Nat.succ_lt_succ_iff.mp h⟩) a.tail]
rw [eraseIdx_succ_tail]
lemma extractEquiv_symm_eraseIdx {I : Type} {f : I → Type}
{l : List I} (n : Fin l.length) (a0 : f l[↑n]) (a : CreateAnnilateSect f (l.eraseIdx n)) :
((extractEquiv n).symm (a0, a)).eraseIdx n = a := by
match l with
| [] => exact Fin.elim0 n
| l0 :: l =>
rw [eraseIdx, extractEquiv]
simp
lemma toList_koszulSignInsert {I : Type} {f : I → Type}
(q : I → Fin 2) (le1 : I → I → Prop) [DecidableRel le1]
(l : List I) (a : CreateAnnilateSect f l) (x : (i : I) × f i) :
koszulSignInsert (fun i j => le1 i.fst j.fst) (fun i => q i.fst) x a.toList =
koszulSignInsert le1 q x.1 l := by
induction l with
| nil => simp [koszulSignInsert]
| cons b l ih =>
simp only [koszulSignInsert, List.tail_cons, Fin.isValue]
rw [ih]
lemma toList_koszulSign {I : Type} {f : I → Type}
(q : I → Fin 2) (le1 : I → I → Prop) [DecidableRel le1]
(l : List I) (a : CreateAnnilateSect f l) :
koszulSign (fun i j => le1 i.fst j.fst) (fun i => q i.fst) a.toList =
koszulSign le1 q l := by
induction l with
| nil => simp [koszulSign]
| cons i l ih =>
simp only [koszulSign, List.tail_cons]
rw [ih]
congr 1
rw [toList_koszulSignInsert]
lemma insertionSortEquiv_toList {I : Type} {f : I → Type}
(le1 : I → I → Prop) [DecidableRel le1](l : List I)
(a : CreateAnnilateSect f l) :
insertionSortEquiv (fun i j => le1 i.fst j.fst) a.toList =
(Fin.castOrderIso (by simp)).toEquiv.trans ((insertionSortEquiv le1 l).trans
(Fin.castOrderIso (by simp)).toEquiv) := by
induction l with
| nil =>
simp [liftM, HepLean.List.insertionSortEquiv]
| cons i l ih =>
simp only [liftM, List.length_cons, Fin.zero_eta, List.insertionSort]
conv_lhs => simp [HepLean.List.insertionSortEquiv]
erw [orderedInsertEquiv_sigma]
rw [ih]
simp only [HepLean.Fin.equivCons_trans, Nat.succ_eq_add_one,
HepLean.Fin.equivCons_castOrderIso, List.length_cons, Nat.add_zero, Nat.zero_eq,
Fin.zero_eta]
ext x
conv_rhs => simp [HepLean.List.insertionSortEquiv]
simp only [Equiv.trans_apply, RelIso.coe_fn_toEquiv, Fin.castOrderIso_apply, Fin.cast_trans,
Fin.coe_cast]
have h2' (i : Σ i, f i) (l' : List (Σ i, f i)) :
List.map (fun i => i.1) (List.orderedInsert (fun i j => le1 i.fst j.fst) i l') =
List.orderedInsert le1 i.1 (List.map (fun i => i.1) l') := by
induction l' with
| nil =>
simp [HepLean.List.orderedInsertEquiv]
| cons j l' ih' =>
by_cases hij : (fun i j => le1 i.fst j.fst) i j
· rw [List.orderedInsert_of_le]
· erw [List.orderedInsert_of_le]
· simp
· exact hij
· exact hij
· simp only [List.orderedInsert, hij, ↓reduceIte, List.unzip_snd, List.map_cons]
simp only [↓reduceIte, List.cons.injEq, true_and]
simpa using ih'
have h2 (l' : List (Σ i, f i)) :
List.map (fun i => i.1) (List.insertionSort (fun i j => le1 i.fst j.fst) l') =
List.insertionSort le1 (List.map (fun i => i.1) l') := by
induction l' with
| nil =>
simp [HepLean.List.orderedInsertEquiv]
| cons i l' ih' =>
simp only [List.insertionSort, List.unzip_snd]
simp only [List.unzip_snd] at h2'
rw [h2']
congr
rw [HepLean.List.orderedInsertEquiv_congr _ _ _ (h2 _)]
simp only [List.length_cons, Equiv.trans_apply, RelIso.coe_fn_toEquiv, Fin.castOrderIso_apply,
Fin.cast_trans, Fin.coe_cast]
have h3 : (List.insertionSort le1 (List.map (fun i => i.1) a.tail.toList)) =
List.insertionSort le1 l := by
congr
have h3' (l : List I) (a : CreateAnnilateSect f l) :
List.map (fun i => i.1) a.toList = l := by
induction l with
| nil => rfl
| cons i l ih' =>
simp only [toList, List.length_cons, Fin.zero_eta, Prod.mk.eta,
List.unzip_snd, List.map_cons, List.cons.injEq, true_and]
simpa using ih' _
rw [h3']
rfl
rw [HepLean.List.orderedInsertEquiv_congr _ _ _ h3]
simp only [List.length_cons, Equiv.trans_apply, RelIso.coe_fn_toEquiv, Fin.castOrderIso_apply,
Fin.cast_trans, Fin.cast_eq_self, Fin.coe_cast]
rfl
/-- Given a section for `l` the corresponding section
for `List.insertionSort le1 l`. -/
def sort (le1 : I → I → Prop) [DecidableRel le1] :
CreateAnnilateSect f (List.insertionSort le1 l) :=
Equiv.piCongr (HepLean.List.insertionSortEquiv le1 l) (fun i => (Equiv.cast (by
congr 1
rw [← HepLean.List.insertionSortEquiv_get]
simp))) a
lemma sort_toList {I : Type} {f : I → Type}
(le1 : I → I → Prop) [DecidableRel le1] (l : List I) (a : CreateAnnilateSect f l) :
(a.sort le1).toList = List.insertionSort (fun i j => le1 i.fst j.fst) a.toList := by
let l1 := List.insertionSort (fun i j => le1 i.fst j.fst) a.toList
let l2 := (a.sort le1).toList
symm
change l1 = l2
have hlen : l1.length = l2.length := by
simp [l1, l2]
have hget : l1.get = l2.get ∘ Fin.cast hlen := by
rw [← HepLean.List.insertionSortEquiv_get]
rw [toList_get, toList_get]
funext i
rw [insertionSortEquiv_toList]
simp only [Function.comp_apply, Equiv.symm_trans_apply,
OrderIso.toEquiv_symm, Fin.symm_castOrderIso, RelIso.coe_fn_toEquiv, Fin.castOrderIso_apply,
Fin.cast_trans, Fin.cast_eq_self, id_eq, eq_mpr_eq_cast, Fin.coe_cast, Sigma.mk.inj_iff]
apply And.intro
· have h1 := congrFun (HepLean.List.insertionSortEquiv_get (r := le1) l) (Fin.cast (by simp) i)
rw [← h1]
simp
· simp only [List.get_eq_getElem, sort, Equiv.piCongr, Equiv.trans_apply, Fin.coe_cast,
Equiv.piCongrLeft_apply, Equiv.piCongrRight_apply, Pi.map_apply, Equiv.cast_apply,
heq_eqRec_iff_heq]
exact (cast_heq _ _).symm
apply List.ext_get hlen
rw [hget]
simp
end CreateAnnilateSect
end Wick

View file

@ -0,0 +1,253 @@
/-
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 Mathlib.Algebra.FreeAlgebra
import Mathlib.Algebra.Lie.OfAssociative
import Mathlib.Analysis.Complex.Basic
import HepLean.PerturbationTheory.Wick.Signs.StaticWickCoef
/-!
# Koszul signs and ordering for lists and algebras
-/
namespace Wick
noncomputable section
/-- Given a relation `r` on `I` sorts elements of `MonoidAlgebra (FreeMonoid I)` by `r` giving it
a signed dependent on `q`. -/
def koszulOrderMonoidAlgebra {I : Type} (r : I → I → Prop) [DecidableRel r] (q : I → Fin 2) :
MonoidAlgebra (FreeMonoid I) →ₗ[] MonoidAlgebra (FreeMonoid I) :=
Finsupp.lift (MonoidAlgebra (FreeMonoid I)) (List I)
(fun i => Finsupp.lsingle (R := ) (List.insertionSort r i) (koszulSign r q i))
lemma koszulOrderMonoidAlgebra_ofList {I : Type} (r : I → I → Prop) [DecidableRel r]
(q : I → Fin 2) (i : List I) :
koszulOrderMonoidAlgebra r q (MonoidAlgebra.of (FreeMonoid I) i) =
(koszulSign r q i) • (MonoidAlgebra.of (FreeMonoid I) (List.insertionSort r i)) := by
simp only [koszulOrderMonoidAlgebra, Finsupp.lsingle_apply, MonoidAlgebra.of_apply,
MonoidAlgebra.smul_single', mul_one]
rw [MonoidAlgebra.ext_iff]
intro x
erw [Finsupp.lift_apply]
simp only [MonoidAlgebra.smul_single', zero_mul, Finsupp.single_zero, Finsupp.sum_single_index,
one_mul]
@[simp]
lemma koszulOrderMonoidAlgebra_single {I : Type} (r : I → I → Prop) [DecidableRel r] (q : I → Fin 2)
(l : FreeMonoid I) (x : ) :
koszulOrderMonoidAlgebra r q (MonoidAlgebra.single l x)
= (koszulSign r q l) • (MonoidAlgebra.single (List.insertionSort r l) x) := by
simp only [koszulOrderMonoidAlgebra, Finsupp.lsingle_apply, MonoidAlgebra.smul_single']
rw [MonoidAlgebra.ext_iff]
intro x'
erw [Finsupp.lift_apply]
simp only [MonoidAlgebra.smul_single', zero_mul, Finsupp.single_zero, Finsupp.sum_single_index,
one_mul, MonoidAlgebra.single]
congr 2
rw [NonUnitalNormedCommRing.mul_comm]
/-- Given a relation `r` on `I` sorts elements of `FreeAlgebra I` by `r` giving it
a signed dependent on `q`. -/
def koszulOrder {I : Type} (r : I → I → Prop) [DecidableRel r] (q : I → Fin 2) :
FreeAlgebra I →ₗ[] FreeAlgebra I :=
FreeAlgebra.equivMonoidAlgebraFreeMonoid.symm.toAlgHom.toLinearMap
∘ₗ koszulOrderMonoidAlgebra r q
∘ₗ FreeAlgebra.equivMonoidAlgebraFreeMonoid.toAlgHom.toLinearMap
@[simp]
lemma koszulOrder_ι {I : Type} (r : I → I → Prop) [DecidableRel r] (q : I → Fin 2) (i : I) :
koszulOrder r q (FreeAlgebra.ι i) = FreeAlgebra.ι i := by
simp only [koszulOrder, AlgEquiv.toAlgHom_eq_coe, AlgEquiv.toAlgHom_toLinearMap,
koszulOrderMonoidAlgebra, Finsupp.lsingle_apply, LinearMap.coe_comp, Function.comp_apply,
AlgEquiv.toLinearMap_apply]
rw [AlgEquiv.symm_apply_eq]
simp only [FreeAlgebra.equivMonoidAlgebraFreeMonoid, MonoidAlgebra.of_apply,
AlgEquiv.ofAlgHom_apply, FreeAlgebra.lift_ι_apply]
rw [@MonoidAlgebra.ext_iff]
intro x
erw [Finsupp.lift_apply]
simp only [MonoidAlgebra.smul_single', List.insertionSort, List.orderedInsert,
koszulSign_freeMonoid_of, mul_one, Finsupp.single_zero, Finsupp.sum_single_index]
rfl
@[simp]
lemma koszulOrder_single {I : Type} (r : I → I → Prop) [DecidableRel r] (q : I → Fin 2)
(l : FreeMonoid I) :
koszulOrder r q (FreeAlgebra.equivMonoidAlgebraFreeMonoid.symm (MonoidAlgebra.single l x))
= FreeAlgebra.equivMonoidAlgebraFreeMonoid.symm
(MonoidAlgebra.single (List.insertionSort r l) (koszulSign r q l * x)) := by
simp [koszulOrder]
@[simp]
lemma koszulOrder_ι_pair {I : Type} (r : I → I → Prop) [DecidableRel r] (q : I → Fin 2) (i j : I) :
koszulOrder r q (FreeAlgebra.ι i * FreeAlgebra.ι j) =
if r i j then FreeAlgebra.ι i * FreeAlgebra.ι j else
(koszulSign r q [i, j]) • (FreeAlgebra.ι j * FreeAlgebra.ι i) := by
have h1 : FreeAlgebra.ι i * FreeAlgebra.ι j =
FreeAlgebra.equivMonoidAlgebraFreeMonoid.symm (MonoidAlgebra.single [i, j] 1) := by
simp only [FreeAlgebra.equivMonoidAlgebraFreeMonoid, MonoidAlgebra.of_apply,
AlgEquiv.ofAlgHom_symm_apply, MonoidAlgebra.lift_single, one_smul]
rfl
conv_lhs => rw [h1]
simp only [koszulOrder, AlgEquiv.toAlgHom_eq_coe, AlgEquiv.toAlgHom_toLinearMap,
LinearMap.coe_comp, Function.comp_apply, AlgEquiv.toLinearMap_apply, AlgEquiv.apply_symm_apply,
koszulOrderMonoidAlgebra_single, List.insertionSort, List.orderedInsert,
MonoidAlgebra.smul_single', mul_one]
by_cases hr : r i j
· rw [if_pos hr, if_pos hr]
simp only [FreeAlgebra.equivMonoidAlgebraFreeMonoid, MonoidAlgebra.of_apply,
AlgEquiv.ofAlgHom_symm_apply, MonoidAlgebra.lift_single]
have hKS : koszulSign r q [i, j] = 1 := by
simp only [koszulSign, koszulSignInsert, Fin.isValue, mul_one, ite_eq_left_iff,
ite_eq_right_iff, and_imp]
exact fun a a_1 a_2 => False.elim (a hr)
rw [hKS]
simp only [one_smul]
rfl
· rw [if_neg hr, if_neg hr]
simp only [FreeAlgebra.equivMonoidAlgebraFreeMonoid, MonoidAlgebra.of_apply,
AlgEquiv.ofAlgHom_symm_apply, MonoidAlgebra.lift_single]
rfl
@[simp]
lemma koszulOrder_one {I : Type} (r : I → I → Prop) [DecidableRel r] (q : I → Fin 2) :
koszulOrder r q 1 = 1 := by
trans koszulOrder r q (FreeAlgebra.equivMonoidAlgebraFreeMonoid.symm (MonoidAlgebra.single [] 1))
congr
· simp only [FreeAlgebra.equivMonoidAlgebraFreeMonoid, MonoidAlgebra.of_apply,
AlgEquiv.ofAlgHom_symm_apply, MonoidAlgebra.lift_single, one_smul]
rfl
· simp only [koszulOrder_single, List.insertionSort, mul_one, EmbeddingLike.map_eq_one_iff]
rfl
lemma mul_koszulOrder_le {I : Type} (r : I → I → Prop) [DecidableRel r] (q : I → Fin 2)
(i : I) (A : FreeAlgebra I) (hi : ∀ j, r i j) :
FreeAlgebra.ι i * koszulOrder r q A = koszulOrder r q (FreeAlgebra.ι i * A) := by
let f : FreeAlgebra I →ₗ[] FreeAlgebra I := {
toFun := fun x => FreeAlgebra.ι i * x,
map_add' := fun x y => by
simp [mul_add],
map_smul' := by simp}
change (f ∘ₗ koszulOrder r q) A = (koszulOrder r q ∘ₗ f) _
have f_single (l : FreeMonoid I) (x : ) :
f ((FreeAlgebra.equivMonoidAlgebraFreeMonoid.symm (MonoidAlgebra.single l x)))
= (FreeAlgebra.equivMonoidAlgebraFreeMonoid.symm (MonoidAlgebra.single (i :: l) x)) := by
simp only [LinearMap.coe_mk, AddHom.coe_mk, f]
have hf : FreeAlgebra.ι i = FreeAlgebra.equivMonoidAlgebraFreeMonoid.symm
(MonoidAlgebra.single [i] 1) := by
simp only [FreeAlgebra.equivMonoidAlgebraFreeMonoid, MonoidAlgebra.of_apply,
AlgEquiv.ofAlgHom_symm_apply, MonoidAlgebra.lift_single, one_smul]
rfl
rw [hf]
rw [@AlgEquiv.eq_symm_apply]
simp only [map_mul, AlgEquiv.apply_symm_apply, MonoidAlgebra.single_mul_single, one_mul]
rfl
have h1 : f ∘ₗ koszulOrder r q = koszulOrder r q ∘ₗ f := by
let e : FreeAlgebra I ≃ₗ[] MonoidAlgebra (FreeMonoid I) :=
FreeAlgebra.equivMonoidAlgebraFreeMonoid.toLinearEquiv
apply (LinearEquiv.eq_comp_toLinearMap_iff (e₁₂ := e.symm) _ _).mp
apply MonoidAlgebra.lhom_ext'
intro l
apply LinearMap.ext
intro x
simp only [LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply,
MonoidAlgebra.lsingle_apply]
erw [koszulOrder_single]
rw [f_single]
erw [f_single]
rw [koszulOrder_single]
congr 2
· simp only [List.insertionSort]
have hi (l : List I) : i :: l = List.orderedInsert r i l := by
induction l with
| nil => rfl
| cons j l ih =>
refine (List.orderedInsert_of_le r l (hi j)).symm
exact hi _
· congr 1
rw [koszulSign]
have h1 (l : List I) : koszulSignInsert r q i l = 1 := by
exact koszulSignInsert_le_forall r q i l hi
rw [h1]
simp
rw [h1]
lemma koszulOrder_mul_ge {I : Type} (r : I → I → Prop) [DecidableRel r] (q : I → Fin 2)
(i : I) (A : FreeAlgebra I) (hi : ∀ j, r j i) :
koszulOrder r q A * FreeAlgebra.ι i = koszulOrder r q (A * FreeAlgebra.ι i) := by
let f : FreeAlgebra I →ₗ[] FreeAlgebra I := {
toFun := fun x => x * FreeAlgebra.ι i,
map_add' := fun x y => by
simp [add_mul],
map_smul' := by simp}
change (f ∘ₗ koszulOrder r q) A = (koszulOrder r q ∘ₗ f) A
have f_single (l : FreeMonoid I) (x : ) :
f ((FreeAlgebra.equivMonoidAlgebraFreeMonoid.symm (MonoidAlgebra.single l x)))
= (FreeAlgebra.equivMonoidAlgebraFreeMonoid.symm
(MonoidAlgebra.single (l.toList ++ [i]) x)) := by
simp only [LinearMap.coe_mk, AddHom.coe_mk, f]
have hf : FreeAlgebra.ι i = FreeAlgebra.equivMonoidAlgebraFreeMonoid.symm
(MonoidAlgebra.single [i] 1) := by
simp only [FreeAlgebra.equivMonoidAlgebraFreeMonoid, MonoidAlgebra.of_apply,
AlgEquiv.ofAlgHom_symm_apply, MonoidAlgebra.lift_single, one_smul]
rfl
rw [hf]
rw [@AlgEquiv.eq_symm_apply]
simp only [map_mul, AlgEquiv.apply_symm_apply, MonoidAlgebra.single_mul_single, mul_one]
rfl
have h1 : f ∘ₗ koszulOrder r q = koszulOrder r q ∘ₗ f := by
let e : FreeAlgebra I ≃ₗ[] MonoidAlgebra (FreeMonoid I) :=
FreeAlgebra.equivMonoidAlgebraFreeMonoid.toLinearEquiv
apply (LinearEquiv.eq_comp_toLinearMap_iff (e₁₂ := e.symm) _ _).mp
apply MonoidAlgebra.lhom_ext'
intro l
apply LinearMap.ext
intro x
simp only [LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply,
MonoidAlgebra.lsingle_apply]
erw [koszulOrder_single]
rw [f_single]
erw [f_single]
rw [koszulOrder_single]
congr 3
· change (List.insertionSort r l) ++ [i] = List.insertionSort r (l.toList ++ [i])
have hoi (l : List I) (j : I) : List.orderedInsert r j (l ++ [i]) =
List.orderedInsert r j l ++ [i] := by
induction l with
| nil => simp [hi]
| cons b l ih =>
simp only [List.orderedInsert, List.append_eq]
by_cases hr : r j b
· rw [if_pos hr, if_pos hr]
rfl
· rw [if_neg hr, if_neg hr]
rw [ih]
rfl
have hI (l : List I) : (List.insertionSort r l) ++ [i] = List.insertionSort r (l ++ [i]) := by
induction l with
| nil => rfl
| cons j l ih =>
simp only [List.insertionSort, List.append_eq]
rw [← ih]
rw [hoi]
rw [hI]
rfl
· have hI (l : List I) : koszulSign r q l = koszulSign r q (l ++ [i]) := by
induction l with
| nil => simp [koszulSign, koszulSignInsert]
| cons j l ih =>
simp only [koszulSign, List.append_eq]
rw [ih]
simp only [mul_eq_mul_right_iff]
apply Or.inl
rw [koszulSignInsert_ge_forall_append r q l j i hi]
rw [hI]
rfl
rw [h1]
end
end Wick

View file

@ -1,35 +0,0 @@
/-
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 HepLean.PerturbationTheory.Wick.Contract
/-!
# Wick contraction in momentum space
Every complete Wick contraction leads to a function on momenta, following
the Feynman rules.
-/
namespace Wick
informal_definition toMomentumTensorTree where
math :≈ "A function which takes a Wick contraction,
and corresponding momenta, and outputs the corresponding
tensor tree associated with that contraction. The rules for how this is done
is given by the `Feynman rules`.
The appropriate ring to consider here is a ring permitting the abstract notion of a
Dirac delta function. "
ref :≈ "
Some references for Feynman rules are:
- QED Feynman rules: http://hitoshi.berkeley.edu/public_html/129A/point.pdf,
- Weyl Fermions: http://scipp.ucsc.edu/~haber/susybook/feyn115.pdf."
informal_definition toMomentumTensor where
math :≈ "The tensor associated to `toMomentumTensorTree` associated with a Wick contraction,
and corresponding internal momenta, and external momenta."
deps :≈ [``toMomentumTensorTree]
end Wick

View file

@ -0,0 +1,205 @@
/-
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 HepLean.PerturbationTheory.Wick.CreateAnnilateSection
import HepLean.PerturbationTheory.Wick.KoszulOrder
/-!
# Koszul signs and ordering for lists and algebras
-/
namespace Wick
open HepLean.List
noncomputable section
/-- The element of the free algebra `FreeAlgebra I` associated with a `List I`. -/
def ofList {I : Type} (l : List I) (x : ) : FreeAlgebra I :=
FreeAlgebra.equivMonoidAlgebraFreeMonoid.symm (MonoidAlgebra.single l x)
lemma ofList_pair {I : Type} (l r : List I) (x y : ) :
ofList (l ++ r) (x * y) = ofList l x * ofList r y := by
simp only [ofList, ← map_mul, MonoidAlgebra.single_mul_single, EmbeddingLike.apply_eq_iff_eq]
rfl
lemma ofList_triple {I : Type} (la lb lc : List I) (xa xb xc : ) :
ofList (la ++ lb ++ lc) (xa * xb * xc) = ofList la xa * ofList lb xb * ofList lc xc := by
rw [ofList_pair, ofList_pair]
lemma ofList_triple_assoc {I : Type} (la lb lc : List I) (xa xb xc : ) :
ofList (la ++ (lb ++ lc)) (xa * (xb * xc)) = ofList la xa * ofList lb xb * ofList lc xc := by
rw [ofList_pair, ofList_pair]
exact Eq.symm (mul_assoc (ofList la xa) (ofList lb xb) (ofList lc xc))
lemma ofList_cons_eq_ofList {I : Type} (l : List I) (i : I) (x : ) :
ofList (i :: l) x = ofList [i] 1 * ofList l x := by
simp only [ofList, ← map_mul, MonoidAlgebra.single_mul_single, one_mul,
EmbeddingLike.apply_eq_iff_eq]
rfl
lemma ofList_singleton {I : Type} (i : I) :
ofList [i] 1 = FreeAlgebra.ι i := by
simp only [ofList, FreeAlgebra.equivMonoidAlgebraFreeMonoid, MonoidAlgebra.of_apply,
MonoidAlgebra.single, AlgEquiv.ofAlgHom_symm_apply, MonoidAlgebra.lift_single, one_smul]
rfl
lemma ofList_eq_smul_one {I : Type} (l : List I) (x : ) :
ofList l x = x • ofList l 1 := by
simp only [ofList]
rw [← map_smul]
simp
lemma ofList_empty {I : Type} : ofList [] 1 = (1 : FreeAlgebra I) := by
simp only [ofList, EmbeddingLike.map_eq_one_iff]
rfl
lemma ofList_empty' {I : Type} : ofList [] x = x • (1 : FreeAlgebra I) := by
rw [ofList_eq_smul_one, ofList_empty]
lemma koszulOrder_ofList {I : Type} (r : I → I → Prop) [DecidableRel r] (q : I → Fin 2)
(l : List I) (x : ) :
koszulOrder r q (ofList l x) = (koszulSign r q l) • ofList (List.insertionSort r l) x := by
rw [ofList]
rw [koszulOrder_single]
change ofList (List.insertionSort r l) _ = _
rw [ofList_eq_smul_one]
conv_rhs => rw [ofList_eq_smul_one]
rw [smul_smul]
lemma ofList_insertionSort_eq_koszulOrder {I : Type} (r : I → I → Prop) [DecidableRel r]
(q : I → Fin 2) (l : List I) (x : ) :
ofList (List.insertionSort r l) x = (koszulSign r q l) • koszulOrder r q (ofList l x) := by
rw [koszulOrder_ofList]
rw [smul_smul]
rw [koszulSign_mul_self]
simp
/-- The map of algebras from `FreeAlgebra I` to `FreeAlgebra (Σ i, f i)` taking
the monomial `i` to the sum of elements in `(Σ i, f i)` above `i`, i.e. the sum of the fiber
above `i`. -/
def sumFiber {I : Type} (f : I → Type) [∀ i, Fintype (f i)] :
FreeAlgebra I →ₐ[] FreeAlgebra (Σ i, f i) :=
FreeAlgebra.lift fun i => ∑ (j : f i), FreeAlgebra.ι ⟨i, j⟩
lemma sumFiber_ι {I : Type} (f : I → Type) [∀ i, Fintype (f i)] (i : I) :
sumFiber f (FreeAlgebra.ι i) = ∑ (b : f i), FreeAlgebra.ι ⟨i, b⟩ := by
simp [sumFiber]
/-- Given a list `l : List I` the corresponding element of `FreeAlgebra (Σ i, f i)`
by mapping each `i : I` to the sum of it's fiber in `Σ i, f i` and taking the product of the
result.
For example, in terms of creation and annihlation opperators,
`[φ₁, φ₂, φ₃]` gets taken to `(φ₁⁰ + φ₁¹)(φ₂⁰ + φ₂¹)(φ₃⁰ + φ₃¹)`.
-/
def ofListLift {I : Type} (f : I → Type) [∀ i, Fintype (f i)] (l : List I) (x : ) :
FreeAlgebra (Σ i, f i) :=
sumFiber f (ofList l x)
lemma ofListLift_empty {I : Type} (f : I → Type) [∀ i, Fintype (f i)] :
ofListLift f [] 1 = 1 := by
simp only [ofListLift, EmbeddingLike.map_eq_one_iff]
rw [ofList_empty]
exact map_one (sumFiber f)
lemma ofListLift_empty_smul {I : Type} (f : I → Type) [∀ i, Fintype (f i)] (x : ) :
ofListLift f [] x = x • 1 := by
simp only [ofListLift, EmbeddingLike.map_eq_one_iff]
rw [ofList_eq_smul_one]
rw [ofList_empty]
simp
lemma ofListLift_cons {I : Type} (f : I → Type) [∀ i, Fintype (f i)] (i : I) (r : List I) (x : ) :
ofListLift f (i :: r) x = (∑ j : f i, FreeAlgebra.ι ⟨i, j⟩) * (ofListLift f r x) := by
rw [ofListLift, ofList_cons_eq_ofList, ofList_singleton, map_mul]
conv_lhs => lhs; rw [sumFiber]
rw [ofListLift]
simp
lemma ofListLift_singleton {I : Type} (f : I → Type) [∀ i, Fintype (f i)] (i : I) (x : ) :
ofListLift f [i] x = ∑ j : f i, x • FreeAlgebra.ι ⟨i, j⟩ := by
simp only [ofListLift]
rw [ofList_eq_smul_one, ofList_singleton, map_smul]
rw [sumFiber_ι]
rw [Finset.smul_sum]
lemma ofListLift_singleton_one {I : Type} (f : I → Type) [∀ i, Fintype (f i)] (i : I) :
ofListLift f [i] 1 = ∑ j : f i, FreeAlgebra.ι ⟨i, j⟩ := by
simp only [ofListLift]
rw [ofList_eq_smul_one, ofList_singleton, map_smul]
rw [sumFiber_ι]
rw [Finset.smul_sum]
simp
lemma ofListLift_cons_eq_ofListLift {I : Type} (f : I → Type) [∀ i, Fintype (f i)] (i : I)
(r : List I) (x : ) :
ofListLift f (i :: r) x = ofListLift f [i] 1 * ofListLift f r x := by
rw [ofListLift_cons, ofListLift_singleton]
simp only [one_smul]
lemma ofListLift_expand {I : Type} (f : I → Type) [∀ i, Fintype (f i)] (x : ) :
(l : List I) → ofListLift f l x = ∑ (a : CreateAnnilateSect f l), ofList a.toList x
| [] => by
simp only [ofListLift, CreateAnnilateSect, List.length_nil, List.get_eq_getElem,
Finset.univ_unique, CreateAnnilateSect.toList, Finset.sum_const, Finset.card_singleton,
one_smul]
rw [ofList_eq_smul_one, map_smul, ofList_empty, ofList_eq_smul_one, ofList_empty, map_one]
| i :: l => by
rw [ofListLift_cons, ofListLift_expand f x l]
conv_rhs => rw [← (CreateAnnilateSect.extractEquiv
⟨0, by exact Nat.zero_lt_succ l.length⟩).symm.sum_comp (α := FreeAlgebra _)]
erw [Finset.sum_product]
rw [Finset.sum_mul]
conv_lhs =>
rhs
intro n
rw [Finset.mul_sum]
congr
funext j
congr
funext n
rw [← ofList_singleton, ← ofList_pair, one_mul]
rfl
lemma koszulOrder_ofListLift {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
(q : I → Fin 2) (le1 : I → I → Prop) [DecidableRel le1]
(l : List I) (x : ) :
koszulOrder (fun i j => le1 i.1 j.1) (fun i => q i.fst) (ofListLift f l x) =
sumFiber f (koszulOrder le1 q (ofList l x)) := by
rw [koszulOrder_ofList]
rw [map_smul]
change _ = _ • ofListLift _ _ _
rw [ofListLift_expand]
rw [map_sum]
conv_lhs =>
rhs
intro a
rw [koszulOrder_ofList]
rw [CreateAnnilateSect.toList_koszulSign]
rw [← Finset.smul_sum]
apply congrArg
conv_lhs =>
rhs
intro n
rw [← CreateAnnilateSect.sort_toList]
rw [ofListLift_expand]
refine Fintype.sum_equiv
((HepLean.List.insertionSortEquiv le1 l).piCongr fun i => Equiv.cast ?_) _ _ ?_
congr 1
· rw [← HepLean.List.insertionSortEquiv_get]
simp
· intro x
rfl
lemma koszulOrder_ofListLift_eq_ofListLift {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
(q : I → Fin 2) (le1 : I → I → Prop) [DecidableRel le1]
(l : List I) (x : ) : koszulOrder (fun i j => le1 i.1 j.1) (fun i => q i.fst)
(ofListLift f l x) =
koszulSign le1 q l • ofListLift f (List.insertionSort le1 l) x := by
rw [koszulOrder_ofListLift, koszulOrder_ofList, map_smul]
rfl
end
end Wick

View file

@ -0,0 +1,358 @@
/-
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 HepLean.PerturbationTheory.Wick.SuperCommute
/-!
# Koszul signs and ordering for lists and algebras
See e.g.
- https://pcteserver.mi.infn.it/~molinari/NOTES/WICK23.pdf
-/
namespace Wick
noncomputable section
/-- A map from the free algebra of fields `FreeAlgebra I` to an algebra `A`, to be
thought of as the operator algebra is said to be an operator map if
all super commutors of fields land in the center of `A`,
if two fields are of a different grade then their super commutor lands on zero,
and the `koszulOrder` (normal order) of any term with a super commutor of two fields present
is zero.
This can be thought as as a condtion on the operator algebra `A` as much as it can
on `F`. -/
class OperatorMap {A : Type} [Semiring A] [Algebra A] (q : I → Fin 2) (le1 : I → I → Prop)
[DecidableRel le1] (F : FreeAlgebra I →ₐ[] A) : Prop where
superCommute_mem_center : ∀ i j, F (superCommute q (FreeAlgebra.ι i) (FreeAlgebra.ι j)) ∈
Subalgebra.center A
superCommute_diff_grade_zero : ∀ i j, q i ≠ q j →
F (superCommute q (FreeAlgebra.ι i) (FreeAlgebra.ι j)) = 0
superCommute_ordered_zero : ∀ i j, ∀ a b,
F (koszulOrder le1 q (a * superCommute q (FreeAlgebra.ι i) (FreeAlgebra.ι j) * b)) = 0
namespace OperatorMap
variable {A : Type} [Semiring A] [Algebra A] {q : I → Fin 2} {le1 : I → I → Prop}
[DecidableRel le1] (F : FreeAlgebra I →ₐ[] A)
lemma superCommute_ofList_singleton_ι_center [OperatorMap q le1 F] (i j :I) :
F (superCommute q (ofList [i] xa) (FreeAlgebra.ι j)) ∈ Subalgebra.center A := by
have h1 : F (superCommute q (ofList [i] xa) (FreeAlgebra.ι j)) =
xa • F (superCommute q (FreeAlgebra.ι i) (FreeAlgebra.ι j)) := by
rw [← map_smul]
congr
rw [ofList_eq_smul_one, ofList_singleton]
rw [map_smul]
rfl
rw [h1]
refine Subalgebra.smul_mem (Subalgebra.center A) ?_ xa
exact superCommute_mem_center (le1 := le1) i j
end OperatorMap
lemma superCommuteSplit_operatorMap {I : Type} (q : I → Fin 2)
(le1 : I → I → Prop) [DecidableRel le1]
(lb : List I) (xa xb : ) (n : )
(hn : n < lb.length) {A : Type} [Semiring A] [Algebra A] (f : FreeAlgebra I →ₐ[] A)
[OperatorMap q le1 f] (i : I) :
f (superCommuteSplit q [i] lb xa xb n hn) =
f (superCommute q (ofList [i] xa) (FreeAlgebra.ι (lb.get ⟨n, hn⟩)))
* (superCommuteCoef q [i] (List.take n lb) •
f (ofList (List.eraseIdx lb n) xb)) := by
have hn : f ((superCommute q) (ofList [i] xa) (FreeAlgebra.ι (lb.get ⟨n, hn⟩))) ∈
Subalgebra.center A :=
OperatorMap.superCommute_ofList_singleton_ι_center (le1 := le1) f i (lb.get ⟨n, hn⟩)
rw [Subalgebra.mem_center_iff] at hn
rw [superCommuteSplit, map_mul, map_mul, map_smul, hn, mul_assoc, smul_mul_assoc,
← map_mul, ← ofList_pair]
congr
· exact Eq.symm (List.eraseIdx_eq_take_drop_succ lb n)
· exact one_mul xb
lemma superCommuteLiftSplit_operatorMap {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
(q : I → Fin 2) (c : (Σ i, f i)) (r : List I) (x y : ) (n : )
(hn : n < r.length)
(le1 : (Σ i, f i) → (Σ i, f i) → Prop) [DecidableRel le1]
{A : Type} [Semiring A] [Algebra A] (F : FreeAlgebra (Σ i, f i) →ₐ[] A)
[OperatorMap (fun i => q i.1) le1 F] :
F (superCommuteLiftSplit q [c] r x y n hn) = superCommuteLiftCoef q [c] (List.take n r) •
(F (superCommute (fun i => q i.1) (ofList [c] x)
(sumFiber f (FreeAlgebra.ι (r.get ⟨n, hn⟩))))
* F (ofListLift f (List.eraseIdx r n) y)) := by
rw [superCommuteLiftSplit]
rw [map_smul]
congr
rw [map_mul, map_mul]
have h1 : F ((superCommute fun i => q i.fst) (ofList [c] x) ((sumFiber f)
(FreeAlgebra.ι (r.get ⟨n, hn⟩)))) ∈ Subalgebra.center A := by
rw [sumFiber_ι]
rw [map_sum, map_sum]
refine Subalgebra.sum_mem _ ?_
intro n
exact fun a => OperatorMap.superCommute_ofList_singleton_ι_center (le1 := le1) F c _
rw [Subalgebra.mem_center_iff] at h1
rw [h1, mul_assoc, ← map_mul]
congr
rw [ofListLift, ofListLift, ofListLift, ← map_mul]
congr
rw [← ofList_pair, one_mul]
congr
exact Eq.symm (List.eraseIdx_eq_take_drop_succ r n)
lemma superCommute_koszulOrder_le_ofList {I : Type}
(q : I → Fin 2) (r : List I) (x : )
(le1 :I → I → Prop) [DecidableRel le1] [IsTotal I le1] [IsTrans I le1]
(i : I)
{A : Type} [Semiring A] [Algebra A]
(F : FreeAlgebra I →ₐ A) [OperatorMap q le1 F] :
F ((superCommute q (FreeAlgebra.ι i) (koszulOrder le1 q (ofList r x)))) =
∑ n : Fin r.length, (superCommuteCoef q [r.get n] (r.take n)) •
(F (((superCommute q) (ofList [i] 1)) (FreeAlgebra.ι (r.get n))) *
F ((koszulOrder le1 q) (ofList (r.eraseIdx ↑n) x))) := by
rw [koszulOrder_ofList, map_smul, map_smul, ← ofList_singleton, superCommute_ofList_sum]
rw [map_sum, ← (HepLean.List.insertionSortEquiv le1 r).sum_comp]
conv_lhs =>
enter [2, 2]
intro n
rw [superCommuteSplit_operatorMap (le1 := le1)]
enter [1, 2, 2, 2]
change ((List.insertionSort le1 r).get ∘ (HepLean.List.insertionSortEquiv le1 r)) n
rw [HepLean.List.insertionSort_get_comp_insertionSortEquiv]
conv_lhs =>
enter [2, 2]
intro n
rw [HepLean.List.eraseIdx_insertionSort_fin le1 r n]
rw [ofList_insertionSort_eq_koszulOrder le1 q]
rw [Finset.smul_sum]
conv_lhs =>
rhs
intro n
rw [map_smul, smul_smul, Algebra.mul_smul_comm, smul_smul]
congr
funext n
by_cases hq : q i ≠ q (r.get n)
· have hn := OperatorMap.superCommute_diff_grade_zero (q := q) (F := F) le1 i (r.get n) hq
conv_lhs =>
enter [2, 1]
rw [ofList_singleton, hn]
conv_rhs =>
enter [2, 1]
rw [ofList_singleton, hn]
simp
· congr 1
trans staticWickCoef q le1 r i n
· rw [staticWickCoef, mul_assoc]
refine staticWickCoef_eq_get q le1 r i n ?_
simpa using hq
lemma koszulOrder_of_le_all_ofList {I : Type}
(q : I → Fin 2) (r : List I) (x : ) (le1 : I → I → Prop) [DecidableRel le1]
(i : I)
{A : Type} [Semiring A] [Algebra A]
(F : FreeAlgebra I →ₐ A) [OperatorMap q le1 F] :
F (koszulOrder le1 q (ofList r x * FreeAlgebra.ι i))
= superCommuteCoef q [i] r • F (koszulOrder le1 q (FreeAlgebra.ι i * ofList r x)) := by
conv_lhs =>
enter [2, 2]
rw [← ofList_singleton]
rw [ofListLift_ofList_superCommute' q]
rw [map_sub]
rw [sub_eq_add_neg]
rw [map_add]
conv_lhs =>
enter [2, 2]
rw [map_smul]
rw [← neg_smul]
rw [map_smul, map_smul, map_smul]
conv_lhs =>
rhs
rhs
rw [superCommute_ofList_sum]
rw [map_sum, map_sum]
dsimp [superCommuteSplit]
rw [ofList_singleton]
rhs
intro n
rw [Algebra.smul_mul_assoc, Algebra.smul_mul_assoc]
rw [map_smul, map_smul]
rw [OperatorMap.superCommute_ordered_zero]
simp only [smul_zero, Finset.sum_const_zero, add_zero]
rw [ofList_singleton]
lemma le_all_mul_koszulOrder_ofList {I : Type}
(q : I → Fin 2) (r : List I) (x : ) (le1 : I → I→ Prop) [DecidableRel le1]
(i : I) (hi : ∀ (j : I), le1 j i)
{A : Type} [Semiring A] [Algebra A]
(F : FreeAlgebra I →ₐ A) [OperatorMap q le1 F] :
F (FreeAlgebra.ι i * koszulOrder le1 q (ofList r x)) =
F ((koszulOrder le1 q) (FreeAlgebra.ι i * ofList r x)) +
F (((superCommute q) (ofList [i] 1)) ((koszulOrder le1 q) (ofList r x))) := by
rw [koszulOrder_ofList, Algebra.mul_smul_comm, map_smul, ← ofList_singleton,
ofList_ofList_superCommute q, map_add, smul_add, ← map_smul]
conv_lhs =>
enter [1, 2]
rw [← Algebra.smul_mul_assoc, smul_smul, mul_comm, ← smul_smul, ← koszulOrder_ofList,
Algebra.smul_mul_assoc, ofList_singleton]
rw [koszulOrder_mul_ge, map_smul]
congr
· rw [koszulOrder_of_le_all_ofList]
rw [superCommuteCoef_perm_snd q [i] (List.insertionSort le1 r) r
(List.perm_insertionSort le1 r)]
rw [smul_smul]
rw [superCommuteCoef_mul_self]
simp [ofList_singleton]
· rw [map_smul, map_smul]
· exact fun j => hi j
/-- In the expansions of `F (FreeAlgebra.ι i * koszulOrder le1 q (ofList r x))`
the ter multiplying `F ((koszulOrder le1 q) (ofList (optionEraseZ r i n) x))`. -/
def superCommuteCenterOrder {I : Type}
(q : I → Fin 2) (r : List I) (i : I)
{A : Type} [Semiring A] [Algebra A]
(F : FreeAlgebra I →ₐ[] A)
(n : Option (Fin r.length)) : A :=
match n with
| none => 1
| some n => superCommuteCoef q [r.get n] (r.take n) • F (((superCommute q) (ofList [i] 1))
(FreeAlgebra.ι (r.get n)))
@[simp]
lemma superCommuteCenterOrder_none {I : Type}
(q : I → Fin 2) (r : List I) (i : I)
{A : Type} [Semiring A] [Algebra A]
(F : FreeAlgebra I →ₐ[] A) :
superCommuteCenterOrder q r i F none = 1 := by
simp [superCommuteCenterOrder]
open HepLean.List
lemma le_all_mul_koszulOrder_ofList_expand {I : Type}
(q : I → Fin 2) (r : List I) (x : ) (le1 : I → I→ Prop) [DecidableRel le1]
[IsTotal I le1] [IsTrans I le1]
(i : I) (hi : ∀ (j : I), le1 j i)
{A : Type} [Semiring A] [Algebra A]
(F : FreeAlgebra I →ₐ[] A) [OperatorMap q le1 F] :
F (FreeAlgebra.ι i * koszulOrder le1 q (ofList r x)) =
∑ n, superCommuteCenterOrder q r i F n *
F ((koszulOrder le1 q) (ofList (optionEraseZ r i n) x)) := by
rw [le_all_mul_koszulOrder_ofList]
conv_lhs =>
rhs
rw [ofList_singleton]
rw [superCommute_koszulOrder_le_ofList]
simp only [List.get_eq_getElem, Fintype.sum_option, superCommuteCenterOrder_none, one_mul]
congr
· rw [← ofList_singleton, ← ofList_pair]
simp only [List.singleton_append, one_mul]
rfl
· funext n
simp only [superCommuteCenterOrder, List.get_eq_getElem, Algebra.smul_mul_assoc]
rfl
exact fun j => hi j
lemma le_all_mul_koszulOrder_ofListLift_expand {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
(q : I → Fin 2) (r : List I) (x : ) (le1 : (Σ i, f i) → (Σ i, f i) → Prop) [DecidableRel le1]
[IsTotal (Σ i, f i) le1] [IsTrans (Σ i, f i) le1]
(i : (Σ i, f i)) (hi : ∀ (j : (Σ i, f i)), le1 j i)
{A : Type} [Semiring A] [Algebra A]
(F : FreeAlgebra (Σ i, f i) →ₐ A) [OperatorMap (fun i => q i.1) le1 F] :
F (ofList [i] 1 * koszulOrder le1 (fun i => q i.1) (ofListLift f r x)) =
F ((koszulOrder le1 fun i => q i.fst) (ofList [i] 1 * ofListLift f r x)) +
∑ n : (Fin r.length), superCommuteCoef q [r.get n] (List.take (↑n) r) •
F (((superCommute fun i => q i.fst) (ofList [i] 1)) (ofListLift f [r.get n] 1)) *
F ((koszulOrder le1 fun i => q i.fst) (ofListLift f (r.eraseIdx ↑n) x)) := by
match r with
| [] =>
simp only [map_mul, List.length_nil, Finset.univ_eq_empty, List.get_eq_getElem, List.take_nil,
List.eraseIdx_nil, Algebra.smul_mul_assoc, Finset.sum_empty, add_zero]
rw [ofListLift_empty_smul]
simp only [map_smul, koszulOrder_one, map_one, Algebra.mul_smul_comm, mul_one]
rw [ofList_singleton, koszulOrder_ι]
| r0 :: r =>
rw [ofListLift_expand, map_sum, Finset.mul_sum, map_sum]
let e1 (a : CreateAnnilateSect f (r0 :: r)) :
Option (Fin a.toList.length) ≃ Option (Fin (r0 :: r).length) :=
Equiv.optionCongr (Fin.castOrderIso (CreateAnnilateSect.toList_length a)).toEquiv
conv_lhs =>
rhs
intro a
rw [ofList_singleton, le_all_mul_koszulOrder_ofList_expand _ _ _ _ _ hi]
rw [← (e1 a).symm.sum_comp]
rhs
intro n
rw [Finset.sum_comm]
simp only [Fintype.sum_option]
congr 1
· simp only [List.length_cons, List.get_eq_getElem, superCommuteCenterOrder,
Equiv.optionCongr_symm, OrderIso.toEquiv_symm, Fin.symm_castOrderIso, Equiv.optionCongr_apply,
RelIso.coe_fn_toEquiv, Option.map_none', optionEraseZ, one_mul, e1]
rw [← map_sum, Finset.mul_sum, ← map_sum]
apply congrArg
apply congrArg
congr
funext x
rw [ofList_cons_eq_ofList]
· congr
funext n
rw [← (CreateAnnilateSect.extractEquiv n).symm.sum_comp]
simp only [List.get_eq_getElem, List.length_cons, Equiv.optionCongr_symm, OrderIso.toEquiv_symm,
Fin.symm_castOrderIso, Equiv.optionCongr_apply, RelIso.coe_fn_toEquiv, Option.map_some',
Fin.castOrderIso_apply, Algebra.smul_mul_assoc, e1]
erw [Finset.sum_product]
have h1 (a0 : f (r0 :: r)[↑n]) (a : CreateAnnilateSect f ((r0 :: r).eraseIdx ↑n)) :
superCommuteCenterOrder (fun i => q i.fst)
((CreateAnnilateSect.extractEquiv n).symm (a0, a)).toList i F
(some (Fin.cast (by simp) n)) =
superCommuteCoef q [(r0 :: r).get n] (List.take (↑n) (r0 :: r)) •
F (((superCommute fun i => q i.fst) (ofList [i] 1))
(FreeAlgebra.ι ⟨(r0 :: r).get n, a0⟩)) := by
simp only [superCommuteCenterOrder, List.get_eq_getElem, List.length_cons, Fin.coe_cast]
erw [CreateAnnilateSect.extractEquiv_symm_toList_get_same]
have hsc : superCommuteCoef (fun i => q i.fst) [⟨(r0 :: r).get n, a0⟩]
(List.take (↑n) ((CreateAnnilateSect.extractEquiv n).symm (a0, a)).toList) =
superCommuteCoef q [(r0 :: r).get n] (List.take (↑n) ((r0 :: r))) := by
simp only [superCommuteCoef, List.get_eq_getElem, List.length_cons, Fin.isValue,
CreateAnnilateSect.toList_grade_take]
rfl
erw [hsc]
rfl
conv_lhs =>
rhs
intro a0
rhs
intro a
erw [h1]
conv_lhs =>
rhs
intro a0
rw [← Finset.mul_sum]
conv_lhs =>
rhs
intro a0
enter [2, 2]
intro a
simp [optionEraseZ]
rhs
rhs
lhs
rw [← CreateAnnilateSect.eraseIdx_toList]
erw [CreateAnnilateSect.extractEquiv_symm_eraseIdx]
rw [← Finset.sum_mul]
conv_lhs =>
lhs
rw [← Finset.smul_sum]
erw [← map_sum, ← map_sum, ← ofListLift_singleton_one]
conv_lhs =>
rhs
rw [← map_sum, ← map_sum]
simp only [List.get_eq_getElem, List.length_cons, Equiv.symm_apply_apply,
Algebra.smul_mul_assoc]
erw [← ofListLift_expand]
simp only [List.get_eq_getElem, List.length_cons, Algebra.smul_mul_assoc]
end
end Wick

View file

@ -1,24 +0,0 @@
/-
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 HepLean.PerturbationTheory.FeynmanDiagrams.Basic
import HepLean.Meta.Informal.Basic
/-!
# Wick contraction in position space
Every complete Wick contraction leads to a function on positions, following
the Feynman rules.
## Further reading
The following reference provides a good resource for Wick contractions of external fields.
- http://www.dylanjtemples.com:82/solutions/QFT_Solution_I-6.pdf
-/
namespace Wick
end Wick

View file

@ -0,0 +1,102 @@
/-
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 Mathlib.Algebra.FreeAlgebra
import Mathlib.Algebra.Lie.OfAssociative
import Mathlib.Analysis.Complex.Basic
/-!
# Koszul sign insert
-/
namespace Wick
/-- Given a grading map `q : I → Fin 2` and a list `l : List I` counts the parity of the number of
elements in `l` which are of grade `1`. -/
def grade {I : Type} (q : I → Fin 2) : (l : List I) → Fin 2
| [] => 0
| a :: l => if q a = grade q l then 0 else 1
@[simp]
lemma grade_freeMonoid {I : Type} (q : I → Fin 2) (i : I) : grade q (FreeMonoid.of i) = q i := by
simp only [grade, Fin.isValue]
have ha (a : Fin 2) : (if a = 0 then 0 else 1) = a := by
fin_cases a <;> rfl
rw [ha]
@[simp]
lemma grade_empty {I : Type} (q : I → Fin 2) : grade q [] = 0 := by
simp [grade]
@[simp]
lemma grade_append {I : Type} (q : I → Fin 2) (l r : List I) :
grade q (l ++ r) = if grade q l = grade q r then 0 else 1 := by
induction l with
| nil =>
simp only [List.nil_append, grade_empty, Fin.isValue]
have ha (a : Fin 2) : (if 0 = a then 0 else 1) = a := by
fin_cases a <;> rfl
exact Eq.symm (Fin.eq_of_val_eq (congrArg Fin.val (ha (grade q r))))
| cons a l ih =>
simp only [grade, List.append_eq, Fin.isValue]
erw [ih]
have hab (a b c : Fin 2) : (if a = if b = c then 0 else 1 then (0 : Fin 2) else 1) =
if (if a = b then 0 else 1) = c then 0 else 1 := by
fin_cases a <;> fin_cases b <;> fin_cases c <;> rfl
exact hab (q a) (grade q l) (grade q r)
lemma grade_count {I : Type} (q : I → Fin 2) (l : List I) :
grade q l = if Nat.mod (List.countP (fun i => decide (q i = 1)) l) 2 = 0 then 0 else 1 := by
induction l with
| nil => simp
| cons r0 r ih =>
simp only [grade, Fin.isValue]
rw [List.countP_cons]
simp only [Fin.isValue, decide_eq_true_eq]
rw [ih]
by_cases h: q r0 = 1
· simp only [h, Fin.isValue, ↓reduceIte]
split
next h1 =>
simp_all only [Fin.isValue, ↓reduceIte, one_ne_zero]
split
next h2 =>
simp_all only [Fin.isValue, one_ne_zero]
have ha (a : ) (ha : a % 2 = 0) : (a + 1) % 2 ≠ 0 := by
omega
exact ha (List.countP (fun i => decide (q i = 1)) r) h1 h2
next h2 => simp_all only [Fin.isValue]
next h1 =>
simp_all only [Fin.isValue, ↓reduceIte]
split
next h2 => simp_all only [Fin.isValue]
next h2 =>
simp_all only [Fin.isValue, zero_ne_one]
have ha (a : ) (ha : ¬ a % 2 = 0) : (a + 1) % 2 = 0 := by
omega
exact h2 (ha (List.countP (fun i => decide (q i = 1)) r) h1)
· have h0 : q r0 = 0 := by omega
simp only [h0, Fin.isValue, zero_ne_one, ↓reduceIte, add_zero]
by_cases hn : (List.countP (fun i => decide (q i = 1)) r).mod 2 = 0
· simp [hn]
· simp [hn]
lemma grade_perm {I : Type} (q : I → Fin 2) {l l' : List I} (h : l.Perm l') :
grade q l = grade q l' := by
rw [grade_count, grade_count, h.countP_eq]
lemma grade_orderedInsert {I : Type} (q : I → Fin 2) (le1 : I → I → Prop) [DecidableRel le1]
(l : List I) (i : I) : grade q (List.orderedInsert le1 i l) = grade q (i :: l) := by
apply grade_perm
exact List.perm_orderedInsert le1 i l
@[simp]
lemma grade_insertionSort {I : Type} (q : I → Fin 2) (le1 : I → I → Prop) [DecidableRel le1]
(l : List I) : grade q (List.insertionSort le1 l) = grade q l := by
apply grade_perm
exact List.perm_insertionSort le1 l
end Wick

View file

@ -0,0 +1,110 @@
/-
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 HepLean.Mathematics.List
import HepLean.PerturbationTheory.Wick.Signs.SuperCommuteCoef
/-!
# Koszul signs and ordering for lists and algebras
-/
namespace Wick
open HepLean.List
/-- The sign associated with inserting `r0` into `r` at the position `n`.
That is the sign associated with commuting `r0` with `List.take n r`. -/
def insertSign {I : Type} (q : I → Fin 2) (n : ) (r0 : I) (r : List I) : :=
superCommuteCoef q [r0] (List.take n r)
lemma take_insert_same {I : Type} (i : I) :
(n : ) → (r : List I) →
List.take n (List.insertIdx n i r) = List.take n r
| 0, _ => by simp
| _+1, [] => by simp
| n+1, a::as => by
simp only [List.insertIdx_succ_cons, List.take_succ_cons, List.cons.injEq, true_and]
exact take_insert_same i n as
lemma insertSign_insert {I : Type} (q : I → Fin 2) (n : )
(r0 : I) (r : List I) : insertSign q n r0 r = insertSign q n r0 (List.insertIdx n r0 r) := by
simp only [insertSign]
congr 1
rw [take_insert_same]
lemma take_eraseIdx_same {I : Type} :
(n : ) → (r : List I) →
List.take n (List.eraseIdx r n) = List.take n r
| 0, _ => by simp
| _+1, [] => by simp
| n+1, a::as => by
simp only [List.eraseIdx_cons_succ, List.take_succ_cons, List.cons.injEq, true_and]
exact take_eraseIdx_same n as
lemma insertSign_eraseIdx {I : Type} (q : I → Fin 2) (n : )
(r0 : I) (r : List I) : insertSign q n r0 (r.eraseIdx n) = insertSign q n r0 r := by
simp only [insertSign]
congr 1
rw [take_eraseIdx_same]
lemma insertSign_zero {I : Type} (q : I → Fin 2) (r0 : I) (r : List I) :
insertSign q 0 r0 r = 1 := by
simp [insertSign, superCommuteCoef]
lemma insertSign_succ_cons {I : Type} (q : I → Fin 2) (n : )
(r0 r1 : I) (r : List I) : insertSign q (n + 1) r0 (r1 :: r) =
superCommuteCoef q [r0] [r1] * insertSign q n r0 r := by
simp only [insertSign, List.take_succ_cons]
rw [superCommuteCoef_cons]
lemma take_insert_gt {I : Type} (i : I) :
(n m : ) → (h : n < m) → (r : List I) →
List.take n (List.insertIdx m i r) = List.take n r
| 0, 0, _, _ => by simp
| 0, m + 1, _, _ => by simp
| n+1, m + 1, _, [] => by simp
| n+1, m + 1, h, a::as => by
simp only [List.insertIdx_succ_cons, List.take_succ_cons, List.cons.injEq, true_and]
refine take_insert_gt i n m (Nat.succ_lt_succ_iff.mp h) as
lemma insertSign_insert_gt {I : Type} (q : I → Fin 2) (n m : )
(r0 r1 : I) (r : List I) (hn : n < m) :
insertSign q n r0 (List.insertIdx m r1 r) = insertSign q n r0 r := by
rw [insertSign, insertSign]
congr 1
exact take_insert_gt r1 n m hn r
lemma take_insert_let {I : Type} (i : I) :
(n m : ) → (h : m ≤ n) → (r : List I) → (hm : m ≤ r.length) →
(List.take (n + 1) (List.insertIdx m i r)).Perm (i :: List.take n r)
| 0, 0, h, _, _ => by simp
| m + 1, 0, h, r, _ => by simp
| n + 1, m + 1, h, [], hm => by
simp at hm
| n + 1, m + 1, h, a::as, hm => by
simp only [List.insertIdx_succ_cons, List.take_succ_cons]
have hp : (i :: a :: List.take n as).Perm (a :: i :: List.take n as) := by
exact List.Perm.swap a i (List.take n as)
refine List.Perm.trans ?_ hp.symm
refine List.Perm.cons a ?_
exact take_insert_let i n m (Nat.le_of_succ_le_succ h) as (Nat.le_of_succ_le_succ hm)
lemma insertSign_insert_lt_eq_insertSort {I : Type} (q : I → Fin 2) (n m : )
(r0 r1 : I) (r : List I) (hn : m ≤ n) (hm : m ≤ r.length) :
insertSign q (n + 1) r0 (List.insertIdx m r1 r) = insertSign q (n + 1) r0 (r1 :: r) := by
rw [insertSign, insertSign]
apply superCommuteCoef_perm_snd
simp only [List.take_succ_cons]
refine take_insert_let r1 n m hn r hm
lemma insertSign_insert_lt {I : Type} (q : I → Fin 2) (n m : )
(r0 r1 : I) (r : List I) (hn : m ≤ n) (hm : m ≤ r.length) :
insertSign q (n + 1) r0 (List.insertIdx m r1 r) = superCommuteCoef q [r0] [r1] *
insertSign q n r0 r := by
rw [insertSign_insert_lt_eq_insertSort, insertSign_succ_cons]
exact hn
exact hm
end Wick

View file

@ -0,0 +1,201 @@
/-
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 Mathlib.Algebra.FreeAlgebra
import Mathlib.Algebra.Lie.OfAssociative
import Mathlib.Analysis.Complex.Basic
import HepLean.PerturbationTheory.Wick.Signs.KoszulSignInsert
/-!
# Koszul sign insert
-/
namespace Wick
open HepLean.List
/-- Gives a factor of `- 1` for every fermion-fermion (`q` is `1`) crossing that occurs when sorting
a list of based on `r`. -/
def koszulSign {I : Type} (r : I → I → Prop) [DecidableRel r] (q : I → Fin 2) :
List I →
| [] => 1
| a :: l => koszulSignInsert r q a l * koszulSign r q l
lemma koszulSign_mul_self {I : Type} (r : I → I → Prop) [DecidableRel r] (q : I → Fin 2)
(l : List I) : koszulSign r q l * koszulSign r q l = 1 := by
induction l with
| nil => simp [koszulSign]
| cons a l ih =>
simp only [koszulSign]
trans (koszulSignInsert r q a l * koszulSignInsert r q a l) *
(koszulSign r q l * koszulSign r q l)
ring
rw [ih]
rw [koszulSignInsert_mul_self, mul_one]
@[simp]
lemma koszulSign_freeMonoid_of {I : Type} (r : I → I → Prop) [DecidableRel r] (q : I → Fin 2)
(i : I) : koszulSign r q (FreeMonoid.of i) = 1 := by
change koszulSign r q [i] = 1
simp only [koszulSign, mul_one]
rfl
lemma koszulSignInsert_erase_boson {I : Type} (q : I → Fin 2) (le1 :I → I → Prop)
[DecidableRel le1] (r0 : I) :
(r : List I) → (n : Fin r.length) → (heq : q (r.get n) = 0) →
koszulSignInsert le1 q r0 (r.eraseIdx n) = koszulSignInsert le1 q r0 r
| [], _, _ => by
simp
| r1 :: r, ⟨0, h⟩, hr => by
simp only [List.eraseIdx_zero, List.tail_cons]
simp only [List.length_cons, Fin.zero_eta, List.get_eq_getElem, Fin.val_zero,
List.getElem_cons_zero, Fin.isValue] at hr
rw [koszulSignInsert]
simp [hr]
| r1 :: r, ⟨n + 1, h⟩, hr => by
simp only [List.eraseIdx_cons_succ]
rw [koszulSignInsert, koszulSignInsert]
rw [koszulSignInsert_erase_boson q le1 r0 r ⟨n, Nat.succ_lt_succ_iff.mp h⟩ hr]
lemma koszulSign_erase_boson {I : Type} (q : I → Fin 2) (le1 :I → I → Prop)
[DecidableRel le1] :
(r : List I) → (n : Fin r.length) → (heq : q (r.get n) = 0) →
koszulSign le1 q (r.eraseIdx n) = koszulSign le1 q r
| [], _ => by
simp
| r0 :: r, ⟨0, h⟩ => by
simp only [List.length_cons, Fin.zero_eta, List.get_eq_getElem, Fin.val_zero,
List.getElem_cons_zero, Fin.isValue, List.eraseIdx_zero, List.tail_cons, koszulSign]
intro h
rw [koszulSignInsert_boson]
simp only [one_mul]
exact h
| r0 :: r, ⟨n + 1, h⟩ => by
simp only [List.length_cons, List.get_eq_getElem, List.getElem_cons_succ, Fin.isValue,
List.eraseIdx_cons_succ]
intro h'
rw [koszulSign, koszulSign]
rw [koszulSign_erase_boson q le1 r ⟨n, Nat.succ_lt_succ_iff.mp h⟩]
congr 1
rw [koszulSignInsert_erase_boson q le1 r0 r ⟨n, Nat.succ_lt_succ_iff.mp h⟩ h']
exact h'
lemma koszulSign_insertIdx {I : Type} (q : I → Fin 2) (le1 : I → I → Prop) [DecidableRel le1]
(i : I) [IsTotal I le1] [IsTrans I le1] : (r : List I) → (n : ) → (hn : n ≤ r.length) →
koszulSign le1 q (List.insertIdx n i r) = insertSign q n i r
* koszulSign le1 q r
* insertSign q (insertionSortEquiv le1 (List.insertIdx n i r) ⟨n, by
rw [List.length_insertIdx _ _ hn]
omega⟩) i
(List.insertionSort le1 (List.insertIdx n i r))
| [], 0, h => by
simp [koszulSign, insertSign, superCommuteCoef, koszulSignInsert]
| [], n + 1, h => by
simp at h
| r0 :: r, 0, h => by
simp only [List.insertIdx_zero, List.insertionSort, List.length_cons, Fin.zero_eta]
rw [koszulSign]
trans koszulSign le1 q (r0 :: r) * koszulSignInsert le1 q i (r0 :: r)
ring
simp only [insertionSortEquiv, List.length_cons, Nat.succ_eq_add_one, List.insertionSort,
orderedInsertEquiv, OrderIso.toEquiv_symm, Fin.symm_castOrderIso, HepLean.Fin.equivCons_trans,
Equiv.trans_apply, HepLean.Fin.equivCons_zero, HepLean.Fin.finExtractOne_apply_eq,
Fin.isValue, HepLean.Fin.finExtractOne_symm_inl_apply, RelIso.coe_fn_toEquiv,
Fin.castOrderIso_apply, Fin.cast_mk, Fin.eta]
conv_rhs =>
rhs
rhs
rw [orderedInsert_eq_insertIdx_orderedInsertPos]
conv_rhs =>
rhs
rw [← insertSign_insert]
change insertSign q (↑(orderedInsertPos le1 ((List.insertionSort le1 (r0 :: r))) i)) i
(List.insertionSort le1 (r0 :: r))
rw [← koszulSignInsert_eq_insertSign q le1]
rw [insertSign_zero]
simp
| r0 :: r, n + 1, h => by
conv_lhs =>
rw [List.insertIdx_succ_cons]
rw [koszulSign]
rw [koszulSign_insertIdx]
conv_rhs =>
rhs
simp only [List.insertIdx_succ_cons]
simp only [List.insertionSort, List.length_cons, insertionSortEquiv, Nat.succ_eq_add_one,
Equiv.trans_apply, HepLean.Fin.equivCons_succ]
erw [orderedInsertEquiv_fin_succ]
simp only [Fin.eta, Fin.coe_cast]
rhs
rw [orderedInsert_eq_insertIdx_orderedInsertPos]
conv_rhs =>
lhs
rw [insertSign_succ_cons, koszulSign]
ring_nf
conv_lhs =>
lhs
rw [mul_assoc, mul_comm]
rw [mul_assoc]
conv_rhs =>
rw [mul_assoc, mul_assoc]
congr 1
let rs := (List.insertionSort le1 (List.insertIdx n i r))
have hnsL : n < (List.insertIdx n i r).length := by
rw [List.length_insertIdx _ _]
simp only [List.length_cons, add_le_add_iff_right] at h
omega
exact Nat.le_of_lt_succ h
let ni : Fin rs.length := (insertionSortEquiv le1 (List.insertIdx n i r))
⟨n, hnsL⟩
let nro : Fin (rs.length + 1) :=
⟨↑(orderedInsertPos le1 rs r0), orderedInsertPos_lt_length le1 rs r0⟩
rw [koszulSignInsert_insertIdx, koszulSignInsert_cons]
trans koszulSignInsert le1 q r0 r * (koszulSignCons q le1 r0 i *insertSign q ni i rs)
· simp only [rs, ni]
ring
trans koszulSignInsert le1 q r0 r * (superCommuteCoef q [i] [r0] *
insertSign q (nro.succAbove ni) i (List.insertIdx nro r0 rs))
swap
· simp only [rs, nro, ni]
ring
congr 1
simp only [Fin.succAbove]
have hns : rs.get ni = i := by
simp only [Fin.eta, rs]
rw [← insertionSortEquiv_get]
simp only [Function.comp_apply, Equiv.symm_apply_apply, List.get_eq_getElem, ni]
simp_all only [List.length_cons, add_le_add_iff_right, List.getElem_insertIdx_self]
have hc1 : ni.castSucc < nro → ¬ le1 r0 i := by
intro hninro
rw [← hns]
exact lt_orderedInsertPos_rel le1 r0 rs ni hninro
have hc2 : ¬ ni.castSucc < nro → le1 r0 i := by
intro hninro
rw [← hns]
refine gt_orderedInsertPos_rel le1 r0 rs ?_ ni hninro
exact List.sorted_insertionSort le1 (List.insertIdx n i r)
by_cases hn : ni.castSucc < nro
· simp only [hn, ↓reduceIte, Fin.coe_castSucc]
rw [insertSign_insert_gt]
swap
· exact hn
congr 1
rw [koszulSignCons_eq_superComuteCoef]
simp only [hc1 hn, ↓reduceIte]
rw [superCommuteCoef_comm]
· simp only [hn, ↓reduceIte, Fin.val_succ]
rw [insertSign_insert_lt]
rw [← mul_assoc]
congr 1
rw [superCommuteCoef_mul_self]
rw [koszulSignCons]
simp only [hc2 hn, ↓reduceIte]
exact Nat.le_of_not_lt hn
exact Nat.le_of_lt_succ (orderedInsertPos_lt_length le1 rs r0)
· exact Nat.le_of_lt_succ h
· exact Nat.le_of_lt_succ h
end Wick

View file

@ -0,0 +1,243 @@
/-
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 Mathlib.Algebra.FreeAlgebra
import Mathlib.Algebra.Lie.OfAssociative
import Mathlib.Analysis.Complex.Basic
import HepLean.PerturbationTheory.Wick.Signs.InsertSign
/-!
# Koszul sign insert
-/
namespace Wick
open HepLean.List
/-- Gives a factor of `-1` when inserting `a` into a list `List I` in the ordered position
for each fermion-fermion cross. -/
def koszulSignInsert {I : Type} (r : I → I → Prop) [DecidableRel r] (q : I → Fin 2) (a : I) :
List I →
| [] => 1
| b :: l => if r a b then koszulSignInsert r q a l else
if q a = 1 ∧ q b = 1 then - koszulSignInsert r q a l else koszulSignInsert r q a l
/-- When inserting a boson the `koszulSignInsert` is always `1`. -/
lemma koszulSignInsert_boson {I : Type} (r : I → I → Prop) [DecidableRel r] (q : I → Fin 2) (a : I)
(ha : q a = 0) : (l : List I) → koszulSignInsert r q a l = 1
| [] => by
simp [koszulSignInsert]
| b :: l => by
simp only [koszulSignInsert, Fin.isValue, ite_eq_left_iff]
rw [koszulSignInsert_boson r q a ha l, ha]
simp only [Fin.isValue, zero_ne_one, false_and, ↓reduceIte, ite_self]
@[simp]
lemma koszulSignInsert_mul_self {I : Type} (r : I → I → Prop) [DecidableRel r] (q : I → Fin 2)
(a : I) : (l : List I) → koszulSignInsert r q a l * koszulSignInsert r q a l = 1
| [] => by
simp [koszulSignInsert]
| b :: l => by
simp only [koszulSignInsert, Fin.isValue, mul_ite, ite_mul, neg_mul, mul_neg]
by_cases hr : r a b
· simp only [hr, ↓reduceIte]
rw [koszulSignInsert_mul_self]
· simp only [hr, ↓reduceIte, Fin.isValue]
by_cases hq : q a = 1 ∧ q b = 1
· simp only [hq, Fin.isValue, and_self, ↓reduceIte, neg_neg]
rw [koszulSignInsert_mul_self]
· simp only [Fin.isValue, hq, ↓reduceIte]
rw [koszulSignInsert_mul_self]
lemma koszulSignInsert_le_forall {I : Type} (r : I → I → Prop) [DecidableRel r] (q : I → Fin 2)
(a : I) (l : List I) (hi : ∀ b, r a b) : koszulSignInsert r q a l = 1 := by
induction l with
| nil => rfl
| cons j l ih =>
simp only [koszulSignInsert, Fin.isValue, ite_eq_left_iff]
rw [ih]
simp only [Fin.isValue, ite_eq_left_iff, ite_eq_right_iff, and_imp]
intro h
exact False.elim (h (hi j))
lemma koszulSignInsert_ge_forall_append {I : Type} (r : I → I → Prop) [DecidableRel r]
(q : I → Fin 2) (l : List I) (j i : I) (hi : ∀ j, r j i) :
koszulSignInsert r q j l = koszulSignInsert r q j (l ++ [i]) := by
induction l with
| nil => simp [koszulSignInsert, hi]
| cons b l ih =>
simp only [koszulSignInsert, Fin.isValue, List.append_eq]
by_cases hr : r j b
· rw [if_pos hr, if_pos hr]
rw [ih]
· rw [if_neg hr, if_neg hr]
rw [ih]
lemma koszulSignInsert_eq_filter {I : Type} (q : I → Fin 2) (le1 : I → I → Prop) [DecidableRel le1]
(r0 : I) : (r : List I) →
koszulSignInsert le1 q r0 r =
koszulSignInsert le1 q r0 (List.filter (fun i => decide (¬ le1 r0 i)) r)
| [] => by
simp [koszulSignInsert]
| r1 :: r => by
dsimp only [koszulSignInsert, Fin.isValue]
simp only [Fin.isValue, List.filter, decide_not]
by_cases h : le1 r0 r1
· simp only [h, ↓reduceIte, decide_True, Bool.not_true]
rw [koszulSignInsert_eq_filter]
congr
simp
· simp only [h, ↓reduceIte, Fin.isValue, decide_False, Bool.not_false]
dsimp only [Fin.isValue, koszulSignInsert]
simp only [Fin.isValue, h, ↓reduceIte]
rw [koszulSignInsert_eq_filter]
congr
simp only [decide_not]
simp
lemma koszulSignInsert_eq_cons {I : Type} (q : I → Fin 2) (le1 : I → I → Prop) [DecidableRel le1]
[IsTotal I le1] (r0 : I) (r : List I) :
koszulSignInsert le1 q r0 r = koszulSignInsert le1 q r0 (r0 :: r) := by
simp only [koszulSignInsert, Fin.isValue, and_self]
have h1 : le1 r0 r0 := by
simpa using IsTotal.total (r := le1) r0 r0
simp [h1]
lemma koszulSignInsert_eq_grade {I : Type} (q : I → Fin 2) (le1 : I → I → Prop) [DecidableRel le1]
(r0 : I) (r : List I) : koszulSignInsert le1 q r0 r = if grade q [r0] = 1 ∧
grade q (List.filter (fun i => decide (¬ le1 r0 i)) r) = 1 then -1 else 1 := by
induction r with
| nil =>
simp [koszulSignInsert]
| cons r1 r ih =>
rw [koszulSignInsert_eq_filter]
by_cases hr1 : ¬ le1 r0 r1
· rw [List.filter_cons_of_pos]
· dsimp only [koszulSignInsert, Fin.isValue, decide_not]
rw [if_neg hr1]
dsimp only [Fin.isValue, grade, ite_eq_right_iff, zero_ne_one, imp_false, decide_not]
simp only [Fin.isValue, decide_not, ite_eq_right_iff, zero_ne_one, imp_false]
have ha (a b c : Fin 2) : (if a = 1 ∧ b = 1 then -if ¬a = 0 ∧
c = 1 then -1 else (1 : )
else if ¬a = 0 ∧ c = 1 then -1 else 1) =
if ¬a = 0 ∧ ¬b = c then -1 else 1 := by
fin_cases a <;> fin_cases b <;> fin_cases c
any_goals rfl
simp
rw [← ha (q r0) (q r1) (grade q (List.filter (fun a => !decide (le1 r0 a)) r))]
congr
· rw [koszulSignInsert_eq_filter] at ih
simpa [grade] using ih
· rw [koszulSignInsert_eq_filter] at ih
simpa [grade] using ih
· simp [hr1]
· rw [List.filter_cons_of_neg]
simp only [decide_not, Fin.isValue]
rw [koszulSignInsert_eq_filter] at ih
simpa [grade] using ih
simpa using hr1
lemma koszulSignInsert_eq_perm {I : Type} (q : I → Fin 2) (le1 : I → I → Prop) (r r' : List I)
(a : I) [DecidableRel le1] (h : r.Perm r') :
koszulSignInsert le1 q a r = koszulSignInsert le1 q a r' := by
rw [koszulSignInsert_eq_grade]
rw [koszulSignInsert_eq_grade]
congr 1
simp only [Fin.isValue, decide_not, eq_iff_iff, and_congr_right_iff]
intro h'
have hg : grade q (List.filter (fun i => !decide (le1 a i)) r) =
grade q (List.filter (fun i => !decide (le1 a i)) r') := by
rw [grade_count, grade_count]
rw [List.countP_filter, List.countP_filter]
rw [h.countP_eq]
rw [hg]
lemma koszulSignInsert_eq_sort {I : Type} (q : I → Fin 2) (le1 : I → I → Prop) (r : List I)
(a : I) [DecidableRel le1] :
koszulSignInsert le1 q a r = koszulSignInsert le1 q a (List.insertionSort le1 r) := by
apply koszulSignInsert_eq_perm
exact List.Perm.symm (List.perm_insertionSort le1 r)
lemma koszulSignInsert_eq_insertSign {I : Type} (q : I → Fin 2) (le1 : I → I → Prop)
[DecidableRel le1] [IsTotal I le1] [IsTrans I le1] (r0 : I) (r : List I) :
koszulSignInsert le1 q r0 r = insertSign q (orderedInsertPos le1 (List.insertionSort le1 r) r0)
r0 (List.insertionSort le1 r) := by
rw [koszulSignInsert_eq_cons, koszulSignInsert_eq_sort, koszulSignInsert_eq_filter,
koszulSignInsert_eq_grade, insertSign, superCommuteCoef]
congr
simp only [List.filter_filter, Bool.and_self]
rw [List.insertionSort]
nth_rewrite 1 [List.orderedInsert_eq_take_drop]
rw [List.filter_append]
have h1 : List.filter (fun a => decide ¬le1 r0 a)
(List.takeWhile (fun b => decide ¬le1 r0 b) (List.insertionSort le1 r))
= (List.takeWhile (fun b => decide ¬le1 r0 b) (List.insertionSort le1 r)) := by
induction r with
| nil => simp
| cons r1 r ih =>
simp only [decide_not, List.insertionSort, List.filter_eq_self, Bool.not_eq_eq_eq_not,
Bool.not_true, decide_eq_false_iff_not]
intro a ha
have ha' := List.mem_takeWhile_imp ha
simp_all
rw [h1]
rw [List.filter_cons]
simp only [decide_not, (IsTotal.to_isRefl le1).refl r0, not_true_eq_false, decide_False,
Bool.false_eq_true, ↓reduceIte]
rw [orderedInsertPos_take]
simp only [decide_not, List.append_right_eq_self, List.filter_eq_nil_iff, Bool.not_eq_eq_eq_not,
Bool.not_true, decide_eq_false_iff_not, Decidable.not_not]
intro a ha
refine List.Sorted.rel_of_mem_take_of_mem_drop
(k := (orderedInsertPos le1 (List.insertionSort le1 r) r0).1 + 1)
(List.sorted_insertionSort le1 (r0 :: r)) ?_ ?_
· simp only [List.insertionSort, List.orderedInsert_eq_take_drop, decide_not]
rw [List.take_append_eq_append_take]
rw [List.take_of_length_le]
· simp [orderedInsertPos]
· simp [orderedInsertPos]
· simp only [List.insertionSort, List.orderedInsert_eq_take_drop, decide_not]
rw [List.drop_append_eq_append_drop]
rw [List.drop_of_length_le]
· simpa [orderedInsertPos] using ha
· simp [orderedInsertPos]
lemma koszulSignInsert_insertIdx {I : Type} (q : I → Fin 2) (le1 : I → I → Prop) [DecidableRel le1]
(i j : I) (r : List I) (n : ) (hn : n ≤ r.length) :
koszulSignInsert le1 q j (List.insertIdx n i r) = koszulSignInsert le1 q j (i :: r) := by
apply koszulSignInsert_eq_perm
exact List.perm_insertIdx i r hn
/-- The difference in `koszulSignInsert` on inserting `r0` into `r` compared to
into `r1 :: r` for any `r`. -/
def koszulSignCons {I : Type} (q : I → Fin 2) (le1 : I → I → Prop) [DecidableRel le1] (r0 r1 : I) :
:=
if le1 r0 r1 then 1 else
if q r0 = 1 ∧ q r1 = 1 then -1 else 1
lemma koszulSignCons_eq_superComuteCoef {I : Type} (q : I → Fin 2) (le1 : I → I → Prop)
[DecidableRel le1] (r0 r1 : I) : koszulSignCons q le1 r0 r1 =
if le1 r0 r1 then 1 else superCommuteCoef q [r0] [r1] := by
simp only [koszulSignCons, Fin.isValue, superCommuteCoef, grade, ite_eq_right_iff, zero_ne_one,
imp_false]
congr 1
by_cases h0 : q r0 = 1
· by_cases h1 : q r1 = 1
· simp [h0, h1]
· have h1 : q r1 = 0 := by omega
simp [h0, h1]
· have h0 : q r0 = 0 := by omega
by_cases h1 : q r1 = 1
· simp [h0, h1]
· have h1 : q r1 = 0 := by omega
simp [h0, h1]
lemma koszulSignInsert_cons {I : Type} (q : I → Fin 2) (le1 : I → I → Prop) [DecidableRel le1]
(r0 r1 : I) (r : List I) :
koszulSignInsert le1 q r0 (r1 :: r) = (koszulSignCons q le1 r0 r1) *
koszulSignInsert le1 q r0 r := by
simp [koszulSignInsert, koszulSignCons]
end Wick

View file

@ -0,0 +1,93 @@
/-
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 Mathlib.Algebra.FreeAlgebra
import Mathlib.Algebra.Lie.OfAssociative
import Mathlib.Analysis.Complex.Basic
import HepLean.PerturbationTheory.Wick.Signs.KoszulSign
/-!
# Koszul sign insert
-/
namespace Wick
open HepLean.List
/-- The sign that appears in the static version of Wicks theorem.
This is actually equal to `superCommuteCoef q [r.get n] (r.take n)`, something
which will be proved in a lemma. -/
def staticWickCoef {I : Type} (q : I → Fin 2) (le1 :I → I → Prop) (r : List I)
[DecidableRel le1] (i : I) (n : Fin r.length) : :=
koszulSign le1 q r *
superCommuteCoef q [i] (List.take (↑((HepLean.List.insertionSortEquiv le1 r) n))
(List.insertionSort le1 r)) *
koszulSign le1 q (r.eraseIdx ↑n)
lemma staticWickCoef_eq_q {I : Type} (q : I → Fin 2) (le1 :I → I → Prop) (r : List I)
[DecidableRel le1] (i : I) (n : Fin r.length)
(hq : q i = q (r.get n)) :
staticWickCoef q le1 r i n =
koszulSign le1 q r *
superCommuteCoef q [r.get n] (List.take (↑(insertionSortEquiv le1 r n))
(List.insertionSort le1 r)) *
koszulSign le1 q (r.eraseIdx ↑n) := by
simp [staticWickCoef, superCommuteCoef, grade, hq]
lemma insertIdx_eraseIdx {I : Type} :
(n : ) → (r : List I) → (hn : n < r.length) →
List.insertIdx n (r.get ⟨n, hn⟩) (r.eraseIdx n) = r
| n, [], hn => by
simp at hn
| 0, r0 :: r, hn => by
simp
| n + 1, r0 :: r, hn => by
simp only [List.length_cons, List.get_eq_getElem, List.getElem_cons_succ,
List.eraseIdx_cons_succ, List.insertIdx_succ_cons, List.cons.injEq, true_and]
exact insertIdx_eraseIdx n r _
lemma staticWickCoef_eq_get {I : Type} (q : I → Fin 2) (le1 :I → I → Prop) (r : List I)
[DecidableRel le1] [IsTotal I le1] [IsTrans I le1] (i : I) (n : Fin r.length)
(heq : q i = q (r.get n)) :
staticWickCoef q le1 r i n = superCommuteCoef q [r.get n] (r.take n) := by
rw [staticWickCoef_eq_q]
let r' := r.eraseIdx ↑n
have hr : List.insertIdx n (r.get n) (r.eraseIdx n) = r := by
exact insertIdx_eraseIdx n.1 r n.prop
conv_lhs =>
lhs
lhs
rw [← hr]
rw [koszulSign_insertIdx q le1 (r.get n) ((r.eraseIdx ↑n)) n (by
rw [List.length_eraseIdx]
simp only [Fin.is_lt, ↓reduceIte]
omega)]
rhs
rhs
rw [hr]
conv_lhs =>
lhs
lhs
rhs
enter [2, 1, 1]
rw [insertionSortEquiv_congr _ _ hr]
simp only [List.get_eq_getElem, Equiv.trans_apply, RelIso.coe_fn_toEquiv, Fin.castOrderIso_apply,
Fin.cast_mk, Fin.eta, Fin.coe_cast]
conv_lhs =>
lhs
rw [mul_assoc]
rhs
rw [insertSign]
rw [superCommuteCoef_mul_self]
simp only [mul_one]
rw [mul_assoc]
rw [koszulSign_mul_self]
simp only [mul_one]
rw [insertSign_eraseIdx]
rfl
exact heq
end Wick

View file

@ -0,0 +1,92 @@
/-
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 HepLean.Mathematics.List
import HepLean.PerturbationTheory.Wick.Signs.Grade
/-!
# Koszul signs and ordering for lists and algebras
-/
namespace Wick
open HepLean.List
/-- Given two lists `la` and `lb` returns `-1` if they are both of grade `1` and
`1` otherwise. This corresponds to the sign associated with the super commutator
when commuting `la` and `lb` in the free algebra.
In terms of physics it is `-1` if commuting two fermionic operators and `1` otherwise. -/
def superCommuteCoef {I : Type} (q : I → Fin 2) (la lb : List I) : :=
if grade q la = 1 ∧ grade q lb = 1 then - 1 else 1
lemma superCommuteCoef_comm {I : Type} (q : I → Fin 2) (la lb : List I) :
superCommuteCoef q la lb = superCommuteCoef q lb la := by
simp only [superCommuteCoef, Fin.isValue]
congr 1
exact Eq.propIntro (fun a => id (And.symm a)) fun a => id (And.symm a)
/-- Given a list `l : List (Σ i, f i)` and a list `r : List I` returns `-1` if the
grade of `l` is `1` and the grade of `r` is `1` and `1` otherwise. This corresponds
to the sign associated with the super commutator when commuting
the lift of `l` and `r` (by summing over fibers) in the
free algebra over `Σ i, f i`.
In terms of physics it is `-1` if commuting two fermionic operators and `1` otherwise. -/
def superCommuteLiftCoef {I : Type} {f : I → Type}
(q : I → Fin 2) (l : List (Σ i, f i)) (r : List I) : :=
(if grade (fun i => q i.fst) l = 1 ∧ grade q r = 1 then -1 else 1)
lemma superCommuteLiftCoef_empty {I : Type} {f : I → Type}
(q : I → Fin 2) (l : List (Σ i, f i)) :
superCommuteLiftCoef q l [] = 1 := by
simp [superCommuteLiftCoef]
lemma superCommuteCoef_perm_snd {I : Type} (q : I → Fin 2) (la lb lb' : List I)
(h : lb.Perm lb') :
superCommuteCoef q la lb = superCommuteCoef q la lb' := by
rw [superCommuteCoef, superCommuteCoef, grade_perm q h]
lemma superCommuteCoef_mul_self {I : Type} (q : I → Fin 2) (l lb : List I) :
superCommuteCoef q l lb * superCommuteCoef q l lb = 1 := by
simp only [superCommuteCoef, Fin.isValue, mul_ite, mul_neg, mul_one]
have ha (a b : Fin 2) : (if a = 1 ∧ b = 1 then -if a = 1 ∧ b = 1 then -1 else 1
else if a = 1 ∧ b = 1 then -1 else 1) = (1 : ) := by
fin_cases a <;> fin_cases b
any_goals rfl
simp
exact ha (grade q l) (grade q lb)
lemma superCommuteCoef_empty {I : Type} (q : I → Fin 2) (la : List I) :
superCommuteCoef q la [] = 1 := by
simp only [superCommuteCoef, Fin.isValue, grade_empty, zero_ne_one, and_false, ↓reduceIte]
lemma superCommuteCoef_append {I : Type} (q : I → Fin 2) (la lb lc : List I) :
superCommuteCoef q la (lb ++ lc) = superCommuteCoef q la lb * superCommuteCoef q la lc := by
simp only [superCommuteCoef, Fin.isValue, grade_append, ite_eq_right_iff, zero_ne_one, imp_false,
mul_ite, mul_neg, mul_one]
by_cases hla : grade q la = 1
· by_cases hlb : grade q lb = 1
· by_cases hlc : grade q lc = 1
· simp [hlc, hlb, hla]
· have hc : grade q lc = 0 := by
omega
simp [hc, hlb, hla]
· have hb : grade q lb = 0 := by
omega
by_cases hlc : grade q lc = 1
· simp [hlc, hb]
· have hc : grade q lc = 0 := by
omega
simp [hc, hb]
· have ha : grade q la = 0 := by
omega
simp [ha]
lemma superCommuteCoef_cons {I : Type} (q : I → Fin 2) (i : I) (la lb : List I) :
superCommuteCoef q la (i :: lb) = superCommuteCoef q la [i] * superCommuteCoef q la lb := by
trans superCommuteCoef q la ([i] ++ lb)
simp only [List.singleton_append]
rw [superCommuteCoef_append]
end Wick

View file

@ -1,81 +0,0 @@
/-
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 Mathlib.Logic.Function.Basic
import HepLean.Meta.Informal.Basic
import HepLean.Meta.Notes.Basic
import HepLean.Lorentz.RealVector.Basic
/-!
# Wick Species
Note: There is very likely a much better name for what we here call a Wick Species.
A Wick Species is a structure containing the basic information needed to write wick contractions
for a theory, and calculate their corresponding Feynman diagrams.
-/
/-! TODO: There should be some sort of notion of a group action on a Wick Species. -/
namespace Wick
note "
<h2>Wick Species</h2>
To do perturbation theory for a quantum field theory, we need a quantum field theory, or
at least enough data from a quantum field theory to write down necessary constructions.
The first bit of data we need is a type of fields `𝓯`. We also need to know what fields
are dual to what other fields, for example in a complex scalar theory `φ` is dual to `φ†`.
We can encode this information in an involution `ξ : 𝓯𝓯`.
<br><br>
The second bit of data we need is how the fields interact with each other. In other words,
a list of interaction vertices `𝓘`, and the type of fields associated to each vertex.
<br><br>
This necessary information to do perturbation theory is encoded in a `Wick Species`, which
we define as:
"
/-- The basic structure needed to write down Wick contractions for a theory and
calculate the corresponding Feynman diagrams.
WARNING: This definition is not yet complete. -/
@[note_attr]
structure Species where
/-- The color of Field operators which appear in a theory.
One may wish to call these `half-edges`, however we restrict this terminology
to Feynman diagrams. -/
𝓯 : Type
/-- The map taking a field operator to its dual operator. -/
ξ : 𝓯𝓯
/-- The condition that `ξ` is an involution. -/
ξ_involutive : Function.Involutive ξ
/-- The color of interaction terms which appear in a theory.
One may wish to call these `vertices`, however we restrict this terminology
to Feynman diagrams. -/
𝓘 : Type
/-- The fields associated to each interaction term. -/
𝓘Fields : 𝓘 → Σ n, Fin n → 𝓯
/-- The map taking a field to `0` if it is a boson and `1` if it is a fermion.
Note that this definition suffers a similar problem to Boolean Blindness. -/
grade : 𝓯 → Fin 2
namespace Species
variable (S : Species)
/-- When commuting two fields `f` and `g`, in the super commuator which is sematically
`[f, g] = f g + c * g f`, this is `c`. -/
def commFactor (f g : S.𝓯) : := - (- 1) ^ (S.grade f * S.grade g : )
informal_definition 𝓕 where
math :≈ "The orbits of the involution `ξ`.
May have to define a multiplicative action of ℤ₂ on `𝓯`, and
take the orbits of this."
physics :≈ "The different types of fields present in a theory."
deps :≈ [``Species]
end Species
end Wick

View file

@ -0,0 +1,109 @@
/-
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 HepLean.PerturbationTheory.Wick.Contraction
/-!
# Static Wick's theorem
-/
namespace Wick
noncomputable section
open HepLean.List
lemma static_wick_nil {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
(q : I → Fin 2)
(le1 : (Σ i, f i) → (Σ i, f i) → Prop) [DecidableRel le1]
{A : Type} [Semiring A] [Algebra A]
(F : FreeAlgebra (Σ i, f i) →ₐ A)
(S : Contractions.Splitting f le1) :
F (ofListLift f [] 1) = ∑ c : Contractions [],
c.toCenterTerm f q le1 F S *
F (koszulOrder le1 (fun i => q i.fst) (ofListLift f c.normalize 1)) := by
rw [← Contractions.nilEquiv.symm.sum_comp]
simp only [Finset.univ_unique, PUnit.default_eq_unit, Contractions.nilEquiv, Equiv.coe_fn_symm_mk,
Finset.sum_const, Finset.card_singleton, one_smul]
dsimp [Contractions.normalize, Contractions.toCenterTerm]
simp [ofListLift_empty]
lemma static_wick_cons {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
(q : I → Fin 2)
(le1 : (Σ i, f i) → (Σ i, f i) → Prop) [DecidableRel le1]
[IsTrans ((i : I) × f i) le1] [IsTotal ((i : I) × f i) le1]
{A : Type} [Semiring A] [Algebra A] (r : List I) (a : I)
(F : FreeAlgebra (Σ i, f i) →ₐ A) [OperatorMap (fun i => q i.1) le1 F]
(S : Contractions.Splitting f le1)
(ih : F (ofListLift f r 1) =
∑ c : Contractions r, c.toCenterTerm f q le1 F S * F (koszulOrder le1 (fun i => q i.fst)
(ofListLift f c.normalize 1))) :
F (ofListLift f (a :: r) 1) = ∑ c : Contractions (a :: r),
c.toCenterTerm f q le1 F S *
F (koszulOrder le1 (fun i => q i.fst) (ofListLift f c.normalize 1)) := by
rw [ofListLift_cons_eq_ofListLift, map_mul, ih, Finset.mul_sum,
← Contractions.consEquiv.symm.sum_comp]
erw [Finset.sum_sigma]
congr
funext c
have hb := S.h𝓑 a
rw [← mul_assoc]
have hi := c.toCenterTerm_center f q le1 F S
rw [Subalgebra.mem_center_iff] at hi
rw [hi, mul_assoc, ← map_mul, hb, add_mul, map_add]
conv_lhs =>
rhs
lhs
rw [ofList_eq_smul_one]
rw [Algebra.smul_mul_assoc]
rw [ofList_singleton]
rw [mul_koszulOrder_le]
conv_lhs =>
rhs
lhs
rw [← map_smul, ← Algebra.smul_mul_assoc]
rw [← ofList_singleton, ← ofList_eq_smul_one]
conv_lhs =>
rhs
rhs
rw [ofList_eq_smul_one, Algebra.smul_mul_assoc, map_smul]
rw [le_all_mul_koszulOrder_ofListLift_expand]
conv_lhs =>
rhs
rhs
rw [smul_add, Finset.smul_sum]
rw [← map_smul, ← map_smul, ← Algebra.smul_mul_assoc, ← ofList_eq_smul_one]
rhs
rhs
intro n
rw [← Algebra.smul_mul_assoc, smul_comm, ← map_smul, ← LinearMap.map_smul₂,
← ofList_eq_smul_one]
rw [← add_assoc, ← map_add, ← map_add, ← add_mul, ← hb, ← ofListLift_cons_eq_ofListLift, mul_add]
rw [Fintype.sum_option]
congr 1
rw [Finset.mul_sum]
congr
funext n
rw [← mul_assoc]
rfl
exact S.h𝓑p a
exact S.h𝓑n a
theorem static_wick_theorem {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
(q : I → Fin 2)
(le1 : (Σ i, f i) → (Σ i, f i) → Prop) [DecidableRel le1] [IsTrans ((i : I) × f i) le1]
[IsTotal ((i : I) × f i) le1]
{A : Type} [Semiring A] [Algebra A] (r : List I)
(F : FreeAlgebra (Σ i, f i) →ₐ A) [OperatorMap (fun i => q i.1) le1 F]
(S : Contractions.Splitting f le1) :
F (ofListLift f r 1) = ∑ c : Contractions r, c.toCenterTerm f q le1 F S *
F (koszulOrder le1 (fun i => q i.fst) (ofListLift f c.normalize 1)) := by
induction r with
| nil => exact static_wick_nil q le1 F S
| cons a r ih => exact static_wick_cons q le1 r a F S ih
end
end Wick

View file

@ -1,133 +0,0 @@
/-
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 HepLean.Meta.Informal.Basic
import HepLean.PerturbationTheory.Wick.Species
import Mathlib.Data.Fin.Tuple.Basic
/-!
# Wick strings
A wick string is defined to be a sequence of input fields,
followed by a squence of vertices, followed by a sequence of output fields.
A wick string can be combined with an appropriate map to spacetime to produce a specific
term in the ring of operators. This has yet to be implemented.
-/
namespace Wick
variable {S : Species}
/-- A helper function for `WickString`. It is used to seperate incoming, vertex, and
outgoing nodes. -/
inductive WickStringLast where
| incoming : WickStringLast
| vertex : WickStringLast
| outgoing : WickStringLast
| final : WickStringLast
open WickStringLast
/-- A wick string is a representation of a string of fields from a theory.
The use of vertices in the Wick string
allows us to identify which fields have the same space-time coordinate.
Note: Fields are added to `c` from right to left - matching how we would write this on
pen and paper.
The incoming and outgoing fields should be viewed as asymptotic fields.
While the internal fields associated with vertices are fields at fixed space-time points.
-/
inductive WickString : {ni : } → (i : Fin ni → S.𝓯) → {n : } → (c : Fin n → S.𝓯) →
{no : } → (o : Fin no → S.𝓯) → WickStringLast → Type where
| empty : WickString Fin.elim0 Fin.elim0 Fin.elim0 incoming
| incoming {n ni no : } {i : Fin ni → S.𝓯} {c : Fin n → S.𝓯}
{o : Fin no → S.𝓯} (w : WickString i c o incoming) (e : S.𝓯) :
WickString (Fin.cons e i) (Fin.cons e c) o incoming
| endIncoming {n ni no : } {i : Fin ni → S.𝓯} {c : Fin n → S.𝓯}
{o : Fin no → S.𝓯} (w : WickString i c o incoming) : WickString i c o vertex
| vertex {n ni no : } {i : Fin ni → S.𝓯} {c : Fin n → S.𝓯}
{o : Fin no → S.𝓯} (w : WickString i c o vertex) (v : S.𝓘) :
WickString i (Fin.append (S.𝓘Fields v).2 c) o vertex
| endVertex {n ni no : } {i : Fin ni → S.𝓯} {c : Fin n → S.𝓯}
{o : Fin no → S.𝓯} (w : WickString i c o vertex) : WickString i c o outgoing
| outgoing {n ni no : } {i : Fin ni → S.𝓯} {c : Fin n → S.𝓯}
{o : Fin no → S.𝓯} (w : WickString i c o outgoing) (e : S.𝓯) :
WickString i (Fin.cons e c) (Fin.cons e o) outgoing
| endOutgoing {n ni no : } {i : Fin ni → S.𝓯} {c : Fin n → S.𝓯}
{o : Fin no → S.𝓯} (w : WickString i c o outgoing) : WickString i c o final
namespace WickString
/-- The number of nodes in a Wick string. This is used to help prove termination. -/
def size {ni : } {i : Fin ni → S.𝓯} {n : } {c : Fin n → S.𝓯} {no : } {o : Fin no → S.𝓯}
{f : WickStringLast} : WickString i c o f → := fun
| empty => 0
| incoming w e => size w + 1
| endIncoming w => size w + 1
| vertex w v => size w + 1
| endVertex w => size w + 1
| outgoing w e => size w + 1
| endOutgoing w => size w + 1
/-- The number of vertices in a Wick string. This does NOT include external vertices. -/
def numIntVertex {ni : } {i : Fin ni → S.𝓯} {n : } {c : Fin n → S.𝓯} {no : } {o : Fin no → S.𝓯}
{f : WickStringLast} : WickString i c o f → := fun
| empty => 0
| incoming w e => numIntVertex w
| endIncoming w => numIntVertex w
| vertex w v => numIntVertex w + 1
| endVertex w => numIntVertex w
| outgoing w e => numIntVertex w
| endOutgoing w => numIntVertex w
/-- The vertices present in a Wick string. This does NOT include external vertices. -/
def intVertex {ni : } {i : Fin ni → S.𝓯} {n : } {c : Fin n → S.𝓯} {no : } {o : Fin no → S.𝓯}
{f : WickStringLast} : (w : WickString i c o f) → Fin w.numIntVertex → S.𝓘 := fun
| empty => Fin.elim0
| incoming w e => intVertex w
| endIncoming w => intVertex w
| vertex w v => Fin.cons v (intVertex w)
| endVertex w => intVertex w
| outgoing w e => intVertex w
| endOutgoing w => intVertex w
informal_definition intExtVertex where
math :≈ "The vertices present in a Wick string, including external vertices."
deps :≈ [``WickString]
informal_definition fieldToIntExtVertex where
math :≈ "A function which takes a field and returns the internal or
external vertex it is associated with."
deps :≈ [``WickString]
informal_definition exponentialPrefactor where
math :≈ "The combinatorical prefactor from the expansion of the
exponential associated with a Wick string."
deps :≈ [``intVertex, ``WickString]
informal_definition vertexPrefactor where
math :≈ "The prefactor arising from the coefficent of vertices in the
Lagrangian. This should not take account of the exponential prefactor."
deps :≈ [``intVertex, ``WickString]
informal_definition minNoLoops where
math :≈ "The minimum number of loops a Feynman diagram based on a given Wick string can have.
There should be a lemma proving this statement."
deps :≈ [``WickString]
informal_definition LoopLevel where
math :≈ "The type of Wick strings for fixed input and output which may permit a Feynman diagram
which have a number of loops less than or equal to some number."
deps :≈ [``minNoLoops, ``WickString]
informal_lemma loopLevel_fintype where
math :≈ "The instance of a finite type on `LoopLevel`."
deps :≈ [``LoopLevel]
end WickString
end Wick

View file

@ -0,0 +1,474 @@
/-
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 HepLean.PerturbationTheory.Wick.OfList
/-!
# Koszul signs and ordering for lists and algebras
-/
namespace Wick
noncomputable section
/-- Given a grading `q : I → Fin 2` and a list `l : List I` the super-commutor on the free algebra
`FreeAlgebra I` corresponding to commuting with `l`
as a linear map from `MonoidAlgebra (FreeMonoid I)` (the module of lists in `I`)
to itself. -/
def superCommuteMonoidAlgebra {I : Type} (q : I → Fin 2) (l : List I) :
MonoidAlgebra (FreeMonoid I) →ₗ[] MonoidAlgebra (FreeMonoid I) :=
Finsupp.lift (MonoidAlgebra (FreeMonoid I)) (List I)
(fun r =>
Finsupp.lsingle (R := ) (l ++ r) 1 +
if grade q l = 1 ∧ grade q r = 1 then
Finsupp.lsingle (R := ) (r ++ l) 1
else
- Finsupp.lsingle (R := ) (r ++ l) 1)
/-- Given a grading `q : I → Fin 2` the super-commutor on the free algebra `FreeAlgebra I`
as a linear map from `MonoidAlgebra (FreeMonoid I)` (the module of lists in `I`)
to `FreeAlgebra I →ₗ[] FreeAlgebra I`. -/
def superCommuteAlgebra {I : Type} (q : I → Fin 2) :
MonoidAlgebra (FreeMonoid I) →ₗ[] FreeAlgebra I →ₗ[] FreeAlgebra I :=
Finsupp.lift (FreeAlgebra I →ₗ[] FreeAlgebra I) (List I) fun l =>
(FreeAlgebra.equivMonoidAlgebraFreeMonoid.symm.toAlgHom.toLinearMap
∘ₗ superCommuteMonoidAlgebra q l
∘ₗ FreeAlgebra.equivMonoidAlgebraFreeMonoid.toAlgHom.toLinearMap)
/-- Given a grading `q : I → Fin 2` the super-commutor on the free algebra `FreeAlgebra I`
as a bi-linear map. -/
def superCommute {I : Type} (q : I → Fin 2) :
FreeAlgebra I →ₗ[] FreeAlgebra I →ₗ[] FreeAlgebra I :=
superCommuteAlgebra q
∘ₗ FreeAlgebra.equivMonoidAlgebraFreeMonoid.toAlgHom.toLinearMap
lemma equivMonoidAlgebraFreeMonoid_freeAlgebra {I : Type} (i : I) :
(FreeAlgebra.equivMonoidAlgebraFreeMonoid (FreeAlgebra.ι i)) =
Finsupp.single (FreeMonoid.of i) 1 := by
simp [FreeAlgebra.equivMonoidAlgebraFreeMonoid, MonoidAlgebra.single]
@[simp]
lemma superCommute_ι {I : Type} (q : I → Fin 2) (i j : I) :
superCommute q (FreeAlgebra.ι i) (FreeAlgebra.ι j) =
FreeAlgebra.ι i * FreeAlgebra.ι j +
if q i = 1 ∧ q j = 1 then
FreeAlgebra.ι j * FreeAlgebra.ι i
else
- FreeAlgebra.ι j * FreeAlgebra.ι i := by
simp only [superCommute, superCommuteAlgebra, AlgEquiv.toAlgHom_eq_coe,
AlgEquiv.toAlgHom_toLinearMap, LinearMap.coe_comp, Function.comp_apply,
AlgEquiv.toLinearMap_apply, equivMonoidAlgebraFreeMonoid_freeAlgebra, Fin.isValue, neg_mul]
erw [Finsupp.lift_apply]
simp only [superCommuteMonoidAlgebra, Finsupp.lsingle_apply, Fin.isValue, grade_freeMonoid,
zero_smul, Finsupp.sum_single_index, one_smul, LinearMap.coe_comp, Function.comp_apply,
AlgEquiv.toLinearMap_apply, equivMonoidAlgebraFreeMonoid_freeAlgebra]
conv_lhs =>
rhs
erw [Finsupp.lift_apply]
simp only [FreeAlgebra.equivMonoidAlgebraFreeMonoid, MonoidAlgebra.of_apply, Fin.isValue,
smul_add, MonoidAlgebra.smul_single', mul_one, smul_ite, smul_neg, Finsupp.sum_add,
Finsupp.single_zero, Finsupp.sum_single_index, grade_freeMonoid, neg_zero, ite_self,
AlgEquiv.ofAlgHom_symm_apply, map_add, MonoidAlgebra.lift_single, one_smul]
congr
by_cases hq : q i = 1 ∧ q j = 1
· rw [if_pos hq, if_pos hq]
simp only [MonoidAlgebra.lift_single, one_smul]
obtain ⟨left, right⟩ := hq
rfl
· rw [if_neg hq, if_neg hq]
simp only [map_neg, MonoidAlgebra.lift_single, one_smul, neg_inj]
rfl
lemma superCommute_ofList_ofList {I : Type} (q : I → Fin 2) (l r : List I) (x y : ) :
superCommute q (ofList l x) (ofList r y) =
ofList (l ++ r) (x * y) + (if grade q l = 1 ∧ grade q r = 1 then
ofList (r ++ l) (y * x) else - ofList (r ++ l) (y * x)) := by
simp only [superCommute, superCommuteAlgebra, AlgEquiv.toAlgHom_eq_coe,
AlgEquiv.toAlgHom_toLinearMap, ofList, LinearMap.coe_comp, Function.comp_apply,
AlgEquiv.toLinearMap_apply, AlgEquiv.apply_symm_apply, Fin.isValue]
erw [Finsupp.lift_apply]
simp only [superCommuteMonoidAlgebra, Finsupp.lsingle_apply, Fin.isValue, zero_smul,
Finsupp.sum_single_index, LinearMap.smul_apply, LinearMap.coe_comp, Function.comp_apply,
AlgEquiv.toLinearMap_apply, AlgEquiv.apply_symm_apply]
conv_lhs =>
rhs
rhs
erw [Finsupp.lift_apply]
simp only [Fin.isValue, smul_add, MonoidAlgebra.smul_single', mul_one, smul_ite, smul_neg,
Finsupp.sum_add, Finsupp.single_zero, Finsupp.sum_single_index, neg_zero, ite_self, map_add]
by_cases hg : grade q l = 1 ∧ grade q r = 1
· simp only [hg, Fin.isValue, and_self, ↓reduceIte]
congr
· rw [← map_smul]
congr
exact MonoidAlgebra.smul_single' x (l ++ r) y
· rw [← map_smul]
congr
rw [mul_comm]
exact MonoidAlgebra.smul_single' x (r ++ l) y
· simp only [Fin.isValue, hg, ↓reduceIte, map_neg, smul_neg]
congr
· rw [← map_smul]
congr
exact MonoidAlgebra.smul_single' x (l ++ r) y
· rw [← map_smul]
congr
rw [mul_comm]
exact MonoidAlgebra.smul_single' x (r ++ l) y
@[simp]
lemma superCommute_zero {I : Type} (q : I → Fin 2) (a : FreeAlgebra I) :
superCommute q a 0 = 0 := by
simp [superCommute]
@[simp]
lemma superCommute_one {I : Type} (q : I → Fin 2) (a : FreeAlgebra I) :
superCommute q a 1 = 0 := by
let f : FreeAlgebra I →ₗ[] FreeAlgebra I := (LinearMap.flip (superCommute q)) 1
have h1 : FreeAlgebra.equivMonoidAlgebraFreeMonoid.symm (MonoidAlgebra.single [] 1) =
(1 : FreeAlgebra I) := by
simp_all only [EmbeddingLike.map_eq_one_iff]
rfl
have f_single (l : FreeMonoid I) (x : ) :
f ((FreeAlgebra.equivMonoidAlgebraFreeMonoid.symm (MonoidAlgebra.single l x)))
= 0 := by
simp only [superCommute, superCommuteAlgebra, AlgEquiv.toAlgHom_eq_coe,
AlgEquiv.toAlgHom_toLinearMap, LinearMap.flip_apply, LinearMap.coe_comp, Function.comp_apply,
AlgEquiv.toLinearMap_apply, AlgEquiv.apply_symm_apply, f]
rw [← h1]
erw [Finsupp.lift_apply]
simp only [superCommuteMonoidAlgebra, Finsupp.lsingle_apply, Fin.isValue, zero_smul,
Finsupp.sum_single_index, LinearMap.smul_apply, LinearMap.coe_comp, Function.comp_apply,
AlgEquiv.toLinearMap_apply, AlgEquiv.apply_symm_apply, smul_eq_zero,
EmbeddingLike.map_eq_zero_iff]
apply Or.inr
conv_lhs =>
erw [Finsupp.lift_apply]
simp
have hf : f = 0 := by
let e : FreeAlgebra I ≃ₗ[] MonoidAlgebra (FreeMonoid I) :=
FreeAlgebra.equivMonoidAlgebraFreeMonoid.toLinearEquiv
apply (LinearEquiv.eq_comp_toLinearMap_iff (e₁₂ := e.symm) _ _).mp
apply MonoidAlgebra.lhom_ext'
intro l
apply LinearMap.ext
intro x
simp only [LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply,
MonoidAlgebra.lsingle_apply, LinearMap.zero_comp, LinearMap.zero_apply]
erw [f_single]
change f a = _
rw [hf]
simp
lemma superCommute_ofList_mul {I : Type} (q : I → Fin 2) (la lb lc : List I) (xa xb xc : ) :
superCommute q (ofList la xa) (ofList lb xb * ofList lc xc) =
(superCommute q (ofList la xa) (ofList lb xb) * ofList lc xc +
superCommuteCoef q la lb • ofList lb xb * superCommute q (ofList la xa) (ofList lc xc)) := by
simp only [Algebra.smul_mul_assoc]
conv_lhs => rw [← ofList_pair]
simp only [superCommute_ofList_ofList, Fin.isValue, grade_append, ite_eq_right_iff, zero_ne_one,
imp_false]
simp only [superCommute_ofList_ofList, Fin.isValue, grade_append, ite_eq_right_iff, zero_ne_one,
imp_false, ofList_triple_assoc, ofList_triple, ofList_pair, superCommuteCoef]
by_cases hla : grade q la = 1
· simp only [hla, Fin.isValue, true_and, ite_not, ite_smul, neg_smul, one_smul]
by_cases hlb : grade q lb = 1
· simp only [hlb, Fin.isValue, ↓reduceIte]
by_cases hlc : grade q lc = 1
· simp only [Fin.isValue, hlc, ↓reduceIte]
simp only [mul_assoc, add_mul, mul_add]
abel
· have hc : grade q lc = 0 := by
omega
simp only [Fin.isValue, hc, one_ne_zero, ↓reduceIte, zero_ne_one]
simp only [mul_assoc, add_mul, mul_add, mul_neg, neg_add_rev, neg_neg]
abel
· have hb : grade q lb = 0 := by
omega
simp only [hb, Fin.isValue, zero_ne_one, ↓reduceIte]
by_cases hlc : grade q lc = 1
· simp only [Fin.isValue, hlc, zero_ne_one, ↓reduceIte]
simp only [mul_assoc, add_mul, neg_mul, mul_add]
abel
· have hc : grade q lc = 0 := by
omega
simp only [Fin.isValue, hc, ↓reduceIte, zero_ne_one]
simp only [mul_assoc, add_mul, neg_mul, mul_add, mul_neg]
abel
· simp only [Fin.isValue, hla, false_and, ↓reduceIte, mul_assoc, add_mul, neg_mul, mul_add,
mul_neg, smul_add, one_smul, smul_neg]
abel
/-- Given two lists `la lb : List I`, in the expansion of the supercommutor of `la` and `lb`
via elements of `lb`the term associated with the `n`th element.
E.g. in the commutator
`[a, bc] = [a, b] c + b [a, c] ` the `superCommuteSplit` for `n=0` is `[a, b] c`
and for `n=1` is `b [a, c]`. -/
def superCommuteSplit {I : Type} (q : I → Fin 2) (la lb : List I) (xa xb : ) (n : )
(hn : n < lb.length) : FreeAlgebra I :=
superCommuteCoef q la (List.take n lb) •
ofList (List.take n lb) 1 *
superCommute q (ofList la xa) (FreeAlgebra.ι (lb.get ⟨n, hn⟩))
* ofList (List.drop (n + 1) lb) xb
lemma superCommute_ofList_cons {I : Type} (q : I → Fin 2) (la lb : List I) (xa xb : ) (b1 : I) :
superCommute q (ofList la xa) (ofList (b1 :: lb) xb) =
superCommute q (ofList la xa) (FreeAlgebra.ι b1) * ofList lb xb +
superCommuteCoef q la [b1] •
(ofList [b1] 1) * superCommute q (ofList la xa) (ofList lb xb) := by
rw [ofList_cons_eq_ofList]
rw [superCommute_ofList_mul]
congr
· exact ofList_singleton b1
lemma superCommute_ofList_sum {I : Type} (q : I → Fin 2) (la lb : List I) (xa xb : ) :
superCommute q (ofList la xa) (ofList lb xb) =
∑ (n : Fin lb.length), superCommuteSplit q la lb xa xb n n.prop := by
induction lb with
| nil =>
simp only [superCommute_ofList_ofList, List.append_nil, Fin.isValue, grade_empty, zero_ne_one,
and_false, ↓reduceIte, List.nil_append, List.length_nil, Finset.univ_eq_empty,
Finset.sum_empty]
ring_nf
abel
| cons b lb ih =>
rw [superCommute_ofList_cons, ih]
have h0 : ((superCommute q) (ofList la xa)) (FreeAlgebra.ι b) * ofList lb xb =
superCommuteSplit q la (b :: lb) xa xb 0 (Nat.zero_lt_succ lb.length) := by
simp [superCommuteSplit, superCommuteCoef_empty, ofList_empty]
rw [h0]
have hf (f : Fin (b :: lb).length → FreeAlgebra I) : ∑ n, f n = f ⟨0,
Nat.zero_lt_succ lb.length⟩ + ∑ n, f (Fin.succ n) := by
exact Fin.sum_univ_succAbove f ⟨0, Nat.zero_lt_succ lb.length⟩
rw [hf]
congr
rw [Finset.mul_sum]
congr
funext n
simp only [superCommuteSplit, Fin.eta, List.get_eq_getElem, Algebra.smul_mul_assoc,
Algebra.mul_smul_comm, smul_smul, List.length_cons, Fin.val_succ, List.take_succ_cons,
List.getElem_cons_succ, List.drop_succ_cons]
congr 1
· rw [mul_comm, ← superCommuteCoef_append]
rfl
· simp only [← mul_assoc, mul_eq_mul_right_iff]
exact Or.inl (Or.inl (ofList_cons_eq_ofList (List.take (↑n) lb) b 1).symm)
lemma superCommute_ofList_ofList_superCommuteCoef {I : Type} (q : I → Fin 2) (la lb : List I)
(xa xb : ) : superCommute q (ofList la xa) (ofList lb xb) =
ofList la xa * ofList lb xb - superCommuteCoef q la lb • ofList lb xb * ofList la xa := by
rw [superCommute_ofList_ofList, superCommuteCoef]
by_cases hq : grade q la = 1 ∧ grade q lb = 1
· simp [hq, ofList_pair]
· simp only [ofList_pair, Fin.isValue, hq, ↓reduceIte, one_smul]
abel
lemma ofList_ofList_superCommute {I : Type} (q : I → Fin 2) (la lb : List I) (xa xb : ) :
ofList la xa * ofList lb xb = superCommuteCoef q la lb • ofList lb xb * ofList la xa
+ superCommute q (ofList la xa) (ofList lb xb) := by
rw [superCommute_ofList_ofList_superCommuteCoef]
abel
lemma ofListLift_ofList_superCommute' {I : Type}
(q : I → Fin 2) (l : List I) (r : List I) (x y : ) :
ofList r y * ofList l x = superCommuteCoef q l r • (ofList l x * ofList r y)
- superCommuteCoef q l r • superCommute q (ofList l x) (ofList r y) := by
nth_rewrite 2 [ofList_ofList_superCommute q]
rw [superCommuteCoef]
by_cases hq : grade q l = 1 ∧ grade q r = 1
· simp [hq, superCommuteCoef]
· simp [hq]
lemma superCommute_ofList_ofListLift {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
(q : I → Fin 2) (l : List (Σ i, f i)) (r : List I) (x y : ) :
superCommute (fun i => q i.1) (ofList l x) (ofListLift f r y) =
ofList l x * ofListLift f r y +
(if grade (fun i => q i.1) l = 1 ∧ grade q r = 1 then
ofListLift f r y * ofList l x else - ofListLift f r y * ofList l x) := by
conv_lhs => rw [ofListLift_expand]
rw [map_sum]
conv_rhs =>
lhs
rw [ofListLift_expand, Finset.mul_sum]
conv_rhs =>
rhs
rhs
rw [ofListLift_expand, ← Finset.sum_neg_distrib, Finset.sum_mul]
conv_rhs =>
rhs
lhs
rw [ofListLift_expand, Finset.sum_mul]
rw [← Finset.sum_ite_irrel]
rw [← Finset.sum_add_distrib]
congr
funext a
rw [superCommute_ofList_ofList]
congr 1
· exact ofList_pair l a.toList x y
congr 1
· simp
· exact ofList_pair a.toList l y x
· rw [ofList_pair]
simp only [neg_mul]
lemma superCommute_ofList_ofListLift_superCommuteLiftCoef {I : Type} {f : I → Type}
[∀ i, Fintype (f i)]
(q : I → Fin 2) (l : List (Σ i, f i)) (r : List I) (x y : ) :
superCommute (fun i => q i.1) (ofList l x) (ofListLift f r y) =
ofList l x * ofListLift f r y - superCommuteLiftCoef q l r • ofListLift f r y * ofList l x := by
rw [superCommute_ofList_ofListLift, superCommuteLiftCoef]
by_cases hq : grade (fun i => q i.fst) l = 1 ∧ grade q r = 1
· simp [hq]
· simp only [Fin.isValue, hq, ↓reduceIte, neg_mul, one_smul]
abel
lemma ofList_ofListLift_superCommute {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
(q : I → Fin 2) (l : List (Σ i, f i)) (r : List I) (x y : ) :
ofList l x * ofListLift f r y = superCommuteLiftCoef q l r • ofListLift f r y * ofList l x
+ superCommute (fun i => q i.1) (ofList l x) (ofListLift f r y) := by
rw [superCommute_ofList_ofListLift_superCommuteLiftCoef]
abel
lemma ofListLift_ofList_superCommute {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
(q : I → Fin 2) (l : List (Σ i, f i)) (r : List I) (x y : ) :
ofListLift f r y * ofList l x = superCommuteLiftCoef q l r • (ofList l x * ofListLift f r y)
- superCommuteLiftCoef q l r •
superCommute (fun i => q i.1) (ofList l x) (ofListLift f r y) := by
rw [ofList_ofListLift_superCommute, superCommuteLiftCoef]
by_cases hq : grade (fun i => q i.fst) l = 1 ∧ grade q r = 1
· simp [hq]
· simp [hq]
lemma superCommuteLiftCoef_append {I : Type} {f : I → Type}
(q : I → Fin 2) (l : List (Σ i, f i)) (r1 r2 : List I) :
superCommuteLiftCoef q l (r1 ++ r2) =
superCommuteLiftCoef q l r1 * superCommuteLiftCoef q l r2 := by
simp only [superCommuteLiftCoef, Fin.isValue, grade_append, ite_eq_right_iff, zero_ne_one,
imp_false, mul_ite, mul_neg, mul_one]
by_cases hla : grade (fun i => q i.1) l = 1
· by_cases hlb : grade q r1 = 1
· by_cases hlc : grade q r2 = 1
· simp [hlc, hlb, hla]
· have hc : grade q r2 = 0 := by
omega
simp [hc, hlb, hla]
· have hb : grade q r1 = 0 := by
omega
by_cases hlc : grade q r2 = 1
· simp [hlc, hb]
· have hc : grade q r2 = 0 := by
omega
simp [hc, hb]
· have ha : grade (fun i => q i.1) l = 0 := by
omega
simp [ha]
/-- Given two lists `l : List (Σ i, f i)` and `r : List I`, on
in the expansion of the supercommutor of `l` and the lift of `r`
via elements of `r`the term associated with the `n`th element.
E.g. in the commutator
`[a, bc] = [a, b] c + b [a, c] ` the `superCommuteSplit` for `n=0` is `[a, b] c`
and for `n=1` is `b [a, c]`. -/
def superCommuteLiftSplit {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
(q : I → Fin 2) (l : List (Σ i, f i)) (r : List I) (x y : ) (n : )
(hn : n < r.length) : FreeAlgebra (Σ i, f i) :=
superCommuteLiftCoef q l (List.take n r) •
(ofListLift f (List.take n r) 1 *
superCommute (fun i => q i.1) (ofList l x) (sumFiber f (FreeAlgebra.ι (r.get ⟨n, hn⟩)))
* ofListLift f (List.drop (n + 1) r) y)
lemma superCommute_ofList_ofListLift_cons {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
(q : I → Fin 2) (l : List (Σ i, f i)) (r : List I) (x y : ) (b1 : I) :
superCommute (fun i => q i.1) (ofList l x) (ofListLift f (b1 :: r) y) =
superCommute (fun i => q i.1) (ofList l x) (sumFiber f (FreeAlgebra.ι b1))
* ofListLift f r y + superCommuteLiftCoef q l [b1] •
(ofListLift f [b1] 1) * superCommute (fun i => q i.1) (ofList l x) (ofListLift f r y) := by
rw [ofListLift_cons]
conv_lhs =>
rhs
rw [ofListLift_expand]
rw [Finset.mul_sum]
rw [map_sum]
trans ∑ (n : CreateAnnilateSect f r), ∑ j : f b1, ((superCommute fun i => q i.fst) (ofList l x))
((FreeAlgebra.ι ⟨b1, j⟩) * ofList n.toList y)
· apply congrArg
funext n
rw [← map_sum]
congr
rw [Finset.sum_mul]
conv_rhs =>
lhs
rw [ofListLift_expand, Finset.mul_sum]
conv_rhs =>
rhs
rhs
rw [ofListLift_expand]
rw [map_sum]
conv_rhs =>
rhs
rw [Finset.mul_sum]
rw [← Finset.sum_add_distrib]
congr
funext n
rw [sumFiber_ι, map_sum, Finset.sum_mul]
conv_rhs =>
rhs
rw [ofListLift_singleton]
rw [Finset.smul_sum, Finset.sum_mul]
rw [← Finset.sum_add_distrib]
congr
funext b
trans ((superCommute fun i => q i.fst) (ofList l x)) (ofList (⟨b1, b⟩ :: n.toList) y)
· congr
rw [ofList_cons_eq_ofList]
rw [ofList_singleton]
rw [superCommute_ofList_cons]
congr
rw [ofList_singleton]
simp
lemma superCommute_ofList_ofListLift_sum {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
(q : I → Fin 2) (l : List (Σ i, f i)) (r : List I) (x y : ) :
superCommute (fun i => q i.1) (ofList l x) (ofListLift f r y) =
∑ (n : Fin r.length), superCommuteLiftSplit q l r x y n n.prop := by
induction r with
| nil =>
simp only [superCommute_ofList_ofListLift, Fin.isValue, grade_empty, zero_ne_one, and_false,
↓reduceIte, neg_mul, List.length_nil, Finset.univ_eq_empty, Finset.sum_empty]
rw [ofListLift, ofList_empty']
simp
| cons b r ih =>
rw [superCommute_ofList_ofListLift_cons]
have h0 : ((superCommute fun i => q i.fst) (ofList l x))
((sumFiber f) (FreeAlgebra.ι b)) * ofListLift f r y =
superCommuteLiftSplit q l (b :: r) x y 0 (Nat.zero_lt_succ r.length) := by
simp [superCommuteLiftSplit, superCommuteLiftCoef_empty, ofListLift_empty]
rw [h0]
have hf (g : Fin (b :: r).length → FreeAlgebra ((i : I) × f i)) : ∑ n, g n = g ⟨0,
Nat.zero_lt_succ r.length⟩ + ∑ n, g (Fin.succ n) := by
exact Fin.sum_univ_succAbove g ⟨0, Nat.zero_lt_succ r.length⟩
rw [hf]
congr
rw [ih]
rw [Finset.mul_sum]
congr
funext n
simp only [superCommuteLiftSplit, Fin.eta, List.get_eq_getElem, Algebra.mul_smul_comm,
Algebra.smul_mul_assoc, smul_smul, List.length_cons, Fin.val_succ, List.take_succ_cons,
List.getElem_cons_succ, List.drop_succ_cons]
congr 1
· rw [mul_comm, ← superCommuteLiftCoef_append]
rfl
· simp only [← mul_assoc, mul_eq_mul_right_iff]
apply Or.inl
apply Or.inl
rw [ofListLift, ofListLift, ofListLift]
rw [← map_mul]
congr
rw [← ofList_pair, one_mul]
rfl
end
end Wick

View file

@ -1,34 +0,0 @@
/-
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 HepLean.PerturbationTheory.Wick.Species
/-!
# Wick's theorem
Wick's theorem is related to a result in probability theory called Isserlis' theorem.
-/
namespace Wick
note r"
<h2>Wick's theorem</h2>
"
informal_lemma_note wicks_theorem where
math :≈ "Wick's theorem for fields which are not normally ordered."
informal_lemma wicks_theorem_normal_order where
math :≈ "Wick's theorem for which fields at the same space-time point are normally ordered."
ref :≈ "https://www.physics.purdue.edu/~clarkt/Courses/Physics662/ps/qftch32.pdf"
informal_lemma wicks_theorem_vev where
math :≈ "Wick's theorem in a vev leaving only full contractions of Wick strings left."
informal_lemma wicks_theorem_asymptotic_states where
math :≈ "Wick's theorem for a term in the Dyson series within asymptotic states
leaves only full contractions with the asymptotic states."
end Wick