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

refactor: Notation for insertAndContract

Browse source
This commit is contained in:
jstoobysmith 2025-01-24 09:03:42 +00:00
parent fa7536bea9
commit eeacdef74e
6 changed files with 69 additions and 65 deletions
Download patch file Download diff file Expand all files Collapse all files

11
HepLean/PerturbationTheory/Algebras/ProtoOperatorAlgebra/Basic.lean
View file

@ -14,10 +14,13 @@ namespace FieldSpecification
variable (𝓕 : FieldSpecification)
open CrAnAlgebra
/-- The structure of an algebra with properties necessary for that algebra
to be isomorphic to the actual operator algebra of a field theory.
These properties are sufficent to prove certain theorems about the Operator algebra
in particular Wick's theorem. -/
/--
A proto-operator algebra for a field specification `𝓕`
is a generalization of the operator algebra of a field theory with field specification `𝓕`.
It is an algebra `A` with a map `crAnF` from the creation and annihilation free algebra
satisfying a number of conditions with respect to super commutators.
The true operator algebra of a field theory with field specification `𝓕`is an
example of a proto-operator algebra.-/
structure ProtoOperatorAlgebra where
/-- The algebra representing the operator algebra. -/
A : Type

44
HepLean/PerturbationTheory/WickContraction/InsertAndContract.lean
View file

