DibyashanuPati/PhysLean
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor: building version

Browse source
This commit is contained in:
jstoobysmith 2024-12-20 13:33:39 +00:00
parent a3113a791c
commit a5e0f3ceac
5 changed files with 53 additions and 42 deletions
Download patch file Download diff file Expand all files Collapse all files

7
HepLean/PerturbationTheory/Wick/Contraction.lean
View file

@ -15,6 +15,7 @@ namespace Wick
noncomputable section
open HepLean.List
open FieldStatistic
/-- Given a list of fields `l`, the type of pairwise-contractions associated with `l`
which have the list `aux` uncontracted. -/
@ -125,7 +126,7 @@ structure Splitting {I : Type} (f : I → Type) [∀ i, Fintype (f 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)
(q : I → FieldStatistic)
(le1 : (Σ i, f i) → (Σ i, f i) → Prop) [DecidableRel le1]
{A : Type} [Semiring A] [Algebra ℂ A]
(F : FreeAlgebra ℂ (Σ i, f i) →ₐ[ℂ] A) :
@ -137,7 +138,7 @@ def toCenterTerm {I : Type} (f : I → Type) [∀ i, Fintype (f i)]
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}
(q : I → FieldStatistic) {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)
@ -150,7 +151,7 @@ lemma toCenterTerm_none {I : Type} (f : I → Type) [∀ i, Fintype (f i)]
rfl
lemma toCenterTerm_center {I : Type} (f : I → Type) [∀ i, Fintype (f i)]
(q : I → Fin 2)
(q : I → FieldStatistic)
(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] :

57
HepLean/PerturbationTheory/Wick/OperatorMap.lean
View file

