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

Merge pull request #307 from HEPLean/FieldOpAlgebra

Browse source 
feat: Wick's theorem for normal ordered lists
This commit is contained in:
Joseph Tooby-Smith 2025-02-03 06:31:58 +00:00 • committed by GitHub
commit 57c7b5a8f0
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
18 changed files with 2703 additions and 16 deletions
Download patch file Download diff file Expand all files Collapse all files

5
HepLean.lean
View file

@ -133,6 +133,7 @@ import HepLean.PerturbationTheory.Algebras.FieldOpAlgebra.StaticWickTheorem
import HepLean.PerturbationTheory.Algebras.FieldOpAlgebra.SuperCommute
import HepLean.PerturbationTheory.Algebras.FieldOpAlgebra.TimeContraction
import HepLean.PerturbationTheory.Algebras.FieldOpAlgebra.TimeOrder
import HepLean.PerturbationTheory.Algebras.FieldOpAlgebra.WicksTheoremNormal
import HepLean.PerturbationTheory.CreateAnnihilate
import HepLean.PerturbationTheory.FeynmanDiagrams.Basic
import HepLean.PerturbationTheory.FeynmanDiagrams.Instances.ComplexScalar
@ -157,8 +158,12 @@ import HepLean.PerturbationTheory.WickContraction.InsertAndContract
import HepLean.PerturbationTheory.WickContraction.InsertAndContractNat
import HepLean.PerturbationTheory.WickContraction.Involutions
import HepLean.PerturbationTheory.WickContraction.IsFull
import HepLean.PerturbationTheory.WickContraction.Join
import HepLean.PerturbationTheory.WickContraction.Sign
import HepLean.PerturbationTheory.WickContraction.Singleton
import HepLean.PerturbationTheory.WickContraction.StaticContract
import HepLean.PerturbationTheory.WickContraction.SubContraction
import HepLean.PerturbationTheory.WickContraction.TimeCond
import HepLean.PerturbationTheory.WickContraction.TimeContract
import HepLean.PerturbationTheory.WickContraction.Uncontracted
import HepLean.PerturbationTheory.WickContraction.UncontractedList

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

@ -52,6 +52,67 @@ lemma normalOrderF_one : normalOrderF (𝓕 := 𝓕) 1 = 1 := by
rw [← ofCrAnList_nil, normalOrderF_ofCrAnList, normalOrderSign_nil, normalOrderList_nil,
ofCrAnList_nil, one_smul]
lemma normalOrderF_normalOrderF_mid (a b c : 𝓕.CrAnAlgebra) :
𝓝ᶠ(a * b * c) = 𝓝ᶠ(a * 𝓝ᶠ(b) * c) := by
let pc (c : 𝓕.CrAnAlgebra) (hc : c ∈ Submodule.span ℂ (Set.range ofCrAnListBasis)) :
Prop := 𝓝ᶠ(a * b * c) = 𝓝ᶠ(a * 𝓝ᶠ(b) * c)
change pc c (Basis.mem_span _ c)
apply Submodule.span_induction
· intro x hx
obtain ⟨φs, rfl⟩ := hx
simp only [ofListBasis_eq_ofList, pc]
let pb (b : 𝓕.CrAnAlgebra) (hb : b ∈ Submodule.span ℂ (Set.range ofCrAnListBasis)) :
Prop := 𝓝ᶠ(a * b * ofCrAnList φs) = 𝓝ᶠ(a * 𝓝ᶠ(b) * ofCrAnList φs)
change pb b (Basis.mem_span _ b)
apply Submodule.span_induction
· intro x hx
obtain ⟨φs', rfl⟩ := hx
simp only [ofListBasis_eq_ofList, pb]
let pa (a : 𝓕.CrAnAlgebra) (ha : a ∈ Submodule.span ℂ (Set.range ofCrAnListBasis)) :
Prop := 𝓝ᶠ(a * ofCrAnList φs' * ofCrAnList φs) = 𝓝ᶠ(a * 𝓝ᶠ(ofCrAnList φs') * ofCrAnList φs)
change pa a (Basis.mem_span _ a)
apply Submodule.span_induction
· intro x hx
obtain ⟨φs'', rfl⟩ := hx
simp only [ofListBasis_eq_ofList, pa]
rw [normalOrderF_ofCrAnList]
simp only [← ofCrAnList_append, Algebra.mul_smul_comm,
Algebra.smul_mul_assoc, map_smul]
rw [normalOrderF_ofCrAnList, normalOrderF_ofCrAnList, smul_smul]
congr 1
· simp only [normalOrderSign, normalOrderList]
rw [Wick.koszulSign_of_append_eq_insertionSort, mul_comm]
· congr 1
simp only [normalOrderList]
rw [HepLean.List.insertionSort_append_insertionSort_append]
· simp [pa]
· intro x y hx hy h1 h2
simp_all [pa, add_mul]
· intro x hx h
simp_all [pa]
· simp [pb]
· intro x y hx hy h1 h2
simp_all [pb, mul_add, add_mul]
· intro x hx h
simp_all [pb]
· simp [pc]
· intro x y hx hy h1 h2
simp_all [pc, mul_add]
· intro x hx h hp
simp_all [pc]
lemma normalOrderF_normalOrderF_right (a b : 𝓕.CrAnAlgebra) : 𝓝ᶠ(a * b) = 𝓝ᶠ(a * 𝓝ᶠ(b)) := by
trans 𝓝ᶠ(a * b * 1)
· simp
· rw [normalOrderF_normalOrderF_mid]
simp
lemma normalOrderF_normalOrderF_left (a b : 𝓕.CrAnAlgebra) : 𝓝ᶠ(a * b) = 𝓝ᶠ(𝓝ᶠ(a) * b) := by
trans 𝓝ᶠ(1 * a * b)
· simp
· rw [normalOrderF_normalOrderF_mid]
simp
/-!
## Normal ordering with a creation operator on the left or annihilation on the right

43
HepLean/PerturbationTheory/Algebras/FieldOpAlgebra/NormalOrder.lean
View file