@ -29,15 +29,17 @@ open HepLean.Fin
`j : Option (c.uncontracted)` of `c`.
The Wick contraction associated with `(φs.insertIdx i φ).length` formed by 'inserting' `φ`
into `φs` after the first `i` elements and contracting it optionally with j. -/
def insertAndContract (φ : 𝓕.States) {φs : List 𝓕.States} (φsΛ : WickContraction φs.length)
def insertAndContract {φs : List 𝓕.States} (φ : 𝓕.States) (φsΛ : WickContraction φs.length)
(i : Fin φs.length.succ) (j : Option φsΛ.uncontracted) :
WickContraction (φs.insertIdx i φ).length :=
congr (by simp) (φsΛ.insertAndContractNat i j)
scoped[WickContraction] notation φs "↩Λ" φ:max i:max j => insertAndContract φ φs i j
@[simp]
lemma insertAndContract_fstFieldOfContract (φ : 𝓕.States) (φs : List 𝓕.States)
(φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (j : Option φsΛ.uncontracted)
(a : φsΛ.1) : (φsΛ.insertAndContract φ i j).fstFieldOfContract
(a : φsΛ.1) : (φsΛ ↩Λ φ i j).fstFieldOfContract
(congrLift (insertIdx_length_fin φ φs i).symm (insertLift i j a)) =
finCongr (insertIdx_length_fin φ φs i).symm (i.succAbove (φsΛ.fstFieldOfContract a)) := by
simp [insertAndContract]
@ -45,7 +47,7 @@ lemma insertAndContract_fstFieldOfContract (φ : 𝓕.States) (φs : List 𝓕.S
@[simp]
lemma insertAndContract_sndFieldOfContract (φ : 𝓕.States) (φs : List 𝓕.States)
(φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (j : Option (φsΛ.uncontracted))
(a : φsΛ.1) : (φsΛ.insertAndContract φ i j).sndFieldOfContract
(a : φsΛ.1) : (φsΛ ↩Λ φ i j).sndFieldOfContract
(congrLift (insertIdx_length_fin φ φs i).symm (insertLift i j a)) =
finCongr (insertIdx_length_fin φ φs i).symm (i.succAbove (φsΛ.sndFieldOfContract a)) := by
simp [insertAndContract]
@ -88,7 +90,7 @@ lemma insertAndContract_fstFieldOfContract_some_incl (φ : 𝓕.States) (φs : L
@[simp]
lemma insertAndContract_none_getDual?_self (φ : 𝓕.States) (φs : List 𝓕.States)
(φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) :
(insertAndContract φ φsΛ i none).getDual? (Fin.cast (insertIdx_length_fin φ φs i).symm i) = none := by
(φsΛ ↩Λ φ i none).getDual? (Fin.cast (insertIdx_length_fin φ φs i).symm i) = none := by
simp only [Nat.succ_eq_add_one, insertAndContract, getDual?_congr, finCongr_apply, Fin.cast_trans,
Fin.cast_eq_self, Option.map_eq_none']
have h1 := φsΛ.insertAndContractNat_none_getDual?_isNone i
@ -96,27 +98,27 @@ lemma insertAndContract_none_getDual?_self (φ : 𝓕.States) (φs : List 𝓕.S
lemma insertAndContract_isSome_getDual?_self (φ : 𝓕.States) (φs : List 𝓕.States)
(φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (j : φsΛ.uncontracted) :
((insertAndContract φ φsΛ i (some j)).getDual?
((φsΛ ↩Λ φ i (some j)).getDual?
(Fin.cast (insertIdx_length_fin φ φs i).symm i)).isSome := by
simp [insertAndContract, getDual?_congr]
lemma insertAndContract_some_getDual?_self_not_none (φ : 𝓕.States) (φs : List 𝓕.States)
(φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (j : φsΛ.uncontracted) :
¬ ((insertAndContract φ φsΛ i (some j)).getDual?
¬ ((φsΛ ↩Λ φ i (some j)).getDual?
(Fin.cast (insertIdx_length_fin φ φs i).symm i)) = none := by
simp [insertAndContract, getDual?_congr]
@[simp]
lemma insertAndContract_some_getDual?_self_eq (φ : 𝓕.States) (φs : List 𝓕.States)
(φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (j : φsΛ.uncontracted) :
((insertAndContract φ φsΛ i (some j)).getDual? (Fin.cast (insertIdx_length_fin φ φs i).symm i))
((φsΛ ↩Λ φ i (some j)).getDual? (Fin.cast (insertIdx_length_fin φ φs i).symm i))
= some (Fin.cast (insertIdx_length_fin φ φs i).symm (i.succAbove j)) := by
simp [insertAndContract, getDual?_congr]
@[simp]
lemma insertAndContract_some_getDual?_some_eq (φ : 𝓕.States) (φs : List 𝓕.States)
(φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (j : φsΛ.uncontracted) :
((insertAndContract φ φsΛ i (some j)).getDual?
((φsΛ ↩Λ φ i (some j)).getDual?
(Fin.cast (insertIdx_length_fin φ φs i).symm (i.succAbove j)))
= some (Fin.cast (insertIdx_length_fin φ φs i).symm i) := by
rw [getDual?_eq_some_iff_mem]
@ -127,7 +129,7 @@ lemma insertAndContract_some_getDual?_some_eq (φ : 𝓕.States) (φs : List
@[simp]
lemma insertAndContract_none_succAbove_getDual?_eq_none_iff (φ : 𝓕.States) (φs : List 𝓕.States)
(φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (j : Fin φs.length) :
(insertAndContract φ φsΛ i none).getDual? (Fin.cast (insertIdx_length_fin φ φs i).symm
(φsΛ ↩Λ φ i none).getDual? (Fin.cast (insertIdx_length_fin φ φs i).symm
(i.succAbove j)) = none ↔ φsΛ.getDual? j = none := by
simp [insertAndContract, getDual?_congr]
@ -135,7 +137,7 @@ lemma insertAndContract_none_succAbove_getDual?_eq_none_iff (φ : 𝓕.States) (
lemma insertAndContract_some_succAbove_getDual?_eq_option (φ : 𝓕.States) (φs : List 𝓕.States)
(φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (j : Fin φs.length)
(k : φsΛ.uncontracted) (hkj : j ≠ k.1) :
(insertAndContract φ φsΛ i (some k)).getDual? (Fin.cast (insertIdx_length_fin φ φs i).symm
(φsΛ ↩Λ φ i (some k)).getDual? (Fin.cast (insertIdx_length_fin φ φs i).symm
(i.succAbove j)) = Option.map (Fin.cast (insertIdx_length_fin φ φs i).symm ∘ i.succAbove)
(φsΛ.getDual? j) := by
simp only [Nat.succ_eq_add_one, insertAndContract, getDual?_congr, finCongr_apply, Fin.cast_trans,
@ -145,7 +147,7 @@ lemma insertAndContract_some_succAbove_getDual?_eq_option (φ : 𝓕.States) (φ
@[simp]
lemma insertAndContract_none_succAbove_getDual?_isSome_iff (φ : 𝓕.States) (φs : List 𝓕.States)
(φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (j : Fin φs.length) :
((insertAndContract φ φsΛ i none).getDual? (Fin.cast (insertIdx_length_fin φ φs i).symm
((φsΛ ↩Λ φ i none).getDual? (Fin.cast (insertIdx_length_fin φ φs i).symm
(i.succAbove j))).isSome ↔ (φsΛ.getDual? j).isSome := by
rw [← not_iff_not]
simp
@ -153,9 +155,9 @@ lemma insertAndContract_none_succAbove_getDual?_isSome_iff (φ : 𝓕.States) (
@[simp]
lemma insertAndContract_none_getDual?_get_eq (φ : 𝓕.States) (φs : List 𝓕.States)
(φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (j : Fin φs.length)
(h : ((insertAndContract φ φsΛ i none).getDual? (Fin.cast (insertIdx_length_fin φ φs i).symm
(h : ((φsΛ ↩Λ φ i none).getDual? (Fin.cast (insertIdx_length_fin φ φs i).symm
(i.succAbove j))).isSome) :
((insertAndContract φ φsΛ i none).getDual? (Fin.cast (insertIdx_length_fin φ φs i).symm
((φsΛ ↩Λ φ i none).getDual? (Fin.cast (insertIdx_length_fin φ φs i).symm
(i.succAbove j))).get h = Fin.cast (insertIdx_length_fin φ φs i).symm
(i.succAbove ((φsΛ.getDual? j).get (by simpa using h))) := by
simp [insertAndContract, getDual?_congr_get]
@ -164,14 +166,14 @@ lemma insertAndContract_none_getDual?_get_eq (φ : 𝓕.States) (φs : List 𝓕
@[simp]
lemma insertAndContract_sndFieldOfContract_some_incl (φ : 𝓕.States) (φs : List 𝓕.States)
(φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (j : φsΛ.uncontracted) :
(insertAndContract φ φsΛ i (some j)).sndFieldOfContract
(φsΛ ↩Λ φ i (some j)).sndFieldOfContract
(congrLift (insertIdx_length_fin φ φs i).symm ⟨{i, i.succAbove j}, by simp [insertAndContractNat]⟩) =
if i < i.succAbove j.1 then
finCongr (insertIdx_length_fin φ φs i).symm (i.succAbove j.1) else
finCongr (insertIdx_length_fin φ φs i).symm i := by
split
· rename_i h
refine (insertAndContract φ φsΛ i (some j)).eq_sndFieldOfContract_of_mem
refine (φsΛ ↩Λ φ i (some j)).eq_sndFieldOfContract_of_mem
(a := congrLift (insertIdx_length_fin φ φs i).symm ⟨{i, i.succAbove j}, by simp [insertAndContractNat]⟩)
(i := finCongr (insertIdx_length_fin φ φs i).symm i) (j :=
finCongr (insertIdx_length_fin φ φs i).symm (i.succAbove j)) ?_ ?_ ?_
@ -180,7 +182,7 @@ lemma insertAndContract_sndFieldOfContract_some_incl (φ : 𝓕.States) (φs : L
· rw [Fin.lt_def] at h ⊢
simp_all
· rename_i h
refine (insertAndContract φ φsΛ i (some j)).eq_sndFieldOfContract_of_mem
refine (φsΛ ↩Λ φ i (some j)).eq_sndFieldOfContract_of_mem
(a := congrLift (insertIdx_length_fin φ φs i).symm ⟨{i, i.succAbove j}, by simp [insertAndContractNat]⟩)
(i := finCongr (insertIdx_length_fin φ φs i).symm (i.succAbove j))
(j := finCongr (insertIdx_length_fin φ φs i).symm i) ?_ ?_ ?_
@ -193,7 +195,7 @@ lemma insertAndContract_sndFieldOfContract_some_incl (φ : 𝓕.States) (φs : L
lemma insertAndContract_none_prod_contractions (φ : 𝓕.States) (φs : List 𝓕.States)
(φsΛ : WickContraction φs.length) (i : Fin φs.length.succ)
(f : (φsΛ.insertAndContract φ i none).1 → M) [CommMonoid M] :
(f : (φsΛ ↩Λ φ i none).1 → M) [CommMonoid M] :
∏ a, f a = ∏ (a : φsΛ.1), f (congrLift (insertIdx_length_fin φ φs i).symm
(insertLift i none a)) := by
let e1 := Equiv.ofBijective (φsΛ.insertLift i none) (insertLift_none_bijective i)
@ -205,7 +207,7 @@ lemma insertAndContract_none_prod_contractions (φ : 𝓕.States) (φs : List
lemma insertAndContract_some_prod_contractions (φ : 𝓕.States) (φs : List 𝓕.States)
(φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (j : φsΛ.uncontracted)
(f : (φsΛ.insertAndContract φ i (some j)).1 → M) [CommMonoid M] :
(f : (φsΛ ↩Λ φ i (some j)).1 → M) [CommMonoid M] :
∏ a, f a = f (congrLift (insertIdx_length_fin φ φs i).symm
⟨{i, i.succAbove j}, by simp [insertAndContractNat]⟩) *
∏ (a : φsΛ.1), f (congrLift (insertIdx_length_fin φ φs i).symm (insertLift i (some j) a)) := by
@ -268,7 +270,7 @@ lemma insert_fin_eq_self (φ : 𝓕.States) {φs : List 𝓕.States}
lemma insertAndContract_uncontractedList_none_map (φ : 𝓕.States) {φs : List 𝓕.States}
(φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) :
[φsΛ.insertAndContract φ i none]ᵘᶜ = List.insertIdx (φsΛ.uncontractedListOrderPos i) φ [φsΛ]ᵘᶜ := by
[φsΛ ↩Λ φ i none]ᵘᶜ = List.insertIdx (φsΛ.uncontractedListOrderPos i) φ [φsΛ]ᵘᶜ := by
simp only [Nat.succ_eq_add_one, insertAndContract, uncontractedListGet]
rw [congr_uncontractedList]
erw [uncontractedList_extractEquiv_symm_none]
@ -283,8 +285,8 @@ lemma insertAndContract_uncontractedList_none_map (φ : 𝓕.States) {φs : List
lemma insertLift_sum (φ : 𝓕.States) {φs : List 𝓕.States}
(i : Fin φs.length.succ) [AddCommMonoid M] (f : WickContraction (φs.insertIdx i φ).length → M) :
∑ c, f c = ∑ (φsΛ : WickContraction φs.length), ∑ (k : Option φsΛ.uncontracted),
f (φsΛ.insertAndContract φ i k) := by
∑ c, f c =
∑ (φsΛ : WickContraction φs.length), ∑ (k : Option φsΛ.uncontracted), f (φsΛ ↩Λ φ i k) := by
rw [sum_extractEquiv_congr (finCongr (insertIdx_length_fin φ φs i).symm i) f
(insertIdx_length_fin φ φs i)]
rfl

25
HepLean/PerturbationTheory/WickContraction/Sign.lean
View file

@ -30,7 +30,7 @@ def signFinset (c : WickContraction n) (i1 i2 : Fin n) : Finset (Fin n) :=
lemma signFinset_insertAndContract_none (φ : 𝓕.States) (φs : List 𝓕.States)
(φsΛ : WickContraction φs.length)
(i : Fin φs.length.succ) (i1 i2 : Fin φs.length) :
(φsΛ.insertAndContract φ i none).signFinset (finCongr (insertIdx_length_fin φ φs i).symm
(φsΛ ↩Λ φ i none).signFinset (finCongr (insertIdx_length_fin φ φs i).symm
(i.succAbove i1)) (finCongr (insertIdx_length_fin φ φs i).symm (i.succAbove i2)) =
if i.succAbove i1 < i ∧ i < i.succAbove i2 then
Insert.insert (finCongr (insertIdx_length_fin φ φs i).symm i)
@ -180,7 +180,7 @@ lemma stat_ofFinset_eq_one_of_gradingCompliant (φs : List 𝓕.States)
lemma signFinset_insertAndContract_some (φ : 𝓕.States) (φs : List 𝓕.States)
(φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (i1 i2 : Fin φs.length)
(j : φsΛ.uncontracted) :
(φsΛ.insertAndContract φ i (some j)).signFinset (finCongr (insertIdx_length_fin φ φs i).symm
(φsΛ ↩Λ φ i (some j)).signFinset (finCongr (insertIdx_length_fin φ φs i).symm
(i.succAbove i1)) (finCongr (insertIdx_length_fin φ φs i).symm (i.succAbove i2)) =
if i.succAbove i1 < i ∧ i < i.succAbove i2 ∧ (i1 < j) then
Insert.insert (finCongr (insertIdx_length_fin φ φs i).symm i)
@ -341,7 +341,7 @@ def signInsertNone (φ : 𝓕.States) (φs : List 𝓕.States) (φsΛ : WickCont
lemma sign_insert_none (φ : 𝓕.States) (φs : List 𝓕.States) (φsΛ : WickContraction φs.length)
(i : Fin φs.length.succ) :
(φsΛ.insertAndContract φ i none).sign = (φsΛ.signInsertNone φ φs i) * φsΛ.sign := by
(φsΛ ↩Λ φ i none).sign = (φsΛ.signInsertNone φ φs i) * φsΛ.sign := by
rw [sign]
rw [signInsertNone, sign, ← Finset.prod_mul_distrib]
rw [insertAndContract_none_prod_contractions]
@ -508,13 +508,12 @@ def signInsertSomeProd (φ : 𝓕.States) (φs : List 𝓕.States) (φsΛ : Wick
coming from putting `i` next to `j`. -/
def signInsertSomeCoef (φ : 𝓕.States) (φs : List 𝓕.States) (φsΛ : WickContraction φs.length)
(i : Fin φs.length.succ) (j : φsΛ.uncontracted) : ℂ :=
let a : (φsΛ.insertAndContract φ i (some j)).1 :=
congrLift (insertIdx_length_fin φ φs i).symm
let a : (φsΛ ↩Λ φ i (some j)).1 := congrLift (insertIdx_length_fin φ φs i).symm
⟨{i, i.succAbove j}, by simp [insertAndContractNat]⟩;
𝓢(𝓕 |>ₛ (φs.insertIdx i φ)[(φsΛ.insertAndContract φ i (some j)).sndFieldOfContract a],
𝓢(𝓕 |>ₛ (φs.insertIdx i φ)[(φsΛ ↩Λ φ i (some j)).sndFieldOfContract a],
𝓕 |>ₛ ⟨(φs.insertIdx i φ).get, signFinset
(φsΛ.insertAndContract φ i (some j)) ((φsΛ.insertAndContract φ i (some j)).fstFieldOfContract a)
((φsΛ.insertAndContract φ i (some j)).sndFieldOfContract a)⟩)
(φsΛ ↩Λ φ i (some j)) ((φsΛ ↩Λ φ i (some j)).fstFieldOfContract a)
((φsΛ ↩Λ φ i (some j)).sndFieldOfContract a)⟩)
/-- Given a Wick contraction `c` associated with a list of states `φs`
and an `i : Fin φs.length.succ`, the change in sign of the contraction associated with
@ -525,7 +524,7 @@ def signInsertSome (φ : 𝓕.States) (φs : List 𝓕.States) (φsΛ : WickCont
lemma sign_insert_some (φ : 𝓕.States) (φs : List 𝓕.States) (φsΛ : WickContraction φs.length)
(i : Fin φs.length.succ) (j : φsΛ.uncontracted) :
(φsΛ.insertAndContract φ i (some j)).sign = (φsΛ.signInsertSome φ φs i j) * φsΛ.sign := by
(φsΛ ↩Λ φ i (some j)).sign = (φsΛ.signInsertSome φ φs i j) * φsΛ.sign := by
rw [sign]
rw [signInsertSome, signInsertSomeProd, sign, mul_assoc, ← Finset.prod_mul_distrib]
rw [insertAndContract_some_prod_contractions]
@ -731,11 +730,11 @@ lemma signInsertSomeCoef_if (φ : 𝓕.States) (φs : List 𝓕.States) (φsΛ :
φsΛ.signInsertSomeCoef φ φs i j =
if i < i.succAbove j then
𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ ⟨(φs.insertIdx i φ).get,
(signFinset (φsΛ.insertAndContract φ i (some j)) (finCongr (insertIdx_length_fin φ φs i).symm i)
(signFinset (φsΛ ↩Λ φ i (some j)) (finCongr (insertIdx_length_fin φ φs i).symm i)
(finCongr (insertIdx_length_fin φ φs i).symm (i.succAbove j)))⟩)
else
𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ ⟨(φs.insertIdx i φ).get,
signFinset (φsΛ.insertAndContract φ i (some j))
signFinset (φsΛ ↩Λ φ i (some j))
(finCongr (insertIdx_length_fin φ φs i).symm (i.succAbove j))
(finCongr (insertIdx_length_fin φ φs i).symm i)⟩) := by
simp only [signInsertSomeCoef, instCommGroup.eq_1, Nat.succ_eq_add_one,
@ -749,7 +748,7 @@ lemma stat_signFinset_insert_some_self_fst
(φ : 𝓕.States) (φs : List 𝓕.States) (φsΛ : WickContraction φs.length)
(i : Fin φs.length.succ) (j : φsΛ.uncontracted) :
(𝓕 |>ₛ ⟨(φs.insertIdx i φ).get,
(signFinset (φsΛ.insertAndContract φ i (some j)) (finCongr (insertIdx_length_fin φ φs i).symm i)
(signFinset (φsΛ ↩Λ φ i (some j)) (finCongr (insertIdx_length_fin φ φs i).symm i)
(finCongr (insertIdx_length_fin φ φs i).symm (i.succAbove j)))⟩) =
𝓕 |>ₛ ⟨φs.get,
(Finset.univ.filter (fun x => i < i.succAbove x ∧ x < j ∧ ((φsΛ.getDual? x = none) ∨
@ -825,7 +824,7 @@ lemma stat_signFinset_insert_some_self_fst
lemma stat_signFinset_insert_some_self_snd (φ : 𝓕.States) (φs : List 𝓕.States)
(φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (j : φsΛ.uncontracted) :
(𝓕 |>ₛ ⟨(φs.insertIdx i φ).get,
(signFinset (φsΛ.insertAndContract φ i (some j))
(signFinset (φsΛ ↩Λ φ i (some j))
(finCongr (insertIdx_length_fin φ φs i).symm (i.succAbove j))
(finCongr (insertIdx_length_fin φ φs i).symm i))⟩) =
𝓕 |>ₛ ⟨φs.get,

8
HepLean/PerturbationTheory/WickContraction/TimeContract.lean
View file

@ -31,7 +31,7 @@ noncomputable def timeContract (𝓞 : 𝓕.ProtoOperatorAlgebra) {φs : List
@[simp]
lemma timeContract_insertAndContract_none (𝓞 : 𝓕.ProtoOperatorAlgebra) (φ : 𝓕.States) (φs : List 𝓕.States)
(φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) :
(φsΛ.insertAndContract φ i none).timeContract 𝓞 = φsΛ.timeContract 𝓞 := by
(φsΛ ↩Λ φ i none).timeContract 𝓞 = φsΛ.timeContract 𝓞 := by
rw [timeContract, insertAndContract_none_prod_contractions]
congr
ext a
@ -39,7 +39,7 @@ lemma timeContract_insertAndContract_none (𝓞 : 𝓕.ProtoOperatorAlgebra) (φ
lemma timeConract_insertAndContract_some (𝓞 : 𝓕.ProtoOperatorAlgebra) (φ : 𝓕.States) (φs : List 𝓕.States)
(φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (j : φsΛ.uncontracted) :
(φsΛ.insertAndContract φ i (some j)).timeContract 𝓞 =
(φsΛ ↩Λ φ i (some j)).timeContract 𝓞 =
(if i < i.succAbove j then
⟨𝓞.timeContract φ φs[j.1], 𝓞.timeContract_mem_center _ _⟩
else ⟨𝓞.timeContract φs[j.1] φ, 𝓞.timeContract_mem_center _ _⟩) * φsΛ.timeContract 𝓞 := by
@ -60,7 +60,7 @@ lemma timeConract_insertAndContract_some_eq_mul_contractStateAtIndex_lt
(𝓞 : 𝓕.ProtoOperatorAlgebra) (φ : 𝓕.States) (φs : List 𝓕.States)
(φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (k : φsΛ.uncontracted)
(ht : 𝓕.timeOrderRel φ φs[k.1]) (hik : i < i.succAbove k) :
(φsΛ.insertAndContract φ i (some k)).timeContract 𝓞 =
(φsΛ ↩Λ φ i (some k)).timeContract 𝓞 =
𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ ⟨φs.get, (φsΛ.uncontracted.filter (fun x => x < k))⟩)
• (𝓞.contractStateAtIndex φ [φsΛ]ᵘᶜ
((uncontractedStatesEquiv φs φsΛ) (some k)) * φsΛ.timeContract 𝓞) := by
@ -95,7 +95,7 @@ lemma timeConract_insertAndContract_some_eq_mul_contractStateAtIndex_not_lt
(𝓞 : 𝓕.ProtoOperatorAlgebra) (φ : 𝓕.States) (φs : List 𝓕.States)
(φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (k : φsΛ.uncontracted)
(ht : ¬ 𝓕.timeOrderRel φs[k.1] φ) (hik : ¬ i < i.succAbove k) :
(φsΛ.insertAndContract φ i (some k)).timeContract 𝓞 =
(φsΛ ↩Λ φ i (some k)).timeContract 𝓞 =
𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ ⟨φs.get, (φsΛ.uncontracted.filter (fun x => x ≤ k))⟩)
• (𝓞.contractStateAtIndex φ [φsΛ]ᵘᶜ
((uncontractedStatesEquiv φs φsΛ) (some k)) * φsΛ.timeContract 𝓞) := by

45
HepLean/PerturbationTheory/WicksTheorem.lean
View file

@ -27,18 +27,18 @@ open FieldStatistic
/--
Let `c` be a Wick Contraction for `φs := φ₀φ₁…φₙ`.
We have (roughly) `𝓝([φsΛ.insertAndContract φ i none]ᵘᶜ) = s • 𝓝(φ :: [φsΛ]ᵘᶜ)`
We have (roughly) `𝓝([φsΛ ↩Λ φ i none]ᵘᶜ) = s • 𝓝(φ :: [φsΛ]ᵘᶜ)`
Where `s` is the exchange sign for `φ` and the uncontracted fields in `φ₀φ₁…φᵢ₋₁`.
-/
lemma insertAndContract_none_normalOrder (φ : 𝓕.States) (φs : List 𝓕.States)
(i : Fin φs.length.succ) (φsΛ : WickContraction φs.length) :
𝓞.crAnF (𝓝([φsΛ.insertAndContract φ i none]ᵘᶜ))
𝓞.crAnF (𝓝([φsΛ ↩Λ φ i none]ᵘᶜ))
= 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ ⟨φs.get, φsΛ.uncontracted.filter (fun x => i.succAbove x < i)⟩) •
𝓞.crAnF 𝓝(φ :: [φsΛ]ᵘᶜ) := by
simp only [Nat.succ_eq_add_one, instCommGroup.eq_1]
rw [crAnF_ofState_normalOrder_insert φ [φsΛ]ᵘᶜ
⟨(φsΛ.uncontractedListOrderPos i), by simp [uncontractedListGet]⟩, smul_smul]
trans (1 : ℂ) • 𝓞.crAnF (𝓝(ofStateList [φsΛ.insertAndContract φ i none]ᵘᶜ))
trans (1 : ℂ) • 𝓞.crAnF (𝓝(ofStateList [φsΛ ↩Λ φ i none]ᵘᶜ))
· simp
congr 1
simp only [instCommGroup.eq_1, uncontractedListGet]
@ -96,13 +96,13 @@ lemma insertAndContract_none_normalOrder (φ : 𝓕.States) (φs : List 𝓕.Sta
/--
Let `c` be a Wick Contraction for `φ₀φ₁…φₙ`.
We have (roughly) `N(c.insertAndContract φ i k).uncontractedList`
We have (roughly) `N(c ↩Λ φ i k).uncontractedList`
is equal to `N((c.uncontractedList).eraseIdx k')`
where `k'` is the position in `c.uncontractedList` corresponding to `k`.
-/
lemma insertAndContract_some_normalOrder (φ : 𝓕.States) (φs : List 𝓕.States)
(i : Fin φs.length.succ) (φsΛ : WickContraction φs.length) (k : φsΛ.uncontracted) :
𝓞.crAnF 𝓝([φsΛ.insertAndContract φ i (some k)]ᵘᶜ)
𝓞.crAnF 𝓝([φsΛ ↩Λ φ i (some k)]ᵘᶜ)
= 𝓞.crAnF 𝓝((optionEraseZ [φsΛ]ᵘᶜ φ ((uncontractedStatesEquiv φs φsΛ) k))) := by
simp only [Nat.succ_eq_add_one, insertAndContract, optionEraseZ, uncontractedStatesEquiv,
Equiv.optionCongr_apply, Equiv.coe_trans, Option.map_some', Function.comp_apply, finCongr_apply,
@ -122,8 +122,8 @@ mulitiplied by the exchange sign of `φ` and `φ₀φ₁…φᵢ₋₁`.
-/
lemma sign_timeContract_normalOrder_insertAndContract_none (φ : 𝓕.States) (φs : List 𝓕.States)
(i : Fin φs.length.succ) (φsΛ : WickContraction φs.length) :
(φsΛ.insertAndContract φ i none).sign • (φsΛ.insertAndContract φ i none).timeContract 𝓞
* 𝓞.crAnF 𝓝([φsΛ.insertAndContract φ i none]ᵘᶜ) =
(φsΛ ↩Λ φ i none).sign • (φsΛ ↩Λ φ i none).timeContract 𝓞
* 𝓞.crAnF 𝓝([φsΛ ↩Λ φ i none]ᵘᶜ) =
𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ ⟨φs.get, (Finset.univ.filter (fun k => i.succAbove k < i))⟩)
• (φsΛ.sign • φsΛ.timeContract 𝓞 * 𝓞.crAnF 𝓝(φ :: [φsΛ]ᵘᶜ)) := by
by_cases hg : GradingCompliant φs φsΛ
@ -165,15 +165,15 @@ lemma sign_timeContract_normalOrder_insertAndContract_none (φ : 𝓕.States) (
Let `c` be a Wick Contraction for `φ₀φ₁…φₙ`.
This lemma states that
`(c.sign • c.timeContract 𝓞) * N(c.uncontracted)`
for `c` equal to `c.insertAndContract φ i (some k)` is equal to that for just `c`
for `c` equal to `c ↩Λ φ i (some k)` is equal to that for just `c`
mulitiplied by the exchange sign of `φ` and `φ₀φ₁…φᵢ₋₁`.
-/
lemma sign_timeContract_normalOrder_insertAndContract_some (φ : 𝓕.States) (φs : List 𝓕.States)
(i : Fin φs.length.succ) (φsΛ : WickContraction φs.length) (k : φsΛ.uncontracted)
(hlt : ∀ (k : Fin φs.length), timeOrderRel φ φs[k])
(hn : ∀ (k : Fin φs.length), i.succAbove k < i → ¬ timeOrderRel φs[k] φ) :
(φsΛ.insertAndContract φ i (some k)).sign • (φsΛ.insertAndContract φ i (some k)).timeContract 𝓞
* 𝓞.crAnF 𝓝([φsΛ.insertAndContract φ i (some k)]ᵘᶜ) =
(φsΛ ↩Λ φ i (some k)).sign • (φsΛ ↩Λ φ i (some k)).timeContract 𝓞
* 𝓞.crAnF 𝓝([φsΛ ↩Λ φ i (some k)]ᵘᶜ) =
𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ ⟨φs.get, (Finset.univ.filter (fun x => i.succAbove x < i))⟩)
• (φsΛ.sign • (𝓞.contractStateAtIndex φ [φsΛ]ᵘᶜ
((uncontractedStatesEquiv φs φsΛ) (some k)) * φsΛ.timeContract 𝓞)
@ -232,21 +232,21 @@ lemma sign_timeContract_normalOrder_insertAndContract_some (φ : 𝓕.States) (
exact hg'
/--
Let `c` be a Wick Contraction for `φ₀φ₁…φₙ`.
This lemma states that
`(c.sign • c.timeContract 𝓞) * N(c.uncontracted)`
is equal to the sum of
`(c'.sign • c'.timeContract 𝓞) * N(c'.uncontracted)`
for all `c' = (c.insertAndContract φ i k)` for `k : Option c.uncontracted`, multiplied by
the exchange sign of `φ` and `φ₀φ₁…φᵢ₋₁`.
Given a Wick contraction `φsΛ` of `φs = φ₀φ₁…φₙ` and an `i`, we have that
`(φsΛ.sign • φsΛ.timeContract 𝓞) * 𝓞.crAnF (φ * 𝓝([φsΛ]ᵘᶜ))`
is equal to the product of
- the exchange sign of `φ` and `φ₀φ₁…φᵢ₋₁`,
- the sum of
`((φsΛ ↩Λ φ i k).sign • (φsΛ ↩Λ φ i k).timeContract 𝓞) * 𝓞.crAnF 𝓝([φsΛ ↩Λ φ i k]ᵘᶜ)`
over all `k` in `Option φsΛ.uncontracted`.
-/
lemma mul_sum_contractions (φ : 𝓕.States) (φs : List 𝓕.States) (i : Fin φs.length.succ)
(φsΛ : WickContraction φs.length) (hlt : ∀ (k : Fin φs.length), timeOrderRel φ φs[k])
(hn : ∀ (k : Fin φs.length), i.succAbove k < i → ¬timeOrderRel φs[k] φ) :
(φsΛ.sign • φsΛ.timeContract 𝓞) * 𝓞.crAnF ((CrAnAlgebra.ofState φ) * 𝓝([φsΛ]ᵘᶜ)) =
𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ ⟨φs.get, (Finset.univ.filter (fun x => i.succAbove x < i))⟩) •
∑ (k : Option φsΛ.uncontracted), ((φsΛ.insertAndContract φ i k).sign •
(φsΛ.insertAndContract φ i k).timeContract 𝓞 * 𝓞.crAnF (𝓝(ofStateList [φsΛ.insertAndContract φ i k]ᵘᶜ))) := by
∑ (k : Option φsΛ.uncontracted), ((φsΛ ↩Λ φ i k).sign •
(φsΛ ↩Λ φ i k).timeContract 𝓞 * 𝓞.crAnF (𝓝([φsΛ ↩Λ φ i k]ᵘᶜ))) := by
rw [crAnF_ofState_mul_normalOrder_ofStatesList_eq_sum, Finset.mul_sum,
uncontractedStatesEquiv_list_sum, Finset.smul_sum]
simp only [instCommGroup.eq_1, Nat.succ_eq_add_one]
@ -339,12 +339,11 @@ theorem wicks_theorem : (φs : List 𝓕.States) → 𝓞.crAnF (ofStateAlgebra
(maxTimeField φ φs) (eraseMaxTimeField φ φs) (maxTimeFieldPosFin φ φs) c]
trans (1 : ℂ) • ∑ k : Option { x // x ∈ c.uncontracted }, sign
(List.insertIdx (↑(maxTimeFieldPosFin φ φs)) (maxTimeField φ φs) (eraseMaxTimeField φ φs))
(insertAndContract (maxTimeField φ φs) c (maxTimeFieldPosFin φ φs) k) •
↑((c.insertAndContract (maxTimeField φ φs) (maxTimeFieldPosFin φ φs) k).timeContract 𝓞) *
(c ↩Λ (maxTimeField φ φs) (maxTimeFieldPosFin φ φs) k) •
↑((c ↩Λ (maxTimeField φ φs) (maxTimeFieldPosFin φ φs) k).timeContract 𝓞) *
𝓞.crAnF 𝓝(ofStateList (List.map (List.insertIdx (↑(maxTimeFieldPosFin φ φs))
(maxTimeField φ φs) (eraseMaxTimeField φ φs)).get
(insertAndContract (maxTimeField φ φs) c
(maxTimeFieldPosFin φ φs) k).uncontractedList))
(c ↩Λ (maxTimeField φ φs) (maxTimeFieldPosFin φ φs) k).uncontractedList))
swap
· simp [uncontractedListGet]
rw [smul_smul]