@ -6,16 +6,16 @@ Authors: Joseph Tooby-Smith
import HepLean.PerturbationTheory.Wick.SuperCommute
/-!
# Koszul signs and ordering for lists and algebras
# Operator map
See e.g.
- https://pcteserver.mi.infn.it/~molinari/NOTES/WICK23.pdf
-/
namespace Wick
noncomputable section
open FieldStatistic
/-- 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`,
@ -24,18 +24,19 @@ noncomputable section
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)
class OperatorMap {A : Type} [Semiring A] [Algebra ℂ A] (q : I → FieldStatistic) (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
F (koszulOrder q le1 (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}
variable {I: Type} {A : Type} [Semiring A] [Algebra ℂ A]
{q : I → FieldStatistic} {le1 : I → I → Prop}
[DecidableRel le1] (F : FreeAlgebra ℂ I →ₐ[ℂ] A)
lemma superCommute_ofList_singleton_ι_center [OperatorMap q le1 F] (i j :I) :
@ -53,7 +54,7 @@ lemma superCommute_ofList_singleton_ι_center [OperatorMap q le1 F] (i j :I) :
end OperatorMap
lemma superCommuteSplit_operatorMap {I : Type} (q : I → Fin 2)
lemma superCommuteSplit_operatorMap {I : Type} (q : I → FieldStatistic)
(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)
@ -73,7 +74,7 @@ lemma superCommuteSplit_operatorMap {I : Type} (q : I → Fin 2)
· 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 : ℕ)
(q : I → FieldStatistic) (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)
@ -103,15 +104,15 @@ lemma superCommuteLiftSplit_operatorMap {I : Type} {f : I → Type} [∀ i, Fint
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 : ℂ)
(q : I → FieldStatistic) (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)))) =
F ((superCommute q (FreeAlgebra.ι ℂ i) (koszulOrder q le1 (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
F ((koszulOrder q le1) (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 =>
@ -125,7 +126,7 @@ lemma superCommute_koszulOrder_le_ofList {I : Type}
enter [2, 2]
intro n
rw [HepLean.List.eraseIdx_insertionSort_fin le1 r n]
rw [ofList_insertionSort_eq_koszulOrder le1 q]
rw [ofList_insertionSort_eq_koszulOrder q le1]
rw [Finset.smul_sum]
conv_lhs =>
rhs
@ -149,12 +150,12 @@ lemma superCommute_koszulOrder_le_ofList {I : Type}
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]
(q : I → FieldStatistic) (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
F (koszulOrder q le1 (ofList r x * FreeAlgebra.ι ℂ i))
= superCommuteCoef q [i] r • F (koszulOrder q le1 (FreeAlgebra.ι ℂ i * ofList r x)) := by
conv_lhs =>
enter [2, 2]
rw [← ofList_singleton]
@ -183,13 +184,13 @@ lemma koszulOrder_of_le_all_ofList {I : Type}
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]
(q : I → FieldStatistic) (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
F (FreeAlgebra.ι ℂ i * koszulOrder q le1 (ofList r x)) =
F ((koszulOrder q le1) (FreeAlgebra.ι ℂ i * ofList r x)) +
F (((superCommute q) (ofList [i] 1)) ((koszulOrder q le1) (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 =>
@ -210,7 +211,7 @@ lemma le_all_mul_koszulOrder_ofList {I : Type}
/-- 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)
(q : I → FieldStatistic) (r : List I) (i : I)
{A : Type} [Semiring A] [Algebra ℂ A]
(F : FreeAlgebra ℂ I →ₐ[ℂ] A)
(n : Option (Fin r.length)) : A :=
@ -221,7 +222,7 @@ def superCommuteCenterOrder {I : Type}
@[simp]
lemma superCommuteCenterOrder_none {I : Type}
(q : I → Fin 2) (r : List I) (i : I)
(q : I → FieldStatistic) (r : List I) (i : I)
{A : Type} [Semiring A] [Algebra ℂ A]
(F : FreeAlgebra ℂ I →ₐ[ℂ] A) :
superCommuteCenterOrder q r i F none = 1 := by
@ -230,14 +231,14 @@ lemma superCommuteCenterOrder_none {I : Type}
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]
(q : I → FieldStatistic) (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)) =
F (FreeAlgebra.ι ℂ i * koszulOrder q le1 (ofList r x)) =
∑ n, superCommuteCenterOrder q r i F n *
F ((koszulOrder le1 q) (ofList (optionEraseZ r i n) x)) := by
F ((koszulOrder q le1) (ofList (optionEraseZ r i n) x)) := by
rw [le_all_mul_koszulOrder_ofList]
conv_lhs =>
rhs
@ -254,16 +255,16 @@ lemma le_all_mul_koszulOrder_ofList_expand {I : Type}
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]
(q : I → FieldStatistic) (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)) +
F (ofList [i] 1 * koszulOrder (fun i => q i.1) le1 (ofListLift f r x)) =
F ((koszulOrder (fun i => q i.fst) le1) (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
F ((koszulOrder (fun i => q i.fst) le1) (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,

6
HepLean/PerturbationTheory/Wick/Signs/KoszulSignInsert.lean
View file

@ -74,10 +74,8 @@ lemma koszulSignInsert_ge_forall_append (l : List 𝓕) (j i : 𝓕) (hi : ∀ j
| cons b l ih =>
simp only [koszulSignInsert, Fin.isValue, List.append_eq]
by_cases hr : le j b
· rw [if_pos hr, if_pos hr]
rw [ih]
· rw [if_neg hr, if_neg hr]
rw [ih]
· rw [if_pos hr, if_pos hr, ih]
· rw [if_neg hr, if_neg hr, ih]
lemma koszulSignInsert_eq_filter (r0 : 𝓕) : (r : List 𝓕) →
koszulSignInsert q le r0 r =

15
HepLean/PerturbationTheory/Wick/StaticTheorem.lean
View file

@ -15,16 +15,17 @@ namespace Wick
noncomputable section
open HepLean.List
open FieldStatistic
lemma static_wick_nil {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
(q : I → Fin 2)
(q : I → FieldStatistic)
(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
F (koszulOrder (fun i => q i.fst) le1 (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]
@ -32,18 +33,18 @@ lemma static_wick_nil {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
simp [ofListLift_empty]
lemma static_wick_cons {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
(q : I → Fin 2)
(q : I → FieldStatistic)
(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)
∑ c : Contractions r, c.toCenterTerm f q le1 F S * F (koszulOrder (fun i => q i.fst) le1
(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
F (koszulOrder (fun i => q i.fst) le1 (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]
@ -86,14 +87,14 @@ lemma static_wick_cons {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
exact S.h𝓑n a
theorem static_wick_theorem {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
(q : I → Fin 2)
(q : I → FieldStatistic)
(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
F (koszulOrder (fun i => q i.fst) le1 (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

10
HepLean/PerturbationTheory/Wick/SuperCommute.lean
View file

@ -276,6 +276,16 @@ lemma ofList_ofList_superCommute (la lb : List 𝓕) (xa xb : ℂ) :
rw [superCommute_ofList_ofList_superCommuteCoef]
abel
lemma ofListLift_ofList_superCommute' (l : List 𝓕) (r : List 𝓕) (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 : FieldStatistic.ofList q l = fermionic ∧ FieldStatistic.ofList q r = fermionic
· simp [hq, superCommuteCoef]
· simp [hq]
section lift
variable {𝓕 : Type} {f : 𝓕 → Type} [∀ i, Fintype (f i)] (q : 𝓕 → FieldStatistic)