@ -261,6 +261,43 @@ lemma ofCrAnFieldOpList_eq_normalOrder (φs : List 𝓕.CrAnStates) :
rw [normalOrder_ofCrAnFieldOpList, smul_smul, normalOrderSign, Wick.koszulSign_mul_self,
one_smul]
lemma normalOrder_normalOrder_mid (a b c : 𝓕.FieldOpAlgebra) :
𝓝(a * b * c) = 𝓝(a * 𝓝(b) * c) := by
obtain ⟨a, rfl⟩ := ι_surjective a
obtain ⟨b, rfl⟩ := ι_surjective b
obtain ⟨c, rfl⟩ := ι_surjective c
rw [normalOrder_eq_ι_normalOrderF]
simp only [← map_mul]
rw [normalOrder_eq_ι_normalOrderF]
rw [normalOrderF_normalOrderF_mid]
rfl
lemma normalOrder_normalOrder_left (a b : 𝓕.FieldOpAlgebra) :
𝓝(a * b) = 𝓝(𝓝(a) * b) := by
obtain ⟨a, rfl⟩ := ι_surjective a
obtain ⟨b, rfl⟩ := ι_surjective b
rw [normalOrder_eq_ι_normalOrderF]
simp only [← map_mul]
rw [normalOrder_eq_ι_normalOrderF]
rw [normalOrderF_normalOrderF_left]
rfl
lemma normalOrder_normalOrder_right (a b : 𝓕.FieldOpAlgebra) :
𝓝(a * b) = 𝓝(a * 𝓝(b)) := by
obtain ⟨a, rfl⟩ := ι_surjective a
obtain ⟨b, rfl⟩ := ι_surjective b
rw [normalOrder_eq_ι_normalOrderF]
simp only [← map_mul]
rw [normalOrder_eq_ι_normalOrderF]
rw [normalOrderF_normalOrderF_right]
rfl
lemma normalOrder_normalOrder (a : 𝓕.FieldOpAlgebra) : 𝓝(𝓝(a)) = 𝓝(a) := by
trans 𝓝(𝓝(a) * 1)
· simp
· rw [← normalOrder_normalOrder_left]
simp
/-!
## mul anpart and crpart
@ -466,7 +503,7 @@ lemma anPart_mul_normalOrder_ofFieldOpList_eq_superCommute_reorder (φ : 𝓕.St
(φs : List 𝓕.States) : anPart φ * 𝓝(ofFieldOpList φs) =
𝓝(anPart φ * ofFieldOpList φs) + [anPart φ, 𝓝(ofFieldOpList φs)]ₛ := by
rw [anPart_mul_normalOrder_ofFieldOpList_eq_superCommute]
simp [instCommGroup.eq_1, map_add, map_smul]
simp only [instCommGroup.eq_1, add_left_inj]
rw [normalOrder_anPart_ofFieldOpList_swap]
/--
@ -525,8 +562,8 @@ lemma ofFieldOpList_normalOrder_insert (φ : 𝓕.States) (φs : List 𝓕.State
rw [hl]
rw [ofFieldOpList_append, ofFieldOpList_append]
rw [ofFieldOpList_mul_ofFieldOpList_eq_superCommute, add_mul]
simp [instCommGroup.eq_1, Nat.succ_eq_add_one, ofList_singleton, Algebra.smul_mul_assoc,
map_add, map_smul, add_zero, smul_smul,
simp only [instCommGroup.eq_1, Nat.succ_eq_add_one, ofList_singleton, Algebra.smul_mul_assoc,
map_add, map_smul, normalOrder_superCommute_left_eq_zero, add_zero, smul_smul,
exchangeSign_mul_self_swap, one_smul]
rw [← ofFieldOpList_append, ← ofFieldOpList_append]
simp

21
HepLean/PerturbationTheory/Algebras/FieldOpAlgebra/StaticWickTheorem.lean
View file

@ -34,15 +34,15 @@ theorem static_wick_theorem : (φs : List 𝓕.States) →
| φ :: φs => by
rw [ofFieldOpList_cons]
rw [static_wick_theorem φs]
rw [show (φ :: φs) = φs.insertIdx (⟨0, Nat.zero_lt_succ φs.length⟩ : Fin φs.length.succ) φ
rw [show (φ :: φs) = φs.insertIdx (⟨0, Nat.zero_lt_succ φs.length⟩ : Fin φs.length.succ) φ
from rfl]
conv_rhs => rw [insertLift_sum ]
conv_rhs => rw [insertLift_sum]
rw [Finset.mul_sum]
apply Finset.sum_congr rfl
intro c _
trans (sign φs c • ↑c.staticContract * (ofFieldOp φ * normalOrder (ofFieldOpList [c]ᵘᶜ)))
trans (sign φs c • ↑c.staticContract * (ofFieldOp φ * normalOrder (ofFieldOpList [c]ᵘᶜ)))
· have ht := Subalgebra.mem_center_iff.mp (Subalgebra.smul_mem (Subalgebra.center ℂ _)
(c.staticContract).2 c.sign )
(c.staticContract).2 c.sign)
conv_rhs => rw [← mul_assoc, ← ht]
simp [mul_assoc]
rw [ofFieldOp_mul_normalOrder_ofFieldOpList_eq_sum]
@ -61,7 +61,7 @@ theorem static_wick_theorem : (φs : List 𝓕.States) →
simp only [Algebra.smul_mul_assoc, Nat.succ_eq_add_one, Fin.zero_eta, Fin.val_zero,
List.insertIdx_zero]
rw [normalOrder_uncontracted_some]
simp [← mul_assoc]
simp only [← mul_assoc]
rw [← smul_mul_assoc]
conv_rhs => rw [← smul_mul_assoc]
congr 1
@ -69,7 +69,7 @@ theorem static_wick_theorem : (φs : List 𝓕.States) →
swap
· simp
rw [smul_smul]
by_cases hn : GradingCompliant φs c ∧ (𝓕|>ₛφ) = (𝓕|>ₛ φs[n.1])
by_cases hn : GradingCompliant φs c ∧ (𝓕|>ₛφ) = (𝓕|>ₛ φs[n.1])
· congr 1
swap
· have h1 := c.staticContract.2
@ -82,19 +82,20 @@ theorem static_wick_theorem : (φs : List 𝓕.States) →
ofFinset_empty, map_one, one_mul]
simp only [Fin.zero_succAbove, Fin.not_lt_zero, not_false_eq_true]
exact hn
· simp at hn
· simp only [Fin.getElem_fin, not_and] at hn
by_cases h0 : ¬ GradingCompliant φs c
· rw [staticContract_of_not_gradingCompliant]
simp only [ZeroMemClass.coe_zero, zero_mul, smul_zero, instCommGroup.eq_1, mul_zero]
exact h0
· simp_all
have h1 : contractStateAtIndex φ [c]ᵘᶜ
· simp_all only [Finset.mem_univ, not_not, instCommGroup.eq_1, forall_const]
have h1 : contractStateAtIndex φ [c]ᵘᶜ
((uncontractedStatesEquiv φs c) (some n)) = 0 := by
simp only [contractStateAtIndex, uncontractedStatesEquiv, Equiv.optionCongr_apply,
Equiv.coe_trans, Option.map_some', Function.comp_apply, finCongr_apply,
instCommGroup.eq_1, Fin.coe_cast, Fin.getElem_fin, smul_eq_zero]
right
simp [uncontractedListGet]
simp only [uncontractedListGet, List.getElem_map,
uncontractedList_getElem_uncontractedIndexEquiv_symm, List.get_eq_getElem]
rw [superCommute_anPart_ofState_diff_grade_zero]
exact hn
rw [h1]

91
HepLean/PerturbationTheory/Algebras/FieldOpAlgebra/TimeContraction.lean
View file

@ -55,6 +55,13 @@ lemma timeContract_of_not_timeOrderRel (φ ψ : 𝓕.States) (h : ¬ timeOrderRe
simp only [instCommGroup.eq_1, map_smul, map_add, smul_add]
rw [smul_smul, smul_smul, mul_comm]
lemma timeContract_of_not_timeOrderRel_expand (φ ψ : 𝓕.States) (h : ¬ timeOrderRel φ ψ) :
timeContract φ ψ = 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ ψ) • [anPart ψ, ofFieldOp φ]ₛ := by
rw [timeContract_of_not_timeOrderRel _ _ h]
rw [timeContract_of_timeOrderRel _ _ _]
have h1 := IsTotal.total (r := 𝓕.timeOrderRel) φ ψ
simp_all
lemma timeContract_mem_center (φ ψ : 𝓕.States) :
timeContract φ ψ ∈ Subalgebra.center ℂ 𝓕.FieldOpAlgebra := by
by_cases h : timeOrderRel φ ψ
@ -81,6 +88,90 @@ lemma timeContract_zero_of_diff_grade (φ ψ : 𝓕.States) (h : (𝓕 |>ₛ φ)
have ht := IsTotal.total (r := 𝓕.timeOrderRel) φ ψ
simp_all
lemma normalOrder_timeContract (φ ψ : 𝓕.States) :
𝓝(timeContract φ ψ) = 0 := by
by_cases h : timeOrderRel φ ψ
· rw [timeContract_of_timeOrderRel _ _ h]
simp
· rw [timeContract_of_not_timeOrderRel _ _ h]
simp only [instCommGroup.eq_1, map_smul, smul_eq_zero]
have h1 : timeOrderRel ψ φ := by
have ht : timeOrderRel φ ψ ∨ timeOrderRel ψ φ := IsTotal.total (r := 𝓕.timeOrderRel) φ ψ
simp_all
rw [timeContract_of_timeOrderRel _ _ h1]
simp
lemma timeOrder_timeContract_eq_time_mid {φ ψ : 𝓕.States}
(h1 : timeOrderRel φ ψ) (h2 : timeOrderRel ψ φ) (a b : 𝓕.FieldOpAlgebra) :
𝓣(a * timeContract φ ψ * b) = timeContract φ ψ * 𝓣(a * b) := by
rw [timeContract_of_timeOrderRel _ _ h1]
rw [ofFieldOp_eq_sum]
simp only [map_sum, Finset.mul_sum, Finset.sum_mul]
congr
funext x
match φ with
| .inAsymp φ =>
simp
| .position φ =>
simp only [anPart_position, instCommGroup.eq_1]
apply timeOrder_superCommute_eq_time_mid _ _
simp only [crAnTimeOrderRel, h1]
simp [crAnTimeOrderRel, h2]
| .outAsymp φ =>
simp only [anPart_posAsymp, instCommGroup.eq_1]
apply timeOrder_superCommute_eq_time_mid _ _
simp only [crAnTimeOrderRel, h1]
simp [crAnTimeOrderRel, h2]
lemma timeOrder_timeContract_eq_time_left {φ ψ : 𝓕.States}
(h1 : timeOrderRel φ ψ) (h2 : timeOrderRel ψ φ) (b : 𝓕.FieldOpAlgebra) :
𝓣(timeContract φ ψ * b) = timeContract φ ψ * 𝓣(b) := by
trans 𝓣(1 * timeContract φ ψ * b)
simp only [one_mul]
rw [timeOrder_timeContract_eq_time_mid h1 h2]
simp
lemma timeOrder_timeContract_neq_time {φ ψ : 𝓕.States}
(h1 : ¬ (timeOrderRel φ ψ ∧ timeOrderRel ψ φ)) :
𝓣(timeContract φ ψ) = 0 := by
by_cases h2 : timeOrderRel φ ψ
· simp_all only [true_and]
rw [timeContract_of_timeOrderRel _ _ h2]
simp only
rw [ofFieldOp_eq_sum]
simp only [map_sum]
apply Finset.sum_eq_zero
intro x hx
match φ with
| .inAsymp φ =>
simp
| .position φ =>
simp only [anPart_position, instCommGroup.eq_1]
apply timeOrder_superCommute_neq_time
simp_all [crAnTimeOrderRel]
| .outAsymp φ =>
simp only [anPart_posAsymp, instCommGroup.eq_1]
apply timeOrder_superCommute_neq_time
simp_all [crAnTimeOrderRel]
· rw [timeContract_of_not_timeOrderRel_expand _ _ h2]
simp only [instCommGroup.eq_1, map_smul, smul_eq_zero]
right
rw [ofFieldOp_eq_sum]
simp only [map_sum]
apply Finset.sum_eq_zero
intro x hx
match ψ with
| .inAsymp ψ =>
simp
| .position ψ =>
simp only [anPart_position, instCommGroup.eq_1]
apply timeOrder_superCommute_neq_time
simp_all [crAnTimeOrderRel]
| .outAsymp ψ =>
simp only [anPart_posAsymp, instCommGroup.eq_1]
apply timeOrder_superCommute_neq_time
simp_all [crAnTimeOrderRel]
end FieldOpAlgebra
end

77
HepLean/PerturbationTheory/Algebras/FieldOpAlgebra/TimeOrder.lean
View file

@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import HepLean.PerturbationTheory.Algebras.CrAnAlgebra.TimeOrder
import HepLean.PerturbationTheory.Algebras.FieldOpAlgebra.Basic
import HepLean.PerturbationTheory.Algebras.FieldOpAlgebra.SuperCommute
/-!
# Time Ordering on Field operator algebra
@ -429,5 +429,80 @@ lemma timeOrder_eq_maxTimeField_mul_finset (φ : 𝓕.States) (φs : List 𝓕.S
rw [ofFieldOpList, timeOrder_eq_ι_timeOrderF, timeOrderF_eq_maxTimeField_mul_finset]
rfl
lemma timeOrder_superCommute_eq_time_mid {φ ψ : 𝓕.CrAnStates}
(hφψ : crAnTimeOrderRel φ ψ) (hψφ : crAnTimeOrderRel ψ φ) (a b : 𝓕.FieldOpAlgebra) :
𝓣(a * [ofCrAnFieldOp φ, ofCrAnFieldOp ψ]ₛ * b) =
[ofCrAnFieldOp φ, ofCrAnFieldOp ψ]ₛ * 𝓣(a * b) := by
rw [ofCrAnFieldOp, ofCrAnFieldOp]
rw [superCommute_eq_ι_superCommuteF]
obtain ⟨a, rfl⟩ := ι_surjective a
obtain ⟨b, rfl⟩ := ι_surjective b
rw [← map_mul, ← map_mul, timeOrder_eq_ι_timeOrderF]
rw [ι_timeOrderF_superCommuteF_eq_time]
rfl
· simp_all
· simp_all
lemma timeOrder_superCommute_eq_time_left {φ ψ : 𝓕.CrAnStates}
(hφψ : crAnTimeOrderRel φ ψ) (hψφ : crAnTimeOrderRel ψ φ) (b : 𝓕.FieldOpAlgebra) :
𝓣([ofCrAnFieldOp φ, ofCrAnFieldOp ψ]ₛ * b) =
[ofCrAnFieldOp φ, ofCrAnFieldOp ψ]ₛ * 𝓣(b) := by
trans 𝓣(1 * [ofCrAnFieldOp φ, ofCrAnFieldOp ψ]ₛ * b)
simp only [one_mul]
rw [timeOrder_superCommute_eq_time_mid hφψ hψφ]
simp
lemma timeOrder_superCommute_neq_time {φ ψ : 𝓕.CrAnStates}
(hφψ : ¬ (crAnTimeOrderRel φ ψ ∧ crAnTimeOrderRel ψ φ)) :
𝓣([ofCrAnFieldOp φ, ofCrAnFieldOp ψ]ₛ) = 0 := by
rw [ofCrAnFieldOp, ofCrAnFieldOp]
rw [superCommute_eq_ι_superCommuteF]
rw [timeOrder_eq_ι_timeOrderF]
trans ι (timeOrderF (1 * (superCommuteF (ofCrAnState φ)) (ofCrAnState ψ) * 1))
simp only [one_mul, mul_one]
rw [ι_timeOrderF_superCommuteF_neq_time]
exact hφψ
lemma timeOrder_superCommute_anPart_ofFieldOp_neq_time {φ ψ : 𝓕.States}
(hφψ : ¬ (timeOrderRel φ ψ ∧ timeOrderRel ψ φ)) :
𝓣([anPart φ,ofFieldOp ψ]ₛ) = 0 := by
rw [ofFieldOp_eq_sum]
simp only [map_sum]
apply Finset.sum_eq_zero
intro a ha
match φ with
| .inAsymp φ =>
simp
| .position φ =>
simp only [anPart_position, instCommGroup.eq_1]
apply timeOrder_superCommute_neq_time
simp_all [crAnTimeOrderRel]
| .outAsymp φ =>
simp only [anPart_posAsymp, instCommGroup.eq_1]
apply timeOrder_superCommute_neq_time
simp_all [crAnTimeOrderRel]
lemma timeOrder_timeOrder_mid (a b c : 𝓕.FieldOpAlgebra) :
𝓣(a * b * c) = 𝓣(a * 𝓣(b) * c) := by
obtain ⟨a, rfl⟩ := ι_surjective a
obtain ⟨b, rfl⟩ := ι_surjective b
obtain ⟨c, rfl⟩ := ι_surjective c
rw [← map_mul, ← map_mul, timeOrder_eq_ι_timeOrderF, timeOrder_eq_ι_timeOrderF,
← map_mul, ← map_mul, timeOrder_eq_ι_timeOrderF, timeOrderF_timeOrderF_mid]
lemma timeOrder_timeOrder_left (b c : 𝓕.FieldOpAlgebra) :
𝓣(b * c) = 𝓣(𝓣(b) * c) := by
trans 𝓣(1 * b * c)
simp only [one_mul]
rw [timeOrder_timeOrder_mid]
simp
lemma timeOrder_timeOrder_right (a b : 𝓕.FieldOpAlgebra) :
𝓣(a * b) = 𝓣(a * 𝓣(b)) := by
trans 𝓣(a * b * 1)
simp only [mul_one]
rw [timeOrder_timeOrder_mid]
simp
end FieldOpAlgebra
end FieldSpecification

201
HepLean/PerturbationTheory/Algebras/FieldOpAlgebra/WicksTheoremNormal.lean Normal file
View file

@ -0,0 +1,201 @@
/-
Copyright (c) 2025 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.WickContraction.TimeCond
import HepLean.PerturbationTheory.Algebras.FieldOpAlgebra.StaticWickTheorem
import HepLean.Meta.Remark.Basic
/-!
# Wick's theorem for normal ordered lists
-/
namespace FieldSpecification
variable {𝓕 : FieldSpecification}
open CrAnAlgebra
namespace FieldOpAlgebra
open WickContraction
open EqTimeOnly
lemma timeOrder_ofFieldOpList_eqTimeOnly (φs : List 𝓕.States) :
timeOrder (ofFieldOpList φs) = ∑ (φsΛ : {φsΛ // φsΛ.EqTimeOnly (φs := φs)}),
φsΛ.1.sign • φsΛ.1.timeContract.1 * 𝓣(𝓝(ofFieldOpList [φsΛ.1]ᵘᶜ)) := by
rw [static_wick_theorem φs]
let e2 : WickContraction φs.length ≃
{φsΛ : WickContraction φs.length // φsΛ.EqTimeOnly} ⊕
{φsΛ : WickContraction φs.length // ¬ φsΛ.EqTimeOnly} :=
(Equiv.sumCompl _).symm
rw [← e2.symm.sum_comp]
simp only [Equiv.symm_symm, Algebra.smul_mul_assoc, Fintype.sum_sum_type,
Equiv.sumCompl_apply_inl, Equiv.sumCompl_apply_inr, map_add, map_sum, map_smul, e2]
conv_lhs =>
enter [2, 2, x]
rw [timeOrder_timeOrder_left]
rw [timeOrder_staticContract_of_not_mem _ x.2]
simp only [Finset.univ_eq_attach, zero_mul, map_zero, smul_zero, Finset.sum_const_zero, add_zero]
congr
funext x
rw [staticContract_eq_timeContract_of_eqTimeOnly]
rw [timeOrder_timeContract_mul_of_eqTimeOnly_left]
exact x.2
exact x.2
lemma timeOrder_ofFieldOpList_eq_eqTimeOnly_empty (φs : List 𝓕.States) :
timeOrder (ofFieldOpList φs) = 𝓣(𝓝(ofFieldOpList φs)) +
∑ (φsΛ : {φsΛ // φsΛ.EqTimeOnly (φs := φs) ∧ φsΛ ≠ empty}),
φsΛ.1.sign • φsΛ.1.timeContract.1 * 𝓣(𝓝(ofFieldOpList [φsΛ.1]ᵘᶜ)) := by
let e1 : {φsΛ : WickContraction φs.length // φsΛ.EqTimeOnly} ≃
{φsΛ : {φsΛ : WickContraction φs.length // φsΛ.EqTimeOnly} // φsΛ.1 = empty} ⊕
{φsΛ : {φsΛ : WickContraction φs.length // φsΛ.EqTimeOnly} // ¬ φsΛ.1 = empty} :=
(Equiv.sumCompl _).symm
rw [timeOrder_ofFieldOpList_eqTimeOnly, ← e1.symm.sum_comp]
simp only [Equiv.symm_symm, Algebra.smul_mul_assoc, Fintype.sum_sum_type,
Equiv.sumCompl_apply_inl, Equiv.sumCompl_apply_inr, ne_eq, e1]
congr 1
· let e2 : {φsΛ : {φsΛ : WickContraction φs.length // φsΛ.EqTimeOnly} // φsΛ.1 = empty } ≃
Unit := {
toFun := fun x => (), invFun := fun x => ⟨⟨empty, by simp⟩, rfl⟩,
left_inv a := by
ext
simp [a.2], right_inv a := by simp}
rw [← e2.symm.sum_comp]
simp [e2, sign_empty]
· let e2 : { φsΛ : {φsΛ : WickContraction φs.length // φsΛ.EqTimeOnly} // ¬ φsΛ.1 = empty } ≃
{φsΛ // φsΛ.EqTimeOnly ∧ φsΛ ≠ empty} := {
toFun := fun x => ⟨x, ⟨x.1.2, x.2⟩⟩, invFun := fun x => ⟨⟨x.1, x.2.1⟩, x.2.2⟩,
left_inv a := by rfl, right_inv a := by rfl }
rw [← e2.symm.sum_comp]
rfl
lemma normalOrder_timeOrder_ofFieldOpList_eq_eqTimeOnly_empty (φs : List 𝓕.States) :
𝓣(𝓝(ofFieldOpList φs)) = 𝓣(ofFieldOpList φs) -
∑ (φsΛ : {φsΛ // φsΛ.EqTimeOnly (φs := φs) ∧ φsΛ ≠ empty}),
φsΛ.1.sign • φsΛ.1.timeContract.1 * 𝓣(𝓝(ofFieldOpList [φsΛ.1]ᵘᶜ)) := by
rw [timeOrder_ofFieldOpList_eq_eqTimeOnly_empty]
simp
lemma normalOrder_timeOrder_ofFieldOpList_eq_haveEqTime_sum_not_haveEqTime (φs : List 𝓕.States) :
𝓣(𝓝(ofFieldOpList φs)) = (∑ (φsΛ : {φsΛ : WickContraction φs.length // ¬ HaveEqTime φsΛ}),
φsΛ.1.sign • φsΛ.1.timeContract.1 * 𝓝(ofFieldOpList [φsΛ.1]ᵘᶜ))
+ (∑ (φsΛ : {φsΛ : WickContraction φs.length // HaveEqTime φsΛ}),
φsΛ.1.sign • φsΛ.1.timeContract.1 * 𝓝(ofFieldOpList [φsΛ.1]ᵘᶜ))
- ∑ (φsΛ : {φsΛ // φsΛ.EqTimeOnly (φs := φs) ∧ φsΛ ≠ empty}),
φsΛ.1.sign • φsΛ.1.timeContract.1 * 𝓣(𝓝(ofFieldOpList [φsΛ.1]ᵘᶜ)) := by
rw [normalOrder_timeOrder_ofFieldOpList_eq_eqTimeOnly_empty]
rw [wicks_theorem]
let e1 : WickContraction φs.length ≃ {φsΛ // HaveEqTime φsΛ} ⊕ {φsΛ // ¬ HaveEqTime φsΛ} := by
exact (Equiv.sumCompl HaveEqTime).symm
rw [← e1.symm.sum_comp]
simp only [Equiv.symm_symm, Algebra.smul_mul_assoc, Fintype.sum_sum_type,
Equiv.sumCompl_apply_inl, Equiv.sumCompl_apply_inr, ne_eq, sub_left_inj, e1]
rw [add_comm]
lemma haveEqTime_wick_sum_eq_split (φs : List 𝓕.States) :
(∑ (φsΛ : {φsΛ : WickContraction φs.length // HaveEqTime φsΛ}),
φsΛ.1.sign • φsΛ.1.timeContract.1 * 𝓝(ofFieldOpList [φsΛ.1]ᵘᶜ)) =
∑ (φsΛ : {φsΛ // φsΛ.EqTimeOnly (φs := φs) ∧ φsΛ ≠ empty}),
(sign φs ↑φsΛ • (φsΛ.1).timeContract *
∑ φssucΛ : { φssucΛ : WickContraction [φsΛ.1]ᵘᶜ.length // ¬φssucΛ.HaveEqTime },
sign [φsΛ.1]ᵘᶜ φssucΛ •
(φssucΛ.1).timeContract * normalOrder (ofFieldOpList [φssucΛ.1]ᵘᶜ)) := by
let f : WickContraction φs.length → 𝓕.FieldOpAlgebra := fun φsΛ =>
φsΛ.sign • φsΛ.timeContract.1 * 𝓝(ofFieldOpList [φsΛ]ᵘᶜ)
change ∑ (φsΛ : {φsΛ : WickContraction φs.length // HaveEqTime φsΛ}), f φsΛ.1 = _
rw [sum_haveEqTime]
congr
funext φsΛ
simp only [f]
conv_lhs =>
enter [2, φsucΛ]
enter [1]
rw [join_sign_timeContract φsΛ.1 φsucΛ.1]
conv_lhs =>
enter [2, φsucΛ]
rw [mul_assoc]
rw [← Finset.mul_sum]
congr
funext φsΛ'
simp only [ne_eq, Algebra.smul_mul_assoc]
congr 1
rw [@join_uncontractedListGet]
lemma normalOrder_timeOrder_ofFieldOpList_eq_not_haveEqTime_sub_inductive (φs : List 𝓕.States) :
𝓣(𝓝(ofFieldOpList φs)) = (∑ (φsΛ : {φsΛ : WickContraction φs.length // ¬ HaveEqTime φsΛ}),
φsΛ.1.sign • φsΛ.1.timeContract.1 * 𝓝(ofFieldOpList [φsΛ.1]ᵘᶜ))
+ ∑ (φsΛ : {φsΛ // φsΛ.EqTimeOnly (φs := φs) ∧ φsΛ ≠ empty}),
sign φs ↑φsΛ • (φsΛ.1).timeContract *
(∑ φssucΛ : { φssucΛ : WickContraction [φsΛ.1]ᵘᶜ.length // ¬ φssucΛ.HaveEqTime },
sign [φsΛ.1]ᵘᶜ φssucΛ • (φssucΛ.1).timeContract * normalOrder (ofFieldOpList [φssucΛ.1]ᵘᶜ) -
𝓣(𝓝(ofFieldOpList [φsΛ.1]ᵘᶜ))) := by
rw [normalOrder_timeOrder_ofFieldOpList_eq_haveEqTime_sum_not_haveEqTime]
rw [add_sub_assoc]
congr 1
rw [haveEqTime_wick_sum_eq_split]
simp only [ne_eq, Algebra.smul_mul_assoc]
rw [← Finset.sum_sub_distrib]
congr 1
funext x
simp only
rw [← smul_sub, ← mul_sub]
lemma wicks_theorem_normal_order_empty : 𝓣(𝓝(ofFieldOpList [])) =
∑ (φsΛ : {φsΛ : WickContraction ([] : List 𝓕.States).length // ¬ HaveEqTime φsΛ}),
φsΛ.1.sign • φsΛ.1.timeContract.1 * 𝓝(ofFieldOpList [φsΛ.1]ᵘᶜ) := by
let e2 : {φsΛ : WickContraction ([] : List 𝓕.States).length // ¬ HaveEqTime φsΛ} ≃ Unit :=
{
toFun := fun x => (),
invFun := fun x => ⟨empty, by simp⟩,
left_inv := by
intro a
simp only [List.length_nil]
apply Subtype.eq
apply Subtype.eq
simp only [empty]
ext i
simp only [Finset.not_mem_empty, false_iff]
by_contra hn
have h2 := a.1.2.1 i hn
rw [@Finset.card_eq_two] at h2
obtain ⟨a, b, ha, hb, hab⟩ := h2
exact Fin.elim0 a,
right_inv := by intro a; simp}
rw [← e2.symm.sum_comp]
simp only [Finset.univ_unique, PUnit.default_eq_unit, List.length_nil, Equiv.coe_fn_symm_mk,
sign_empty, timeContract_empty, OneMemClass.coe_one, one_smul, uncontractedListGet_empty,
one_mul, Finset.sum_const, Finset.card_singleton, e2]
have h1' : ofFieldOpList (𝓕 := 𝓕) [] = ofCrAnFieldOpList [] := by rfl
rw [h1']
rw [normalOrder_ofCrAnFieldOpList]
simp only [normalOrderSign_nil, normalOrderList_nil, one_smul]
rw [ofCrAnFieldOpList, timeOrder_eq_ι_timeOrderF]
rw [timeOrderF_ofCrAnList]
simp
theorem wicks_theorem_normal_order : (φs : List 𝓕.States) →
𝓣(𝓝(ofFieldOpList φs)) = ∑ (φsΛ : {φsΛ : WickContraction φs.length // ¬ HaveEqTime φsΛ}),
φsΛ.1.sign • φsΛ.1.timeContract.1 * 𝓝(ofFieldOpList [φsΛ.1]ᵘᶜ)
| [] => wicks_theorem_normal_order_empty
| φ :: φs => by
rw [normalOrder_timeOrder_ofFieldOpList_eq_not_haveEqTime_sub_inductive]
simp only [Algebra.smul_mul_assoc, ne_eq, add_right_eq_self]
apply Finset.sum_eq_zero
intro φsΛ hφsΛ
simp only [smul_eq_zero]
right
have ih := wicks_theorem_normal_order [φsΛ.1]ᵘᶜ
rw [ih]
simp
termination_by φs => φs.length
decreasing_by
simp only [uncontractedListGet, List.length_cons, List.length_map, gt_iff_lt]
rw [uncontractedList_length_eq_card]
have hc := uncontracted_card_eq_iff φsΛ.1
simp only [List.length_cons, φsΛ.2.2, iff_false] at hc
have hc' := uncontracted_card_le φsΛ.1
simp_all only [Algebra.smul_mul_assoc, List.length_cons, Finset.mem_univ, gt_iff_lt]
omega
end FieldOpAlgebra
end FieldSpecification

20
HepLean/PerturbationTheory/FieldStatistics/OfFinset.lean
View file

@ -106,4 +106,24 @@ lemma ofFinset_union_disjoint (q : 𝓕 → FieldStatistic) (φs : List 𝓕) (a
rw [ofFinset_union, Finset.disjoint_iff_inter_eq_empty.mp h]
simp
lemma ofFinset_filter_mul_neg (q : 𝓕 → FieldStatistic) (φs : List 𝓕) (a : Finset (Fin φs.length))
(p : Fin φs.length → Prop) [DecidablePred p] :
ofFinset q φs.get (Finset.filter p a) *
ofFinset q φs.get (Finset.filter (fun i => ¬ p i) a) = ofFinset q φs.get a := by
rw [ofFinset_union_disjoint]
congr
exact Finset.filter_union_filter_neg_eq p a
exact Finset.disjoint_filter_filter_neg a a p
lemma ofFinset_filter (q : 𝓕 → FieldStatistic) (φs : List 𝓕) (a : Finset (Fin φs.length))
(p : Fin φs.length → Prop) [DecidablePred p] :
ofFinset q φs.get (Finset.filter p a) = ofFinset q φs.get (Finset.filter (fun i => ¬ p i) a) *
ofFinset q φs.get a := by
rw [← ofFinset_filter_mul_neg q φs a p]
conv_rhs =>
rhs
rw [mul_comm]
rw [← mul_assoc]
simp
end FieldStatistic

53
HepLean/PerturbationTheory/WickContraction/Basic.lean
View file

@ -38,9 +38,32 @@ namespace WickContraction
variable {n : ℕ} (c : WickContraction n)
open HepLean.List
/-- Wick contractions are decidable. -/
instance : DecidableEq (WickContraction n) := Subtype.instDecidableEq
/-- The contraction consisting of no contracted pairs. -/
def empty : WickContraction n := ⟨∅, by simp, by simp⟩
lemma card_zero_iff_empty (c : WickContraction n) : c.1.card = 0 ↔ c = empty := by
rw [Subtype.eq_iff]
simp [empty]
lemma exists_pair_of_not_eq_empty (c : WickContraction n) (h : c ≠ empty) :
∃ i j, {i, j} ∈ c.1 := by
by_contra hn
simp only [not_exists] at hn
have hc : c.1 = ∅ := by
ext a
simp only [Finset.not_mem_empty, iff_false]
by_contra hn'
have hc := c.2.1 a hn'
rw [@Finset.card_eq_two] at hc
obtain ⟨x, y, hx, rfl⟩ := hc
exact hn x y hn'
apply h
apply Subtype.eq
simp [empty, hc]
/-- The equivalence between `WickContraction n` and `WickContraction m`
derived from a propositional equality of `n` and `m`. -/
def congr : {n m : ℕ} → (h : n = m) → WickContraction n ≃ WickContraction m
@ -48,9 +71,14 @@ def congr : {n m : ℕ} → (h : n = m) → WickContraction n ≃ WickContractio
@[simp]
lemma congr_refl : c.congr rfl = c := by
cases c
rfl
@[simp]
lemma card_congr {n m : ℕ} (h : n = m) (c : WickContraction n) :
(congr h c).1.card = c.1.card := by
subst h
simp
lemma congr_contractions {n m : ℕ} (h : n = m) (c : WickContraction n) :
((congr h) c).1 = Finset.map (Finset.mapEmbedding (finCongr h)).toEmbedding c.1 := by
subst h
@ -83,6 +111,11 @@ lemma congr_trans_apply {n m o : ℕ} (h1 : n = m) (h2 : m = o) (c : WickContrac
subst h1 h2
simp
lemma mem_congr_iff {n m : ℕ} (h : n = m) {c : WickContraction n } {a : Finset (Fin m)} :
a ∈ (congr h c).1 ↔ Finset.map (finCongr h.symm).toEmbedding a ∈ c.1 := by
subst h
simp
/-- Given a contracted pair in `c : WickContraction n` the contracted pair
in `congr h c`. -/
def congrLift {n m : ℕ} (h : n = m) {c : WickContraction n} (a : c.1) : (congr h c).1 :=
@ -112,6 +145,18 @@ lemma congrLift_bijective {n m : ℕ} {c : WickContraction n} (h : n = m) :
Function.Bijective (c.congrLift h) := by
exact ⟨c.congrLift_injective h, c.congrLift_surjective h⟩
/-- Given a contracted pair in `c : WickContraction n` the contracted pair
in `congr h c`. -/
def congrLiftInv {n m : ℕ} (h : n = m) {c : WickContraction n} (a : (congr h c).1) : c.1 :=
⟨a.1.map (finCongr h.symm).toEmbedding, by
subst h
simp⟩
lemma congrLiftInv_rfl {n : ℕ} {c : WickContraction n} :
c.congrLiftInv rfl = id := by
funext a
simp [congrLiftInv]
lemma eq_filter_mem_self : c.1 = Finset.filter (fun x => x ∈ c.1) Finset.univ := by
exact Eq.symm (Finset.filter_univ_mem c.1)
@ -481,6 +526,12 @@ lemma prod_finset_eq_mul_fst_snd (c : WickContraction n) (a : c.1)
def GradingCompliant (φs : List 𝓕.States) (φsΛ : WickContraction φs.length) :=
∀ (a : φsΛ.1), (𝓕 |>ₛ φs[φsΛ.fstFieldOfContract a]) = (𝓕 |>ₛ φs[φsΛ.sndFieldOfContract a])
lemma gradingCompliant_congr {φs φs' : List 𝓕.States} (h : φs = φs')
(φsΛ : WickContraction φs.length) :
GradingCompliant φs φsΛ ↔ GradingCompliant φs' (congr (by simp [h]) φsΛ) := by
subst h
rfl
/-- An equivalence from the sigma type `(a : c.1) × a` to the subtype of `Fin n` consisting of
those positions which are contracted. -/
def sigmaContractedEquiv : (a : c.1) × a ≃ {x : Fin n // (c.getDual? x).isSome} where

1081
HepLean/PerturbationTheory/WickContraction/Join.lean Normal file
View file

File diff suppressed because it is too large Load diff

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

@ -324,6 +324,16 @@ def sign (φs : List 𝓕.States) (φsΛ : WickContraction φs.length) : ℂ :=
∏ (a : φsΛ.1), 𝓢(𝓕 |>ₛ φs[φsΛ.sndFieldOfContract a],
𝓕 |>ₛ ⟨φs.get, φsΛ.signFinset (φsΛ.fstFieldOfContract a) (φsΛ.sndFieldOfContract a)⟩)
lemma sign_empty (φs : List 𝓕.States) :
sign φs empty = 1 := by
rw [sign]
simp [empty]
lemma sign_congr {φs φs' : List 𝓕.States} (h : φs = φs') (φsΛ : WickContraction φs.length) :
sign φs' (congr (by simp [h]) φsΛ) = sign φs φsΛ := by
subst h
rfl
/-!
## Sign insert

137
HepLean/PerturbationTheory/WickContraction/Singleton.lean Normal file
View file

@ -0,0 +1,137 @@
/-
Copyright (c) 2025 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.WickContraction.TimeContract
import HepLean.PerturbationTheory.WickContraction.StaticContract
import HepLean.PerturbationTheory.Algebras.FieldOpAlgebra.TimeContraction
import HepLean.PerturbationTheory.WickContraction.SubContraction
/-!
# Singleton of contractions
-/
open FieldSpecification
variable {𝓕 : FieldSpecification}
namespace WickContraction
variable {n : ℕ} (c : WickContraction n)
open HepLean.List
open FieldOpAlgebra
open FieldStatistic
/-- The Wick contraction formed from a single ordered pair. -/
def singleton {i j : Fin n} (hij : i < j) : WickContraction n :=
⟨{{i, j}}, by
intro i hi
simp only [Finset.mem_singleton] at hi
subst hi
rw [@Finset.card_eq_two]
use i, j
simp only [ne_eq, and_true]
omega, by
intro i hi j hj
simp_all⟩
lemma mem_singleton {i j : Fin n} (hij : i < j) :
{i, j} ∈ (singleton hij).1 := by
simp [singleton]
lemma mem_singleton_iff {i j : Fin n} (hij : i < j) {a : Finset (Fin n)} :
a ∈ (singleton hij).1 ↔ a = {i, j} := by
simp [singleton]
lemma of_singleton_eq {i j : Fin n} (hij : i < j) (a : (singleton hij).1) :
a = ⟨{i, j}, mem_singleton hij⟩ := by
have ha2 := a.2
rw [@mem_singleton_iff] at ha2
exact Subtype.coe_eq_of_eq_mk ha2
lemma singleton_prod {φs : List 𝓕.States} {i j : Fin φs.length} (hij : i < j)
(f : (singleton hij).1 → M) [CommMonoid M] :
∏ a, f a = f ⟨{i,j}, mem_singleton hij⟩:= by
simp [singleton, of_singleton_eq]
@[simp]
lemma singleton_fstFieldOfContract {i j : Fin n} (hij : i < j) :
(singleton hij).fstFieldOfContract ⟨{i, j}, mem_singleton hij⟩ = i := by
refine eq_fstFieldOfContract_of_mem (singleton hij) ⟨{i, j}, mem_singleton hij⟩ i j ?_ ?_ ?_
· simp
· simp
· exact hij
@[simp]
lemma singleton_sndFieldOfContract {i j : Fin n} (hij : i < j) :
(singleton hij).sndFieldOfContract ⟨{i, j}, mem_singleton hij⟩ = j := by
refine eq_sndFieldOfContract_of_mem (singleton hij) ⟨{i, j}, mem_singleton hij⟩ i j ?_ ?_ ?_
· simp
· simp
· exact hij
lemma singleton_sign_expand {φs : List 𝓕.States} {i j : Fin φs.length} (hij : i < j) :
(singleton hij).sign = 𝓢(𝓕 |>ₛ φs[j], 𝓕 |>ₛ ⟨φs.get, (singleton hij).signFinset i j⟩) := by
rw [sign, singleton_prod]
simp
lemma singleton_getDual?_eq_none_iff_neq {i j : Fin n} (hij : i < j) (a : Fin n) :
(singleton hij).getDual? a = none ↔ (i ≠ a ∧ j ≠ a) := by
rw [getDual?_eq_none_iff_mem_uncontracted]
rw [mem_uncontracted_iff_not_contracted]
simp only [singleton, Finset.mem_singleton, forall_eq, Finset.mem_insert, not_or, ne_eq]
omega
lemma singleton_uncontractedEmd_neq_left {φs : List 𝓕.States} {i j : Fin φs.length} (hij : i < j)
(a : Fin [singleton hij]ᵘᶜ.length) :
(singleton hij).uncontractedListEmd a ≠ i := by
by_contra hn
have h1 : (singleton hij).uncontractedListEmd a ∈ (singleton hij).uncontracted := by
simp [uncontractedListEmd]
have h2 : i ∉ (singleton hij).uncontracted := by
rw [mem_uncontracted_iff_not_contracted]
simp [singleton]
simp_all
lemma singleton_uncontractedEmd_neq_right {φs : List 𝓕.States} {i j : Fin φs.length} (hij : i < j)
(a : Fin [singleton hij]ᵘᶜ.length) :
(singleton hij).uncontractedListEmd a ≠ j := by
by_contra hn
have h1 : (singleton hij).uncontractedListEmd a ∈ (singleton hij).uncontracted := by
simp [uncontractedListEmd]
have h2 : j ∉ (singleton hij).uncontracted := by
rw [mem_uncontracted_iff_not_contracted]
simp [singleton]
simp_all
@[simp]
lemma mem_signFinset {i j : Fin n} (hij : i < j) (a : Fin n) :
a ∈ (singleton hij).signFinset i j ↔ i < a ∧ a < j := by
simp only [signFinset, Finset.mem_filter, Finset.mem_univ, true_and, and_congr_right_iff,
and_iff_left_iff_imp]
intro h1 h2
rw [@singleton_getDual?_eq_none_iff_neq]
apply Or.inl
omega
lemma subContraction_singleton_eq_singleton {φs : List 𝓕.States}
(φsΛ : WickContraction φs.length)
(a : φsΛ.1) : φsΛ.subContraction {a.1} (by simp) =
singleton (φsΛ.fstFieldOfContract_lt_sndFieldOfContract a) := by
apply Subtype.ext
simp only [subContraction, singleton, Finset.singleton_inj]
exact finset_eq_fstFieldOfContract_sndFieldOfContract φsΛ a
lemma singleton_timeContract {φs : List 𝓕.States} {i j : Fin φs.length} (hij : i < j) :
(singleton hij).timeContract =
⟨FieldOpAlgebra.timeContract φs[i] φs[j], timeContract_mem_center _ _⟩ := by
rw [timeContract, singleton_prod]
simp
lemma singleton_staticContract {φs : List 𝓕.States} {i j : Fin φs.length} (hij : i < j) :
(singleton hij).staticContract.1 =
[anPart φs[i], ofFieldOp φs[j]]ₛ := by
rw [staticContract, singleton_prod]
simp
end WickContraction

2
HepLean/PerturbationTheory/WickContraction/StaticContract.lean
View file

@ -51,7 +51,7 @@ lemma staticContract_insertAndContract_some
(φsΛ ↩Λ φ i (some j)).staticContract =
(if i < i.succAbove j then
⟨[anPart φ, ofFieldOp φs[j.1]]ₛ, superCommute_anPart_ofFieldOp_mem_center _ _⟩
else ⟨[anPart φs[j.1], ofFieldOp φ]ₛ, superCommute_anPart_ofFieldOp_mem_center _ _⟩) *
else ⟨[anPart φs[j.1], ofFieldOp φ]ₛ, superCommute_anPart_ofFieldOp_mem_center _ _⟩) *
φsΛ.staticContract := by
rw [staticContract, insertAndContract_some_prod_contractions]
congr 1

201
HepLean/PerturbationTheory/WickContraction/SubContraction.lean Normal file
View file

@ -0,0 +1,201 @@
/-
Copyright (c) 2025 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.WickContraction.TimeContract
import HepLean.PerturbationTheory.WickContraction.StaticContract
import HepLean.PerturbationTheory.Algebras.FieldOpAlgebra.TimeContraction
/-!
# Sub contractions
-/
open FieldSpecification
variable {𝓕 : FieldSpecification}
namespace WickContraction
variable {n : ℕ} {φs : List 𝓕.States} {φsΛ : WickContraction φs.length}
open HepLean.List
open FieldOpAlgebra
/-- Given a Wick contraction `φsΛ`, and a subset of `φsΛ.1`, the Wick contraction
conisting of contracted pairs within that subset. -/
def subContraction (S : Finset (Finset (Fin φs.length))) (ha : S ⊆ φsΛ.1) :
WickContraction φs.length :=
⟨S, by
intro i hi
exact φsΛ.2.1 i (ha hi),
by
intro i hi j hj
exact φsΛ.2.2 i (ha hi) j (ha hj)⟩
lemma mem_of_mem_subContraction {S : Finset (Finset (Fin φs.length))} {hs : S ⊆ φsΛ.1}
{a : Finset (Fin φs.length)} (ha : a ∈ (φsΛ.subContraction S hs).1) : a ∈ φsΛ.1 := by
exact hs ha
/-- Given a Wick contraction `φsΛ`, and a subset `S` of `φsΛ.1`, the Wick contraction
on the uncontracted list `[φsΛ.subContraction S ha]ᵘᶜ`
consisting of the remaining contracted pairs of `φsΛ` not in `S`. -/
def quotContraction (S : Finset (Finset (Fin φs.length))) (ha : S ⊆ φsΛ.1) :
WickContraction [φsΛ.subContraction S ha]ᵘᶜ.length :=
⟨Finset.filter (fun a => Finset.map uncontractedListEmd a ∈ φsΛ.1) Finset.univ,
by
intro a ha'
simp only [Finset.mem_filter, Finset.mem_univ, true_and] at ha'
simpa using φsΛ.2.1 (Finset.map uncontractedListEmd a) ha', by
intro a ha b hb
simp only [Finset.mem_filter, Finset.mem_univ, true_and] at ha hb
by_cases hab : a = b
· simp [hab]
· simp only [hab, false_or]
have hx := φsΛ.2.2 (Finset.map uncontractedListEmd a) ha (Finset.map uncontractedListEmd b) hb
simp_all⟩
lemma mem_of_mem_quotContraction {S : Finset (Finset (Fin φs.length))} {hs : S ⊆ φsΛ.1}
{a : Finset (Fin [φsΛ.subContraction S hs]ᵘᶜ.length)}
(ha : a ∈ (quotContraction S hs).1) : Finset.map uncontractedListEmd a ∈ φsΛ.1 := by
simp only [quotContraction, Finset.mem_filter, Finset.mem_univ, true_and] at ha
exact ha
lemma mem_subContraction_or_quotContraction {S : Finset (Finset (Fin φs.length))} {hs : S ⊆ φsΛ.1}
{a : Finset (Fin φs.length)} (ha : a ∈ φsΛ.1) :
a ∈ (φsΛ.subContraction S hs).1 ∨
∃ a', Finset.map uncontractedListEmd a' = a ∧ a' ∈ (quotContraction S hs).1 := by
by_cases h1 : a ∈ (φsΛ.subContraction S hs).1
· simp [h1]
simp only [h1, false_or]
simp only [subContraction] at h1
have h2 := φsΛ.2.1 a ha
rw [@Finset.card_eq_two] at h2
obtain ⟨i, j, hij, rfl⟩ := h2
have hi : i ∈ (φsΛ.subContraction S hs).uncontracted := by
rw [mem_uncontracted_iff_not_contracted]
intro p hp
have hp' : p ∈ φsΛ.1 := hs hp
have hp2 := φsΛ.2.2 p hp' {i, j} ha
simp only [subContraction] at hp
rcases hp2 with hp2 | hp2
· simp_all
simp only [Finset.disjoint_insert_right, Finset.disjoint_singleton_right] at hp2
exact hp2.1
have hj : j ∈ (φsΛ.subContraction S hs).uncontracted := by
rw [mem_uncontracted_iff_not_contracted]
intro p hp
have hp' : p ∈ φsΛ.1 := hs hp
have hp2 := φsΛ.2.2 p hp' {i, j} ha
simp only [subContraction] at hp
rcases hp2 with hp2 | hp2
· simp_all
simp only [Finset.disjoint_insert_right, Finset.disjoint_singleton_right] at hp2
exact hp2.2
obtain ⟨i, rfl⟩ := uncontractedListEmd_surjective_mem_uncontracted i hi
obtain ⟨j, rfl⟩ := uncontractedListEmd_surjective_mem_uncontracted j hj
use {i, j}
simp only [Finset.map_insert, Finset.map_singleton, quotContraction, Finset.mem_filter,
Finset.mem_univ, true_and]
exact ha
@[simp]
lemma subContraction_uncontractedList_get {S : Finset (Finset (Fin φs.length))} {hs : S ⊆ φsΛ.1}
{a : Fin [subContraction S hs]ᵘᶜ.length} :
[subContraction S hs]ᵘᶜ[a] = φs[uncontractedListEmd a] := by
erw [← getElem_uncontractedListEmd]
rfl
@[simp]
lemma subContraction_fstFieldOfContract {S : Finset (Finset (Fin φs.length))} {hs : S ⊆ φsΛ.1}
(a : (subContraction S hs).1) :
(subContraction S hs).fstFieldOfContract a =
φsΛ.fstFieldOfContract ⟨a.1, mem_of_mem_subContraction a.2⟩:= by
apply eq_fstFieldOfContract_of_mem _ _ _
(φsΛ.sndFieldOfContract ⟨a.1, mem_of_mem_subContraction a.2⟩)
· have ha := finset_eq_fstFieldOfContract_sndFieldOfContract _
⟨a.1, mem_of_mem_subContraction a.2⟩
simp only at ha
conv_lhs =>
rw [ha]
simp
· have ha := finset_eq_fstFieldOfContract_sndFieldOfContract _
⟨a.1, mem_of_mem_subContraction a.2⟩
simp only at ha
conv_lhs =>
rw [ha]
simp
· exact fstFieldOfContract_lt_sndFieldOfContract φsΛ ⟨↑a, mem_of_mem_subContraction a.property⟩
@[simp]
lemma subContraction_sndFieldOfContract {S : Finset (Finset (Fin φs.length))} {hs : S ⊆ φsΛ.1}
(a : (subContraction S hs).1) :
(subContraction S hs).sndFieldOfContract a =
φsΛ.sndFieldOfContract ⟨a.1, mem_of_mem_subContraction a.2⟩:= by
apply eq_sndFieldOfContract_of_mem _ _
(φsΛ.fstFieldOfContract ⟨a.1, mem_of_mem_subContraction a.2⟩)
· have ha := finset_eq_fstFieldOfContract_sndFieldOfContract _
⟨a.1, mem_of_mem_subContraction a.2⟩
simp only at ha
conv_lhs =>
rw [ha]
simp
· have ha := finset_eq_fstFieldOfContract_sndFieldOfContract _
⟨a.1, mem_of_mem_subContraction a.2⟩
simp only at ha
conv_lhs =>
rw [ha]
simp
· exact fstFieldOfContract_lt_sndFieldOfContract φsΛ ⟨↑a, mem_of_mem_subContraction a.property⟩
@[simp]
lemma quotContraction_fstFieldOfContract_uncontractedListEmd {S : Finset (Finset (Fin φs.length))}
{hs : S ⊆ φsΛ.1} (a : (quotContraction S hs).1) :
uncontractedListEmd ((quotContraction S hs).fstFieldOfContract a) =
(φsΛ.fstFieldOfContract
⟨Finset.map uncontractedListEmd a.1, mem_of_mem_quotContraction a.2⟩) := by
symm
apply eq_fstFieldOfContract_of_mem _ _ _
(uncontractedListEmd ((quotContraction S hs).sndFieldOfContract a))
· simp only [Finset.mem_map', fstFieldOfContract_mem]
· simp
· apply uncontractedListEmd_strictMono
exact fstFieldOfContract_lt_sndFieldOfContract (quotContraction S hs) a
@[simp]
lemma quotContraction_sndFieldOfContract_uncontractedListEmd {S : Finset (Finset (Fin φs.length))}
{hs : S ⊆ φsΛ.1} (a : (quotContraction S hs).1) :
uncontractedListEmd ((quotContraction S hs).sndFieldOfContract a) =
(φsΛ.sndFieldOfContract
⟨Finset.map uncontractedListEmd a.1, mem_of_mem_quotContraction a.2⟩) := by
symm
apply eq_sndFieldOfContract_of_mem _ _
(uncontractedListEmd ((quotContraction S hs).fstFieldOfContract a))
· simp only [Finset.mem_map', fstFieldOfContract_mem]
· simp
· apply uncontractedListEmd_strictMono
exact fstFieldOfContract_lt_sndFieldOfContract (quotContraction S hs) a
lemma quotContraction_gradingCompliant {S : Finset (Finset (Fin φs.length))} {hs : S ⊆ φsΛ.1}
(hsΛ : φsΛ.GradingCompliant) :
GradingCompliant [φsΛ.subContraction S hs]ᵘᶜ (quotContraction S hs) := by
simp only [GradingCompliant, Fin.getElem_fin, Subtype.forall]
intro a ha
erw [subContraction_uncontractedList_get]
erw [subContraction_uncontractedList_get]
simp only [quotContraction_fstFieldOfContract_uncontractedListEmd, Fin.getElem_fin,
quotContraction_sndFieldOfContract_uncontractedListEmd]
apply hsΛ
lemma mem_quotContraction_iff {S : Finset (Finset (Fin φs.length))} {hs : S ⊆ φsΛ.1}
{a : Finset (Fin [φsΛ.subContraction S hs]ᵘᶜ.length)} :
a ∈ (quotContraction S hs).1 ↔ a.map uncontractedListEmd ∈ φsΛ.1
∧ a.map uncontractedListEmd ∉ (subContraction S hs).1 := by
apply Iff.intro
· intro h
apply And.intro
· exact mem_of_mem_quotContraction h
· exact uncontractedListEmd_finset_not_mem _
· intro h
have h2 := mem_subContraction_or_quotContraction (S := S) (hs := hs) h.1
simp_all
end WickContraction

554
HepLean/PerturbationTheory/WickContraction/TimeCond.lean Normal file
View file

@ -0,0 +1,554 @@
/-
Copyright (c) 2025 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.WickContraction.TimeContract
import HepLean.PerturbationTheory.WickContraction.Join
import HepLean.PerturbationTheory.Algebras.FieldOpAlgebra.TimeContraction
/-!
# Time contractions
-/
open FieldSpecification
variable {𝓕 : FieldSpecification}
namespace WickContraction
variable {n : ℕ} (c : WickContraction n)
open HepLean.List
open FieldOpAlgebra
/-- The condition on a Wick contraction which is true iff and only if every contraction
is between two fields of equal time. -/
def EqTimeOnly {φs : List 𝓕.States} (φsΛ : WickContraction φs.length) : Prop :=
∀ (i j), {i, j} ∈ φsΛ.1 → timeOrderRel φs[i] φs[j]
noncomputable section
instance {φs : List 𝓕.States} (φsΛ : WickContraction φs.length) :
Decidable (EqTimeOnly φsΛ) :=
inferInstanceAs (Decidable (∀ (i j), {i, j} ∈ φsΛ.1 → timeOrderRel φs[i] φs[j]))
namespace EqTimeOnly
variable {φs : List 𝓕.States} (φsΛ : WickContraction φs.length)
lemma timeOrderRel_of_eqTimeOnly_pair {i j : Fin φs.length} (h : {i, j} ∈ φsΛ.1)
(hc : EqTimeOnly φsΛ) :
timeOrderRel φs[i] φs[j] := by
have h' := hc
simp only [EqTimeOnly, ne_eq, Fin.getElem_fin, Finset.mem_filter, Finset.mem_univ,
true_and] at h'
exact h' i j h
lemma timeOrderRel_both_of_eqTimeOnly {i j : Fin φs.length} (h : {i, j} ∈ φsΛ.1)
(hc : EqTimeOnly φsΛ) :
timeOrderRel φs[i] φs[j] ∧ timeOrderRel φs[j] φs[i] := by
apply And.intro
· exact timeOrderRel_of_eqTimeOnly_pair φsΛ h hc
· apply timeOrderRel_of_eqTimeOnly_pair φsΛ _ hc
rw [@Finset.pair_comm]
exact h
lemma eqTimeOnly_iff_forall_finset {φs : List 𝓕.States} (φsΛ : WickContraction φs.length) :
φsΛ.EqTimeOnly ↔ ∀ (a : φsΛ.1),
timeOrderRel (φs[φsΛ.fstFieldOfContract a]) (φs[φsΛ.sndFieldOfContract a])
∧ timeOrderRel (φs[φsΛ.sndFieldOfContract a]) (φs[φsΛ.fstFieldOfContract a]) := by
apply Iff.intro
· intro h a
apply timeOrderRel_both_of_eqTimeOnly φsΛ _ h
rw [← finset_eq_fstFieldOfContract_sndFieldOfContract]
simp
· intro h
simp only [EqTimeOnly, Fin.getElem_fin, Finset.mem_filter, Finset.mem_univ,
true_and]
intro i j h1
have h' := h ⟨{i, j}, h1⟩
by_cases hij: i < j
· have hi : φsΛ.fstFieldOfContract ⟨{i, j}, h1⟩ = i := by
apply eq_fstFieldOfContract_of_mem _ _ i j
· simp
· simp
· exact hij
have hj : φsΛ.sndFieldOfContract ⟨{i, j}, h1⟩ = j := by
apply eq_sndFieldOfContract_of_mem _ _ i j
· simp
· simp
· exact hij
simp_all
· have hij : i ≠ j := by
by_contra hij
subst hij
have h2 := φsΛ.2.1 {i, i} h1
simp at h2
have hj : φsΛ.fstFieldOfContract ⟨{i, j}, h1⟩ = j := by
apply eq_fstFieldOfContract_of_mem _ _ j i
· simp
· simp
· omega
have hi : φsΛ.sndFieldOfContract ⟨{i, j}, h1⟩ = i := by
apply eq_sndFieldOfContract_of_mem _ _ j i
· simp
· simp
· omega
simp_all
@[simp]
lemma empty_mem {φs : List 𝓕.States} : empty (n := φs.length).EqTimeOnly := by
rw [eqTimeOnly_iff_forall_finset]
simp [empty]
lemma staticContract_eq_timeContract_of_eqTimeOnly (h : φsΛ.EqTimeOnly) :
φsΛ.staticContract = φsΛ.timeContract := by
simp only [staticContract, timeContract]
apply congrArg
funext a
ext
simp only [List.get_eq_getElem]
rw [timeContract_of_timeOrderRel]
apply timeOrderRel_of_eqTimeOnly_pair φsΛ
rw [← finset_eq_fstFieldOfContract_sndFieldOfContract]
exact a.2
exact h
lemma eqTimeOnly_congr {φs φs' : List 𝓕.States} (h : φs = φs') (φsΛ : WickContraction φs.length) :
(congr (by simp [h]) φsΛ).EqTimeOnly (φs := φs') ↔ φsΛ.EqTimeOnly := by
subst h
simp
lemma quotContraction_eqTimeOnly {φs : List 𝓕.States} {φsΛ : WickContraction φs.length}
(h : φsΛ.EqTimeOnly) (S : Finset (Finset (Fin φs.length))) (ha : S ⊆ φsΛ.1) :
(φsΛ.quotContraction S ha).EqTimeOnly := by
rw [eqTimeOnly_iff_forall_finset]
intro a
simp only [Fin.getElem_fin]
erw [subContraction_uncontractedList_get]
erw [subContraction_uncontractedList_get]
simp only [quotContraction_fstFieldOfContract_uncontractedListEmd, Fin.getElem_fin,
quotContraction_sndFieldOfContract_uncontractedListEmd]
rw [eqTimeOnly_iff_forall_finset] at h
apply h
lemma exists_join_singleton_of_card_ge_zero {φs : List 𝓕.States} (φsΛ : WickContraction φs.length)
(h : 0 < φsΛ.1.card) (h1 : φsΛ.EqTimeOnly) :
∃ (i j : Fin φs.length) (h : i < j) (φsucΛ : WickContraction [singleton h]ᵘᶜ.length),
φsΛ = join (singleton h) φsucΛ ∧ (timeOrderRel φs[i] φs[j] ∧ timeOrderRel φs[j] φs[i])
∧ φsucΛ.EqTimeOnly ∧ φsucΛ.1.card + 1 = φsΛ.1.card := by
obtain ⟨a, ha⟩ := exists_contraction_pair_of_card_ge_zero φsΛ h
use φsΛ.fstFieldOfContract ⟨a, ha⟩
use φsΛ.sndFieldOfContract ⟨a, ha⟩
use φsΛ.fstFieldOfContract_lt_sndFieldOfContract ⟨a, ha⟩
let φsucΛ :
WickContraction [singleton (φsΛ.fstFieldOfContract_lt_sndFieldOfContract ⟨a, ha⟩)]ᵘᶜ.length :=
congr (by simp [← subContraction_singleton_eq_singleton])
(φsΛ.quotContraction {a} (by simpa using ha))
use φsucΛ
simp only [Fin.getElem_fin]
apply And.intro
· have h1 := join_congr (subContraction_singleton_eq_singleton _ ⟨a, ha⟩).symm (φsucΛ := φsucΛ)
simp only [id_eq, eq_mpr_eq_cast, h1, congr_trans_apply, congr_refl, φsucΛ]
rw [join_sub_quot]
· apply And.intro
· apply timeOrderRel_both_of_eqTimeOnly φsΛ _ h1
rw [← finset_eq_fstFieldOfContract_sndFieldOfContract]
simp [ha]
apply And.intro
· simp only [id_eq, eq_mpr_eq_cast, φsucΛ]
rw [eqTimeOnly_congr (φs := [(φsΛ.subContraction {a} (by simpa using ha))]ᵘᶜ)]
simp only [id_eq, eq_mpr_eq_cast]
exact quotContraction_eqTimeOnly h1 _ _
rw [← subContraction_singleton_eq_singleton]
· simp only [id_eq, eq_mpr_eq_cast, card_congr, φsucΛ]
have h1 := subContraction_card_plus_quotContraction_card_eq _ {a} (by simpa using ha)
simp only [subContraction, Finset.card_singleton, id_eq, eq_mpr_eq_cast] at h1
omega
lemma timeOrder_timeContract_mul_of_eqTimeOnly_mid_induction {φs : List 𝓕.States}
(φsΛ : WickContraction φs.length)
(hl : φsΛ.EqTimeOnly) (a b: 𝓕.FieldOpAlgebra) : (n : ℕ) → (hn : φsΛ.1.card = n) →
𝓣(a * φsΛ.timeContract.1 * b) = φsΛ.timeContract.1 * 𝓣(a * b)
| 0, hn => by
rw [@card_zero_iff_empty] at hn
subst hn
simp
| Nat.succ n, hn => by
obtain ⟨i, j, hij, φsucΛ, rfl, h2, h3, h4⟩ :=
exists_join_singleton_of_card_ge_zero φsΛ (by simp [hn]) hl
rw [join_timeContract]
rw [singleton_timeContract]
simp only [Fin.getElem_fin, MulMemClass.coe_mul]
trans timeOrder (a * FieldOpAlgebra.timeContract φs[↑i] φs[↑j] * (φsucΛ.timeContract.1 * b))
simp only [mul_assoc, Fin.getElem_fin]
rw [timeOrder_timeContract_eq_time_mid]
have ih := timeOrder_timeContract_mul_of_eqTimeOnly_mid_induction φsucΛ h3 a b n (by omega)
rw [← mul_assoc, ih]
simp only [Fin.getElem_fin, mul_assoc]
simp_all only [Nat.succ_eq_add_one, Fin.getElem_fin, add_left_inj]
simp_all
lemma timeOrder_timeContract_mul_of_eqTimeOnly_mid {φs : List 𝓕.States}
(φsΛ : WickContraction φs.length)
(hl : φsΛ.EqTimeOnly) (a b : 𝓕.FieldOpAlgebra) :
𝓣(a * φsΛ.timeContract.1 * b) = φsΛ.timeContract.1 * 𝓣(a * b) := by
exact timeOrder_timeContract_mul_of_eqTimeOnly_mid_induction φsΛ hl a b φsΛ.1.card rfl
lemma timeOrder_timeContract_mul_of_eqTimeOnly_left {φs : List 𝓕.States}
(φsΛ : WickContraction φs.length)
(hl : φsΛ.EqTimeOnly) (b : 𝓕.FieldOpAlgebra) :
𝓣(φsΛ.timeContract.1 * b) = φsΛ.timeContract.1 * 𝓣(b) := by
trans 𝓣(1 * φsΛ.timeContract.1 * b)
simp only [one_mul]
rw [timeOrder_timeContract_mul_of_eqTimeOnly_mid φsΛ hl]
simp
lemma exists_join_singleton_of_not_eqTimeOnly {φs : List 𝓕.States} (φsΛ : WickContraction φs.length)
(h1 : ¬ φsΛ.EqTimeOnly) :
∃ (i j : Fin φs.length) (h : i < j) (φsucΛ : WickContraction [singleton h]ᵘᶜ.length),
φsΛ = join (singleton h) φsucΛ ∧ (¬ timeOrderRel φs[i] φs[j] ∨ ¬ timeOrderRel φs[j] φs[i]) := by
rw [eqTimeOnly_iff_forall_finset] at h1
simp only [Fin.getElem_fin, Subtype.forall, not_forall, not_and] at h1
obtain ⟨a, ha, hr⟩ := h1
use φsΛ.fstFieldOfContract ⟨a, ha⟩
use φsΛ.sndFieldOfContract ⟨a, ha⟩
use φsΛ.fstFieldOfContract_lt_sndFieldOfContract ⟨a, ha⟩
let φsucΛ :
WickContraction [singleton (φsΛ.fstFieldOfContract_lt_sndFieldOfContract ⟨a, ha⟩)]ᵘᶜ.length :=
congr (by simp [← subContraction_singleton_eq_singleton])
(φsΛ.quotContraction {a} (by simpa using ha))
use φsucΛ
simp only [Fin.getElem_fin]
apply And.intro
· have h1 := join_congr (subContraction_singleton_eq_singleton _ ⟨a, ha⟩).symm (φsucΛ := φsucΛ)
simp only [id_eq, eq_mpr_eq_cast, h1, congr_trans_apply, congr_refl, φsucΛ]
rw [join_sub_quot]
· by_cases h1 : timeOrderRel φs[↑(φsΛ.fstFieldOfContract ⟨a, ha⟩)]
φs[↑(φsΛ.sndFieldOfContract ⟨a, ha⟩)]
· simp_all [h1]
· simp_all [h1]
lemma timeOrder_timeContract_of_not_eqTimeOnly {φs : List 𝓕.States}
(φsΛ : WickContraction φs.length)
(hl : ¬ φsΛ.EqTimeOnly) : 𝓣(φsΛ.timeContract.1) = 0 := by
obtain ⟨i, j, hij, φsucΛ, rfl, hr⟩ := exists_join_singleton_of_not_eqTimeOnly φsΛ hl
rw [join_timeContract]
rw [singleton_timeContract]
simp only [Fin.getElem_fin, MulMemClass.coe_mul]
rw [timeOrder_timeOrder_left]
rw [timeOrder_timeContract_neq_time]
simp only [zero_mul, map_zero]
simp_all only [Fin.getElem_fin, not_and]
intro h
simp_all
lemma timeOrder_staticContract_of_not_mem {φs : List 𝓕.States} (φsΛ : WickContraction φs.length)
(hl : ¬ φsΛ.EqTimeOnly) : 𝓣(φsΛ.staticContract.1) = 0 := by
obtain ⟨i, j, hij, φsucΛ, rfl, hr⟩ := exists_join_singleton_of_not_eqTimeOnly φsΛ hl
rw [join_staticContract]
simp only [MulMemClass.coe_mul]
rw [singleton_staticContract]
rw [timeOrder_timeOrder_left]
rw [timeOrder_superCommute_anPart_ofFieldOp_neq_time]
simp only [zero_mul, map_zero]
intro h
simp_all
end EqTimeOnly
/-- The condition on a Wick contraction which is true if it has at least one contraction
which is between two equal time fields. -/
def HaveEqTime {φs : List 𝓕.States} (φsΛ : WickContraction φs.length) : Prop :=
∃ (i j : Fin φs.length) (h : {i, j} ∈ φsΛ.1),
timeOrderRel φs[i] φs[j] ∧ timeOrderRel φs[j] φs[i]
noncomputable instance {φs : List 𝓕.States} (φsΛ : WickContraction φs.length) :
Decidable (HaveEqTime φsΛ) :=
inferInstanceAs (Decidable (∃ (i j : Fin φs.length)
(h : ({i, j} : Finset (Fin φs.length)) ∈ φsΛ.1),
timeOrderRel φs[i] φs[j] ∧ timeOrderRel φs[j] φs[i]))
lemma haveEqTime_iff_finset {φs : List 𝓕.States} (φsΛ : WickContraction φs.length) :
HaveEqTime φsΛ ↔ ∃ (a : Finset (Fin φs.length)) (h : a ∈ φsΛ.1),
timeOrderRel φs[φsΛ.fstFieldOfContract ⟨a, h⟩] φs[φsΛ.sndFieldOfContract ⟨a, h⟩]
∧ timeOrderRel φs[φsΛ.sndFieldOfContract ⟨a, h⟩] φs[φsΛ.fstFieldOfContract ⟨a, h⟩] := by
simp only [HaveEqTime, Fin.getElem_fin, exists_and_left, exists_prop]
apply Iff.intro
· intro h
obtain ⟨i, j, hij, h1, h2⟩ := h
use {i, j}, h1
by_cases hij : i < j
· have h1n := eq_fstFieldOfContract_of_mem φsΛ ⟨{i,j}, h1⟩ i j (by simp) (by simp) hij
have h2n := eq_sndFieldOfContract_of_mem φsΛ ⟨{i,j}, h1⟩ i j (by simp) (by simp) hij
simp only [h1n, h2n]
simp_all only [forall_true_left, true_and]
· have hineqj : i ≠ j := by
by_contra hineqj
subst hineqj
have h2 := φsΛ.2.1 {i, i} h1
simp_all
have hji : j < i := by omega
have h1n := eq_fstFieldOfContract_of_mem φsΛ ⟨{i,j}, h1⟩ j i (by simp) (by simp) hji
have h2n := eq_sndFieldOfContract_of_mem φsΛ ⟨{i,j}, h1⟩ j i (by simp) (by simp) hji
simp only [h1n, h2n]
simp_all
· intro h
obtain ⟨a, h1, h2, h3⟩ := h
use φsΛ.fstFieldOfContract ⟨a, h1⟩
use φsΛ.sndFieldOfContract ⟨a, h1⟩
simp_all only [and_true, true_and]
rw [← finset_eq_fstFieldOfContract_sndFieldOfContract]
exact h1
@[simp]
lemma empty_not_haveEqTime {φs : List 𝓕.States} :
¬ HaveEqTime (empty : WickContraction φs.length) := by
rw [haveEqTime_iff_finset]
simp [empty]
/-- Given a Wick contraction the subset of contracted pairs between eqaul time fields. -/
def eqTimeContractSet {φs : List 𝓕.States} (φsΛ : WickContraction φs.length) :
Finset (Finset (Fin φs.length)) :=
Finset.univ.filter (fun a =>
a ∈ φsΛ.1 ∧ ∀ (h : a ∈ φsΛ.1),
timeOrderRel φs[φsΛ.fstFieldOfContract ⟨a, h⟩] φs[φsΛ.sndFieldOfContract ⟨a, h⟩]
∧ timeOrderRel φs[φsΛ.sndFieldOfContract ⟨a, h⟩] φs[φsΛ.fstFieldOfContract ⟨a, h⟩])
lemma eqTimeContractSet_subset {φs : List 𝓕.States} (φsΛ : WickContraction φs.length) :
eqTimeContractSet φsΛ ⊆ φsΛ.1 := by
simp only [eqTimeContractSet, Fin.getElem_fin]
intro a
simp only [Finset.mem_filter, Finset.mem_univ, true_and, and_imp]
intro h _
exact h
lemma mem_of_mem_eqTimeContractSet{φs : List 𝓕.States} {φsΛ : WickContraction φs.length}
{a : Finset (Fin φs.length)} (h : a ∈ eqTimeContractSet φsΛ) : a ∈ φsΛ.1 := by
simp only [eqTimeContractSet, Fin.getElem_fin, Finset.mem_filter, Finset.mem_univ, true_and] at h
exact h.1
lemma join_eqTimeContractSet {φs : List 𝓕.States} (φsΛ : WickContraction φs.length)
(φsucΛ : WickContraction [φsΛ]ᵘᶜ.length) :
eqTimeContractSet (join φsΛ φsucΛ) = φsΛ.eqTimeContractSet ∪
φsucΛ.eqTimeContractSet.map (Finset.mapEmbedding uncontractedListEmd).toEmbedding := by
ext a
apply Iff.intro
· intro h
have hmem := mem_of_mem_eqTimeContractSet h
have ht := joinLiftLeft_or_joinLiftRight_of_mem_join (φsucΛ := φsucΛ) _ hmem
rcases ht with ht | ht
· obtain ⟨b, rfl⟩ := ht
simp only [Finset.le_eq_subset, Finset.mem_union, Finset.mem_map,
RelEmbedding.coe_toEmbedding]
left
simp only [eqTimeContractSet, Fin.getElem_fin, Finset.mem_filter, Finset.mem_univ, true_and]
apply And.intro (by simp [joinLiftLeft])
intro h'
simp only [eqTimeContractSet, Fin.getElem_fin, Finset.mem_filter, Finset.mem_univ,
Finset.coe_mem, Subtype.coe_eta, join_fstFieldOfContract_joinLiftLeft,
join_sndFieldOfContract_joinLift, forall_true_left, true_and] at h
exact h
· obtain ⟨b, rfl⟩ := ht
simp only [Finset.le_eq_subset, Finset.mem_union, Finset.mem_map,
RelEmbedding.coe_toEmbedding]
right
use b
rw [Finset.mapEmbedding_apply]
simp only [joinLiftRight, and_true]
simpa [eqTimeContractSet] using h
· intro h
simp only [Finset.le_eq_subset, Finset.mem_union, Finset.mem_map,
RelEmbedding.coe_toEmbedding] at h
rcases h with h | h
· simp only [eqTimeContractSet, Fin.getElem_fin, Finset.mem_filter, Finset.mem_univ, true_and]
simp only [eqTimeContractSet, Fin.getElem_fin, Finset.mem_filter, Finset.mem_univ,
true_and] at h
apply And.intro
· simp [join, h.1]
· intro h'
have h2 := h.2 h.1
exact h2
· simp only [eqTimeContractSet, Fin.getElem_fin, Finset.mem_filter, Finset.mem_univ, true_and]
simp only [eqTimeContractSet, Fin.getElem_fin, Finset.mem_filter, Finset.mem_univ,
true_and] at h
obtain ⟨b, h1, h2, rfl⟩ := h
apply And.intro
· simp [join, h1]
· intro h'
have h2 := h1.2 h1.1
have hj : ⟨(Finset.mapEmbedding uncontractedListEmd) b, h'⟩
= joinLiftRight ⟨b, h1.1⟩ := by rfl
simp only [hj, join_fstFieldOfContract_joinLiftRight, getElem_uncontractedListEmd,
join_sndFieldOfContract_joinLiftRight]
simpa using h2
lemma eqTimeContractSet_of_not_haveEqTime {φs : List 𝓕.States} {φsΛ : WickContraction φs.length}
(h : ¬ HaveEqTime φsΛ) : eqTimeContractSet φsΛ = ∅ := by
ext a
simp only [Finset.not_mem_empty, iff_false]
by_contra hn
rw [haveEqTime_iff_finset] at h
simp only [Fin.getElem_fin, not_exists, not_and] at h
simp only [eqTimeContractSet, Fin.getElem_fin, Finset.mem_filter, Finset.mem_univ, true_and] at hn
have h2 := hn.2 hn.1
simp_all
lemma eqTimeContractSet_of_mem_eqTimeOnly {φs : List 𝓕.States} {φsΛ : WickContraction φs.length}
(h : φsΛ.EqTimeOnly) : eqTimeContractSet φsΛ = φsΛ.1 := by
ext a
simp only [eqTimeContractSet, Fin.getElem_fin, Finset.mem_filter, Finset.mem_univ, true_and,
and_iff_left_iff_imp, imp_forall_iff_forall]
rw [EqTimeOnly.eqTimeOnly_iff_forall_finset] at h
exact fun h_1 => h ⟨a, h_1⟩
lemma subContraction_eqTimeContractSet_eqTimeOnly {φs : List 𝓕.States}
(φsΛ : WickContraction φs.length) :
(φsΛ.subContraction (eqTimeContractSet φsΛ) (eqTimeContractSet_subset φsΛ)).EqTimeOnly := by
rw [EqTimeOnly.eqTimeOnly_iff_forall_finset]
intro a
have ha2 := a.2
simp only [subContraction, eqTimeContractSet, Fin.getElem_fin, Finset.mem_filter, Finset.mem_univ,
true_and] at ha2
simp only [subContraction_fstFieldOfContract, Fin.getElem_fin, subContraction_sndFieldOfContract]
exact ha2.2 ha2.1
lemma pair_mem_eqTimeContractSet_iff {φs : List 𝓕.States} {i j : Fin φs.length}
(φsΛ : WickContraction φs.length) (h : {i, j} ∈ φsΛ.1) :
{i, j} ∈ φsΛ.eqTimeContractSet ↔ timeOrderRel φs[i] φs[j] ∧ timeOrderRel φs[j] φs[i] := by
simp only [eqTimeContractSet, Fin.getElem_fin, Finset.mem_filter, Finset.mem_univ, true_and]
by_cases hij : i < j
· have h1 := eq_fstFieldOfContract_of_mem φsΛ ⟨{i,j}, h⟩ i j (by simp) (by simp) hij
have h2 := eq_sndFieldOfContract_of_mem φsΛ ⟨{i,j}, h⟩ i j (by simp) (by simp) hij
simp only [h1, h2]
simp_all only [forall_true_left, true_and]
· have hineqj : i ≠ j := by
by_contra hineqj
subst hineqj
have h2 := φsΛ.2.1 {i, i} h
simp_all
have hji : j < i := by omega
have h1 := eq_fstFieldOfContract_of_mem φsΛ ⟨{i,j}, h⟩ j i (by simp) (by simp) hji
have h2 := eq_sndFieldOfContract_of_mem φsΛ ⟨{i,j}, h⟩ j i (by simp) (by simp) hji
simp only [h1, h2]
simp_all only [not_lt, ne_eq, forall_true_left, true_and]
apply Iff.intro
· intro a
simp_all only [and_self]
· intro a
simp_all only [and_self]
lemma subContraction_eqTimeContractSet_not_empty_of_haveEqTime
{φs : List 𝓕.States} (φsΛ : WickContraction φs.length) (h : HaveEqTime φsΛ) :
φsΛ.subContraction (eqTimeContractSet φsΛ) (eqTimeContractSet_subset φsΛ) ≠ empty := by
simp only [ne_eq]
erw [Subtype.eq_iff]
simp only [subContraction, empty]
rw [Finset.eq_empty_iff_forall_not_mem]
simp only [HaveEqTime, Fin.getElem_fin, exists_and_left, exists_prop] at h
obtain ⟨i, j, hij, h1, h2⟩ := h
simp only [not_forall, Decidable.not_not]
use {i, j}
rw [pair_mem_eqTimeContractSet_iff]
simp_all only [Fin.getElem_fin, and_self]
exact h1
lemma quotContraction_eqTimeContractSet_not_haveEqTime {φs : List 𝓕.States}
(φsΛ : WickContraction φs.length) :
¬ HaveEqTime (φsΛ.quotContraction (eqTimeContractSet φsΛ) (eqTimeContractSet_subset φsΛ)) := by
rw [haveEqTime_iff_finset]
simp only [Fin.getElem_fin, not_exists, not_and]
intro a ha
erw [subContraction_uncontractedList_get]
erw [subContraction_uncontractedList_get]
simp only [quotContraction_fstFieldOfContract_uncontractedListEmd, Fin.getElem_fin,
quotContraction_sndFieldOfContract_uncontractedListEmd]
simp only [quotContraction, Finset.mem_filter, Finset.mem_univ, true_and] at ha
have hn' : Finset.map uncontractedListEmd a ∉
(φsΛ.subContraction (eqTimeContractSet φsΛ) (eqTimeContractSet_subset φsΛ)).1 := by
exact uncontractedListEmd_finset_not_mem a
simp only [subContraction, eqTimeContractSet, Fin.getElem_fin, Finset.mem_filter, Finset.mem_univ,
true_and, not_and, not_forall] at hn'
have hn'' := hn' ha
obtain ⟨h, h1⟩ := hn''
simp_all
lemma join_haveEqTime_of_eqTimeOnly_nonEmpty {φs : List 𝓕.States} (φsΛ : WickContraction φs.length)
(h1 : φsΛ.EqTimeOnly) (h2 : φsΛ ≠ empty)
(φsucΛ : WickContraction [φsΛ]ᵘᶜ.length) :
HaveEqTime (join φsΛ φsucΛ) := by
simp only [HaveEqTime, Fin.getElem_fin, join, Finset.le_eq_subset, Finset.mem_union,
Finset.mem_map, RelEmbedding.coe_toEmbedding, exists_and_left, exists_prop]
simp only [EqTimeOnly, Fin.getElem_fin, Finset.mem_filter, Finset.mem_univ,
true_and] at h1
obtain ⟨i, j, h⟩ := exists_pair_of_not_eq_empty _ h2
use i, j
simp_all only [ne_eq, true_or, true_and]
apply h1 j i
rw [Finset.pair_comm]
exact h
lemma hasEqTimeEquiv_ext_sigma {φs : List 𝓕.States} {x1 x2 :
Σ (φsΛ : {φsΛ : WickContraction φs.length // φsΛ.EqTimeOnly ∧ φsΛ ≠ empty}),
{φssucΛ : WickContraction [φsΛ.1]ᵘᶜ.length // ¬ HaveEqTime φssucΛ}}
(h1 : x1.1.1 = x2.1.1) (h2 : x1.2.1 = congr (by simp [h1]) x2.2.1) : x1 = x2 := by
match x1, x2 with
| ⟨⟨a1, b1⟩, ⟨c1, d1⟩⟩, ⟨⟨a2, b2⟩, ⟨c2, d2⟩⟩ =>
simp only at h1
subst h1
simp only [ne_eq, congr_refl] at h2
simp [h2]
/-- The equivalence which seperates a Wick contraction which has an equal time contraction
into a non-empty contraction only between equal-time fields and a Wick contraction which
does not have equal time contractions. -/
def hasEqTimeEquiv (φs : List 𝓕.States) :
{φsΛ : WickContraction φs.length // HaveEqTime φsΛ} ≃
Σ (φsΛ : {φsΛ : WickContraction φs.length // φsΛ.EqTimeOnly ∧ φsΛ ≠ empty}),
{φssucΛ : WickContraction [φsΛ.1]ᵘᶜ.length // ¬ HaveEqTime φssucΛ} where
toFun φsΛ := ⟨⟨φsΛ.1.subContraction (eqTimeContractSet φsΛ.1) (eqTimeContractSet_subset φsΛ.1),
subContraction_eqTimeContractSet_eqTimeOnly φsΛ.1,
subContraction_eqTimeContractSet_not_empty_of_haveEqTime φsΛ.1 φsΛ.2⟩,
⟨φsΛ.1.quotContraction (eqTimeContractSet φsΛ.1) (eqTimeContractSet_subset φsΛ.1),
quotContraction_eqTimeContractSet_not_haveEqTime φsΛ.1⟩⟩
invFun φsΛ := ⟨join φsΛ.1.1 φsΛ.2.1,
join_haveEqTime_of_eqTimeOnly_nonEmpty φsΛ.1.1 φsΛ.1.2.1 φsΛ.1.2.2 φsΛ.2⟩
left_inv φsΛ := by
match φsΛ with
| ⟨φsΛ, h1, h2⟩ =>
simp only [ne_eq, Fin.getElem_fin, Subtype.mk.injEq]
exact join_sub_quot φsΛ φsΛ.eqTimeContractSet (eqTimeContractSet_subset φsΛ)
right_inv φsΛ' := by
match φsΛ' with
| ⟨⟨φsΛ, h1⟩, ⟨φsucΛ, h2⟩⟩ =>
have hs : subContraction (φsΛ.join φsucΛ).eqTimeContractSet
(eqTimeContractSet_subset (φsΛ.join φsucΛ)) = φsΛ := by
apply Subtype.ext
ext a
simp only [subContraction]
rw [join_eqTimeContractSet]
rw [eqTimeContractSet_of_not_haveEqTime h2]
simp only [Finset.le_eq_subset, ne_eq, Finset.map_empty, Finset.union_empty]
rw [eqTimeContractSet_of_mem_eqTimeOnly h1.1]
refine hasEqTimeEquiv_ext_sigma ?_ ?_
· simp only [ne_eq]
exact hs
· simp only [ne_eq]
apply Subtype.ext
ext a
simp only [quotContraction, Finset.mem_filter, Finset.mem_univ, true_and]
rw [mem_congr_iff]
rw [mem_join_right_iff]
simp only [ne_eq]
rw [uncontractedListEmd_congr hs]
rw [Finset.map_map]
lemma sum_haveEqTime (φs : List 𝓕.States)
(f : WickContraction φs.length → M) [AddCommMonoid M]:
∑ (φsΛ : {φsΛ : WickContraction φs.length // HaveEqTime φsΛ}), f φsΛ =
∑ (φsΛ : {φsΛ : WickContraction φs.length // φsΛ.EqTimeOnly ∧ φsΛ ≠ empty}),
∑ (φssucΛ : {φssucΛ : WickContraction [φsΛ.1]ᵘᶜ.length // ¬ HaveEqTime φssucΛ}),
f (join φsΛ.1 φssucΛ.1) := by
rw [← (hasEqTimeEquiv φs).symm.sum_comp]
erw [Finset.sum_sigma]
rfl
end
end WickContraction

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

@ -70,6 +70,12 @@ lemma timeConract_insertAndContract_some
ext a
simp
@[simp]
lemma timeContract_empty (φs : List 𝓕.States) :
(@empty φs.length).timeContract = 1 := by
rw [timeContract, empty]
simp
open FieldStatistic
lemma timeConract_insertAndContract_some_eq_mul_contractStateAtIndex_lt

40
HepLean/PerturbationTheory/WickContraction/Uncontracted.lean
View file

@ -24,6 +24,10 @@ lemma congr_uncontracted {n m : ℕ} (c : WickContraction n) (h : n = m) :
subst h
simp
lemma getDual?_eq_none_iff_mem_uncontracted (i : Fin n) :
c.getDual? i = none ↔ i ∈ c.uncontracted := by
simp [uncontracted]
/-- The equivalence of `Option c.uncontracted` for two propositionally equal Wick contractions. -/
def uncontractedCongr {c c': WickContraction n} (h : c = c') :
Option c.uncontracted ≃ Option c'.uncontracted :=
@ -64,4 +68,40 @@ lemma mem_uncontracted_iff_not_contracted (i : Fin n) :
apply h {i, j} hj
simp
lemma mem_uncontracted_empty (i : Fin n) : i ∈ empty.uncontracted := by
rw [@mem_uncontracted_iff_not_contracted]
intro p hp
simp [empty] at hp
@[simp]
lemma getDual?_empty_eq_none (i : Fin n) : empty.getDual? i = none := by
simpa [uncontracted] using mem_uncontracted_empty i
@[simp]
lemma uncontracted_empty {n : ℕ} : (@empty n).uncontracted = Finset.univ := by
simp [uncontracted]
lemma uncontracted_card_le (c : WickContraction n) : c.uncontracted.card ≤ n := by
simp only [uncontracted]
apply le_of_le_of_eq (Finset.card_filter_le _ _)
simp
lemma uncontracted_card_eq_iff (c : WickContraction n) :
c.uncontracted.card = n ↔ c = empty := by
apply Iff.intro
· intro h
have hc : c.uncontracted.card = (Finset.univ (α := Fin n)).card := by simpa using h
simp only [uncontracted] at hc
rw [Finset.card_filter_eq_iff] at hc
by_contra hn
have hc' := exists_pair_of_not_eq_empty c hn
obtain ⟨i, j, hij⟩ := hc'
have hci : c.getDual? i = some j := by
rw [@getDual?_eq_some_iff_mem]
exact hij
simp_all
· intro h
subst h
simp
end WickContraction

116
HepLean/PerturbationTheory/WickContraction/UncontractedList.lean
View file

@ -46,6 +46,24 @@ lemma fin_list_sorted_succAboveEmb_sorted (l: List (Fin n)) (hl : l.Sorted (·
simp only [Fin.coe_succAboveEmb]
exact Fin.strictMono_succAbove i
lemma fin_finset_sort_map_monotone {n m : ℕ} (a : Finset (Fin n)) (f : Fin n ↪ Fin m)
(hf : StrictMono f) : (Finset.sort (· ≤ ·) a).map f =
(Finset.sort (· ≤ ·) (a.map f)) := by
have h1 : ((Finset.sort (· ≤ ·) a).map f).Sorted (· ≤ ·) := by
apply fin_list_sorted_monotone_sorted
exact Finset.sort_sorted (fun x1 x2 => x1 ≤ x2) a
exact hf
have h2 : ((Finset.sort (· ≤ ·) a).map f).Nodup := by
refine (List.nodup_map_iff_inj_on ?_).mpr ?_
exact Finset.sort_nodup (fun x1 x2 => x1 ≤ x2) a
intro a ha b hb hf
exact f.2 hf
have h3 : ((Finset.sort (· ≤ ·) a).map f).toFinset = (a.map f) := by
ext a
simp
rw [← h3]
exact ((List.toFinset_sort (· ≤ ·) h2).mpr h1).symm
lemma fin_list_sorted_split :
(l : List (Fin n)) → (hl : l.Sorted (· ≤ ·)) → (i : ℕ) →
l = l.filter (fun x => x.1 < i) ++ l.filter (fun x => i ≤ x.1)
@ -178,6 +196,9 @@ lemma uncontractedList_mem_iff (i : Fin n) :
simp [uncontractedList]
@[simp]
lemma uncontractedList_empty : (empty (n := n)).uncontractedList = List.finRange n := by
simp [uncontractedList]
lemma nil_zero_uncontractedList : (empty (n := 0)).uncontractedList = [] := by
simp [empty, uncontractedList]
@ -197,6 +218,12 @@ lemma uncontractedList_sorted : List.Sorted (· ≤ ·) c.uncontractedList := by
rw [← List.ofFn_id]
exact Monotone.ofFn_sorted fun ⦃a b⦄ a => a
lemma uncontractedList_sorted_lt : List.Sorted (· < ·) c.uncontractedList := by
rw [uncontractedList]
apply List.Sorted.filter
rw [← List.ofFn_id]
exact List.sorted_lt_ofFn_iff.mpr fun ⦃a b⦄ a => a
lemma uncontractedList_nodup : c.uncontractedList.Nodup := by
rw [uncontractedList]
refine List.Nodup.filter (fun x => decide (x ∈ c.uncontracted)) ?_
@ -294,6 +321,12 @@ def uncontractedListGet {φs : List 𝓕.States} (φsΛ : WickContraction φs.le
@[inherit_doc uncontractedListGet]
scoped[WickContraction] notation "[" φsΛ "]ᵘᶜ" => uncontractedListGet φsΛ
@[simp]
lemma uncontractedListGet_empty {φs : List 𝓕.States} :
(empty (n := φs.length)).uncontractedListGet = φs := by
simp [uncontractedListGet]
/-!
## uncontractedStatesEquiv
@ -321,6 +354,89 @@ lemma uncontractedStatesEquiv_list_sum [AddCommMonoid α] (φs : List 𝓕.State
/-!
## uncontractedListEmd
-/
/-- The embedding of `Fin [φsΛ]ᵘᶜ.length` into `Fin φs.length`. -/
def uncontractedListEmd {φs : List 𝓕.States} {φsΛ : WickContraction φs.length} :
Fin [φsΛ]ᵘᶜ.length ↪ Fin φs.length := ((finCongr (by simp [uncontractedListGet])).trans
φsΛ.uncontractedIndexEquiv).toEmbedding.trans
(Function.Embedding.subtype fun x => x ∈ φsΛ.uncontracted)
lemma uncontractedListEmd_congr {φs : List 𝓕.States} {φsΛ φsΛ' : WickContraction φs.length}
(h : φsΛ = φsΛ') : φsΛ.uncontractedListEmd =
(finCongr (by simp [h])).toEmbedding.trans φsΛ'.uncontractedListEmd := by
subst h
rfl
lemma uncontractedListEmd_toFun_eq_get (φs : List 𝓕.States) (φsΛ : WickContraction φs.length) :
(uncontractedListEmd (φsΛ := φsΛ)).toFun =
φsΛ.uncontractedList.get ∘ (finCongr (by simp [uncontractedListGet])) := by
rfl
lemma uncontractedListEmd_strictMono {φs : List 𝓕.States} {φsΛ : WickContraction φs.length}
{i j : Fin [φsΛ]ᵘᶜ.length} (h : i < j) : uncontractedListEmd i < uncontractedListEmd j := by
simp only [uncontractedListEmd, uncontractedIndexEquiv, List.get_eq_getElem,
Equiv.trans_toEmbedding, Function.Embedding.trans_apply, Equiv.coe_toEmbedding, finCongr_apply,
Equiv.coe_fn_mk, Fin.coe_cast, Function.Embedding.coe_subtype]
exact List.Sorted.get_strictMono φsΛ.uncontractedList_sorted_lt h
lemma uncontractedListEmd_mem_uncontracted {φs : List 𝓕.States} {φsΛ : WickContraction φs.length}
(i : Fin [φsΛ]ᵘᶜ.length) : uncontractedListEmd i ∈ φsΛ.uncontracted := by
simp [uncontractedListEmd]
lemma uncontractedListEmd_surjective_mem_uncontracted {φs : List 𝓕.States}
{φsΛ : WickContraction φs.length} (i : Fin φs.length) (hi : i ∈ φsΛ.uncontracted) :
∃ j, φsΛ.uncontractedListEmd j = i := by
simp only [uncontractedListEmd, Equiv.trans_toEmbedding, Function.Embedding.trans_apply,
Equiv.coe_toEmbedding, finCongr_apply, Function.Embedding.coe_subtype]
have hj : ∃ j, φsΛ.uncontractedIndexEquiv j = ⟨i, hi⟩ := by
exact φsΛ.uncontractedIndexEquiv.surjective ⟨i, hi⟩
obtain ⟨j, hj⟩ := hj
have hj' : ∃ j', Fin.cast uncontractedListEmd.proof_1 j' = j := by
exact (finCongr uncontractedListEmd.proof_1).surjective j
obtain ⟨j', rfl⟩ := hj'
use j'
rw [hj]
@[simp]
lemma uncontractedListEmd_finset_disjoint_left {φs : List 𝓕.States}
{φsΛ : WickContraction φs.length} (a : Finset (Fin [φsΛ]ᵘᶜ.length))
(b : Finset (Fin φs.length)) (hb : b ∈ φsΛ.1) : Disjoint (a.map uncontractedListEmd) b := by
rw [Finset.disjoint_left]
intro x hx
simp only [Finset.mem_map] at hx
obtain ⟨x, hx, rfl⟩ := hx
have h1 : uncontractedListEmd x ∈ φsΛ.uncontracted :=
uncontractedListEmd_mem_uncontracted x
rw [mem_uncontracted_iff_not_contracted] at h1
exact h1 b hb
lemma uncontractedListEmd_finset_not_mem {φs : List 𝓕.States} {φsΛ : WickContraction φs.length}
(a : Finset (Fin [φsΛ]ᵘᶜ.length)) :
a.map uncontractedListEmd ∉ φsΛ.1 := by
by_contra hn
have h1 := uncontractedListEmd_finset_disjoint_left a (a.map uncontractedListEmd) hn
simp only [disjoint_self, Finset.bot_eq_empty, Finset.map_eq_empty] at h1
have h2 := φsΛ.2.1 (a.map uncontractedListEmd) hn
rw [h1] at h2
simp at h2
@[simp]
lemma getElem_uncontractedListEmd {φs : List 𝓕.States} {φsΛ : WickContraction φs.length}
(k : Fin [φsΛ]ᵘᶜ.length) : φs[(uncontractedListEmd k).1] = [φsΛ]ᵘᶜ[k.1] := by
simp only [uncontractedListGet, List.getElem_map, List.get_eq_getElem]
rfl
@[simp]
lemma uncontractedListEmd_empty {φs : List 𝓕.States} :
(empty (n := φs.length)).uncontractedListEmd = (finCongr (by simp)).toEmbedding := by
ext x
simp [uncontractedListEmd, uncontractedIndexEquiv]
/-!
## Uncontracted List for extractEquiv symm none
-/