feat: Add Wick terms
This commit is contained in:
jstoobysmith
parent
7d9e6af80c
commit
2e82f842a2
12 changed files with 634 additions and 553 deletions
|
|
@ -128,11 +128,14 @@ import HepLean.PerturbationTheory.FeynmanDiagrams.Instances.Phi4
|
||||||
import HepLean.PerturbationTheory.FeynmanDiagrams.Momentum
|
import HepLean.PerturbationTheory.FeynmanDiagrams.Momentum
|
||||||
import HepLean.PerturbationTheory.FieldOpAlgebra.Basic
|
import HepLean.PerturbationTheory.FieldOpAlgebra.Basic
|
||||||
import HepLean.PerturbationTheory.FieldOpAlgebra.Grading
|
import HepLean.PerturbationTheory.FieldOpAlgebra.Grading
|
||||||
import HepLean.PerturbationTheory.FieldOpAlgebra.NormalOrder
|
import HepLean.PerturbationTheory.FieldOpAlgebra.NormalOrder.Basic
|
||||||
|
import HepLean.PerturbationTheory.FieldOpAlgebra.NormalOrder.Lemmas
|
||||||
|
import HepLean.PerturbationTheory.FieldOpAlgebra.NormalOrder.WickContractions
|
||||||
import HepLean.PerturbationTheory.FieldOpAlgebra.StaticWickTheorem
|
import HepLean.PerturbationTheory.FieldOpAlgebra.StaticWickTheorem
|
||||||
import HepLean.PerturbationTheory.FieldOpAlgebra.SuperCommute
|
import HepLean.PerturbationTheory.FieldOpAlgebra.SuperCommute
|
||||||
import HepLean.PerturbationTheory.FieldOpAlgebra.TimeContraction
|
import HepLean.PerturbationTheory.FieldOpAlgebra.TimeContraction
|
||||||
import HepLean.PerturbationTheory.FieldOpAlgebra.TimeOrder
|
import HepLean.PerturbationTheory.FieldOpAlgebra.TimeOrder
|
||||||
|
import HepLean.PerturbationTheory.FieldOpAlgebra.WickTerm
|
||||||
import HepLean.PerturbationTheory.FieldOpAlgebra.WicksTheorem
|
import HepLean.PerturbationTheory.FieldOpAlgebra.WicksTheorem
|
||||||
import HepLean.PerturbationTheory.FieldOpAlgebra.WicksTheoremNormal
|
import HepLean.PerturbationTheory.FieldOpAlgebra.WicksTheoremNormal
|
||||||
import HepLean.PerturbationTheory.FieldOpFreeAlgebra.Basic
|
import HepLean.PerturbationTheory.FieldOpFreeAlgebra.Basic
|
||||||
|
|
|
||||||
240
HepLean/PerturbationTheory/FieldOpAlgebra/NormalOrder/Basic.lean
Normal file
240
HepLean/PerturbationTheory/FieldOpAlgebra/NormalOrder/Basic.lean
Normal file
|
|
@ -0,0 +1,240 @@
|
||||||
|
/-
|
||||||
|
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.FieldOpFreeAlgebra.NormalOrder
|
||||||
|
import HepLean.PerturbationTheory.FieldOpAlgebra.SuperCommute
|
||||||
|
/-!
|
||||||
|
|
||||||
|
# Normal Ordering on Field operator algebra
|
||||||
|
|
||||||
|
-/
|
||||||
|
|
||||||
|
namespace FieldSpecification
|
||||||
|
open FieldOpFreeAlgebra
|
||||||
|
open HepLean.List
|
||||||
|
open FieldStatistic
|
||||||
|
|
||||||
|
namespace FieldOpAlgebra
|
||||||
|
variable {𝓕 : FieldSpecification}
|
||||||
|
|
||||||
|
/-!
|
||||||
|
|
||||||
|
## Normal order on super-commutators.
|
||||||
|
|
||||||
|
The main result of this is
|
||||||
|
`ι_normalOrderF_superCommuteF_eq_zero_mul`
|
||||||
|
which states that applying `ι` to the normal order of something containing a super-commutator
|
||||||
|
is zero.
|
||||||
|
|
||||||
|
-/
|
||||||
|
|
||||||
|
lemma ι_normalOrderF_superCommuteF_ofCrAnListF_ofCrAnListF_eq_zero
|
||||||
|
(φa φa' : 𝓕.CrAnFieldOp) (φs φs' : List 𝓕.CrAnFieldOp) :
|
||||||
|
ι 𝓝ᶠ(ofCrAnListF φs * [ofCrAnOpF φa, ofCrAnOpF φa']ₛca * ofCrAnListF φ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 [normalOrderF_superCommuteF_ofCrAnListF_create_create_ofCrAnListF φa φa' hφa hφa' φs φs']
|
||||||
|
rw [map_smul, map_mul, map_mul, map_mul, ι_superCommuteF_of_create_create φa φa' hφa hφa']
|
||||||
|
simp
|
||||||
|
· rw [normalOrderF_superCommuteF_create_annihilate φa φa' hφa hφa' (ofCrAnListF φs)
|
||||||
|
(ofCrAnListF φs')]
|
||||||
|
simp
|
||||||
|
· rw [normalOrderF_superCommuteF_annihilate_create φa' φa hφa' hφa (ofCrAnListF φs)
|
||||||
|
(ofCrAnListF φs')]
|
||||||
|
simp
|
||||||
|
· rw [normalOrderF_superCommuteF_ofCrAnListF_annihilate_annihilate_ofCrAnListF
|
||||||
|
φa φa' hφa hφa' φs φs']
|
||||||
|
rw [map_smul, map_mul, map_mul, map_mul,
|
||||||
|
ι_superCommuteF_of_annihilate_annihilate φa φa' hφa hφa']
|
||||||
|
simp
|
||||||
|
|
||||||
|
lemma ι_normalOrderF_superCommuteF_ofCrAnListF_eq_zero
|
||||||
|
(φa φa' : 𝓕.CrAnFieldOp) (φs : List 𝓕.CrAnFieldOp)
|
||||||
|
(a : 𝓕.FieldOpFreeAlgebra) :
|
||||||
|
ι 𝓝ᶠ(ofCrAnListF φs * [ofCrAnOpF φa, ofCrAnOpF φa']ₛca * a) = 0 := by
|
||||||
|
have hf : ι.toLinearMap ∘ₗ normalOrderF ∘ₗ
|
||||||
|
mulLinearMap (ofCrAnListF φs * [ofCrAnOpF φa, ofCrAnOpF φa']ₛca) = 0 := by
|
||||||
|
apply ofCrAnListFBasis.ext
|
||||||
|
intro l
|
||||||
|
simp only [FieldOpFreeAlgebra.ofListBasis_eq_ofList, LinearMap.coe_comp, Function.comp_apply,
|
||||||
|
AlgHom.toLinearMap_apply, LinearMap.zero_apply]
|
||||||
|
exact ι_normalOrderF_superCommuteF_ofCrAnListF_ofCrAnListF_eq_zero φa φa' φs l
|
||||||
|
change (ι.toLinearMap ∘ₗ normalOrderF ∘ₗ
|
||||||
|
mulLinearMap ((ofCrAnListF φs * [ofCrAnOpF φa, ofCrAnOpF φa']ₛca))) a = 0
|
||||||
|
rw [hf]
|
||||||
|
simp
|
||||||
|
|
||||||
|
lemma ι_normalOrderF_superCommuteF_ofCrAnOpF_eq_zero_mul (φa φa' : 𝓕.CrAnFieldOp)
|
||||||
|
(a b : 𝓕.FieldOpFreeAlgebra) :
|
||||||
|
ι 𝓝ᶠ(a * [ofCrAnOpF φa, ofCrAnOpF φa']ₛca * b) = 0 := by
|
||||||
|
rw [mul_assoc]
|
||||||
|
change (ι.toLinearMap ∘ₗ normalOrderF ∘ₗ mulLinearMap.flip
|
||||||
|
([ofCrAnOpF φa, ofCrAnOpF φa']ₛca * b)) a = 0
|
||||||
|
have hf : ι.toLinearMap ∘ₗ normalOrderF ∘ₗ mulLinearMap.flip
|
||||||
|
([ofCrAnOpF φa, ofCrAnOpF φa']ₛca * b) = 0 := by
|
||||||
|
apply ofCrAnListFBasis.ext
|
||||||
|
intro l
|
||||||
|
simp only [mulLinearMap, FieldOpFreeAlgebra.ofListBasis_eq_ofList, LinearMap.coe_comp,
|
||||||
|
Function.comp_apply, LinearMap.flip_apply, LinearMap.coe_mk, AddHom.coe_mk,
|
||||||
|
AlgHom.toLinearMap_apply, LinearMap.zero_apply]
|
||||||
|
rw [← mul_assoc]
|
||||||
|
exact ι_normalOrderF_superCommuteF_ofCrAnListF_eq_zero φa φa' _ _
|
||||||
|
rw [hf]
|
||||||
|
simp
|
||||||
|
|
||||||
|
lemma ι_normalOrderF_superCommuteF_ofCrAnOpF_ofCrAnListF_eq_zero_mul (φa : 𝓕.CrAnFieldOp)
|
||||||
|
(φs : List 𝓕.CrAnFieldOp) (a b : 𝓕.FieldOpFreeAlgebra) :
|
||||||
|
ι 𝓝ᶠ(a * [ofCrAnOpF φa, ofCrAnListF φs]ₛca * b) = 0 := by
|
||||||
|
rw [← ofCrAnListF_singleton, superCommuteF_ofCrAnListF_ofCrAnListF_eq_sum]
|
||||||
|
rw [Finset.mul_sum, Finset.sum_mul]
|
||||||
|
rw [map_sum, map_sum]
|
||||||
|
apply Fintype.sum_eq_zero
|
||||||
|
intro n
|
||||||
|
rw [← mul_assoc, ← mul_assoc]
|
||||||
|
rw [mul_assoc _ _ b, ofCrAnListF_singleton]
|
||||||
|
rw [ι_normalOrderF_superCommuteF_ofCrAnOpF_eq_zero_mul]
|
||||||
|
|
||||||
|
lemma ι_normalOrderF_superCommuteF_ofCrAnListF_ofCrAnOpF_eq_zero_mul (φa : 𝓕.CrAnFieldOp)
|
||||||
|
(φs : List 𝓕.CrAnFieldOp) (a b : 𝓕.FieldOpFreeAlgebra) :
|
||||||
|
ι 𝓝ᶠ(a * [ofCrAnListF φs, ofCrAnOpF φa]ₛca * b) = 0 := by
|
||||||
|
rw [← ofCrAnListF_singleton, superCommuteF_ofCrAnListF_ofCrAnListF_symm, ofCrAnListF_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]
|
||||||
|
rw [ι_normalOrderF_superCommuteF_ofCrAnOpF_ofCrAnListF_eq_zero_mul]
|
||||||
|
simp
|
||||||
|
|
||||||
|
lemma ι_normalOrderF_superCommuteF_ofCrAnListF_ofCrAnListF_eq_zero_mul
|
||||||
|
(φs φs' : List 𝓕.CrAnFieldOp) (a b : 𝓕.FieldOpFreeAlgebra) :
|
||||||
|
ι 𝓝ᶠ(a * [ofCrAnListF φs, ofCrAnListF φs']ₛca * b) = 0 := by
|
||||||
|
rw [superCommuteF_ofCrAnListF_ofCrAnListF_eq_sum, Finset.mul_sum, Finset.sum_mul]
|
||||||
|
rw [map_sum, map_sum]
|
||||||
|
apply Fintype.sum_eq_zero
|
||||||
|
intro n
|
||||||
|
rw [← mul_assoc, ← mul_assoc]
|
||||||
|
rw [mul_assoc _ _ b]
|
||||||
|
rw [ι_normalOrderF_superCommuteF_ofCrAnListF_ofCrAnOpF_eq_zero_mul]
|
||||||
|
|
||||||
|
lemma ι_normalOrderF_superCommuteF_ofCrAnListF_eq_zero_mul
|
||||||
|
(φs : List 𝓕.CrAnFieldOp)
|
||||||
|
(a b c : 𝓕.FieldOpFreeAlgebra) :
|
||||||
|
ι 𝓝ᶠ(a * [ofCrAnListF φs, c]ₛca * b) = 0 := by
|
||||||
|
change (ι.toLinearMap ∘ₗ normalOrderF ∘ₗ
|
||||||
|
mulLinearMap.flip b ∘ₗ mulLinearMap a ∘ₗ superCommuteF (ofCrAnListF φs)) c = 0
|
||||||
|
have hf : (ι.toLinearMap ∘ₗ normalOrderF ∘ₗ
|
||||||
|
mulLinearMap.flip b ∘ₗ mulLinearMap a ∘ₗ superCommuteF (ofCrAnListF φs)) = 0 := by
|
||||||
|
apply ofCrAnListFBasis.ext
|
||||||
|
intro φs'
|
||||||
|
simp only [mulLinearMap, LinearMap.coe_mk, AddHom.coe_mk, ofListBasis_eq_ofList,
|
||||||
|
LinearMap.coe_comp, Function.comp_apply, LinearMap.flip_apply, AlgHom.toLinearMap_apply,
|
||||||
|
LinearMap.zero_apply]
|
||||||
|
rw [ι_normalOrderF_superCommuteF_ofCrAnListF_ofCrAnListF_eq_zero_mul]
|
||||||
|
rw [hf]
|
||||||
|
simp
|
||||||
|
|
||||||
|
@[simp]
|
||||||
|
lemma ι_normalOrderF_superCommuteF_eq_zero_mul
|
||||||
|
(a b c d : 𝓕.FieldOpFreeAlgebra) : ι 𝓝ᶠ(a * [d, c]ₛca * b) = 0 := by
|
||||||
|
change (ι.toLinearMap ∘ₗ normalOrderF ∘ₗ
|
||||||
|
mulLinearMap.flip b ∘ₗ mulLinearMap a ∘ₗ superCommuteF.flip c) d = 0
|
||||||
|
have hf : (ι.toLinearMap ∘ₗ normalOrderF ∘ₗ
|
||||||
|
mulLinearMap.flip b ∘ₗ mulLinearMap a ∘ₗ superCommuteF.flip c) = 0 := by
|
||||||
|
apply ofCrAnListFBasis.ext
|
||||||
|
intro φs
|
||||||
|
simp only [mulLinearMap, LinearMap.coe_mk, AddHom.coe_mk, ofListBasis_eq_ofList,
|
||||||
|
LinearMap.coe_comp, Function.comp_apply, LinearMap.flip_apply, AlgHom.toLinearMap_apply,
|
||||||
|
LinearMap.zero_apply]
|
||||||
|
rw [ι_normalOrderF_superCommuteF_ofCrAnListF_eq_zero_mul]
|
||||||
|
rw [hf]
|
||||||
|
simp
|
||||||
|
|
||||||
|
@[simp]
|
||||||
|
lemma ι_normalOrder_superCommuteF_eq_zero_mul_right (b c d : 𝓕.FieldOpFreeAlgebra) :
|
||||||
|
ι 𝓝ᶠ([d, c]ₛca * b) = 0 := by
|
||||||
|
rw [← ι_normalOrderF_superCommuteF_eq_zero_mul 1 b c d]
|
||||||
|
simp
|
||||||
|
|
||||||
|
@[simp]
|
||||||
|
lemma ι_normalOrderF_superCommuteF_eq_zero_mul_left (a c d : 𝓕.FieldOpFreeAlgebra) :
|
||||||
|
ι 𝓝ᶠ(a * [d, c]ₛca) = 0 := by
|
||||||
|
rw [← ι_normalOrderF_superCommuteF_eq_zero_mul a 1 c d]
|
||||||
|
simp
|
||||||
|
|
||||||
|
@[simp]
|
||||||
|
lemma ι_normalOrderF_superCommuteF_eq_zero_mul_mul_right (a b1 b2 c d: 𝓕.FieldOpFreeAlgebra) :
|
||||||
|
ι 𝓝ᶠ(a * [d, c]ₛca * b1 * b2) = 0 := by
|
||||||
|
rw [← ι_normalOrderF_superCommuteF_eq_zero_mul a (b1 * b2) c d]
|
||||||
|
congr 2
|
||||||
|
noncomm_ring
|
||||||
|
|
||||||
|
@[simp]
|
||||||
|
lemma ι_normalOrderF_superCommuteF_eq_zero (c d : 𝓕.FieldOpFreeAlgebra) : ι 𝓝ᶠ([d, c]ₛca) = 0 := by
|
||||||
|
rw [← ι_normalOrderF_superCommuteF_eq_zero_mul 1 1 c d]
|
||||||
|
simp
|
||||||
|
|
||||||
|
/-!
|
||||||
|
|
||||||
|
## Defining normal order for `FiedOpAlgebra`.
|
||||||
|
|
||||||
|
-/
|
||||||
|
|
||||||
|
lemma ι_normalOrderF_zero_of_mem_ideal (a : 𝓕.FieldOpFreeAlgebra)
|
||||||
|
(h : a ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet) : ι 𝓝ᶠ(a) = 0 := by
|
||||||
|
rw [TwoSidedIdeal.mem_span_iff_mem_addSubgroup_closure] at h
|
||||||
|
let p {k : Set 𝓕.FieldOpFreeAlgebra} (a : FieldOpFreeAlgebra 𝓕)
|
||||||
|
(h : a ∈ AddSubgroup.closure k) := ι 𝓝ᶠ(a) = 0
|
||||||
|
change p a h
|
||||||
|
apply AddSubgroup.closure_induction
|
||||||
|
· intro x hx
|
||||||
|
obtain ⟨a, ha, b, hb, rfl⟩ := Set.mem_mul.mp hx
|
||||||
|
obtain ⟨a, ha, c, hc, rfl⟩ := ha
|
||||||
|
simp only [p]
|
||||||
|
simp only [fieldOpIdealSet, exists_prop, exists_and_left, Set.mem_setOf_eq] at hc
|
||||||
|
match hc with
|
||||||
|
| Or.inl hc =>
|
||||||
|
obtain ⟨φa, φa', hφa, hφa', rfl⟩ := hc
|
||||||
|
simp [mul_sub, sub_mul, ← mul_assoc]
|
||||||
|
| Or.inr (Or.inl hc) =>
|
||||||
|
obtain ⟨φa, φa', hφa, hφa', rfl⟩ := hc
|
||||||
|
simp [mul_sub, sub_mul, ← mul_assoc]
|
||||||
|
| Or.inr (Or.inr (Or.inl hc)) =>
|
||||||
|
obtain ⟨φa, φa', hφa, hφa', rfl⟩ := hc
|
||||||
|
simp [mul_sub, sub_mul, ← mul_assoc]
|
||||||
|
| Or.inr (Or.inr (Or.inr hc)) =>
|
||||||
|
obtain ⟨φa, φa', hφa, hφa', rfl⟩ := hc
|
||||||
|
simp [mul_sub, sub_mul, ← mul_assoc]
|
||||||
|
· simp [p]
|
||||||
|
· intro x y hx hy
|
||||||
|
simp only [map_add, p]
|
||||||
|
intro h1 h2
|
||||||
|
simp [h1, h2]
|
||||||
|
· intro x hx
|
||||||
|
simp [p]
|
||||||
|
|
||||||
|
lemma ι_normalOrderF_eq_of_equiv (a b : 𝓕.FieldOpFreeAlgebra) (h : a ≈ b) :
|
||||||
|
ι 𝓝ᶠ(a) = ι 𝓝ᶠ(b) := by
|
||||||
|
rw [equiv_iff_sub_mem_ideal] at h
|
||||||
|
rw [LinearMap.sub_mem_ker_iff.mp]
|
||||||
|
simp only [LinearMap.mem_ker, ← map_sub]
|
||||||
|
exact ι_normalOrderF_zero_of_mem_ideal (a - b) h
|
||||||
|
|
||||||
|
/-- Normal ordering on `FieldOpAlgebra`. -/
|
||||||
|
noncomputable def normalOrder : FieldOpAlgebra 𝓕 →ₗ[ℂ] FieldOpAlgebra 𝓕 where
|
||||||
|
toFun := Quotient.lift (ι.toLinearMap ∘ₗ normalOrderF) ι_normalOrderF_eq_of_equiv
|
||||||
|
map_add' x y := by
|
||||||
|
obtain ⟨x, rfl⟩ := ι_surjective x
|
||||||
|
obtain ⟨y, rfl⟩ := ι_surjective y
|
||||||
|
rw [← map_add, ι_apply, ι_apply, ι_apply]
|
||||||
|
rw [Quotient.lift_mk, Quotient.lift_mk, Quotient.lift_mk]
|
||||||
|
simp
|
||||||
|
map_smul' c y := by
|
||||||
|
obtain ⟨y, rfl⟩ := ι_surjective y
|
||||||
|
rw [← map_smul, ι_apply, ι_apply]
|
||||||
|
simp
|
||||||
|
|
||||||
|
@[inherit_doc normalOrder]
|
||||||
|
scoped[FieldSpecification.FieldOpAlgebra] notation "𝓝(" a ")" => normalOrder a
|
||||||
|
|
||||||
|
end FieldOpAlgebra
|
||||||
|
end FieldSpecification
|
||||||
|
|
@ -3,11 +3,10 @@ Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
|
||||||
Released under Apache 2.0 license as described in the file LICENSE.
|
Released under Apache 2.0 license as described in the file LICENSE.
|
||||||
Authors: Joseph Tooby-Smith
|
Authors: Joseph Tooby-Smith
|
||||||
-/
|
-/
|
||||||
import HepLean.PerturbationTheory.FieldOpFreeAlgebra.NormalOrder
|
import HepLean.PerturbationTheory.FieldOpAlgebra.NormalOrder.Basic
|
||||||
import HepLean.PerturbationTheory.FieldOpAlgebra.SuperCommute
|
|
||||||
/-!
|
/-!
|
||||||
|
|
||||||
# Normal Ordering on Field operator algebra
|
# Basic properties of normal ordering
|
||||||
|
|
||||||
-/
|
-/
|
||||||
|
|
||||||
|
|
@ -21,224 +20,6 @@ variable {𝓕 : FieldSpecification}
|
||||||
|
|
||||||
/-!
|
/-!
|
||||||
|
|
||||||
## Normal order on super-commutators.
|
|
||||||
|
|
||||||
The main result of this is
|
|
||||||
`ι_normalOrderF_superCommuteF_eq_zero_mul`
|
|
||||||
which states that applying `ι` to the normal order of something containing a super-commutator
|
|
||||||
is zero.
|
|
||||||
|
|
||||||
-/
|
|
||||||
|
|
||||||
lemma ι_normalOrderF_superCommuteF_ofCrAnListF_ofCrAnListF_eq_zero
|
|
||||||
(φa φa' : 𝓕.CrAnFieldOp) (φs φs' : List 𝓕.CrAnFieldOp) :
|
|
||||||
ι 𝓝ᶠ(ofCrAnListF φs * [ofCrAnOpF φa, ofCrAnOpF φa']ₛca * ofCrAnListF φ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 [normalOrderF_superCommuteF_ofCrAnListF_create_create_ofCrAnListF φa φa' hφa hφa' φs φs']
|
|
||||||
rw [map_smul, map_mul, map_mul, map_mul, ι_superCommuteF_of_create_create φa φa' hφa hφa']
|
|
||||||
simp
|
|
||||||
· rw [normalOrderF_superCommuteF_create_annihilate φa φa' hφa hφa' (ofCrAnListF φs)
|
|
||||||
(ofCrAnListF φs')]
|
|
||||||
simp
|
|
||||||
· rw [normalOrderF_superCommuteF_annihilate_create φa' φa hφa' hφa (ofCrAnListF φs)
|
|
||||||
(ofCrAnListF φs')]
|
|
||||||
simp
|
|
||||||
· rw [normalOrderF_superCommuteF_ofCrAnListF_annihilate_annihilate_ofCrAnListF
|
|
||||||
φa φa' hφa hφa' φs φs']
|
|
||||||
rw [map_smul, map_mul, map_mul, map_mul,
|
|
||||||
ι_superCommuteF_of_annihilate_annihilate φa φa' hφa hφa']
|
|
||||||
simp
|
|
||||||
|
|
||||||
lemma ι_normalOrderF_superCommuteF_ofCrAnListF_eq_zero
|
|
||||||
(φa φa' : 𝓕.CrAnFieldOp) (φs : List 𝓕.CrAnFieldOp)
|
|
||||||
(a : 𝓕.FieldOpFreeAlgebra) :
|
|
||||||
ι 𝓝ᶠ(ofCrAnListF φs * [ofCrAnOpF φa, ofCrAnOpF φa']ₛca * a) = 0 := by
|
|
||||||
have hf : ι.toLinearMap ∘ₗ normalOrderF ∘ₗ
|
|
||||||
mulLinearMap (ofCrAnListF φs * [ofCrAnOpF φa, ofCrAnOpF φa']ₛca) = 0 := by
|
|
||||||
apply ofCrAnListFBasis.ext
|
|
||||||
intro l
|
|
||||||
simp only [FieldOpFreeAlgebra.ofListBasis_eq_ofList, LinearMap.coe_comp, Function.comp_apply,
|
|
||||||
AlgHom.toLinearMap_apply, LinearMap.zero_apply]
|
|
||||||
exact ι_normalOrderF_superCommuteF_ofCrAnListF_ofCrAnListF_eq_zero φa φa' φs l
|
|
||||||
change (ι.toLinearMap ∘ₗ normalOrderF ∘ₗ
|
|
||||||
mulLinearMap ((ofCrAnListF φs * [ofCrAnOpF φa, ofCrAnOpF φa']ₛca))) a = 0
|
|
||||||
rw [hf]
|
|
||||||
simp
|
|
||||||
|
|
||||||
lemma ι_normalOrderF_superCommuteF_ofCrAnOpF_eq_zero_mul (φa φa' : 𝓕.CrAnFieldOp)
|
|
||||||
(a b : 𝓕.FieldOpFreeAlgebra) :
|
|
||||||
ι 𝓝ᶠ(a * [ofCrAnOpF φa, ofCrAnOpF φa']ₛca * b) = 0 := by
|
|
||||||
rw [mul_assoc]
|
|
||||||
change (ι.toLinearMap ∘ₗ normalOrderF ∘ₗ mulLinearMap.flip
|
|
||||||
([ofCrAnOpF φa, ofCrAnOpF φa']ₛca * b)) a = 0
|
|
||||||
have hf : ι.toLinearMap ∘ₗ normalOrderF ∘ₗ mulLinearMap.flip
|
|
||||||
([ofCrAnOpF φa, ofCrAnOpF φa']ₛca * b) = 0 := by
|
|
||||||
apply ofCrAnListFBasis.ext
|
|
||||||
intro l
|
|
||||||
simp only [mulLinearMap, FieldOpFreeAlgebra.ofListBasis_eq_ofList, LinearMap.coe_comp,
|
|
||||||
Function.comp_apply, LinearMap.flip_apply, LinearMap.coe_mk, AddHom.coe_mk,
|
|
||||||
AlgHom.toLinearMap_apply, LinearMap.zero_apply]
|
|
||||||
rw [← mul_assoc]
|
|
||||||
exact ι_normalOrderF_superCommuteF_ofCrAnListF_eq_zero φa φa' _ _
|
|
||||||
rw [hf]
|
|
||||||
simp
|
|
||||||
|
|
||||||
lemma ι_normalOrderF_superCommuteF_ofCrAnOpF_ofCrAnListF_eq_zero_mul (φa : 𝓕.CrAnFieldOp)
|
|
||||||
(φs : List 𝓕.CrAnFieldOp)
|
|
||||||
(a b : 𝓕.FieldOpFreeAlgebra) :
|
|
||||||
ι 𝓝ᶠ(a * [ofCrAnOpF φa, ofCrAnListF φs]ₛca * b) = 0 := by
|
|
||||||
rw [← ofCrAnListF_singleton, superCommuteF_ofCrAnListF_ofCrAnListF_eq_sum]
|
|
||||||
rw [Finset.mul_sum, Finset.sum_mul]
|
|
||||||
rw [map_sum, map_sum]
|
|
||||||
apply Fintype.sum_eq_zero
|
|
||||||
intro n
|
|
||||||
rw [← mul_assoc, ← mul_assoc]
|
|
||||||
rw [mul_assoc _ _ b, ofCrAnListF_singleton]
|
|
||||||
rw [ι_normalOrderF_superCommuteF_ofCrAnOpF_eq_zero_mul]
|
|
||||||
|
|
||||||
lemma ι_normalOrderF_superCommuteF_ofCrAnListF_ofCrAnOpF_eq_zero_mul (φa : 𝓕.CrAnFieldOp)
|
|
||||||
(φs : List 𝓕.CrAnFieldOp) (a b : 𝓕.FieldOpFreeAlgebra) :
|
|
||||||
ι 𝓝ᶠ(a * [ofCrAnListF φs, ofCrAnOpF φa]ₛca * b) = 0 := by
|
|
||||||
rw [← ofCrAnListF_singleton, superCommuteF_ofCrAnListF_ofCrAnListF_symm, ofCrAnListF_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]
|
|
||||||
rw [ι_normalOrderF_superCommuteF_ofCrAnOpF_ofCrAnListF_eq_zero_mul]
|
|
||||||
simp
|
|
||||||
|
|
||||||
lemma ι_normalOrderF_superCommuteF_ofCrAnListF_ofCrAnListF_eq_zero_mul
|
|
||||||
(φs φs' : List 𝓕.CrAnFieldOp) (a b : 𝓕.FieldOpFreeAlgebra) :
|
|
||||||
ι 𝓝ᶠ(a * [ofCrAnListF φs, ofCrAnListF φs']ₛca * b) = 0 := by
|
|
||||||
rw [superCommuteF_ofCrAnListF_ofCrAnListF_eq_sum, Finset.mul_sum, Finset.sum_mul]
|
|
||||||
rw [map_sum, map_sum]
|
|
||||||
apply Fintype.sum_eq_zero
|
|
||||||
intro n
|
|
||||||
rw [← mul_assoc, ← mul_assoc]
|
|
||||||
rw [mul_assoc _ _ b]
|
|
||||||
rw [ι_normalOrderF_superCommuteF_ofCrAnListF_ofCrAnOpF_eq_zero_mul]
|
|
||||||
|
|
||||||
lemma ι_normalOrderF_superCommuteF_ofCrAnListF_eq_zero_mul
|
|
||||||
(φs : List 𝓕.CrAnFieldOp)
|
|
||||||
(a b c : 𝓕.FieldOpFreeAlgebra) :
|
|
||||||
ι 𝓝ᶠ(a * [ofCrAnListF φs, c]ₛca * b) = 0 := by
|
|
||||||
change (ι.toLinearMap ∘ₗ normalOrderF ∘ₗ
|
|
||||||
mulLinearMap.flip b ∘ₗ mulLinearMap a ∘ₗ superCommuteF (ofCrAnListF φs)) c = 0
|
|
||||||
have hf : (ι.toLinearMap ∘ₗ normalOrderF ∘ₗ
|
|
||||||
mulLinearMap.flip b ∘ₗ mulLinearMap a ∘ₗ superCommuteF (ofCrAnListF φs)) = 0 := by
|
|
||||||
apply ofCrAnListFBasis.ext
|
|
||||||
intro φs'
|
|
||||||
simp only [mulLinearMap, LinearMap.coe_mk, AddHom.coe_mk, ofListBasis_eq_ofList,
|
|
||||||
LinearMap.coe_comp, Function.comp_apply, LinearMap.flip_apply, AlgHom.toLinearMap_apply,
|
|
||||||
LinearMap.zero_apply]
|
|
||||||
rw [ι_normalOrderF_superCommuteF_ofCrAnListF_ofCrAnListF_eq_zero_mul]
|
|
||||||
rw [hf]
|
|
||||||
simp
|
|
||||||
|
|
||||||
@[simp]
|
|
||||||
lemma ι_normalOrderF_superCommuteF_eq_zero_mul
|
|
||||||
(a b c d : 𝓕.FieldOpFreeAlgebra) : ι 𝓝ᶠ(a * [d, c]ₛca * b) = 0 := by
|
|
||||||
change (ι.toLinearMap ∘ₗ normalOrderF ∘ₗ
|
|
||||||
mulLinearMap.flip b ∘ₗ mulLinearMap a ∘ₗ superCommuteF.flip c) d = 0
|
|
||||||
have hf : (ι.toLinearMap ∘ₗ normalOrderF ∘ₗ
|
|
||||||
mulLinearMap.flip b ∘ₗ mulLinearMap a ∘ₗ superCommuteF.flip c) = 0 := by
|
|
||||||
apply ofCrAnListFBasis.ext
|
|
||||||
intro φs
|
|
||||||
simp only [mulLinearMap, LinearMap.coe_mk, AddHom.coe_mk, ofListBasis_eq_ofList,
|
|
||||||
LinearMap.coe_comp, Function.comp_apply, LinearMap.flip_apply, AlgHom.toLinearMap_apply,
|
|
||||||
LinearMap.zero_apply]
|
|
||||||
rw [ι_normalOrderF_superCommuteF_ofCrAnListF_eq_zero_mul]
|
|
||||||
rw [hf]
|
|
||||||
simp
|
|
||||||
|
|
||||||
@[simp]
|
|
||||||
lemma ι_normalOrder_superCommuteF_eq_zero_mul_right (b c d : 𝓕.FieldOpFreeAlgebra) :
|
|
||||||
ι 𝓝ᶠ([d, c]ₛca * b) = 0 := by
|
|
||||||
rw [← ι_normalOrderF_superCommuteF_eq_zero_mul 1 b c d]
|
|
||||||
simp
|
|
||||||
|
|
||||||
@[simp]
|
|
||||||
lemma ι_normalOrderF_superCommuteF_eq_zero_mul_left (a c d : 𝓕.FieldOpFreeAlgebra) :
|
|
||||||
ι 𝓝ᶠ(a * [d, c]ₛca) = 0 := by
|
|
||||||
rw [← ι_normalOrderF_superCommuteF_eq_zero_mul a 1 c d]
|
|
||||||
simp
|
|
||||||
|
|
||||||
@[simp]
|
|
||||||
lemma ι_normalOrderF_superCommuteF_eq_zero_mul_mul_right (a b1 b2 c d: 𝓕.FieldOpFreeAlgebra) :
|
|
||||||
ι 𝓝ᶠ(a * [d, c]ₛca * b1 * b2) = 0 := by
|
|
||||||
rw [← ι_normalOrderF_superCommuteF_eq_zero_mul a (b1 * b2) c d]
|
|
||||||
congr 2
|
|
||||||
noncomm_ring
|
|
||||||
|
|
||||||
@[simp]
|
|
||||||
lemma ι_normalOrderF_superCommuteF_eq_zero (c d : 𝓕.FieldOpFreeAlgebra) : ι 𝓝ᶠ([d, c]ₛca) = 0 := by
|
|
||||||
rw [← ι_normalOrderF_superCommuteF_eq_zero_mul 1 1 c d]
|
|
||||||
simp
|
|
||||||
|
|
||||||
/-!
|
|
||||||
|
|
||||||
## Defining normal order for `FiedOpAlgebra`.
|
|
||||||
|
|
||||||
-/
|
|
||||||
|
|
||||||
lemma ι_normalOrderF_zero_of_mem_ideal (a : 𝓕.FieldOpFreeAlgebra)
|
|
||||||
(h : a ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet) : ι 𝓝ᶠ(a) = 0 := by
|
|
||||||
rw [TwoSidedIdeal.mem_span_iff_mem_addSubgroup_closure] at h
|
|
||||||
let p {k : Set 𝓕.FieldOpFreeAlgebra} (a : FieldOpFreeAlgebra 𝓕)
|
|
||||||
(h : a ∈ AddSubgroup.closure k) := ι 𝓝ᶠ(a) = 0
|
|
||||||
change p a h
|
|
||||||
apply AddSubgroup.closure_induction
|
|
||||||
· intro x hx
|
|
||||||
obtain ⟨a, ha, b, hb, rfl⟩ := Set.mem_mul.mp hx
|
|
||||||
obtain ⟨a, ha, c, hc, rfl⟩ := ha
|
|
||||||
simp only [p]
|
|
||||||
simp only [fieldOpIdealSet, exists_prop, exists_and_left, Set.mem_setOf_eq] at hc
|
|
||||||
match hc with
|
|
||||||
| Or.inl hc =>
|
|
||||||
obtain ⟨φa, φa', hφa, hφa', rfl⟩ := hc
|
|
||||||
simp [mul_sub, sub_mul, ← mul_assoc]
|
|
||||||
| Or.inr (Or.inl hc) =>
|
|
||||||
obtain ⟨φa, φa', hφa, hφa', rfl⟩ := hc
|
|
||||||
simp [mul_sub, sub_mul, ← mul_assoc]
|
|
||||||
| Or.inr (Or.inr (Or.inl hc)) =>
|
|
||||||
obtain ⟨φa, φa', hφa, hφa', rfl⟩ := hc
|
|
||||||
simp [mul_sub, sub_mul, ← mul_assoc]
|
|
||||||
| Or.inr (Or.inr (Or.inr hc)) =>
|
|
||||||
obtain ⟨φa, φa', hφa, hφa', rfl⟩ := hc
|
|
||||||
simp [mul_sub, sub_mul, ← mul_assoc]
|
|
||||||
· simp [p]
|
|
||||||
· intro x y hx hy
|
|
||||||
simp only [map_add, p]
|
|
||||||
intro h1 h2
|
|
||||||
simp [h1, h2]
|
|
||||||
· intro x hx
|
|
||||||
simp [p]
|
|
||||||
|
|
||||||
lemma ι_normalOrderF_eq_of_equiv (a b : 𝓕.FieldOpFreeAlgebra) (h : a ≈ b) :
|
|
||||||
ι 𝓝ᶠ(a) = ι 𝓝ᶠ(b) := by
|
|
||||||
rw [equiv_iff_sub_mem_ideal] at h
|
|
||||||
rw [LinearMap.sub_mem_ker_iff.mp]
|
|
||||||
simp only [LinearMap.mem_ker, ← map_sub]
|
|
||||||
exact ι_normalOrderF_zero_of_mem_ideal (a - b) h
|
|
||||||
|
|
||||||
/-- Normal ordering on `FieldOpAlgebra`. -/
|
|
||||||
noncomputable def normalOrder : FieldOpAlgebra 𝓕 →ₗ[ℂ] FieldOpAlgebra 𝓕 where
|
|
||||||
toFun := Quotient.lift (ι.toLinearMap ∘ₗ normalOrderF) ι_normalOrderF_eq_of_equiv
|
|
||||||
map_add' x y := by
|
|
||||||
obtain ⟨x, rfl⟩ := ι_surjective x
|
|
||||||
obtain ⟨y, rfl⟩ := ι_surjective y
|
|
||||||
rw [← map_add, ι_apply, ι_apply, ι_apply]
|
|
||||||
rw [Quotient.lift_mk, Quotient.lift_mk, Quotient.lift_mk]
|
|
||||||
simp
|
|
||||||
map_smul' c y := by
|
|
||||||
obtain ⟨y, rfl⟩ := ι_surjective y
|
|
||||||
rw [← map_smul, ι_apply, ι_apply]
|
|
||||||
simp
|
|
||||||
|
|
||||||
@[inherit_doc normalOrder]
|
|
||||||
scoped[FieldSpecification.FieldOpAlgebra] notation "𝓝(" a ")" => normalOrder a
|
|
||||||
|
|
||||||
/-!
|
|
||||||
|
|
||||||
## Properties of normal ordering.
|
## Properties of normal ordering.
|
||||||
|
|
||||||
-/
|
-/
|
||||||
|
|
@ -532,14 +313,13 @@ noncomputable def contractStateAtIndex (φ : 𝓕.FieldOp) (φs : List 𝓕.Fiel
|
||||||
| some n => 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ (φs.take n)) • [anPart φ, ofFieldOp φs[n]]ₛ
|
| some n => 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ (φs.take n)) • [anPart φ, ofFieldOp φs[n]]ₛ
|
||||||
|
|
||||||
/--
|
/--
|
||||||
Within a proto-operator algebra,
|
For a field specification `𝓕`, the following relation holds in the algebra `𝓕.FieldOpAlgebra`,
|
||||||
`φ * N(φ₀φ₁…φₙ) = N(φφ₀φ₁…φₙ) + ∑ i, (sᵢ • [anPartF φ, φᵢ]ₛ) * N(φ₀φ₁…φᵢ₋₁φᵢ₊₁…φₙ)`,
|
`φ * 𝓝(φ₀φ₁…φₙ) = 𝓝(φφ₀φ₁…φₙ) + ∑ i, (𝓢(φ,φ₀φ₁…φᵢ₋₁) • [anPartF φ, φᵢ]ₛ) * 𝓝(φ₀φ₁…φᵢ₋₁φᵢ₊₁…φₙ)`.
|
||||||
where `sₙ` is the exchange sign for `φ` and `φ₀φ₁…φᵢ₋₁`.
|
|
||||||
-/
|
-/
|
||||||
lemma ofFieldOp_mul_normalOrder_ofFieldOpList_eq_sum (φ : 𝓕.FieldOp)
|
lemma ofFieldOp_mul_normalOrder_ofFieldOpList_eq_sum (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) :
|
||||||
(φs : List 𝓕.FieldOp) : ofFieldOp φ * 𝓝(ofFieldOpList φs) =
|
ofFieldOp φ * 𝓝(ofFieldOpList φs) =
|
||||||
∑ n : Option (Fin φs.length), contractStateAtIndex φ φs n *
|
∑ n : Option (Fin φs.length), contractStateAtIndex φ φs n *
|
||||||
𝓝(ofFieldOpList (HepLean.List.optionEraseZ φs φ n)) := by
|
𝓝(ofFieldOpList (optionEraseZ φs φ n)) := by
|
||||||
rw [ofFieldOp_mul_normalOrder_ofFieldOpList_eq_superCommute]
|
rw [ofFieldOp_mul_normalOrder_ofFieldOpList_eq_superCommute]
|
||||||
rw [anPart_superCommute_normalOrder_ofFieldOpList_sum]
|
rw [anPart_superCommute_normalOrder_ofFieldOpList_sum]
|
||||||
simp only [instCommGroup.eq_1, Fin.getElem_fin, Algebra.smul_mul_assoc, contractStateAtIndex,
|
simp only [instCommGroup.eq_1, Fin.getElem_fin, Algebra.smul_mul_assoc, contractStateAtIndex,
|
||||||
|
|
@ -0,0 +1,118 @@
|
||||||
|
/-
|
||||||
|
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.FieldOpAlgebra.NormalOrder.Lemmas
|
||||||
|
import HepLean.PerturbationTheory.WickContraction.InsertAndContract
|
||||||
|
/-!
|
||||||
|
|
||||||
|
# Normal ordering with relation to Wick contractions
|
||||||
|
|
||||||
|
-/
|
||||||
|
|
||||||
|
namespace FieldSpecification
|
||||||
|
open FieldOpFreeAlgebra
|
||||||
|
open HepLean.List
|
||||||
|
open FieldStatistic
|
||||||
|
open WickContraction
|
||||||
|
namespace FieldOpAlgebra
|
||||||
|
variable {𝓕 : FieldSpecification}
|
||||||
|
|
||||||
|
/-!
|
||||||
|
|
||||||
|
## Normal order of uncontracted terms within proto-algebra.
|
||||||
|
|
||||||
|
-/
|
||||||
|
|
||||||
|
/--
|
||||||
|
Let `c` be a Wick Contraction for `φs := φ₀φ₁…φₙ`.
|
||||||
|
We have (roughly) `𝓝ᶠ([φsΛ ↩Λ φ i none]ᵘᶜ) = s • 𝓝ᶠ(φ :: [φsΛ]ᵘᶜ)`
|
||||||
|
Where `s` is the exchange sign for `φ` and the uncontracted fields in `φ₀φ₁…φᵢ₋₁`.
|
||||||
|
-/
|
||||||
|
lemma normalOrder_uncontracted_none (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
|
||||||
|
(i : Fin φs.length.succ) (φsΛ : WickContraction φs.length) :
|
||||||
|
𝓝(ofFieldOpList [φsΛ ↩Λ φ i none]ᵘᶜ)
|
||||||
|
= 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ ⟨φs.get, φsΛ.uncontracted.filter (fun x => i.succAbove x < i)⟩) •
|
||||||
|
𝓝(ofFieldOpList (φ :: [φsΛ]ᵘᶜ)) := by
|
||||||
|
simp only [Nat.succ_eq_add_one, instCommGroup.eq_1]
|
||||||
|
rw [ofFieldOpList_normalOrder_insert φ [φsΛ]ᵘᶜ
|
||||||
|
⟨(φsΛ.uncontractedListOrderPos i), by simp [uncontractedListGet]⟩, smul_smul]
|
||||||
|
trans (1 : ℂ) • (𝓝(ofFieldOpList [φsΛ ↩Λ φ i none]ᵘᶜ))
|
||||||
|
· simp
|
||||||
|
congr 1
|
||||||
|
simp only [instCommGroup.eq_1, uncontractedListGet]
|
||||||
|
rw [← List.map_take, take_uncontractedListOrderPos_eq_filter]
|
||||||
|
have h1 : (𝓕 |>ₛ List.map φs.get (List.filter (fun x => decide (↑x < i.1)) φsΛ.uncontractedList))
|
||||||
|
= 𝓕 |>ₛ ⟨φs.get, (φsΛ.uncontracted.filter (fun x => x.val < i.1))⟩ := by
|
||||||
|
simp only [Nat.succ_eq_add_one, ofFinset]
|
||||||
|
congr
|
||||||
|
rw [uncontractedList_eq_sort]
|
||||||
|
have hdup : (List.filter (fun x => decide (x.1 < i.1))
|
||||||
|
(Finset.sort (fun x1 x2 => x1 ≤ x2) φsΛ.uncontracted)).Nodup := by
|
||||||
|
exact List.Nodup.filter _ (Finset.sort_nodup (fun x1 x2 => x1 ≤ x2) φsΛ.uncontracted)
|
||||||
|
have hsort : (List.filter (fun x => decide (x.1 < i.1))
|
||||||
|
(Finset.sort (fun x1 x2 => x1 ≤ x2) φsΛ.uncontracted)).Sorted (· ≤ ·) := by
|
||||||
|
exact List.Sorted.filter _ (Finset.sort_sorted (fun x1 x2 => x1 ≤ x2) φsΛ.uncontracted)
|
||||||
|
rw [← (List.toFinset_sort (· ≤ ·) hdup).mpr hsort]
|
||||||
|
congr
|
||||||
|
ext a
|
||||||
|
simp
|
||||||
|
rw [h1]
|
||||||
|
simp only [Nat.succ_eq_add_one]
|
||||||
|
have h2 : (Finset.filter (fun x => x.1 < i.1) φsΛ.uncontracted) =
|
||||||
|
(Finset.filter (fun x => i.succAbove x < i) φsΛ.uncontracted) := by
|
||||||
|
ext a
|
||||||
|
simp only [Nat.succ_eq_add_one, Finset.mem_filter, and_congr_right_iff]
|
||||||
|
intro ha
|
||||||
|
simp only [Fin.succAbove]
|
||||||
|
split
|
||||||
|
· apply Iff.intro
|
||||||
|
· intro h
|
||||||
|
omega
|
||||||
|
· intro h
|
||||||
|
rename_i h
|
||||||
|
rw [Fin.lt_def] at h
|
||||||
|
simp only [Fin.coe_castSucc] at h
|
||||||
|
omega
|
||||||
|
· apply Iff.intro
|
||||||
|
· intro h
|
||||||
|
rename_i h'
|
||||||
|
rw [Fin.lt_def]
|
||||||
|
simp only [Fin.val_succ]
|
||||||
|
rw [Fin.lt_def] at h'
|
||||||
|
simp only [Fin.coe_castSucc, not_lt] at h'
|
||||||
|
omega
|
||||||
|
· intro h
|
||||||
|
rename_i h
|
||||||
|
rw [Fin.lt_def] at h
|
||||||
|
simp only [Fin.val_succ] at h
|
||||||
|
omega
|
||||||
|
rw [h2]
|
||||||
|
simp only [exchangeSign_mul_self]
|
||||||
|
congr
|
||||||
|
simp only [Nat.succ_eq_add_one]
|
||||||
|
rw [insertAndContract_uncontractedList_none_map]
|
||||||
|
|
||||||
|
/--
|
||||||
|
Let `c` be a Wick Contraction for `φ₀φ₁…φₙ`.
|
||||||
|
We have (roughly) `N(c ↩Λ φ i k).uncontractedList`
|
||||||
|
is equal to `N((c.uncontractedList).eraseIdx k')`
|
||||||
|
where `k'` is the position in `c.uncontractedList` corresponding to `k`.
|
||||||
|
-/
|
||||||
|
lemma normalOrder_uncontracted_some (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
|
||||||
|
(i : Fin φs.length.succ) (φsΛ : WickContraction φs.length) (k : φsΛ.uncontracted) :
|
||||||
|
𝓝(ofFieldOpList [φsΛ ↩Λ φ i (some k)]ᵘᶜ)
|
||||||
|
= 𝓝(ofFieldOpList (optionEraseZ [φsΛ]ᵘᶜ φ ((uncontractedFieldOpEquiv φs φsΛ) k))) := by
|
||||||
|
simp only [Nat.succ_eq_add_one, insertAndContract, optionEraseZ, uncontractedFieldOpEquiv,
|
||||||
|
Equiv.optionCongr_apply, Equiv.coe_trans, Option.map_some', Function.comp_apply, finCongr_apply,
|
||||||
|
Fin.coe_cast, uncontractedListGet]
|
||||||
|
congr
|
||||||
|
rw [congr_uncontractedList]
|
||||||
|
erw [uncontractedList_extractEquiv_symm_some]
|
||||||
|
simp only [Fin.coe_succAboveEmb, List.map_eraseIdx, List.map_map]
|
||||||
|
congr
|
||||||
|
conv_rhs => rw [get_eq_insertIdx_succAbove φ φs i]
|
||||||
|
|
||||||
|
end FieldOpAlgebra
|
||||||
|
end FieldSpecification
|
||||||
|
|
@ -3,9 +3,10 @@ Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
|
||||||
Released under Apache 2.0 license as described in the file LICENSE.
|
Released under Apache 2.0 license as described in the file LICENSE.
|
||||||
Authors: Joseph Tooby-Smith
|
Authors: Joseph Tooby-Smith
|
||||||
-/
|
-/
|
||||||
|
import HepLean.PerturbationTheory.FieldOpAlgebra.NormalOrder.WickContractions
|
||||||
|
import HepLean.PerturbationTheory.WickContraction.Sign.InsertNone
|
||||||
|
import HepLean.PerturbationTheory.WickContraction.Sign.InsertSome
|
||||||
import HepLean.PerturbationTheory.WickContraction.StaticContract
|
import HepLean.PerturbationTheory.WickContraction.StaticContract
|
||||||
import HepLean.PerturbationTheory.FieldOpAlgebra.WicksTheorem
|
|
||||||
import HepLean.Meta.Remark.Basic
|
|
||||||
/-!
|
/-!
|
||||||
|
|
||||||
# Static Wick's theorem
|
# Static Wick's theorem
|
||||||
|
|
@ -29,11 +30,16 @@ lemma static_wick_theorem_nil : ofFieldOpList [] = ∑ (φsΛ : WickContraction
|
||||||
|
|
||||||
/--
|
/--
|
||||||
The static Wicks theorem states that
|
The static Wicks theorem states that
|
||||||
`φ₀…φₙ` is equal to the sum of
|
`φ₀…φₙ` is equal to
|
||||||
`φsΛ.1.sign • φsΛ.1.staticContract * 𝓝(ofFieldOpList [φsΛ.1]ᵘᶜ)`
|
`∑ φsΛ, φsΛ.1.sign • φsΛ.1.staticContract * 𝓝(ofFieldOpList [φsΛ.1]ᵘᶜ)`
|
||||||
over all Wick contraction `φsΛ`.
|
over all Wick contraction `φsΛ`.
|
||||||
This is compared to the ordinary Wicks theorem in which `staticContract` is replaced with
|
This is compared to the ordinary Wicks theorem in which `staticContract` is replaced with
|
||||||
`timeContract`.
|
`timeContract`.
|
||||||
|
|
||||||
|
The proof is via induction on `φs`. The base case `φs = []` is handled by `static_wick_theorem_nil`.
|
||||||
|
The inductive step works as follows:
|
||||||
|
- The proof considers `φ₀…φₙ` as `φ₀(φ₁…φₙ)` and use the induction hypothesis on `φ₁…φₙ`.
|
||||||
|
- It also uses `ofFieldOp_mul_normalOrder_ofFieldOpList_eq_sum`
|
||||||
-/
|
-/
|
||||||
theorem static_wick_theorem : (φs : List 𝓕.FieldOp) →
|
theorem static_wick_theorem : (φs : List 𝓕.FieldOp) →
|
||||||
ofFieldOpList φs = ∑ (φsΛ : WickContraction φs.length),
|
ofFieldOpList φs = ∑ (φsΛ : WickContraction φs.length),
|
||||||
|
|
|
||||||
|
|
@ -3,7 +3,7 @@ Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
|
||||||
Released under Apache 2.0 license as described in the file LICENSE.
|
Released under Apache 2.0 license as described in the file LICENSE.
|
||||||
Authors: Joseph Tooby-Smith
|
Authors: Joseph Tooby-Smith
|
||||||
-/
|
-/
|
||||||
import HepLean.PerturbationTheory.FieldOpAlgebra.NormalOrder
|
import HepLean.PerturbationTheory.FieldOpAlgebra.NormalOrder.Lemmas
|
||||||
import HepLean.PerturbationTheory.FieldOpAlgebra.TimeOrder
|
import HepLean.PerturbationTheory.FieldOpAlgebra.TimeOrder
|
||||||
/-!
|
/-!
|
||||||
|
|
||||||
|
|
|
||||||
215
HepLean/PerturbationTheory/FieldOpAlgebra/WickTerm.lean
Normal file
215
HepLean/PerturbationTheory/FieldOpAlgebra/WickTerm.lean
Normal file
|
|
@ -0,0 +1,215 @@
|
||||||
|
/-
|
||||||
|
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.Sign.Basic
|
||||||
|
import HepLean.PerturbationTheory.WickContraction.Sign.InsertNone
|
||||||
|
import HepLean.PerturbationTheory.WickContraction.Sign.InsertSome
|
||||||
|
import HepLean.PerturbationTheory.WickContraction.TimeContract
|
||||||
|
import HepLean.PerturbationTheory.FieldOpAlgebra.NormalOrder.WickContractions
|
||||||
|
/-!
|
||||||
|
|
||||||
|
# Wick term
|
||||||
|
|
||||||
|
-/
|
||||||
|
|
||||||
|
open FieldSpecification
|
||||||
|
variable {𝓕 : FieldSpecification}
|
||||||
|
|
||||||
|
namespace WickContraction
|
||||||
|
variable {n : ℕ} (c : WickContraction n)
|
||||||
|
open HepLean.List
|
||||||
|
open FieldOpAlgebra
|
||||||
|
open FieldStatistic
|
||||||
|
noncomputable section
|
||||||
|
|
||||||
|
/-- For a Wick contraction `φsΛ`, we define `wickTerm φsΛ` to be the element of `𝓕.FieldOpAlgebra`
|
||||||
|
given by `φsΛ.sign • φsΛ.timeContract * 𝓝([φsΛ]ᵘᶜ)`. -/
|
||||||
|
def wickTerm {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) : 𝓕.FieldOpAlgebra :=
|
||||||
|
φsΛ.sign • φsΛ.timeContract * 𝓝(ofFieldOpList [φsΛ]ᵘᶜ)
|
||||||
|
|
||||||
|
/--
|
||||||
|
Let `φsΛ` be a Wick Contraction for `φs = φ₀φ₁…φₙ`. Then the wick-term of ` (φsΛ ↩Λ φ i none)`
|
||||||
|
|
||||||
|
```(φsΛ ↩Λ φ i none).sign • (φsΛ ↩Λ φ i none).timeContract 𝓞 * 𝓞.crAnF 𝓝ᶠ([φsΛ ↩Λ φ i none]ᵘᶜ)```
|
||||||
|
|
||||||
|
is equal to
|
||||||
|
|
||||||
|
`s • (φsΛ.sign • φsΛ.timeContract 𝓞 * 𝓞.crAnF 𝓝ᶠ(φ :: [φsΛ]ᵘᶜ))`
|
||||||
|
|
||||||
|
where `s` is the exchange sign of `φ` and the uncontracted fields in `φ₀φ₁…φᵢ₋₁`.
|
||||||
|
|
||||||
|
The proof of this result relies primarily on:
|
||||||
|
- `normalOrderF_uncontracted_none` which replaces `𝓝ᶠ([φsΛ ↩Λ φ i none]ᵘᶜ)` with
|
||||||
|
`𝓝ᶠ(φ :: [φsΛ]ᵘᶜ)` up to a sign.
|
||||||
|
- `timeContract_insertAndContract_none` which replaces `(φsΛ ↩Λ φ i none).timeContract 𝓞` with
|
||||||
|
`φsΛ.timeContract 𝓞`.
|
||||||
|
- `sign_insert_none` and `signInsertNone_eq_filterset` which are used to take account of
|
||||||
|
signs.
|
||||||
|
-/
|
||||||
|
lemma wickTerm_none_eq_wick_term_cons (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
|
||||||
|
(i : Fin φs.length.succ) (φsΛ : WickContraction φs.length) :
|
||||||
|
(φsΛ ↩Λ φ i none).wickTerm =
|
||||||
|
𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ ⟨φs.get, (Finset.univ.filter (fun k => i.succAbove k < i))⟩)
|
||||||
|
• (φsΛ.sign • φsΛ.timeContract * 𝓝(ofFieldOpList (φ :: [φsΛ]ᵘᶜ))) := by
|
||||||
|
rw [wickTerm]
|
||||||
|
by_cases hg : GradingCompliant φs φsΛ
|
||||||
|
· rw [normalOrder_uncontracted_none, sign_insert_none]
|
||||||
|
simp only [Nat.succ_eq_add_one, timeContract_insertAndContract_none, instCommGroup.eq_1,
|
||||||
|
Algebra.mul_smul_comm, Algebra.smul_mul_assoc, smul_smul]
|
||||||
|
congr 1
|
||||||
|
rw [← mul_assoc]
|
||||||
|
congr 1
|
||||||
|
rw [signInsertNone_eq_filterset _ _ _ _ hg, ← map_mul]
|
||||||
|
congr
|
||||||
|
rw [ofFinset_union]
|
||||||
|
congr
|
||||||
|
ext a
|
||||||
|
simp only [Finset.mem_sdiff, Finset.mem_union, Finset.mem_filter, Finset.mem_univ, true_and,
|
||||||
|
Finset.mem_inter, not_and, not_lt, and_imp]
|
||||||
|
apply Iff.intro
|
||||||
|
· intro ha
|
||||||
|
have ha1 := ha.1
|
||||||
|
rcases ha1 with ha1 | ha1
|
||||||
|
· exact ha1.2
|
||||||
|
· exact ha1.2
|
||||||
|
· intro ha
|
||||||
|
simp only [uncontracted, Finset.mem_filter, Finset.mem_univ, true_and, ha, and_true,
|
||||||
|
forall_const]
|
||||||
|
have hx : φsΛ.getDual? a = none ↔ ¬ (φsΛ.getDual? a).isSome := by
|
||||||
|
simp
|
||||||
|
rw [hx]
|
||||||
|
simp only [Bool.not_eq_true, Bool.eq_false_or_eq_true_self, true_and]
|
||||||
|
intro h1 h2
|
||||||
|
simp_all
|
||||||
|
· simp only [Nat.succ_eq_add_one, timeContract_insertAndContract_none, Algebra.smul_mul_assoc,
|
||||||
|
instCommGroup.eq_1]
|
||||||
|
rw [timeContract_of_not_gradingCompliant]
|
||||||
|
simp only [ZeroMemClass.coe_zero, zero_mul, smul_zero]
|
||||||
|
exact hg
|
||||||
|
|
||||||
|
/--
|
||||||
|
Let `c` be a Wick Contraction for `φ₀φ₁…φₙ`.
|
||||||
|
This lemma states that
|
||||||
|
`(c.sign • c.timeContract 𝓞) * N(c.uncontracted)`
|
||||||
|
for `c` equal to `c ↩Λ φ i (some k)` is equal to that for just `c`
|
||||||
|
mulitiplied by the exchange sign of `φ` and `φ₀φ₁…φᵢ₋₁`.
|
||||||
|
-/
|
||||||
|
lemma wickTerm_some_eq_wick_term_optionEraseZ (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
|
||||||
|
(i : Fin φs.length.succ) (φsΛ : WickContraction φs.length) (k : φsΛ.uncontracted)
|
||||||
|
(hlt : ∀ (k : Fin φs.length), timeOrderRel φ φs[k])
|
||||||
|
(hn : ∀ (k : Fin φs.length), i.succAbove k < i → ¬ timeOrderRel φs[k] φ) :
|
||||||
|
(φsΛ ↩Λ φ i (some k)).wickTerm =
|
||||||
|
𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ ⟨φs.get, (Finset.univ.filter (fun x => i.succAbove x < i))⟩)
|
||||||
|
• (φsΛ.sign • (contractStateAtIndex φ [φsΛ]ᵘᶜ
|
||||||
|
((uncontractedFieldOpEquiv φs φsΛ) (some k)) * φsΛ.timeContract)
|
||||||
|
* 𝓝(ofFieldOpList (optionEraseZ [φsΛ]ᵘᶜ φ (uncontractedFieldOpEquiv φs φsΛ k)))) := by
|
||||||
|
rw [wickTerm]
|
||||||
|
by_cases hg : GradingCompliant φs φsΛ ∧ (𝓕 |>ₛ φ) = (𝓕 |>ₛ φs[k.1])
|
||||||
|
· by_cases hk : i.succAbove k < i
|
||||||
|
· rw [WickContraction.timeConract_insertAndContract_some_eq_mul_contractStateAtIndex_not_lt]
|
||||||
|
swap
|
||||||
|
· exact hn _ hk
|
||||||
|
rw [normalOrder_uncontracted_some, sign_insert_some]
|
||||||
|
simp only [instCommGroup.eq_1, smul_smul, Algebra.smul_mul_assoc]
|
||||||
|
congr 1
|
||||||
|
rw [mul_assoc, mul_comm (sign φs φsΛ), ← mul_assoc]
|
||||||
|
congr 1
|
||||||
|
exact signInsertSome_mul_filter_contracted_of_lt φ φs φsΛ i k hk hg
|
||||||
|
· omega
|
||||||
|
· have hik : i.succAbove ↑k ≠ i := Fin.succAbove_ne i ↑k
|
||||||
|
rw [timeContract_insertAndContract_some_eq_mul_contractStateAtIndex_lt]
|
||||||
|
swap
|
||||||
|
· exact hlt _
|
||||||
|
rw [normalOrder_uncontracted_some]
|
||||||
|
rw [sign_insert_some]
|
||||||
|
simp only [instCommGroup.eq_1, smul_smul, Algebra.smul_mul_assoc]
|
||||||
|
congr 1
|
||||||
|
rw [mul_assoc, mul_comm (sign φs φsΛ), ← mul_assoc]
|
||||||
|
congr 1
|
||||||
|
exact signInsertSome_mul_filter_contracted_of_not_lt φ φs φsΛ i k hk hg
|
||||||
|
· omega
|
||||||
|
· rw [timeConract_insertAndContract_some]
|
||||||
|
simp only [Fin.getElem_fin, not_and] at hg
|
||||||
|
by_cases hg' : GradingCompliant φs φsΛ
|
||||||
|
· have hg := hg hg'
|
||||||
|
simp only [Nat.succ_eq_add_one, Fin.getElem_fin, ite_mul, Algebra.smul_mul_assoc,
|
||||||
|
instCommGroup.eq_1, contractStateAtIndex, uncontractedFieldOpEquiv, Equiv.optionCongr_apply,
|
||||||
|
Equiv.coe_trans, Option.map_some', Function.comp_apply, finCongr_apply, Fin.coe_cast,
|
||||||
|
List.getElem_map, uncontractedList_getElem_uncontractedIndexEquiv_symm, List.get_eq_getElem,
|
||||||
|
uncontractedListGet]
|
||||||
|
by_cases h1 : i < i.succAbove ↑k
|
||||||
|
· simp only [h1, ↓reduceIte, MulMemClass.coe_mul]
|
||||||
|
rw [timeContract_zero_of_diff_grade]
|
||||||
|
simp only [zero_mul, smul_zero]
|
||||||
|
rw [superCommute_anPart_ofFieldOpF_diff_grade_zero]
|
||||||
|
simp only [zero_mul, smul_zero]
|
||||||
|
exact hg
|
||||||
|
exact hg
|
||||||
|
· simp only [h1, ↓reduceIte, MulMemClass.coe_mul]
|
||||||
|
rw [timeContract_zero_of_diff_grade]
|
||||||
|
simp only [zero_mul, smul_zero]
|
||||||
|
rw [superCommute_anPart_ofFieldOpF_diff_grade_zero]
|
||||||
|
simp only [zero_mul, smul_zero]
|
||||||
|
exact hg
|
||||||
|
exact fun a => hg (id (Eq.symm a))
|
||||||
|
· rw [timeContract_of_not_gradingCompliant]
|
||||||
|
simp only [Nat.succ_eq_add_one, Fin.getElem_fin, mul_zero, ZeroMemClass.coe_zero, smul_zero,
|
||||||
|
zero_mul, instCommGroup.eq_1]
|
||||||
|
exact hg'
|
||||||
|
|
||||||
|
/--
|
||||||
|
Given a Wick contraction `φsΛ` of `φs = φ₀φ₁…φₙ` and an `i`, we have that
|
||||||
|
`(φsΛ.sign • φsΛ.timeContract 𝓞) * 𝓞.crAnF (φ * 𝓝ᶠ([φsΛ]ᵘᶜ))`
|
||||||
|
is equal to the product of
|
||||||
|
- the exchange sign of `φ` and `φ₀φ₁…φᵢ₋₁`,
|
||||||
|
- the sum of `((φsΛ ↩Λ φ i k).sign • (φsΛ ↩Λ φ i k).timeContract 𝓞) * 𝓞.crAnF 𝓝ᶠ([φsΛ ↩Λ φ i k]ᵘᶜ)`
|
||||||
|
over all `k` in `Option φsΛ.uncontracted`.
|
||||||
|
|
||||||
|
The proof of this result primarily depends on
|
||||||
|
- `crAnF_ofFieldOpF_mul_normalOrderF_ofFieldOpFsList_eq_sum` to rewrite `𝓞.crAnF (φ * 𝓝ᶠ([φsΛ]ᵘᶜ))`
|
||||||
|
- `wick_term_none_eq_wick_term_cons`
|
||||||
|
- `wick_term_some_eq_wick_term_optionEraseZ`
|
||||||
|
-/
|
||||||
|
lemma wickTerm_cons_eq_sum_wick_term (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) (i : Fin φs.length.succ)
|
||||||
|
(φsΛ : WickContraction φs.length) (hlt : ∀ (k : Fin φs.length), timeOrderRel φ φs[k])
|
||||||
|
(hn : ∀ (k : Fin φs.length), i.succAbove k < i → ¬timeOrderRel φs[k] φ) :
|
||||||
|
ofFieldOp φ * φsΛ.wickTerm =
|
||||||
|
𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ ⟨φs.get, (Finset.univ.filter (fun x => i.succAbove x < i))⟩) •
|
||||||
|
∑ (k : Option φsΛ.uncontracted), (φsΛ ↩Λ φ i k).wickTerm := by
|
||||||
|
trans (φsΛ.sign • φsΛ.timeContract) * ((ofFieldOp φ) * 𝓝(ofFieldOpList [φsΛ]ᵘᶜ))
|
||||||
|
· have ht := Subalgebra.mem_center_iff.mp (Subalgebra.smul_mem (Subalgebra.center ℂ _)
|
||||||
|
(WickContraction.timeContract φsΛ).2 (φsΛ.sign))
|
||||||
|
rw [wickTerm]
|
||||||
|
rw [← mul_assoc, ht, mul_assoc]
|
||||||
|
rw [ofFieldOp_mul_normalOrder_ofFieldOpList_eq_sum, Finset.mul_sum,
|
||||||
|
uncontractedFieldOpEquiv_list_sum, Finset.smul_sum]
|
||||||
|
simp only [instCommGroup.eq_1, Nat.succ_eq_add_one]
|
||||||
|
congr 1
|
||||||
|
funext n
|
||||||
|
match n with
|
||||||
|
| none =>
|
||||||
|
rw [wickTerm_none_eq_wick_term_cons]
|
||||||
|
simp only [contractStateAtIndex, uncontractedFieldOpEquiv, Equiv.optionCongr_apply,
|
||||||
|
Equiv.coe_trans, Option.map_none', one_mul, Algebra.smul_mul_assoc, instCommGroup.eq_1,
|
||||||
|
smul_smul]
|
||||||
|
congr 1
|
||||||
|
rw [← mul_assoc, exchangeSign_mul_self]
|
||||||
|
simp
|
||||||
|
| some n =>
|
||||||
|
rw [wickTerm_some_eq_wick_term_optionEraseZ _ _ _ _ _
|
||||||
|
(fun k => hlt k) (fun k a => hn k a)]
|
||||||
|
simp only [uncontractedFieldOpEquiv, Equiv.optionCongr_apply, Equiv.coe_trans, Option.map_some',
|
||||||
|
Function.comp_apply, finCongr_apply, Algebra.smul_mul_assoc, instCommGroup.eq_1, smul_smul]
|
||||||
|
congr 1
|
||||||
|
· rw [← mul_assoc, exchangeSign_mul_self]
|
||||||
|
rw [one_mul]
|
||||||
|
· rw [← mul_assoc]
|
||||||
|
congr 1
|
||||||
|
have ht := (WickContraction.timeContract φsΛ).prop
|
||||||
|
rw [@Subalgebra.mem_center_iff] at ht
|
||||||
|
rw [ht]
|
||||||
|
|
||||||
|
end
|
||||||
|
end WickContraction
|
||||||
|
|
@ -6,6 +6,8 @@ Authors: Joseph Tooby-Smith
|
||||||
import HepLean.PerturbationTheory.WickContraction.TimeContract
|
import HepLean.PerturbationTheory.WickContraction.TimeContract
|
||||||
import HepLean.PerturbationTheory.WickContraction.Sign.InsertNone
|
import HepLean.PerturbationTheory.WickContraction.Sign.InsertNone
|
||||||
import HepLean.PerturbationTheory.WickContraction.Sign.InsertSome
|
import HepLean.PerturbationTheory.WickContraction.Sign.InsertSome
|
||||||
|
import HepLean.PerturbationTheory.FieldOpAlgebra.NormalOrder.WickContractions
|
||||||
|
import HepLean.PerturbationTheory.FieldOpAlgebra.WickTerm
|
||||||
import HepLean.Meta.Remark.Basic
|
import HepLean.Meta.Remark.Basic
|
||||||
/-!
|
/-!
|
||||||
|
|
||||||
|
|
@ -28,289 +30,10 @@ open FieldStatistic
|
||||||
|
|
||||||
/-!
|
/-!
|
||||||
|
|
||||||
## Normal order of uncontracted terms within proto-algebra.
|
|
||||||
|
|
||||||
-/
|
|
||||||
|
|
||||||
/--
|
|
||||||
Let `c` be a Wick Contraction for `φs := φ₀φ₁…φₙ`.
|
|
||||||
We have (roughly) `𝓝ᶠ([φsΛ ↩Λ φ i none]ᵘᶜ) = s • 𝓝ᶠ(φ :: [φsΛ]ᵘᶜ)`
|
|
||||||
Where `s` is the exchange sign for `φ` and the uncontracted fields in `φ₀φ₁…φᵢ₋₁`.
|
|
||||||
-/
|
|
||||||
lemma normalOrder_uncontracted_none (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
|
|
||||||
(i : Fin φs.length.succ) (φsΛ : WickContraction φs.length) :
|
|
||||||
𝓝(ofFieldOpList [φsΛ ↩Λ φ i none]ᵘᶜ)
|
|
||||||
= 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ ⟨φs.get, φsΛ.uncontracted.filter (fun x => i.succAbove x < i)⟩) •
|
|
||||||
𝓝(ofFieldOpList (φ :: [φsΛ]ᵘᶜ)) := by
|
|
||||||
simp only [Nat.succ_eq_add_one, instCommGroup.eq_1]
|
|
||||||
rw [ofFieldOpList_normalOrder_insert φ [φsΛ]ᵘᶜ
|
|
||||||
⟨(φsΛ.uncontractedListOrderPos i), by simp [uncontractedListGet]⟩, smul_smul]
|
|
||||||
trans (1 : ℂ) • (𝓝(ofFieldOpList [φsΛ ↩Λ φ i none]ᵘᶜ))
|
|
||||||
· simp
|
|
||||||
congr 1
|
|
||||||
simp only [instCommGroup.eq_1, uncontractedListGet]
|
|
||||||
rw [← List.map_take, take_uncontractedListOrderPos_eq_filter]
|
|
||||||
have h1 : (𝓕 |>ₛ List.map φs.get (List.filter (fun x => decide (↑x < i.1)) φsΛ.uncontractedList))
|
|
||||||
= 𝓕 |>ₛ ⟨φs.get, (φsΛ.uncontracted.filter (fun x => x.val < i.1))⟩ := by
|
|
||||||
simp only [Nat.succ_eq_add_one, ofFinset]
|
|
||||||
congr
|
|
||||||
rw [uncontractedList_eq_sort]
|
|
||||||
have hdup : (List.filter (fun x => decide (x.1 < i.1))
|
|
||||||
(Finset.sort (fun x1 x2 => x1 ≤ x2) φsΛ.uncontracted)).Nodup := by
|
|
||||||
exact List.Nodup.filter _ (Finset.sort_nodup (fun x1 x2 => x1 ≤ x2) φsΛ.uncontracted)
|
|
||||||
have hsort : (List.filter (fun x => decide (x.1 < i.1))
|
|
||||||
(Finset.sort (fun x1 x2 => x1 ≤ x2) φsΛ.uncontracted)).Sorted (· ≤ ·) := by
|
|
||||||
exact List.Sorted.filter _ (Finset.sort_sorted (fun x1 x2 => x1 ≤ x2) φsΛ.uncontracted)
|
|
||||||
rw [← (List.toFinset_sort (· ≤ ·) hdup).mpr hsort]
|
|
||||||
congr
|
|
||||||
ext a
|
|
||||||
simp
|
|
||||||
rw [h1]
|
|
||||||
simp only [Nat.succ_eq_add_one]
|
|
||||||
have h2 : (Finset.filter (fun x => x.1 < i.1) φsΛ.uncontracted) =
|
|
||||||
(Finset.filter (fun x => i.succAbove x < i) φsΛ.uncontracted) := by
|
|
||||||
ext a
|
|
||||||
simp only [Nat.succ_eq_add_one, Finset.mem_filter, and_congr_right_iff]
|
|
||||||
intro ha
|
|
||||||
simp only [Fin.succAbove]
|
|
||||||
split
|
|
||||||
· apply Iff.intro
|
|
||||||
· intro h
|
|
||||||
omega
|
|
||||||
· intro h
|
|
||||||
rename_i h
|
|
||||||
rw [Fin.lt_def] at h
|
|
||||||
simp only [Fin.coe_castSucc] at h
|
|
||||||
omega
|
|
||||||
· apply Iff.intro
|
|
||||||
· intro h
|
|
||||||
rename_i h'
|
|
||||||
rw [Fin.lt_def]
|
|
||||||
simp only [Fin.val_succ]
|
|
||||||
rw [Fin.lt_def] at h'
|
|
||||||
simp only [Fin.coe_castSucc, not_lt] at h'
|
|
||||||
omega
|
|
||||||
· intro h
|
|
||||||
rename_i h
|
|
||||||
rw [Fin.lt_def] at h
|
|
||||||
simp only [Fin.val_succ] at h
|
|
||||||
omega
|
|
||||||
rw [h2]
|
|
||||||
simp only [exchangeSign_mul_self]
|
|
||||||
congr
|
|
||||||
simp only [Nat.succ_eq_add_one]
|
|
||||||
rw [insertAndContract_uncontractedList_none_map]
|
|
||||||
|
|
||||||
/--
|
|
||||||
Let `c` be a Wick Contraction for `φ₀φ₁…φₙ`.
|
|
||||||
We have (roughly) `N(c ↩Λ φ i k).uncontractedList`
|
|
||||||
is equal to `N((c.uncontractedList).eraseIdx k')`
|
|
||||||
where `k'` is the position in `c.uncontractedList` corresponding to `k`.
|
|
||||||
-/
|
|
||||||
lemma normalOrder_uncontracted_some (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
|
|
||||||
(i : Fin φs.length.succ) (φsΛ : WickContraction φs.length) (k : φsΛ.uncontracted) :
|
|
||||||
𝓝(ofFieldOpList [φsΛ ↩Λ φ i (some k)]ᵘᶜ)
|
|
||||||
= 𝓝(ofFieldOpList (optionEraseZ [φsΛ]ᵘᶜ φ ((uncontractedFieldOpEquiv φs φsΛ) k))) := by
|
|
||||||
simp only [Nat.succ_eq_add_one, insertAndContract, optionEraseZ, uncontractedFieldOpEquiv,
|
|
||||||
Equiv.optionCongr_apply, Equiv.coe_trans, Option.map_some', Function.comp_apply, finCongr_apply,
|
|
||||||
Fin.coe_cast, uncontractedListGet]
|
|
||||||
congr
|
|
||||||
rw [congr_uncontractedList]
|
|
||||||
erw [uncontractedList_extractEquiv_symm_some]
|
|
||||||
simp only [Fin.coe_succAboveEmb, List.map_eraseIdx, List.map_map]
|
|
||||||
congr
|
|
||||||
conv_rhs => rw [get_eq_insertIdx_succAbove φ φs i]
|
|
||||||
|
|
||||||
/-!
|
|
||||||
|
|
||||||
## Wick terms
|
## Wick terms
|
||||||
|
|
||||||
-/
|
-/
|
||||||
|
|
||||||
remark wick_term_terminology := "
|
|
||||||
Let `φsΛ` be a Wick contraction. We informally call the term
|
|
||||||
`(φsΛ.sign • φsΛ.timeContract 𝓞) * 𝓞.crAnF 𝓝ᶠ([φsΛ]ᵘᶜ)` the Wick term
|
|
||||||
associated with `φsΛ`. We do not make this a fully-fledge definition, as
|
|
||||||
in most cases we want to consider slight modifications of this term."
|
|
||||||
|
|
||||||
/--
|
|
||||||
Let `φsΛ` be a Wick Contraction for `φs = φ₀φ₁…φₙ`. Then the wick-term of ` (φsΛ ↩Λ φ i none)`
|
|
||||||
|
|
||||||
```(φsΛ ↩Λ φ i none).sign • (φsΛ ↩Λ φ i none).timeContract 𝓞 * 𝓞.crAnF 𝓝ᶠ([φsΛ ↩Λ φ i none]ᵘᶜ)```
|
|
||||||
|
|
||||||
is equal to
|
|
||||||
|
|
||||||
`s • (φsΛ.sign • φsΛ.timeContract 𝓞 * 𝓞.crAnF 𝓝ᶠ(φ :: [φsΛ]ᵘᶜ))`
|
|
||||||
|
|
||||||
where `s` is the exchange sign of `φ` and the uncontracted fields in `φ₀φ₁…φᵢ₋₁`.
|
|
||||||
|
|
||||||
The proof of this result relies primarily on:
|
|
||||||
- `normalOrderF_uncontracted_none` which replaces `𝓝ᶠ([φsΛ ↩Λ φ i none]ᵘᶜ)` with
|
|
||||||
`𝓝ᶠ(φ :: [φsΛ]ᵘᶜ)` up to a sign.
|
|
||||||
- `timeContract_insertAndContract_none` which replaces `(φsΛ ↩Λ φ i none).timeContract 𝓞` with
|
|
||||||
`φsΛ.timeContract 𝓞`.
|
|
||||||
- `sign_insert_none` and `signInsertNone_eq_filterset` which are used to take account of
|
|
||||||
signs.
|
|
||||||
-/
|
|
||||||
lemma wick_term_none_eq_wick_term_cons (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
|
|
||||||
(i : Fin φs.length.succ) (φsΛ : WickContraction φs.length) :
|
|
||||||
(φsΛ ↩Λ φ i none).sign • (φsΛ ↩Λ φ i none).timeContract
|
|
||||||
* 𝓝(ofFieldOpList [φsΛ ↩Λ φ i none]ᵘᶜ) =
|
|
||||||
𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ ⟨φs.get, (Finset.univ.filter (fun k => i.succAbove k < i))⟩)
|
|
||||||
• (φsΛ.sign • φsΛ.timeContract * 𝓝(ofFieldOpList (φ :: [φsΛ]ᵘᶜ))) := by
|
|
||||||
by_cases hg : GradingCompliant φs φsΛ
|
|
||||||
· rw [normalOrder_uncontracted_none, sign_insert_none]
|
|
||||||
simp only [Nat.succ_eq_add_one, timeContract_insertAndContract_none, instCommGroup.eq_1,
|
|
||||||
Algebra.mul_smul_comm, Algebra.smul_mul_assoc, smul_smul]
|
|
||||||
congr 1
|
|
||||||
rw [← mul_assoc]
|
|
||||||
congr 1
|
|
||||||
rw [signInsertNone_eq_filterset _ _ _ _ hg, ← map_mul]
|
|
||||||
congr
|
|
||||||
rw [ofFinset_union]
|
|
||||||
congr
|
|
||||||
ext a
|
|
||||||
simp only [Finset.mem_sdiff, Finset.mem_union, Finset.mem_filter, Finset.mem_univ, true_and,
|
|
||||||
Finset.mem_inter, not_and, not_lt, and_imp]
|
|
||||||
apply Iff.intro
|
|
||||||
· intro ha
|
|
||||||
have ha1 := ha.1
|
|
||||||
rcases ha1 with ha1 | ha1
|
|
||||||
· exact ha1.2
|
|
||||||
· exact ha1.2
|
|
||||||
· intro ha
|
|
||||||
simp only [uncontracted, Finset.mem_filter, Finset.mem_univ, true_and, ha, and_true,
|
|
||||||
forall_const]
|
|
||||||
have hx : φsΛ.getDual? a = none ↔ ¬ (φsΛ.getDual? a).isSome := by
|
|
||||||
simp
|
|
||||||
rw [hx]
|
|
||||||
simp only [Bool.not_eq_true, Bool.eq_false_or_eq_true_self, true_and]
|
|
||||||
intro h1 h2
|
|
||||||
simp_all
|
|
||||||
· simp only [Nat.succ_eq_add_one, timeContract_insertAndContract_none, Algebra.smul_mul_assoc,
|
|
||||||
instCommGroup.eq_1]
|
|
||||||
rw [timeContract_of_not_gradingCompliant]
|
|
||||||
simp only [ZeroMemClass.coe_zero, zero_mul, smul_zero]
|
|
||||||
exact hg
|
|
||||||
|
|
||||||
/--
|
|
||||||
Let `c` be a Wick Contraction for `φ₀φ₁…φₙ`.
|
|
||||||
This lemma states that
|
|
||||||
`(c.sign • c.timeContract 𝓞) * N(c.uncontracted)`
|
|
||||||
for `c` equal to `c ↩Λ φ i (some k)` is equal to that for just `c`
|
|
||||||
mulitiplied by the exchange sign of `φ` and `φ₀φ₁…φᵢ₋₁`.
|
|
||||||
-/
|
|
||||||
lemma wick_term_some_eq_wick_term_optionEraseZ (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
|
|
||||||
(i : Fin φs.length.succ) (φsΛ : WickContraction φs.length) (k : φsΛ.uncontracted)
|
|
||||||
(hlt : ∀ (k : Fin φs.length), timeOrderRel φ φs[k])
|
|
||||||
(hn : ∀ (k : Fin φs.length), i.succAbove k < i → ¬ timeOrderRel φs[k] φ) :
|
|
||||||
(φsΛ ↩Λ φ i (some k)).sign • (φsΛ ↩Λ φ i (some k)).timeContract
|
|
||||||
* 𝓝(ofFieldOpList [φsΛ ↩Λ φ i (some k)]ᵘᶜ) =
|
|
||||||
𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ ⟨φs.get, (Finset.univ.filter (fun x => i.succAbove x < i))⟩)
|
|
||||||
• (φsΛ.sign • (contractStateAtIndex φ [φsΛ]ᵘᶜ
|
|
||||||
((uncontractedFieldOpEquiv φs φsΛ) (some k)) * φsΛ.timeContract)
|
|
||||||
* 𝓝(ofFieldOpList (optionEraseZ [φsΛ]ᵘᶜ φ (uncontractedFieldOpEquiv φs φsΛ k)))) := by
|
|
||||||
by_cases hg : GradingCompliant φs φsΛ ∧ (𝓕 |>ₛ φ) = (𝓕 |>ₛ φs[k.1])
|
|
||||||
· by_cases hk : i.succAbove k < i
|
|
||||||
· rw [WickContraction.timeConract_insertAndContract_some_eq_mul_contractStateAtIndex_not_lt]
|
|
||||||
swap
|
|
||||||
· exact hn _ hk
|
|
||||||
rw [normalOrder_uncontracted_some, sign_insert_some]
|
|
||||||
simp only [instCommGroup.eq_1, smul_smul, Algebra.smul_mul_assoc]
|
|
||||||
congr 1
|
|
||||||
rw [mul_assoc, mul_comm (sign φs φsΛ), ← mul_assoc]
|
|
||||||
congr 1
|
|
||||||
exact signInsertSome_mul_filter_contracted_of_lt φ φs φsΛ i k hk hg
|
|
||||||
· omega
|
|
||||||
· have hik : i.succAbove ↑k ≠ i := Fin.succAbove_ne i ↑k
|
|
||||||
rw [WickContraction.timeConract_insertAndContract_some_eq_mul_contractStateAtIndex_lt]
|
|
||||||
swap
|
|
||||||
· exact hlt _
|
|
||||||
rw [normalOrder_uncontracted_some]
|
|
||||||
rw [sign_insert_some]
|
|
||||||
simp only [instCommGroup.eq_1, smul_smul, Algebra.smul_mul_assoc]
|
|
||||||
congr 1
|
|
||||||
rw [mul_assoc, mul_comm (sign φs φsΛ), ← mul_assoc]
|
|
||||||
congr 1
|
|
||||||
exact signInsertSome_mul_filter_contracted_of_not_lt φ φs φsΛ i k hk hg
|
|
||||||
· omega
|
|
||||||
· rw [timeConract_insertAndContract_some]
|
|
||||||
simp only [Fin.getElem_fin, not_and] at hg
|
|
||||||
by_cases hg' : GradingCompliant φs φsΛ
|
|
||||||
· have hg := hg hg'
|
|
||||||
simp only [Nat.succ_eq_add_one, Fin.getElem_fin, ite_mul, Algebra.smul_mul_assoc,
|
|
||||||
instCommGroup.eq_1, contractStateAtIndex, uncontractedFieldOpEquiv, Equiv.optionCongr_apply,
|
|
||||||
Equiv.coe_trans, Option.map_some', Function.comp_apply, finCongr_apply, Fin.coe_cast,
|
|
||||||
List.getElem_map, uncontractedList_getElem_uncontractedIndexEquiv_symm, List.get_eq_getElem,
|
|
||||||
uncontractedListGet]
|
|
||||||
by_cases h1 : i < i.succAbove ↑k
|
|
||||||
· simp only [h1, ↓reduceIte, MulMemClass.coe_mul]
|
|
||||||
rw [timeContract_zero_of_diff_grade]
|
|
||||||
simp only [zero_mul, smul_zero]
|
|
||||||
rw [superCommute_anPart_ofFieldOpF_diff_grade_zero]
|
|
||||||
simp only [zero_mul, smul_zero]
|
|
||||||
exact hg
|
|
||||||
exact hg
|
|
||||||
· simp only [h1, ↓reduceIte, MulMemClass.coe_mul]
|
|
||||||
rw [timeContract_zero_of_diff_grade]
|
|
||||||
simp only [zero_mul, smul_zero]
|
|
||||||
rw [superCommute_anPart_ofFieldOpF_diff_grade_zero]
|
|
||||||
simp only [zero_mul, smul_zero]
|
|
||||||
exact hg
|
|
||||||
exact fun a => hg (id (Eq.symm a))
|
|
||||||
· rw [timeContract_of_not_gradingCompliant]
|
|
||||||
simp only [Nat.succ_eq_add_one, Fin.getElem_fin, mul_zero, ZeroMemClass.coe_zero, smul_zero,
|
|
||||||
zero_mul, instCommGroup.eq_1]
|
|
||||||
exact hg'
|
|
||||||
|
|
||||||
/--
|
|
||||||
Given a Wick contraction `φsΛ` of `φs = φ₀φ₁…φₙ` and an `i`, we have that
|
|
||||||
`(φsΛ.sign • φsΛ.timeContract 𝓞) * 𝓞.crAnF (φ * 𝓝ᶠ([φsΛ]ᵘᶜ))`
|
|
||||||
is equal to the product of
|
|
||||||
- the exchange sign of `φ` and `φ₀φ₁…φᵢ₋₁`,
|
|
||||||
- the sum of `((φsΛ ↩Λ φ i k).sign • (φsΛ ↩Λ φ i k).timeContract 𝓞) * 𝓞.crAnF 𝓝ᶠ([φsΛ ↩Λ φ i k]ᵘᶜ)`
|
|
||||||
over all `k` in `Option φsΛ.uncontracted`.
|
|
||||||
|
|
||||||
The proof of this result primarily depends on
|
|
||||||
- `crAnF_ofFieldOpF_mul_normalOrderF_ofFieldOpFsList_eq_sum` to rewrite `𝓞.crAnF (φ * 𝓝ᶠ([φsΛ]ᵘᶜ))`
|
|
||||||
- `wick_term_none_eq_wick_term_cons`
|
|
||||||
- `wick_term_some_eq_wick_term_optionEraseZ`
|
|
||||||
-/
|
|
||||||
lemma wick_term_cons_eq_sum_wick_term (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) (i : Fin φs.length.succ)
|
|
||||||
(φsΛ : WickContraction φs.length) (hlt : ∀ (k : Fin φs.length), timeOrderRel φ φs[k])
|
|
||||||
(hn : ∀ (k : Fin φs.length), i.succAbove k < i → ¬timeOrderRel φs[k] φ) :
|
|
||||||
(φsΛ.sign • φsΛ.timeContract) * ((ofFieldOp φ) * 𝓝(ofFieldOpList [φsΛ]ᵘᶜ)) =
|
|
||||||
𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ ⟨φs.get, (Finset.univ.filter (fun x => i.succAbove x < i))⟩) •
|
|
||||||
∑ (k : Option φsΛ.uncontracted), ((φsΛ ↩Λ φ i k).sign •
|
|
||||||
(φsΛ ↩Λ φ i k).timeContract * (𝓝(ofFieldOpList [φsΛ ↩Λ φ i k]ᵘᶜ))) := by
|
|
||||||
rw [ofFieldOp_mul_normalOrder_ofFieldOpList_eq_sum, Finset.mul_sum,
|
|
||||||
uncontractedFieldOpEquiv_list_sum, Finset.smul_sum]
|
|
||||||
simp only [instCommGroup.eq_1, Nat.succ_eq_add_one]
|
|
||||||
congr 1
|
|
||||||
funext n
|
|
||||||
match n with
|
|
||||||
| none =>
|
|
||||||
rw [wick_term_none_eq_wick_term_cons]
|
|
||||||
simp only [contractStateAtIndex, uncontractedFieldOpEquiv, Equiv.optionCongr_apply,
|
|
||||||
Equiv.coe_trans, Option.map_none', one_mul, Algebra.smul_mul_assoc, instCommGroup.eq_1,
|
|
||||||
smul_smul]
|
|
||||||
congr 1
|
|
||||||
rw [← mul_assoc, exchangeSign_mul_self]
|
|
||||||
simp
|
|
||||||
| some n =>
|
|
||||||
rw [wick_term_some_eq_wick_term_optionEraseZ _ _ _ _ _
|
|
||||||
(fun k => hlt k) (fun k a => hn k a)]
|
|
||||||
simp only [uncontractedFieldOpEquiv, Equiv.optionCongr_apply, Equiv.coe_trans, Option.map_some',
|
|
||||||
Function.comp_apply, finCongr_apply, Algebra.smul_mul_assoc, instCommGroup.eq_1, smul_smul]
|
|
||||||
congr 1
|
|
||||||
· rw [← mul_assoc, exchangeSign_mul_self]
|
|
||||||
rw [one_mul]
|
|
||||||
· rw [← mul_assoc]
|
|
||||||
congr 1
|
|
||||||
have ht := (WickContraction.timeContract φsΛ).prop
|
|
||||||
rw [@Subalgebra.mem_center_iff] at ht
|
|
||||||
rw [ht]
|
|
||||||
|
|
||||||
/-!
|
/-!
|
||||||
|
|
||||||
## Wick's theorem
|
## Wick's theorem
|
||||||
|
|
@ -335,9 +58,8 @@ lemma wicks_theorem_nil :
|
||||||
rfl
|
rfl
|
||||||
|
|
||||||
lemma wicks_theorem_congr {φs φs' : List 𝓕.FieldOp} (h : φs = φs') :
|
lemma wicks_theorem_congr {φs φs' : List 𝓕.FieldOp} (h : φs = φs') :
|
||||||
∑ (φsΛ : WickContraction φs.length), (φsΛ.sign • φsΛ.timeContract) * 𝓝(ofFieldOpList [φsΛ]ᵘᶜ)
|
∑ (φsΛ : WickContraction φs.length), φsΛ.wickTerm
|
||||||
= ∑ (φs'Λ : WickContraction φs'.length), (φs'Λ.sign • φs'Λ.timeContract) *
|
= ∑ (φs'Λ : WickContraction φs'.length), φs'Λ.wickTerm := by
|
||||||
𝓝(ofFieldOpList [φs'Λ]ᵘᶜ) := by
|
|
||||||
subst h
|
subst h
|
||||||
simp
|
simp
|
||||||
|
|
||||||
|
|
@ -356,17 +78,21 @@ remark wicks_theorem_context := "
|
||||||
The statement of these theorems for bosons is simplier then when fermions are involved, since
|
The statement of these theorems for bosons is simplier then when fermions are involved, since
|
||||||
one does not have to worry about the minus-signs picked up on exchanging fields."
|
one does not have to worry about the minus-signs picked up on exchanging fields."
|
||||||
|
|
||||||
/-- Wick's theorem for time-ordered products of bosonic and fermionic fields.
|
/-- Wick's theorem states that for a list of fields `φs = φ₀…φₙ`
|
||||||
The time ordered product `T(φ₀φ₁…φₙ)` is equal to the sum of terms,
|
`𝓣(φs) = ∑ φsΛ, (φsΛ.sign • φsΛ.timeContract) * 𝓝([φsΛ]ᵘᶜ)`
|
||||||
for all possible Wick contractions `c` of the list of fields `φs := φ₀φ₁…φₙ`, given by
|
where the sum is over all Wick contractions `φsΛ` of `φs`.
|
||||||
the multiple of:
|
|
||||||
- The sign corresponding to the number of fermionic-fermionic exchanges one must do
|
The proof is via induction on `φs`. The base case `φs = []` is handled by `wicks_theorem_nil`.
|
||||||
to put elements in contracted pairs of `c` next to each other.
|
The inductive step works as follows:
|
||||||
- The product of time-contractions of the contracted pairs of `c`.
|
- The lemma `timeOrder_eq_maxTimeField_mul_finset` is used to write
|
||||||
- The normal-ordering of the uncontracted fields in `c`.
|
`𝓣(φ₀…φₙ)` as ` 𝓢(φᵢ,φ₀…φᵢ₋₁) • φᵢ * 𝓣(φ₀…φᵢ₋₁φᵢ₊₁φₙ)` where `φᵢ` is
|
||||||
|
the maximal time field in `φ₀…φₙ`.
|
||||||
|
- The induction hypothesis is used to expand `𝓣(φ₀…φᵢ₋₁φᵢ₊₁φₙ)` as a sum over Wick contractions of
|
||||||
|
`φ₀…φᵢ₋₁φᵢ₊₁φₙ`.
|
||||||
|
- Further the lemmas `wick_term_cons_eq_sum_wick_term` and `insertLift_sum` are used.
|
||||||
-/
|
-/
|
||||||
theorem wicks_theorem : (φs : List 𝓕.FieldOp) → 𝓣(ofFieldOpList φs) =
|
theorem wicks_theorem : (φs : List 𝓕.FieldOp) → 𝓣(ofFieldOpList φs) =
|
||||||
∑ (φsΛ : WickContraction φs.length), (φsΛ.sign • φsΛ.timeContract) * 𝓝(ofFieldOpList [φsΛ]ᵘᶜ)
|
∑ (φsΛ : WickContraction φs.length), φsΛ.wickTerm
|
||||||
| [] => wicks_theorem_nil
|
| [] => wicks_theorem_nil
|
||||||
| φ :: φs => by
|
| φ :: φs => by
|
||||||
have ih := wicks_theorem (eraseMaxTimeField φ φs)
|
have ih := wicks_theorem (eraseMaxTimeField φ φs)
|
||||||
|
|
@ -380,18 +106,10 @@ theorem wicks_theorem : (φs : List 𝓕.FieldOp) → 𝓣(ofFieldOpList φs) =
|
||||||
conv_rhs => rw [insertLift_sum]
|
conv_rhs => rw [insertLift_sum]
|
||||||
apply Finset.sum_congr rfl
|
apply Finset.sum_congr rfl
|
||||||
intro c _
|
intro c _
|
||||||
have ht := Subalgebra.mem_center_iff.mp (Subalgebra.smul_mem (Subalgebra.center ℂ _)
|
rw [Algebra.smul_mul_assoc, wickTerm_cons_eq_sum_wick_term
|
||||||
(WickContraction.timeContract c).2 (sign (eraseMaxTimeField φ φs) c))
|
|
||||||
rw [Algebra.smul_mul_assoc, ← mul_assoc, ht, mul_assoc]
|
|
||||||
rw [wick_term_cons_eq_sum_wick_term
|
|
||||||
(maxTimeField φ φs) (eraseMaxTimeField φ φs) (maxTimeFieldPosFin φ φs) c]
|
(maxTimeField φ φs) (eraseMaxTimeField φ φs) (maxTimeFieldPosFin φ φs) c]
|
||||||
trans (1 : ℂ) • ∑ k : Option { x // x ∈ c.uncontracted }, sign
|
trans (1 : ℂ) • ∑ k : Option { x // x ∈ c.uncontracted },
|
||||||
(List.insertIdx (↑(maxTimeFieldPosFin φ φs)) (maxTimeField φ φs) (eraseMaxTimeField φ φs))
|
(c ↩Λ (maxTimeField φ φs) (maxTimeFieldPosFin φ φs) k).wickTerm
|
||||||
(c ↩Λ (maxTimeField φ φs) (maxTimeFieldPosFin φ φs) k) •
|
|
||||||
↑((c ↩Λ (maxTimeField φ φs) (maxTimeFieldPosFin φ φs) k).timeContract) *
|
|
||||||
𝓝(ofFieldOpList (List.map (List.insertIdx (↑(maxTimeFieldPosFin φ φs))
|
|
||||||
(maxTimeField φ φs) (eraseMaxTimeField φ φs)).get
|
|
||||||
(c ↩Λ (maxTimeField φ φs) (maxTimeFieldPosFin φ φs) k).uncontractedList))
|
|
||||||
swap
|
swap
|
||||||
· simp [uncontractedListGet]
|
· simp [uncontractedListGet]
|
||||||
rw [smul_smul]
|
rw [smul_smul]
|
||||||
|
|
|
||||||
|
|
@ -3,10 +3,10 @@ Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
|
||||||
Released under Apache 2.0 license as described in the file LICENSE.
|
Released under Apache 2.0 license as described in the file LICENSE.
|
||||||
Authors: Joseph Tooby-Smith
|
Authors: Joseph Tooby-Smith
|
||||||
-/
|
-/
|
||||||
import HepLean.PerturbationTheory.WickContraction.TimeCond
|
|
||||||
import HepLean.PerturbationTheory.WickContraction.Sign.Join
|
|
||||||
import HepLean.PerturbationTheory.FieldOpAlgebra.StaticWickTheorem
|
import HepLean.PerturbationTheory.FieldOpAlgebra.StaticWickTheorem
|
||||||
import HepLean.Meta.Remark.Basic
|
import HepLean.PerturbationTheory.FieldOpAlgebra.WicksTheorem
|
||||||
|
import HepLean.PerturbationTheory.WickContraction.Sign.Join
|
||||||
|
import HepLean.PerturbationTheory.WickContraction.TimeCond
|
||||||
/-!
|
/-!
|
||||||
|
|
||||||
# Wick's theorem for normal ordered lists
|
# Wick's theorem for normal ordered lists
|
||||||
|
|
@ -21,7 +21,7 @@ open WickContraction
|
||||||
open EqTimeOnly
|
open EqTimeOnly
|
||||||
|
|
||||||
lemma timeOrder_ofFieldOpList_eqTimeOnly (φs : List 𝓕.FieldOp) :
|
lemma timeOrder_ofFieldOpList_eqTimeOnly (φs : List 𝓕.FieldOp) :
|
||||||
timeOrder (ofFieldOpList φs) = ∑ (φsΛ : {φsΛ // φsΛ.EqTimeOnly (φs := φs)}),
|
𝓣(ofFieldOpList φs) = ∑ (φsΛ : {φsΛ // φsΛ.EqTimeOnly (φs := φs)}),
|
||||||
φsΛ.1.sign • φsΛ.1.timeContract.1 * 𝓣(𝓝(ofFieldOpList [φsΛ.1]ᵘᶜ)) := by
|
φsΛ.1.sign • φsΛ.1.timeContract.1 * 𝓣(𝓝(ofFieldOpList [φsΛ.1]ᵘᶜ)) := by
|
||||||
rw [static_wick_theorem φs]
|
rw [static_wick_theorem φs]
|
||||||
let e2 : WickContraction φs.length ≃
|
let e2 : WickContraction φs.length ≃
|
||||||
|
|
@ -86,6 +86,7 @@ lemma normalOrder_timeOrder_ofFieldOpList_eq_haveEqTime_sum_not_haveEqTime (φs
|
||||||
φsΛ.1.sign • φsΛ.1.timeContract.1 * 𝓣(𝓝(ofFieldOpList [φsΛ.1]ᵘᶜ)) := by
|
φsΛ.1.sign • φsΛ.1.timeContract.1 * 𝓣(𝓝(ofFieldOpList [φsΛ.1]ᵘᶜ)) := by
|
||||||
rw [normalOrder_timeOrder_ofFieldOpList_eq_eqTimeOnly_empty]
|
rw [normalOrder_timeOrder_ofFieldOpList_eq_eqTimeOnly_empty]
|
||||||
rw [wicks_theorem]
|
rw [wicks_theorem]
|
||||||
|
simp only [wickTerm]
|
||||||
let e1 : WickContraction φs.length ≃ {φsΛ // HaveEqTime φsΛ} ⊕ {φsΛ // ¬ HaveEqTime φsΛ} := by
|
let e1 : WickContraction φs.length ≃ {φsΛ // HaveEqTime φsΛ} ⊕ {φsΛ // ¬ HaveEqTime φsΛ} := by
|
||||||
exact (Equiv.sumCompl HaveEqTime).symm
|
exact (Equiv.sumCompl HaveEqTime).symm
|
||||||
rw [← e1.symm.sum_comp]
|
rw [← e1.symm.sum_comp]
|
||||||
|
|
@ -143,7 +144,8 @@ lemma normalOrder_timeOrder_ofFieldOpList_eq_not_haveEqTime_sub_inductive (φs :
|
||||||
|
|
||||||
lemma wicks_theorem_normal_order_empty : 𝓣(𝓝(ofFieldOpList [])) =
|
lemma wicks_theorem_normal_order_empty : 𝓣(𝓝(ofFieldOpList [])) =
|
||||||
∑ (φsΛ : {φsΛ : WickContraction ([] : List 𝓕.FieldOp).length // ¬ HaveEqTime φsΛ}),
|
∑ (φsΛ : {φsΛ : WickContraction ([] : List 𝓕.FieldOp).length // ¬ HaveEqTime φsΛ}),
|
||||||
φsΛ.1.sign • φsΛ.1.timeContract.1 * 𝓝(ofFieldOpList [φsΛ.1]ᵘᶜ) := by
|
φsΛ.1.wickTerm := by
|
||||||
|
simp only [wickTerm]
|
||||||
let e2 : {φsΛ : WickContraction ([] : List 𝓕.FieldOp).length // ¬ HaveEqTime φsΛ} ≃ Unit :=
|
let e2 : {φsΛ : WickContraction ([] : List 𝓕.FieldOp).length // ¬ HaveEqTime φsΛ} ≃ Unit :=
|
||||||
{
|
{
|
||||||
toFun := fun x => (),
|
toFun := fun x => (),
|
||||||
|
|
@ -176,16 +178,17 @@ lemma wicks_theorem_normal_order_empty : 𝓣(𝓝(ofFieldOpList [])) =
|
||||||
|
|
||||||
/--
|
/--
|
||||||
Wicks theorem for normal ordering followed by time-ordering, states that
|
Wicks theorem for normal ordering followed by time-ordering, states that
|
||||||
`𝓣(𝓝(φ₀…φₙ))` is equal to the sum over
|
`𝓣(𝓝(φ₀…φₙ))` is equal to
|
||||||
`φsΛ.1.sign • φsΛ.1.timeContract.1 * 𝓝(ofFieldOpList [φsΛ.1]ᵘᶜ)`
|
`∑ φsΛ, φsΛ.1.sign • φsΛ.1.timeContract.1 * 𝓝(ofFieldOpList [φsΛ.1]ᵘᶜ)`
|
||||||
for those Wick contraction `φsΛ` which do not have any equal time contractions.
|
over those Wick contraction `φsΛ` which do not have any equal time contractions.
|
||||||
This is compared to the ordinary Wicks theorem which sums over all Wick contractions.
|
This is compared to the ordinary Wicks theorem which sums over all Wick contractions.
|
||||||
-/
|
-/
|
||||||
theorem wicks_theorem_normal_order : (φs : List 𝓕.FieldOp) →
|
theorem wicks_theorem_normal_order : (φs : List 𝓕.FieldOp) →
|
||||||
𝓣(𝓝(ofFieldOpList φs)) = ∑ (φsΛ : {φsΛ : WickContraction φs.length // ¬ HaveEqTime φsΛ}),
|
𝓣(𝓝(ofFieldOpList φs)) =
|
||||||
φsΛ.1.sign • φsΛ.1.timeContract.1 * 𝓝(ofFieldOpList [φsΛ.1]ᵘᶜ)
|
∑ (φsΛ : {φsΛ : WickContraction φs.length // ¬ HaveEqTime φsΛ}), φsΛ.1.wickTerm
|
||||||
| [] => wicks_theorem_normal_order_empty
|
| [] => wicks_theorem_normal_order_empty
|
||||||
| φ :: φs => by
|
| φ :: φs => by
|
||||||
|
simp only [wickTerm]
|
||||||
rw [normalOrder_timeOrder_ofFieldOpList_eq_not_haveEqTime_sub_inductive]
|
rw [normalOrder_timeOrder_ofFieldOpList_eq_not_haveEqTime_sub_inductive]
|
||||||
simp only [Algebra.smul_mul_assoc, ne_eq, add_right_eq_self]
|
simp only [Algebra.smul_mul_assoc, ne_eq, add_right_eq_self]
|
||||||
apply Finset.sum_eq_zero
|
apply Finset.sum_eq_zero
|
||||||
|
|
@ -194,7 +197,7 @@ theorem wicks_theorem_normal_order : (φs : List 𝓕.FieldOp) →
|
||||||
right
|
right
|
||||||
have ih := wicks_theorem_normal_order [φsΛ.1]ᵘᶜ
|
have ih := wicks_theorem_normal_order [φsΛ.1]ᵘᶜ
|
||||||
rw [ih]
|
rw [ih]
|
||||||
simp
|
simp [wickTerm]
|
||||||
termination_by φs => φs.length
|
termination_by φs => φs.length
|
||||||
decreasing_by
|
decreasing_by
|
||||||
simp only [uncontractedListGet, List.length_cons, List.length_map, gt_iff_lt]
|
simp only [uncontractedListGet, List.length_cons, List.length_map, gt_iff_lt]
|
||||||
|
|
|
||||||
|
|
@ -3,8 +3,7 @@ Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
|
||||||
Released under Apache 2.0 license as described in the file LICENSE.
|
Released under Apache 2.0 license as described in the file LICENSE.
|
||||||
Authors: Joseph Tooby-Smith
|
Authors: Joseph Tooby-Smith
|
||||||
-/
|
-/
|
||||||
import HepLean.PerturbationTheory.FieldOpAlgebra.NormalOrder
|
import HepLean.PerturbationTheory.FieldSpecification.Basic
|
||||||
import HepLean.Mathematics.List.InsertIdx
|
|
||||||
/-!
|
/-!
|
||||||
|
|
||||||
# Wick contractions
|
# Wick contractions
|
||||||
|
|
|
||||||
|
|
@ -34,8 +34,7 @@ noncomputable def timeContract {φs : List 𝓕.FieldOp}
|
||||||
This result follows from the fact that `timeContract` only depends on contracted pairs,
|
This result follows from the fact that `timeContract` only depends on contracted pairs,
|
||||||
and `(φsΛ ↩Λ φ i none)` has the 'same' contracted pairs as `φsΛ`. -/
|
and `(φsΛ ↩Λ φ i none)` has the 'same' contracted pairs as `φsΛ`. -/
|
||||||
@[simp]
|
@[simp]
|
||||||
lemma timeContract_insertAndContract_none
|
lemma timeContract_insertAndContract_none (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
|
||||||
(φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
|
|
||||||
(φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) :
|
(φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) :
|
||||||
(φsΛ ↩Λ φ i none).timeContract = φsΛ.timeContract := by
|
(φsΛ ↩Λ φ i none).timeContract = φsΛ.timeContract := by
|
||||||
rw [timeContract, insertAndContract_none_prod_contractions]
|
rw [timeContract, insertAndContract_none_prod_contractions]
|
||||||
|
|
@ -78,7 +77,7 @@ lemma timeContract_empty (φs : List 𝓕.FieldOp) :
|
||||||
|
|
||||||
open FieldStatistic
|
open FieldStatistic
|
||||||
|
|
||||||
lemma timeConract_insertAndContract_some_eq_mul_contractStateAtIndex_lt
|
lemma timeContract_insertAndContract_some_eq_mul_contractStateAtIndex_lt
|
||||||
(φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
|
(φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
|
||||||
(φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (k : φsΛ.uncontracted)
|
(φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (k : φsΛ.uncontracted)
|
||||||
(ht : 𝓕.timeOrderRel φ φs[k.1]) (hik : i < i.succAbove k) :
|
(ht : 𝓕.timeOrderRel φ φs[k.1]) (hik : i < i.succAbove k) :
|
||||||
|
|
|
||||||
|
|
@ -145,6 +145,7 @@ def perturbationTheory : Note where
|
||||||
.name `FieldSpecification.FieldOpFreeAlgebra.superCommuteF,
|
.name `FieldSpecification.FieldOpFreeAlgebra.superCommuteF,
|
||||||
.h2 "Field-operator algebra",
|
.h2 "Field-operator algebra",
|
||||||
.name `FieldSpecification.FieldOpAlgebra,
|
.name `FieldSpecification.FieldOpAlgebra,
|
||||||
|
.name `FieldSpecification.FieldOpAlgebra.fieldOpAlgebraGrade,
|
||||||
.name `FieldSpecification.FieldOpAlgebra.superCommute,
|
.name `FieldSpecification.FieldOpAlgebra.superCommute,
|
||||||
.h1 "Time ordering",
|
.h1 "Time ordering",
|
||||||
.name `FieldSpecification.crAnTimeOrderRel,
|
.name `FieldSpecification.crAnTimeOrderRel,
|
||||||
|
|
@ -169,14 +170,13 @@ def perturbationTheory : Note where
|
||||||
.name `WickContraction.join,
|
.name `WickContraction.join,
|
||||||
.h2 "Sign",
|
.h2 "Sign",
|
||||||
.name `WickContraction.sign,
|
.name `WickContraction.sign,
|
||||||
|
.name `WickContraction.join_sign,
|
||||||
.name `WickContraction.signInsertNone_eq_filterset,
|
.name `WickContraction.signInsertNone_eq_filterset,
|
||||||
.name `WickContraction.signInsertSome_mul_filter_contracted_of_not_lt,
|
.name `WickContraction.signInsertSome_mul_filter_contracted_of_not_lt,
|
||||||
.name `WickContraction.join_sign,
|
|
||||||
.h2 "Cardinality",
|
.h2 "Cardinality",
|
||||||
.name `WickContraction.card_eq_cardFun,
|
.name `WickContraction.card_eq_cardFun,
|
||||||
.h1 "Time and static contractions",
|
.h1 "Time and static contractions",
|
||||||
.h1 "Useful results",
|
.h1 "Useful results",
|
||||||
|
|
||||||
.h1 "The three Wick's theorems",
|
.h1 "The three Wick's theorems",
|
||||||
.name `FieldSpecification.wicks_theorem,
|
.name `FieldSpecification.wicks_theorem,
|
||||||
.name `FieldSpecification.FieldOpAlgebra.static_wick_theorem,
|
.name `FieldSpecification.FieldOpAlgebra.static_wick_theorem,
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue