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

refactor: Simplify some notation

Browse source
This commit is contained in:
jstoobysmith 2025-01-24 05:19:04 +00:00
parent 7d053695dd
commit 6701ee7b37
8 changed files with 106 additions and 111 deletions
Download patch file Download diff file Expand all files Collapse all files

2
HepLean/PerturbationTheory/Algebras/CrAnAlgebra/NormalOrder.lean
View file

@ -391,7 +391,7 @@ lemma normalOrder_superCommute_ofCrAnList_annihilate_annihilate_ofCrAnList
𝓝(ofCrAnList φs * [ofCrAnState φa, ofCrAnState φa']ₛca * ofCrAnList φs') =
normalOrderSign (φs ++ φa' :: φa :: φs') •
(ofCrAnList (createFilter (φs ++ φs'))
* ofCrAnList (annihilateFilter φs) * superCommute (ofCrAnState φa) (ofCrAnState φa')
* ofCrAnList (annihilateFilter φs) * [ofCrAnState φa, ofCrAnState φa']ₛca
* ofCrAnList (annihilateFilter φs')) := by
rw [superCommute_ofCrAnState_ofCrAnState, mul_sub, sub_mul, map_sub]
conv_lhs =>

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

@ -29,19 +29,15 @@ structure ProtoOperatorAlgebra where
algebra A. -/
crAnF : 𝓕.CrAnAlgebra →ₐ[ℂ] A
superCommute_crAn_center : ∀ (φ ψ : 𝓕.CrAnStates),
crAnF (superCommute (ofCrAnState φ) (ofCrAnState ψ))
∈ Subalgebra.center ℂ A
crAnF [ofCrAnState φ, ofCrAnState ψ]ₛca ∈ Subalgebra.center ℂ A
superCommute_create_create : ∀ (φc φc' : 𝓕.CrAnStates)
(_ : 𝓕 |>ᶜ φc = CreateAnnihilate.create)
(_ : 𝓕 |>ᶜ φc' = CreateAnnihilate.create),
crAnF (superCommute (ofCrAnState φc) (ofCrAnState φc')) = 0
(_ : 𝓕 |>ᶜ φc = .create) (_ : 𝓕 |>ᶜ φc' = .create),
crAnF [ofCrAnState φc, ofCrAnState φc']ₛca = 0
superCommute_annihilate_annihilate : ∀ (φa φa' : 𝓕.CrAnStates)
(_ : 𝓕 |>ᶜ φa = CreateAnnihilate.annihilate)
(_ : 𝓕 |>ᶜ φa' = CreateAnnihilate.annihilate),
crAnF (superCommute (ofCrAnState φa) (ofCrAnState φa')) = 0
superCommute_different_statistics : ∀ (φ φ' : 𝓕.CrAnStates)
(_ : ¬ (𝓕 |>ₛ φ) = (𝓕 |>ₛ φ')),
crAnF (superCommute (ofCrAnState φ) (ofCrAnState φ')) = 0
(_ : 𝓕 |>ᶜ φa = .annihilate) (_ : 𝓕 |>ᶜ φa' = .annihilate),
crAnF [ofCrAnState φa, ofCrAnState φa']ₛca = 0
superCommute_different_statistics : ∀ (φ φ' : 𝓕.CrAnStates) (_ : ¬ (𝓕 |>ₛ φ) = (𝓕 |>ₛ φ')),
crAnF [ofCrAnState φ, ofCrAnState φ']ₛca = 0
namespace ProtoOperatorAlgebra
open FieldStatistic
@ -54,7 +50,7 @@ instance : Semiring 𝓞.A := 𝓞.A_semiRing
instance : Algebra ℂ 𝓞.A := 𝓞.A_algebra
lemma crAnF_superCommute_ofCrAnState_ofState_mem_center (φ : 𝓕.CrAnStates) (ψ : 𝓕.States) :
𝓞.crAnF (superCommute (ofCrAnState φ) (ofState ψ)) ∈ Subalgebra.center ℂ 𝓞.A := by
𝓞.crAnF [ofCrAnState φ, ofState ψ]ₛca ∈ Subalgebra.center ℂ 𝓞.A := by
rw [ofState, map_sum, map_sum]
refine Subalgebra.sum_mem (Subalgebra.center ℂ 𝓞.A) ?h
intro x _
@ -75,7 +71,7 @@ lemma crAnF_superCommute_anPart_ofState_mem_center (φ ψ : 𝓕.States) :
lemma crAnF_superCommute_ofCrAnState_ofState_diff_grade_zero (φ : 𝓕.CrAnStates) (ψ : 𝓕.States)
(h : (𝓕 |>ₛ φ) ≠ (𝓕 |>ₛ ψ)) :
𝓞.crAnF (superCommute (ofCrAnState φ) (ofState ψ)) = 0 := by
𝓞.crAnF [ofCrAnState φ, ofState ψ]ₛca = 0 := by
rw [ofState, map_sum, map_sum]
rw [Finset.sum_eq_zero]
intro x hx
@ -84,7 +80,7 @@ lemma crAnF_superCommute_ofCrAnState_ofState_diff_grade_zero (φ : 𝓕.CrAnStat
lemma crAnF_superCommute_anPart_ofState_diff_grade_zero (φ ψ : 𝓕.States)
(h : (𝓕 |>ₛ φ) ≠ (𝓕 |>ₛ ψ)) :
𝓞.crAnF (superCommute (anPart (StateAlgebra.ofState φ)) (ofState ψ)) = 0 := by
𝓞.crAnF [anPart (StateAlgebra.ofState φ), ofState ψ]ₛca = 0 := by
match φ with
| States.inAsymp _ =>
simp
@ -98,7 +94,7 @@ lemma crAnF_superCommute_anPart_ofState_diff_grade_zero (φ ψ : 𝓕.States)
simpa [crAnStatistics] using h
lemma crAnF_superCommute_ofState_ofState_mem_center (φ ψ : 𝓕.States) :
𝓞.crAnF (superCommute (ofState φ) (ofState ψ)) ∈ Subalgebra.center ℂ 𝓞.A := by
𝓞.crAnF [ofState φ, ofState ψ]ₛca ∈ Subalgebra.center ℂ 𝓞.A := by
rw [ofState, map_sum]
simp only [LinearMap.coeFn_sum, Finset.sum_apply, map_sum]
refine Subalgebra.sum_mem (Subalgebra.center ℂ 𝓞.A) ?h

32
HepLean/PerturbationTheory/Algebras/ProtoOperatorAlgebra/NormalOrder.lean
View file

@ -47,7 +47,7 @@ lemma crAnF_normalOrder_superCommute_ofCrAnList_annihilate_annihilate_ofCrAnList
lemma crAnF_normalOrder_superCommute_ofCrAnList_ofCrAnList_eq_zero
(φa φa' : 𝓕.CrAnStates) (φs φs' : List 𝓕.CrAnStates) :
𝓞.crAnF (normalOrder
(ofCrAnList φs * superCommute (ofCrAnState φa) (ofCrAnState φa') * ofCrAnList φs')) = 0 := by
(ofCrAnList φs * [ofCrAnState φa, ofCrAnState φa']ₛca * ofCrAnList φs')) = 0 := by
rcases CreateAnnihilate.eq_create_or_annihilate (𝓕 |>ᶜ φa) with hφa | hφa
<;> rcases CreateAnnihilate.eq_create_or_annihilate (𝓕 |>ᶜ φa') with hφa' | hφa'
· rw [normalOrder_superCommute_ofCrAnList_create_create_ofCrAnList φa φa' hφa hφa' φs φs']
@ -66,11 +66,11 @@ lemma crAnF_normalOrder_superCommute_ofCrAnList_ofCrAnList_eq_zero
lemma crAnF_normalOrder_superCommute_ofCrAnList_eq_zero
(φa φa' : 𝓕.CrAnStates) (φs : List 𝓕.CrAnStates)
(a : 𝓕.CrAnAlgebra) : 𝓞.crAnF (normalOrder (ofCrAnList φs *
superCommute (ofCrAnState φa) (ofCrAnState φa') * a)) = 0 := by
[ofCrAnState φa, ofCrAnState φa']ₛca * a)) = 0 := by
change (𝓞.crAnF.toLinearMap ∘ₗ normalOrder ∘ₗ
mulLinearMap ((ofCrAnList φs * superCommute (ofCrAnState φa) (ofCrAnState φa')))) a = 0
mulLinearMap ((ofCrAnList φs * [ofCrAnState φa, ofCrAnState φa']ₛca))) a = 0
have hf : 𝓞.crAnF.toLinearMap ∘ₗ normalOrder ∘ₗ
mulLinearMap ((ofCrAnList φs * superCommute (ofCrAnState φa) (ofCrAnState φa'))) = 0 := by
mulLinearMap (ofCrAnList φs * [ofCrAnState φa, ofCrAnState φa']ₛca) = 0 := by
apply ofCrAnListBasis.ext
intro l
simp only [ofListBasis_eq_ofList, LinearMap.coe_comp, Function.comp_apply,
@ -81,12 +81,12 @@ lemma crAnF_normalOrder_superCommute_ofCrAnList_eq_zero
lemma crAnF_normalOrder_superCommute_ofCrAnState_eq_zero_mul (φa φa' : 𝓕.CrAnStates)
(a b : 𝓕.CrAnAlgebra) :
𝓞.crAnF (normalOrder (a * superCommute (ofCrAnState φa) (ofCrAnState φa') * b)) = 0 := by
𝓞.crAnF (normalOrder (a * [ofCrAnState φa, ofCrAnState φa']ₛca * b)) = 0 := by
rw [mul_assoc]
change (𝓞.crAnF.toLinearMap ∘ₗ normalOrder ∘ₗ mulLinearMap.flip
((superCommute (ofCrAnState φa) (ofCrAnState φa') * b))) a = 0
have hf : (𝓞.crAnF.toLinearMap ∘ₗ normalOrder ∘ₗ mulLinearMap.flip
((superCommute (ofCrAnState φa) (ofCrAnState φa') * b))) = 0 := by
([ofCrAnState φa, ofCrAnState φa']ₛca * b)) a = 0
have hf : 𝓞.crAnF.toLinearMap ∘ₗ normalOrder ∘ₗ mulLinearMap.flip
([ofCrAnState φa, ofCrAnState φa']ₛca * b) = 0 := by
apply ofCrAnListBasis.ext
intro l
simp only [mulLinearMap, ofListBasis_eq_ofList, LinearMap.coe_comp, Function.comp_apply,
@ -100,7 +100,7 @@ lemma crAnF_normalOrder_superCommute_ofCrAnState_eq_zero_mul (φa φa' : 𝓕.Cr
lemma crAnF_normalOrder_superCommute_ofCrAnState_ofCrAnList_eq_zero_mul (φa : 𝓕.CrAnStates)
(φs : List 𝓕.CrAnStates)
(a b : 𝓕.CrAnAlgebra) :
𝓞.crAnF (normalOrder (a * superCommute (ofCrAnState φa) (ofCrAnList φs) * b)) = 0 := by
𝓞.crAnF (normalOrder (a * [ofCrAnState φa, ofCrAnList φs]ₛca * b)) = 0 := by
rw [← ofCrAnList_singleton, superCommute_ofCrAnList_ofCrAnList_eq_sum]
rw [Finset.mul_sum, Finset.sum_mul]
rw [map_sum, map_sum]
@ -113,7 +113,7 @@ lemma crAnF_normalOrder_superCommute_ofCrAnState_ofCrAnList_eq_zero_mul (φa :
lemma crAnF_normalOrder_superCommute_ofCrAnList_ofCrAnState_eq_zero_mul (φa : 𝓕.CrAnStates)
(φs : List 𝓕.CrAnStates)
(a b : 𝓕.CrAnAlgebra) :
𝓞.crAnF (normalOrder (a * superCommute (ofCrAnList φs) (ofCrAnState φa) * b)) = 0 := by
𝓞.crAnF (normalOrder (a * [ofCrAnList φs, ofCrAnState φa]ₛca * b)) = 0 := by
rw [← ofCrAnList_singleton, superCommute_ofCrAnList_ofCrAnList_symm, ofCrAnList_singleton]
simp only [FieldStatistic.instCommGroup.eq_1, FieldStatistic.ofList_singleton, mul_neg,
Algebra.mul_smul_comm, neg_mul, Algebra.smul_mul_assoc, map_neg, map_smul]
@ -123,7 +123,7 @@ lemma crAnF_normalOrder_superCommute_ofCrAnList_ofCrAnState_eq_zero_mul (φa :
lemma crAnF_normalOrder_superCommute_ofCrAnList_ofCrAnList_eq_zero_mul
(φs φs' : List 𝓕.CrAnStates)
(a b : 𝓕.CrAnAlgebra) :
𝓞.crAnF (normalOrder (a * superCommute (ofCrAnList φs) (ofCrAnList φs') * b)) = 0 := by
𝓞.crAnF (normalOrder (a * [ofCrAnList φs, ofCrAnList φs']ₛca * b)) = 0 := by
rw [superCommute_ofCrAnList_ofCrAnList_eq_sum, Finset.mul_sum, Finset.sum_mul]
rw [map_sum, map_sum]
apply Fintype.sum_eq_zero
@ -135,7 +135,7 @@ lemma crAnF_normalOrder_superCommute_ofCrAnList_ofCrAnList_eq_zero_mul
lemma crAnF_normalOrder_superCommute_ofCrAnList_eq_zero_mul
(φs : List 𝓕.CrAnStates)
(a b c : 𝓕.CrAnAlgebra) :
𝓞.crAnF (normalOrder (a * superCommute (ofCrAnList φs) c * b)) = 0 := by
𝓞.crAnF (normalOrder (a * [ofCrAnList φs, c]ₛca * b)) = 0 := by
change (𝓞.crAnF.toLinearMap ∘ₗ normalOrder ∘ₗ
mulLinearMap.flip b ∘ₗ mulLinearMap a ∘ₗ superCommute (ofCrAnList φs)) c = 0
have hf : (𝓞.crAnF.toLinearMap ∘ₗ normalOrder ∘ₗ
@ -151,7 +151,7 @@ lemma crAnF_normalOrder_superCommute_ofCrAnList_eq_zero_mul
@[simp]
lemma crAnF_normalOrder_superCommute_eq_zero_mul
(a b c d : 𝓕.CrAnAlgebra) : 𝓞.crAnF (normalOrder (a * superCommute d c * b)) = 0 := by
(a b c d : 𝓕.CrAnAlgebra) : 𝓞.crAnF (normalOrder (a * [d, c]ₛca * b)) = 0 := by
change (𝓞.crAnF.toLinearMap ∘ₗ normalOrder ∘ₗ
mulLinearMap.flip b ∘ₗ mulLinearMap a ∘ₗ superCommute.flip c) d = 0
have hf : (𝓞.crAnF.toLinearMap ∘ₗ normalOrder ∘ₗ
@ -167,19 +167,19 @@ lemma crAnF_normalOrder_superCommute_eq_zero_mul
@[simp]
lemma crAnF_normalOrder_superCommute_eq_zero_mul_right
(b c d : 𝓕.CrAnAlgebra) : 𝓞.crAnF (normalOrder (superCommute d c * b)) = 0 := by
(b c d : 𝓕.CrAnAlgebra) : 𝓞.crAnF (normalOrder ([d, c]ₛca * b)) = 0 := by
rw [← crAnF_normalOrder_superCommute_eq_zero_mul 1 b c d]
simp
@[simp]
lemma crAnF_normalOrder_superCommute_eq_zero_mul_left
(a c d : 𝓕.CrAnAlgebra) : 𝓞.crAnF (normalOrder (a * superCommute d c)) = 0 := by
(a c d : 𝓕.CrAnAlgebra) : 𝓞.crAnF (normalOrder (a * [d, c]ₛca)) = 0 := by
rw [← crAnF_normalOrder_superCommute_eq_zero_mul a 1 c d]
simp
@[simp]
lemma crAnF_normalOrder_superCommute_eq_zero
(c d : 𝓕.CrAnAlgebra) : 𝓞.crAnF (normalOrder (superCommute d c)) = 0 := by
(c d : 𝓕.CrAnAlgebra) : 𝓞.crAnF (normalOrder [d, c]ₛca) = 0 := by
rw [← crAnF_normalOrder_superCommute_eq_zero_mul 1 1 c d]
simp

4
HepLean/PerturbationTheory/Algebras/ProtoOperatorAlgebra/TimeContraction.lean
View file

@ -29,12 +29,12 @@ open FieldStatistic
creation and annihlation algebra, both mapped to `𝓞.A`.. -/
def timeContract (φ ψ : 𝓕.States) : 𝓞.A :=
𝓞.crAnF (ofStateAlgebra (StateAlgebra.timeOrder (StateAlgebra.ofState φ * StateAlgebra.ofState ψ))
- normalOrder (ofState φ * ofState ψ))
- 𝓝(ofState φ * ofState ψ))
lemma timeContract_eq_smul (φ ψ : 𝓕.States) : 𝓞.timeContract φ ψ =
𝓞.crAnF (ofStateAlgebra (StateAlgebra.timeOrder
(StateAlgebra.ofState φ * StateAlgebra.ofState ψ))
+ (-1 : ℂ) • normalOrder (ofState φ * ofState ψ)) := by rfl
+ (-1 : ℂ) • 𝓝(ofState φ * ofState ψ)) := by rfl
lemma timeContract_of_timeOrderRel (φ ψ : 𝓕.States) (h : timeOrderRel φ ψ) :
𝓞.timeContract φ ψ = 𝓞.crAnF ([anPart (StateAlgebra.ofState φ), ofState ψ]ₛca) := by

46
HepLean/PerturbationTheory/WickContraction/InsertList.lean
View file

@ -29,7 +29,7 @@ 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 insertList (φ : 𝓕.States) (φs : List 𝓕.States)
def insertList (φ : 𝓕.States) {φs : List 𝓕.States}
(c : WickContraction φs.length) (i : Fin φs.length.succ) (j : Option (c.uncontracted)) :
WickContraction (φs.insertIdx i φ).length :=
congr (by simp) (c.insert i j)
@ -37,7 +37,7 @@ def insertList (φ : 𝓕.States) (φs : List 𝓕.States)
@[simp]
lemma insertList_fstFieldOfContract (φ : 𝓕.States) (φs : List 𝓕.States)
(c : WickContraction φs.length) (i : Fin φs.length.succ) (j : Option (c.uncontracted))
(a : c.1) : (insertList φ φs c i j).fstFieldOfContract
(a : c.1) : (c.insertList φ i j).fstFieldOfContract
(congrLift (insertIdx_length_fin φ φs i).symm (insertLift i j a)) =
finCongr (insertIdx_length_fin φ φs i).symm (i.succAbove (c.fstFieldOfContract a)) := by
simp [insertList]
@ -45,7 +45,7 @@ lemma insertList_fstFieldOfContract (φ : 𝓕.States) (φs : List 𝓕.States)
@[simp]
lemma insertList_sndFieldOfContract (φ : 𝓕.States) (φs : List 𝓕.States)
(c : WickContraction φs.length) (i : Fin φs.length.succ) (j : Option (c.uncontracted))
(a : c.1) : (insertList φ φs c i j).sndFieldOfContract
(a : c.1) : (c.insertList φ i j).sndFieldOfContract
(congrLift (insertIdx_length_fin φ φs i).symm (insertLift i j a)) =
finCongr (insertIdx_length_fin φ φs i).symm (i.succAbove (c.sndFieldOfContract a)) := by
simp [insertList]
@ -53,14 +53,14 @@ lemma insertList_sndFieldOfContract (φ : 𝓕.States) (φs : List 𝓕.States)
@[simp]
lemma insertList_fstFieldOfContract_some_incl (φ : 𝓕.States) (φs : List 𝓕.States)
(c : WickContraction φs.length) (i : Fin φs.length.succ) (j : c.uncontracted) :
(insertList φ φs c i (some j)).fstFieldOfContract
(insertList φ c i (some j)).fstFieldOfContract
(congrLift (insertIdx_length_fin φ φs i).symm ⟨{i, i.succAbove j}, by simp [insert]⟩) =
if i < i.succAbove j.1 then
finCongr (insertIdx_length_fin φ φs i).symm i else
finCongr (insertIdx_length_fin φ φs i).symm (i.succAbove j.1) := by
split
· rename_i h
refine (insertList φ φs c i (some j)).eq_fstFieldOfContract_of_mem
refine (insertList φ c i (some j)).eq_fstFieldOfContract_of_mem
(a := congrLift (insertIdx_length_fin φ φs i).symm ⟨{i, i.succAbove j}, by simp [insert]⟩)
(i := finCongr (insertIdx_length_fin φ φs i).symm i) (j :=
finCongr (insertIdx_length_fin φ φs i).symm (i.succAbove j)) ?_ ?_ ?_
@ -69,7 +69,7 @@ lemma insertList_fstFieldOfContract_some_incl (φ : 𝓕.States) (φs : List
· rw [Fin.lt_def] at h ⊢
simp_all
· rename_i h
refine (insertList φ φs c i (some j)).eq_fstFieldOfContract_of_mem
refine (insertList φ c i (some j)).eq_fstFieldOfContract_of_mem
(a := congrLift (insertIdx_length_fin φ φs i).symm ⟨{i, i.succAbove j}, by simp [insert]⟩)
(i := finCongr (insertIdx_length_fin φ φs i).symm (i.succAbove j))
(j := finCongr (insertIdx_length_fin φ φs i).symm i) ?_ ?_ ?_
@ -88,7 +88,7 @@ lemma insertList_fstFieldOfContract_some_incl (φ : 𝓕.States) (φs : List
@[simp]
lemma insertList_none_getDual?_self (φ : 𝓕.States) (φs : List 𝓕.States)
(c : WickContraction φs.length) (i : Fin φs.length.succ) :
(insertList φ φs c i none).getDual? (Fin.cast (insertIdx_length_fin φ φs i).symm i) = none := by
(insertList φ c i none).getDual? (Fin.cast (insertIdx_length_fin φ φs i).symm i) = none := by
simp only [Nat.succ_eq_add_one, insertList, getDual?_congr, finCongr_apply, Fin.cast_trans,
Fin.cast_eq_self, Option.map_eq_none']
have h1 := c.insert_none_getDual?_isNone i
@ -96,27 +96,27 @@ lemma insertList_none_getDual?_self (φ : 𝓕.States) (φs : List 𝓕.States)
lemma insertList_isSome_getDual?_self (φ : 𝓕.States) (φs : List 𝓕.States)
(c : WickContraction φs.length) (i : Fin φs.length.succ) (j : c.uncontracted) :
((insertList φ φs c i (some j)).getDual?
((insertList φ c i (some j)).getDual?
(Fin.cast (insertIdx_length_fin φ φs i).symm i)).isSome := by
simp [insertList, getDual?_congr]
lemma insertList_some_getDual?_self_not_none (φ : 𝓕.States) (φs : List 𝓕.States)
(c : WickContraction φs.length) (i : Fin φs.length.succ) (j : c.uncontracted) :
¬ ((insertList φ φs c i (some j)).getDual?
¬ ((insertList φ c i (some j)).getDual?
(Fin.cast (insertIdx_length_fin φ φs i).symm i)) = none := by
simp [insertList, getDual?_congr]
@[simp]
lemma insertList_some_getDual?_self_eq (φ : 𝓕.States) (φs : List 𝓕.States)
(c : WickContraction φs.length) (i : Fin φs.length.succ) (j : c.uncontracted) :
((insertList φ φs c i (some j)).getDual? (Fin.cast (insertIdx_length_fin φ φs i).symm i))
((insertList φ c 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 [insertList, getDual?_congr]
@[simp]
lemma insertList_some_getDual?_some_eq (φ : 𝓕.States) (φs : List 𝓕.States)
(c : WickContraction φs.length) (i : Fin φs.length.succ) (j : c.uncontracted) :
((insertList φ φs c i (some j)).getDual?
((insertList φ c 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 +127,7 @@ lemma insertList_some_getDual?_some_eq (φ : 𝓕.States) (φs : List 𝓕.State
@[simp]
lemma insertList_none_succAbove_getDual?_eq_none_iff (φ : 𝓕.States) (φs : List 𝓕.States)
(c : WickContraction φs.length) (i : Fin φs.length.succ) (j : Fin φs.length) :
(insertList φ φs c i none).getDual? (Fin.cast (insertIdx_length_fin φ φs i).symm
(insertList φ c i none).getDual? (Fin.cast (insertIdx_length_fin φ φs i).symm
(i.succAbove j)) = none ↔ c.getDual? j = none := by
simp [insertList, getDual?_congr]
@ -135,7 +135,7 @@ lemma insertList_none_succAbove_getDual?_eq_none_iff (φ : 𝓕.States) (φs : L
lemma insertList_some_succAbove_getDual?_eq_option (φ : 𝓕.States) (φs : List 𝓕.States)
(c : WickContraction φs.length) (i : Fin φs.length.succ) (j : Fin φs.length)
(k : c.uncontracted) (hkj : j ≠ k.1) :
(insertList φ φs c i (some k)).getDual? (Fin.cast (insertIdx_length_fin φ φs i).symm
(insertList φ c 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)
(c.getDual? j) := by
simp only [Nat.succ_eq_add_one, insertList, getDual?_congr, finCongr_apply, Fin.cast_trans,
@ -145,7 +145,7 @@ lemma insertList_some_succAbove_getDual?_eq_option (φ : 𝓕.States) (φs : Lis
@[simp]
lemma insertList_none_succAbove_getDual?_isSome_iff (φ : 𝓕.States) (φs : List 𝓕.States)
(c : WickContraction φs.length) (i : Fin φs.length.succ) (j : Fin φs.length) :
((insertList φ φs c i none).getDual? (Fin.cast (insertIdx_length_fin φ φs i).symm
((insertList φ c i none).getDual? (Fin.cast (insertIdx_length_fin φ φs i).symm
(i.succAbove j))).isSome ↔ (c.getDual? j).isSome := by
rw [← not_iff_not]
simp
@ -153,9 +153,9 @@ lemma insertList_none_succAbove_getDual?_isSome_iff (φ : 𝓕.States) (φs : Li
@[simp]
lemma insertList_none_getDual?_get_eq (φ : 𝓕.States) (φs : List 𝓕.States)
(c : WickContraction φs.length) (i : Fin φs.length.succ) (j : Fin φs.length)
(h : ((insertList φ φs c i none).getDual? (Fin.cast (insertIdx_length_fin φ φs i).symm
(h : ((insertList φ c i none).getDual? (Fin.cast (insertIdx_length_fin φ φs i).symm
(i.succAbove j))).isSome) :
((insertList φ φs c i none).getDual? (Fin.cast (insertIdx_length_fin φ φs i).symm
((insertList φ c 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 ((c.getDual? j).get (by simpa using h))) := by
simp [insertList, getDual?_congr_get]
@ -164,14 +164,14 @@ lemma insertList_none_getDual?_get_eq (φ : 𝓕.States) (φs : List 𝓕.States
@[simp]
lemma insertList_sndFieldOfContract_some_incl (φ : 𝓕.States) (φs : List 𝓕.States)
(c : WickContraction φs.length) (i : Fin φs.length.succ) (j : c.uncontracted) :
(insertList φ φs c i (some j)).sndFieldOfContract
(insertList φ c i (some j)).sndFieldOfContract
(congrLift (insertIdx_length_fin φ φs i).symm ⟨{i, i.succAbove j}, by simp [insert]⟩) =
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 (insertList φ φs c i (some j)).eq_sndFieldOfContract_of_mem
refine (insertList φ c i (some j)).eq_sndFieldOfContract_of_mem
(a := congrLift (insertIdx_length_fin φ φs i).symm ⟨{i, i.succAbove j}, by simp [insert]⟩)
(i := finCongr (insertIdx_length_fin φ φs i).symm i) (j :=
finCongr (insertIdx_length_fin φ φs i).symm (i.succAbove j)) ?_ ?_ ?_
@ -180,7 +180,7 @@ lemma insertList_sndFieldOfContract_some_incl (φ : 𝓕.States) (φs : List
· rw [Fin.lt_def] at h ⊢
simp_all
· rename_i h
refine (insertList φ φs c i (some j)).eq_sndFieldOfContract_of_mem
refine (insertList φ c i (some j)).eq_sndFieldOfContract_of_mem
(a := congrLift (insertIdx_length_fin φ φs i).symm ⟨{i, i.succAbove j}, by simp [insert]⟩)
(i := finCongr (insertIdx_length_fin φ φs i).symm (i.succAbove j))
(j := finCongr (insertIdx_length_fin φ φs i).symm i) ?_ ?_ ?_
@ -193,7 +193,7 @@ lemma insertList_sndFieldOfContract_some_incl (φ : 𝓕.States) (φs : List
lemma insertList_none_prod_contractions (φ : 𝓕.States) (φs : List 𝓕.States)
(c : WickContraction φs.length) (i : Fin φs.length.succ)
(f : (c.insertList φ φs i none).1 → M) [CommMonoid M] :
(f : (c.insertList φ i none).1 → M) [CommMonoid M] :
∏ a, f a = ∏ (a : c.1), f (congrLift (insertIdx_length_fin φ φs i).symm
(insertLift i none a)) := by
let e1 := Equiv.ofBijective (c.insertLift i none) (insertLift_none_bijective i)
@ -205,7 +205,7 @@ lemma insertList_none_prod_contractions (φ : 𝓕.States) (φs : List 𝓕.Stat
lemma insertList_some_prod_contractions (φ : 𝓕.States) (φs : List 𝓕.States)
(c : WickContraction φs.length) (i : Fin φs.length.succ) (j : c.uncontracted)
(f : (c.insertList φ φs i (some j)).1 → M) [CommMonoid M] :
(f : (c.insertList φ i (some j)).1 → M) [CommMonoid M] :
∏ a, f a = f (congrLift (insertIdx_length_fin φ φs i).symm
⟨{i, i.succAbove j}, by simp [insert]⟩) *
∏ (a : c.1), f (congrLift (insertIdx_length_fin φ φs i).symm (insertLift i (some j) a)) := by
@ -268,7 +268,7 @@ lemma insert_fin_eq_self (φ : 𝓕.States) {φs : List 𝓕.States}
lemma insertList_uncontractedList_none_map (φ : 𝓕.States) {φs : List 𝓕.States}
(c : WickContraction φs.length) (i : Fin φs.length.succ) :
List.map (List.insertIdx (↑i) φ φs).get (insertList φ φs c i none).uncontractedList =
List.map (List.insertIdx (↑i) φ φs).get (insertList φ c i none).uncontractedList =
List.insertIdx (c.uncontractedListOrderPos i) φ (List.map φs.get c.uncontractedList) := by
simp only [Nat.succ_eq_add_one, insertList]
rw [congr_uncontractedList]
@ -285,7 +285,7 @@ lemma insertList_uncontractedList_none_map (φ : 𝓕.States) {φs : List 𝓕.S
lemma insertLift_sum (φ : 𝓕.States) {φs : List 𝓕.States}
(i : Fin φs.length.succ) [AddCommMonoid M] (f : WickContraction (φs.insertIdx i φ).length → M) :
∑ c, f c = ∑ (c : WickContraction φs.length), ∑ (k : Option (c.uncontracted)),
f (insertList φ φs c i k) := by
f (insertList φ c i k) := by
rw [sum_extractEquiv_congr (finCongr (insertIdx_length_fin φ φs i).symm i) f
(insertIdx_length_fin φ φs i)]
rfl

24
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_insertList_none (φ : 𝓕.States) (φs : List 𝓕.States)
(c : WickContraction φs.length)
(i : Fin φs.length.succ) (i1 i2 : Fin φs.length) :
(c.insertList φ φs i none).signFinset (finCongr (insertIdx_length_fin φ φs i).symm
(c.insertList φ 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_insertList_some (φ : 𝓕.States) (φs : List 𝓕.States)
(c : WickContraction φs.length) (i : Fin φs.length.succ) (i1 i2 : Fin φs.length)
(j : c.uncontracted) :
(c.insertList φ φs i (some j)).signFinset (finCongr (insertIdx_length_fin φ φs i).symm
(c.insertList φ 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) (c : WickContract
lemma sign_insert_none (φ : 𝓕.States) (φs : List 𝓕.States) (c : WickContraction φs.length)
(i : Fin φs.length.succ) :
(c.insertList φ φs i none).sign = (c.signInsertNone φ φs i) * c.sign := by
(c.insertList φ i none).sign = (c.signInsertNone φ φs i) * c.sign := by
rw [sign]
rw [signInsertNone, sign, ← Finset.prod_mul_distrib]
rw [insertList_none_prod_contractions]
@ -508,13 +508,13 @@ def signInsertSomeProd (φ : 𝓕.States) (φs : List 𝓕.States) (c : WickCont
coming from putting `i` next to `j`. -/
def signInsertSomeCoef (φ : 𝓕.States) (φs : List 𝓕.States) (c : WickContraction φs.length)
(i : Fin φs.length.succ) (j : c.uncontracted) : ℂ :=
let a : (c.insertList φ φs i (some j)).1 :=
let a : (c.insertList φ i (some j)).1 :=
congrLift (insertIdx_length_fin φ φs i).symm
⟨{i, i.succAbove j}, by simp [insert]⟩;
𝓢(𝓕 |>ₛ (φs.insertIdx i φ)[(c.insertList φ φs i (some j)).sndFieldOfContract a],
𝓢(𝓕 |>ₛ (φs.insertIdx i φ)[(c.insertList φ i (some j)).sndFieldOfContract a],
𝓕 |>ₛ ⟨(φs.insertIdx i φ).get, signFinset
(c.insertList φ φs i (some j)) ((c.insertList φ φs i (some j)).fstFieldOfContract a)
((c.insertList φ φs i (some j)).sndFieldOfContract a)⟩)
(c.insertList φ i (some j)) ((c.insertList φ i (some j)).fstFieldOfContract a)
((c.insertList φ 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 +525,7 @@ def signInsertSome (φ : 𝓕.States) (φs : List 𝓕.States) (c : WickContract
lemma sign_insert_some (φ : 𝓕.States) (φs : List 𝓕.States) (c : WickContraction φs.length)
(i : Fin φs.length.succ) (j : c.uncontracted) :
(c.insertList φ φs i (some j)).sign = (c.signInsertSome φ φs i j) * c.sign := by
(c.insertList φ i (some j)).sign = (c.signInsertSome φ φs i j) * c.sign := by
rw [sign]
rw [signInsertSome, signInsertSomeProd, sign, mul_assoc, ← Finset.prod_mul_distrib]
rw [insertList_some_prod_contractions]
@ -730,11 +730,11 @@ lemma signInsertSomeCoef_if (φ : 𝓕.States) (φs : List 𝓕.States) (c : Wic
c.signInsertSomeCoef φ φs i j =
if i < i.succAbove j then
𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ ⟨(φs.insertIdx i φ).get,
(signFinset (c.insertList φ φs i (some j)) (finCongr (insertIdx_length_fin φ φs i).symm i)
(signFinset (c.insertList φ 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 (c.insertList φ φs i (some j))
signFinset (c.insertList φ 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,
@ -748,7 +748,7 @@ lemma stat_signFinset_insert_some_self_fst
(φ : 𝓕.States) (φs : List 𝓕.States) (c : WickContraction φs.length)
(i : Fin φs.length.succ) (j : c.uncontracted) :
(𝓕 |>ₛ ⟨(φs.insertIdx i φ).get,
(signFinset (c.insertList φ φs i (some j)) (finCongr (insertIdx_length_fin φ φs i).symm i)
(signFinset (c.insertList φ 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 ∧ ((c.getDual? x = none) ∨
@ -824,7 +824,7 @@ lemma stat_signFinset_insert_some_self_fst
lemma stat_signFinset_insert_some_self_snd (φ : 𝓕.States) (φs : List 𝓕.States)
(c : WickContraction φs.length) (i : Fin φs.length.succ) (j : c.uncontracted) :
(𝓕 |>ₛ ⟨(φs.insertIdx i φ).get,
(signFinset (c.insertList φ φs i (some j))
(signFinset (c.insertList φ 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

@ -30,7 +30,7 @@ noncomputable def timeContract (𝓞 : 𝓕.ProtoOperatorAlgebra) {φs : List
@[simp]
lemma timeContract_insertList_none (𝓞 : 𝓕.ProtoOperatorAlgebra) (φ : 𝓕.States) (φs : List 𝓕.States)
(c : WickContraction φs.length) (i : Fin φs.length.succ) :
(c.insertList φ φs i none).timeContract 𝓞 = c.timeContract 𝓞 := by
(c.insertList φ i none).timeContract 𝓞 = c.timeContract 𝓞 := by
rw [timeContract, insertList_none_prod_contractions]
congr
ext a
@ -38,7 +38,7 @@ lemma timeContract_insertList_none (𝓞 : 𝓕.ProtoOperatorAlgebra) (φ : 𝓕
lemma timeConract_insertList_some (𝓞 : 𝓕.ProtoOperatorAlgebra) (φ : 𝓕.States) (φs : List 𝓕.States)
(c : WickContraction φs.length) (i : Fin φs.length.succ) (j : c.uncontracted) :
(c.insertList φ φs i (some j)).timeContract 𝓞 =
(c.insertList φ 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 _ _⟩) * c.timeContract 𝓞 := by
@ -59,7 +59,7 @@ lemma timeConract_insertList_some_eq_mul_contractStateAtIndex_lt
(𝓞 : 𝓕.ProtoOperatorAlgebra) (φ : 𝓕.States) (φs : List 𝓕.States)
(c : WickContraction φs.length) (i : Fin φs.length.succ) (k : c.uncontracted)
(ht : 𝓕.timeOrderRel φ φs[k.1]) (hik : i < i.succAbove k) :
(c.insertList φ φs i (some k)).timeContract 𝓞 =
(c.insertList φ i (some k)).timeContract 𝓞 =
𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ ⟨φs.get, (c.uncontracted.filter (fun x => x < k))⟩)
• (𝓞.contractStateAtIndex φ (List.map φs.get c.uncontractedList)
((uncontractedStatesEquiv φs c) (some k)) * c.timeContract 𝓞) := by
@ -94,7 +94,7 @@ lemma timeConract_insertList_some_eq_mul_contractStateAtIndex_not_lt
(𝓞 : 𝓕.ProtoOperatorAlgebra) (φ : 𝓕.States) (φs : List 𝓕.States)
(c : WickContraction φs.length) (i : Fin φs.length.succ) (k : c.uncontracted)
(ht : ¬ 𝓕.timeOrderRel φs[k.1] φ) (hik : ¬ i < i.succAbove k) :
(c.insertList φ φs i (some k)).timeContract 𝓞 =
(c.insertList φ i (some k)).timeContract 𝓞 =
𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ ⟨φs.get, (c.uncontracted.filter (fun x => x ≤ k))⟩)
• (𝓞.contractStateAtIndex φ (List.map φs.get c.uncontractedList)
((uncontractedStatesEquiv φs c) (some k)) * c.timeContract 𝓞) := by

75
HepLean/PerturbationTheory/WicksTheorem.lean
View file

@ -27,20 +27,20 @@ open FieldStatistic
/--
Let `c` be a Wick Contraction for `φ₀φ₁…φₙ`.
We have (roughly) `N(c.insertList φ φs i none).uncontractedList = s • N(φ * c.uncontractedList)`
We have (roughly) `N(c.insertList φ i none).uncontractedList = s • N(φ * c.uncontractedList)`
Where `s` is the exchange sign for `φ` and the uncontracted fields in `φ₀φ₁…φᵢ`.
-/
lemma insertList_none_normalOrder (φ : 𝓕.States) (φs : List 𝓕.States)
(i : Fin φs.length.succ) (c : WickContraction φs.length) :
𝓞.crAnF (normalOrder (ofStateList (List.map (φs.insertIdx i φ).get
(c.insertList φ φs i none).uncontractedList)))
𝓞.crAnF (𝓝(ofStateList (List.map (φs.insertIdx i φ).get
(c.insertList φ i none).uncontractedList)))
= 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ ⟨φs.get, c.uncontracted.filter (fun x => i.succAbove x < i)⟩) •
𝓞.crAnF (normalOrder (ofStateList (optionEraseZ (c.uncontractedList.map φs.get) φ none))) := by
𝓞.crAnF (𝓝(ofStateList (optionEraseZ (c.uncontractedList.map φs.get) φ none))) := by
simp only [Nat.succ_eq_add_one, instCommGroup.eq_1, optionEraseZ]
rw [crAnF_ofState_normalOrder_insert φ (c.uncontractedList.map φs.get)
⟨(c.uncontractedListOrderPos i), by simp⟩, smul_smul]
trans (1 : ℂ) • 𝓞.crAnF (normalOrder (ofStateList
(List.map (List.insertIdx (↑i) φ φs).get (insertList φ φs c i none).uncontractedList)))
trans (1 : ℂ) • 𝓞.crAnF (𝓝(ofStateList
(List.map (List.insertIdx (↑i) φ φs).get (insertList φ c i none).uncontractedList)))
· simp
congr 1
simp only [instCommGroup.eq_1]
@ -98,16 +98,16 @@ lemma insertList_none_normalOrder (φ : 𝓕.States) (φs : List 𝓕.States)
/--
Let `c` be a Wick Contraction for `φ₀φ₁…φₙ`.
We have (roughly) `N(c.insertList φ φs i k).uncontractedList`
We have (roughly) `N(c.insertList φ i k).uncontractedList`
is equal to `N((c.uncontractedList).eraseIdx k')`
where `k'` is the position in `c.uncontractedList` corresponding to `k`.
-/
lemma insertList_some_normalOrder (φ : 𝓕.States) (φs : List 𝓕.States)
(i : Fin φs.length.succ) (c : WickContraction φs.length) (k : c.uncontracted) :
𝓞.crAnF (normalOrder (ofStateList (List.map (φs.insertIdx i φ).get
(c.insertList φ φs i (some k)).uncontractedList)))
= 𝓞.crAnF (normalOrder (ofStateList (optionEraseZ (c.uncontractedList.map φs.get) φ
((uncontractedStatesEquiv φs c) k)))) := by
𝓞.crAnF 𝓝(ofStateList (List.map (φs.insertIdx i φ).get
(c.insertList φ i (some k)).uncontractedList))
= 𝓞.crAnF 𝓝(ofStateList (optionEraseZ (c.uncontractedList.map φs.get) φ
((uncontractedStatesEquiv φs c) k))) := by
simp only [Nat.succ_eq_add_one, insertList, optionEraseZ, uncontractedStatesEquiv,
Equiv.optionCongr_apply, Equiv.coe_trans, Option.map_some', Function.comp_apply, finCongr_apply,
Fin.coe_cast]
@ -121,17 +121,17 @@ lemma insertList_some_normalOrder (φ : 𝓕.States) (φs : List 𝓕.States)
/--
Let `c` be a Wick Contraction for `φ₀φ₁…φₙ`.
This lemma states that `(c.sign • c.timeContract 𝓞) * N(c.uncontracted)`
for `c` equal to `c.insertList φ φs i none` is equal to that for just `c`
for `c` equal to `c.insertList φ i none` is equal to that for just `c`
mulitiplied by the exchange sign of `φ` and `φ₀φ₁…φᵢ₋₁`.
-/
lemma sign_timeContract_normalOrder_insertList_none (φ : 𝓕.States) (φs : List 𝓕.States)
(i : Fin φs.length.succ) (c : WickContraction φs.length) :
(c.insertList φ φs i none).sign • (c.insertList φ φs i none).timeContract 𝓞
* 𝓞.crAnF (normalOrder (ofStateList (List.map (φs.insertIdx i φ).get
(c.insertList φ φs i none).uncontractedList))) =
(c.insertList φ i none).sign • (c.insertList φ i none).timeContract 𝓞
* 𝓞.crAnF 𝓝(ofStateList (List.map (φs.insertIdx i φ).get
(c.insertList φ i none).uncontractedList)) =
𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ ⟨φs.get, (Finset.univ.filter (fun k => i.succAbove k < i))⟩)
• (c.sign • c.timeContract 𝓞 * 𝓞.crAnF (normalOrder
(ofStateList (optionEraseZ (c.uncontractedList.map φs.get) φ none)))) := by
• (c.sign • c.timeContract 𝓞 *
𝓞.crAnF 𝓝(ofStateList (optionEraseZ (c.uncontractedList.map φs.get) φ none))) := by
by_cases hg : GradingCompliant φs c
· rw [insertList_none_normalOrder, sign_insert_none]
simp only [Nat.succ_eq_add_one, timeContract_insertList_none, instCommGroup.eq_1,
@ -171,21 +171,21 @@ lemma sign_timeContract_normalOrder_insertList_none (φ : 𝓕.States) (φs : Li
Let `c` be a Wick Contraction for `φ₀φ₁…φₙ`.
This lemma states that
`(c.sign • c.timeContract 𝓞) * N(c.uncontracted)`
for `c` equal to `c.insertList φ φs i (some k)` is equal to that for just `c`
for `c` equal to `c.insertList φ i (some k)` is equal to that for just `c`
mulitiplied by the exchange sign of `φ` and `φ₀φ₁…φᵢ₋₁`.
-/
lemma sign_timeContract_normalOrder_insertList_some (φ : 𝓕.States) (φs : List 𝓕.States)
(i : Fin φs.length.succ) (c : WickContraction φs.length) (k : c.uncontracted)
(hlt : ∀ (k : Fin φs.length), timeOrderRel φ φs[k])
(hn : ∀ (k : Fin φs.length), i.succAbove k < i → ¬ timeOrderRel φs[k] φ) :
(c.insertList φ φs i (some k)).sign • (c.insertList φ φs i (some k)).timeContract 𝓞
* 𝓞.crAnF (normalOrder (ofStateList (List.map (φs.insertIdx i φ).get
(c.insertList φ φs i (some k)).uncontractedList))) =
(c.insertList φ i (some k)).sign • (c.insertList φ i (some k)).timeContract 𝓞
* 𝓞.crAnF 𝓝(ofStateList (List.map (φs.insertIdx i φ).get
(c.insertList φ i (some k)).uncontractedList)) =
𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ ⟨φs.get, (Finset.univ.filter (fun x => i.succAbove x < i))⟩)
• (c.sign • (𝓞.contractStateAtIndex φ (List.map φs.get c.uncontractedList)
((uncontractedStatesEquiv φs c) (some k)) * c.timeContract 𝓞)
* 𝓞.crAnF (normalOrder (ofStateList (optionEraseZ (c.uncontractedList.map φs.get) φ
((uncontractedStatesEquiv φs c) k))))) := by
* 𝓞.crAnF 𝓝(ofStateList (optionEraseZ (c.uncontractedList.map φs.get) φ
((uncontractedStatesEquiv φs c) k)))) := by
by_cases hg : GradingCompliant φs c ∧ (𝓕 |>ₛ φ) = (𝓕 |>ₛ φs[k.1])
· by_cases hk : i.succAbove k < i
· rw [WickContraction.timeConract_insertList_some_eq_mul_contractStateAtIndex_not_lt]
@ -244,19 +244,19 @@ 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.insertList φ φs i k)` for `k : Option (c.uncontracted)`, multiplied by
for all `c' = (c.insertList φ i k)` for `k : Option (c.uncontracted)`, multiplied by
the exchange sign of `φ` and `φ₀φ₁…φᵢ₋₁`.
-/
lemma mul_sum_contractions (φ : 𝓕.States) (φs : List 𝓕.States) (i : Fin φs.length.succ)
(c : WickContraction φs.length) (hlt : ∀ (k : Fin φs.length), timeOrderRel φ φs[k])
(hn : ∀ (k : Fin φs.length), i.succAbove k < i → ¬timeOrderRel φs[k] φ) :
(c.sign • c.timeContract 𝓞) * 𝓞.crAnF ((CrAnAlgebra.ofState φ) *
normalOrder (ofStateList (c.uncontractedList.map φs.get))) =
𝓝(ofStateList (c.uncontractedList.map φs.get))) =
𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ ⟨φs.get, (Finset.univ.filter (fun x => i.succAbove x < i))⟩) •
∑ (k : Option (c.uncontracted)),
((c.insertList φ φs i k).sign • (c.insertList φ φs i k).timeContract 𝓞
* 𝓞.crAnF (normalOrder
(ofStateList ((c.insertList φ φs i k).uncontractedList.map (φs.insertIdx i φ).get)))) := by
((c.insertList φ i k).sign • (c.insertList φ i k).timeContract 𝓞
* 𝓞.crAnF (𝓝(ofStateList
((c.insertList φ i k).uncontractedList.map (φs.insertIdx i φ).get)))) := 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]
@ -287,9 +287,9 @@ lemma mul_sum_contractions (φ : 𝓕.States) (φs : List 𝓕.States) (i : Fin
lemma wicks_theorem_congr {φs φs' : List 𝓕.States} (h : φs = φs') :
∑ (c : WickContraction φs.length), (c.sign • c.timeContract 𝓞) *
𝓞.crAnF (normalOrder (ofStateList (c.uncontractedList.map φs.get)))
𝓞.crAnF 𝓝(ofStateList (c.uncontractedList.map φs.get))
= ∑ (c : WickContraction φs'.length), (c.sign • c.timeContract 𝓞) *
𝓞.crAnF (normalOrder (ofStateList (c.uncontractedList.map φs'.get))) := by
𝓞.crAnF 𝓝(ofStateList (c.uncontractedList.map φs'.get)) := by
subst h
simp
@ -303,7 +303,7 @@ lemma wicks_theorem_congr {φs φs' : List 𝓕.States} (h : φs = φs') :
lemma wicks_theorem_nil :
𝓞.crAnF (ofStateAlgebra (timeOrder (ofList []))) = ∑ (c : WickContraction [].length),
(c.sign [] • c.timeContract 𝓞) *
𝓞.crAnF (normalOrder (ofStateList (c.uncontractedList.map [].get))) := by
𝓞.crAnF 𝓝(ofStateList (c.uncontractedList.map [].get)) := by
rw [timeOrder_ofList_nil]
simp only [map_one, List.length_nil, Algebra.smul_mul_assoc]
rw [sum_WickContraction_nil, nil_zero_uncontractedList]
@ -330,7 +330,7 @@ remark wicks_theorem_context := "
-/
theorem wicks_theorem : (φs : List 𝓕.States) → 𝓞.crAnF (ofStateAlgebra (timeOrder (ofList φs))) =
∑ (c : WickContraction φs.length), (c.sign φs • c.timeContract 𝓞) *
𝓞.crAnF (normalOrder (ofStateList (c.uncontractedList.map φs.get)))
𝓞.crAnF 𝓝(ofStateList (c.uncontractedList.map φs.get))
| [] => wicks_theorem_nil
| φ :: φs => by
have ih := wicks_theorem (eraseMaxTimeField φ φs)
@ -351,13 +351,12 @@ 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))
(insertList (maxTimeField φ φs) (eraseMaxTimeField φ φs) c (maxTimeFieldPosFin φ φs) k) •
↑(WickContraction.timeContract 𝓞 (insertList (maxTimeField φ φs) (eraseMaxTimeField φ φs) c
(maxTimeFieldPosFin φ φs) k)) *
𝓞.crAnF (normalOrder (ofStateList (List.map (List.insertIdx (↑(maxTimeFieldPosFin φ φs))
(insertList (maxTimeField φ φs) c (maxTimeFieldPosFin φ φs) k) •
↑((c.insertList (maxTimeField φ φs) (maxTimeFieldPosFin φ φs) k).timeContract 𝓞) *
𝓞.crAnF 𝓝(ofStateList (List.map (List.insertIdx (↑(maxTimeFieldPosFin φ φs))
(maxTimeField φ φs) (eraseMaxTimeField φ φs)).get
(insertList (maxTimeField φ φs) (eraseMaxTimeField φ φs) c
(maxTimeFieldPosFin φ φs) k).uncontractedList)))
(insertList (maxTimeField φ φs) c
(maxTimeFieldPosFin φ φs) k).uncontractedList))
swap
· simp
rw [smul_smul]