refactor: rename timeOrder for CrAnAlgebra
This commit is contained in:
jstoobysmith
parent
f5e7bbad59
commit
c53299d40a
4 changed files with 95 additions and 95 deletions
|
|
@ -27,19 +27,19 @@ open HepLean.List
|
|||
-/
|
||||
|
||||
/-- Time ordering for the `CrAnAlgebra`. -/
|
||||
def timeOrder : CrAnAlgebra 𝓕 →ₗ[ℂ] CrAnAlgebra 𝓕 :=
|
||||
def timeOrderF : CrAnAlgebra 𝓕 →ₗ[ℂ] CrAnAlgebra 𝓕 :=
|
||||
Basis.constr ofCrAnListBasis ℂ fun φs =>
|
||||
crAnTimeOrderSign φs • ofCrAnList (crAnTimeOrderList φs)
|
||||
|
||||
@[inherit_doc timeOrder]
|
||||
scoped[FieldSpecification.CrAnAlgebra] notation "𝓣ᶠ(" a ")" => timeOrder a
|
||||
@[inherit_doc timeOrderF]
|
||||
scoped[FieldSpecification.CrAnAlgebra] notation "𝓣ᶠ(" a ")" => timeOrderF a
|
||||
|
||||
lemma timeOrder_ofCrAnList (φs : List 𝓕.CrAnStates) :
|
||||
lemma timeOrderF_ofCrAnList (φs : List 𝓕.CrAnStates) :
|
||||
𝓣ᶠ(ofCrAnList φs) = crAnTimeOrderSign φs • ofCrAnList (crAnTimeOrderList φs) := by
|
||||
rw [← ofListBasis_eq_ofList]
|
||||
simp only [timeOrder, Basis.constr_basis]
|
||||
simp only [timeOrderF, Basis.constr_basis]
|
||||
|
||||
lemma timeOrder_timeOrder_mid (a b c : 𝓕.CrAnAlgebra) : 𝓣ᶠ(a * b * c) = 𝓣ᶠ(a * 𝓣ᶠ(b) * c) := by
|
||||
lemma timeOrderF_timeOrderF_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)
|
||||
|
|
@ -61,10 +61,10 @@ lemma timeOrder_timeOrder_mid (a b c : 𝓕.CrAnAlgebra) : 𝓣ᶠ(a * b * c) =
|
|||
· intro x hx
|
||||
obtain ⟨φs'', rfl⟩ := hx
|
||||
simp only [ofListBasis_eq_ofList, pa]
|
||||
rw [timeOrder_ofCrAnList]
|
||||
rw [timeOrderF_ofCrAnList]
|
||||
simp only [← ofCrAnList_append, Algebra.mul_smul_comm,
|
||||
Algebra.smul_mul_assoc, map_smul]
|
||||
rw [timeOrder_ofCrAnList, timeOrder_ofCrAnList, smul_smul]
|
||||
rw [timeOrderF_ofCrAnList, timeOrderF_ofCrAnList, smul_smul]
|
||||
congr 1
|
||||
· simp only [crAnTimeOrderSign, crAnTimeOrderList]
|
||||
rw [Wick.koszulSign_of_append_eq_insertionSort, mul_comm]
|
||||
|
|
@ -87,68 +87,68 @@ lemma timeOrder_timeOrder_mid (a b c : 𝓕.CrAnAlgebra) : 𝓣ᶠ(a * b * c) =
|
|||
· intro x hx h hp
|
||||
simp_all [pc]
|
||||
|
||||
lemma timeOrder_timeOrder_right (a b : 𝓕.CrAnAlgebra) : 𝓣ᶠ(a * b) = 𝓣ᶠ(a * 𝓣ᶠ(b)) := by
|
||||
lemma timeOrderF_timeOrderF_right (a b : 𝓕.CrAnAlgebra) : 𝓣ᶠ(a * b) = 𝓣ᶠ(a * 𝓣ᶠ(b)) := by
|
||||
trans 𝓣ᶠ(a * b * 1)
|
||||
· simp
|
||||
· rw [timeOrder_timeOrder_mid]
|
||||
· rw [timeOrderF_timeOrderF_mid]
|
||||
simp
|
||||
|
||||
lemma timeOrder_timeOrder_left (a b : 𝓕.CrAnAlgebra) : 𝓣ᶠ(a * b) = 𝓣ᶠ(𝓣ᶠ(a) * b) := by
|
||||
lemma timeOrderF_timeOrderF_left (a b : 𝓕.CrAnAlgebra) : 𝓣ᶠ(a * b) = 𝓣ᶠ(𝓣ᶠ(a) * b) := by
|
||||
trans 𝓣ᶠ(1 * a * b)
|
||||
· simp
|
||||
· rw [timeOrder_timeOrder_mid]
|
||||
· rw [timeOrderF_timeOrderF_mid]
|
||||
simp
|
||||
|
||||
lemma timeOrder_ofStateList (φs : List 𝓕.States) :
|
||||
lemma timeOrderF_ofStateList (φs : List 𝓕.States) :
|
||||
𝓣ᶠ(ofStateList φs) = timeOrderSign φs • ofStateList (timeOrderList φs) := by
|
||||
conv_lhs =>
|
||||
rw [ofStateList_sum, map_sum]
|
||||
enter [2, x]
|
||||
rw [timeOrder_ofCrAnList]
|
||||
rw [timeOrderF_ofCrAnList]
|
||||
simp only [crAnTimeOrderSign_crAnSection]
|
||||
rw [← Finset.smul_sum]
|
||||
congr
|
||||
rw [ofStateList_sum, sum_crAnSections_timeOrder]
|
||||
rfl
|
||||
|
||||
lemma timeOrder_ofStateList_nil : timeOrder (𝓕 := 𝓕) (ofStateList []) = 1 := by
|
||||
rw [timeOrder_ofStateList]
|
||||
lemma timeOrderF_ofStateList_nil : timeOrderF (𝓕 := 𝓕) (ofStateList []) = 1 := by
|
||||
rw [timeOrderF_ofStateList]
|
||||
simp [timeOrderSign, Wick.koszulSign, timeOrderList]
|
||||
|
||||
@[simp]
|
||||
lemma timeOrder_ofStateList_singleton (φ : 𝓕.States) : 𝓣ᶠ(ofStateList [φ]) = ofStateList [φ] := by
|
||||
simp [timeOrder_ofStateList, timeOrderSign, timeOrderList]
|
||||
lemma timeOrderF_ofStateList_singleton (φ : 𝓕.States) : 𝓣ᶠ(ofStateList [φ]) = ofStateList [φ] := by
|
||||
simp [timeOrderF_ofStateList, timeOrderSign, timeOrderList]
|
||||
|
||||
lemma timeOrder_ofState_ofState_ordered {φ ψ : 𝓕.States} (h : timeOrderRel φ ψ) :
|
||||
lemma timeOrderF_ofState_ofState_ordered {φ ψ : 𝓕.States} (h : timeOrderRel φ ψ) :
|
||||
𝓣ᶠ(ofState φ * ofState ψ) = ofState φ * ofState ψ := by
|
||||
rw [← ofStateList_singleton, ← ofStateList_singleton, ← ofStateList_append, timeOrder_ofStateList]
|
||||
rw [← ofStateList_singleton, ← ofStateList_singleton, ← ofStateList_append, timeOrderF_ofStateList]
|
||||
simp only [List.singleton_append]
|
||||
rw [timeOrderSign_pair_ordered h, timeOrderList_pair_ordered h]
|
||||
simp
|
||||
|
||||
lemma timeOrder_ofState_ofState_not_ordered {φ ψ : 𝓕.States} (h : ¬ timeOrderRel φ ψ) :
|
||||
lemma timeOrderF_ofState_ofState_not_ordered {φ ψ : 𝓕.States} (h : ¬ timeOrderRel φ ψ) :
|
||||
𝓣ᶠ(ofState φ * ofState ψ) = 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ ψ) • ofState ψ * ofState φ := by
|
||||
rw [← ofStateList_singleton, ← ofStateList_singleton,
|
||||
← ofStateList_append, timeOrder_ofStateList]
|
||||
← ofStateList_append, timeOrderF_ofStateList]
|
||||
simp only [List.singleton_append, instCommGroup.eq_1, Algebra.smul_mul_assoc]
|
||||
rw [timeOrderSign_pair_not_ordered h, timeOrderList_pair_not_ordered h]
|
||||
simp [← ofStateList_append]
|
||||
|
||||
lemma timeOrder_ofState_ofState_not_ordered_eq_timeOrder {φ ψ : 𝓕.States} (h : ¬ timeOrderRel φ ψ) :
|
||||
lemma timeOrderF_ofState_ofState_not_ordered_eq_timeOrderF {φ ψ : 𝓕.States} (h : ¬ timeOrderRel φ ψ) :
|
||||
𝓣ᶠ(ofState φ * ofState ψ) = 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ ψ) • 𝓣ᶠ(ofState ψ * ofState φ) := by
|
||||
rw [timeOrder_ofState_ofState_not_ordered h]
|
||||
rw [timeOrder_ofState_ofState_ordered]
|
||||
rw [timeOrderF_ofState_ofState_not_ordered h]
|
||||
rw [timeOrderF_ofState_ofState_ordered]
|
||||
simp only [instCommGroup.eq_1, Algebra.smul_mul_assoc]
|
||||
have hx := IsTotal.total (r := timeOrderRel) ψ φ
|
||||
simp_all
|
||||
|
||||
lemma timeOrder_superCommuteF_ofCrAnState_ofCrAnState_not_crAnTimeOrderRel
|
||||
lemma timeOrderF_superCommuteF_ofCrAnState_ofCrAnState_not_crAnTimeOrderRel
|
||||
{φ ψ : 𝓕.CrAnStates} (h : ¬ crAnTimeOrderRel φ ψ) :
|
||||
𝓣ᶠ([ofCrAnState φ, ofCrAnState ψ]ₛca) = 0 := by
|
||||
rw [superCommuteF_ofCrAnState_ofCrAnState]
|
||||
simp only [instCommGroup.eq_1, Algebra.smul_mul_assoc, map_sub, map_smul]
|
||||
rw [← ofCrAnList_singleton, ← ofCrAnList_singleton,
|
||||
← ofCrAnList_append, ← ofCrAnList_append, timeOrder_ofCrAnList, timeOrder_ofCrAnList]
|
||||
← ofCrAnList_append, ← ofCrAnList_append, timeOrderF_ofCrAnList, timeOrderF_ofCrAnList]
|
||||
simp only [List.singleton_append]
|
||||
rw [crAnTimeOrderSign_pair_not_ordered h, crAnTimeOrderList_pair_not_ordered h]
|
||||
rw [sub_eq_zero, smul_smul]
|
||||
|
|
@ -160,51 +160,51 @@ lemma timeOrder_superCommuteF_ofCrAnState_ofCrAnState_not_crAnTimeOrderRel
|
|||
· rw [crAnTimeOrderList_pair_ordered]
|
||||
simp_all
|
||||
|
||||
lemma timeOrder_superCommuteF_ofCrAnState_ofCrAnState_not_crAnTimeOrderRel_right
|
||||
lemma timeOrderF_superCommuteF_ofCrAnState_ofCrAnState_not_crAnTimeOrderRel_right
|
||||
{φ ψ : 𝓕.CrAnStates} (h : ¬ crAnTimeOrderRel φ ψ) (a : 𝓕.CrAnAlgebra) :
|
||||
𝓣ᶠ(a * [ofCrAnState φ, ofCrAnState ψ]ₛca) = 0 := by
|
||||
rw [timeOrder_timeOrder_right,
|
||||
timeOrder_superCommuteF_ofCrAnState_ofCrAnState_not_crAnTimeOrderRel h]
|
||||
rw [timeOrderF_timeOrderF_right,
|
||||
timeOrderF_superCommuteF_ofCrAnState_ofCrAnState_not_crAnTimeOrderRel h]
|
||||
simp
|
||||
|
||||
lemma timeOrder_superCommuteF_ofCrAnState_ofCrAnState_not_crAnTimeOrderRel_left
|
||||
lemma timeOrderF_superCommuteF_ofCrAnState_ofCrAnState_not_crAnTimeOrderRel_left
|
||||
{φ ψ : 𝓕.CrAnStates} (h : ¬ crAnTimeOrderRel φ ψ) (a : 𝓕.CrAnAlgebra) :
|
||||
𝓣ᶠ([ofCrAnState φ, ofCrAnState ψ]ₛca * a) = 0 := by
|
||||
rw [timeOrder_timeOrder_left,
|
||||
timeOrder_superCommuteF_ofCrAnState_ofCrAnState_not_crAnTimeOrderRel h]
|
||||
rw [timeOrderF_timeOrderF_left,
|
||||
timeOrderF_superCommuteF_ofCrAnState_ofCrAnState_not_crAnTimeOrderRel h]
|
||||
simp
|
||||
|
||||
lemma timeOrder_superCommuteF_ofCrAnState_ofCrAnState_not_crAnTimeOrderRel_mid
|
||||
lemma timeOrderF_superCommuteF_ofCrAnState_ofCrAnState_not_crAnTimeOrderRel_mid
|
||||
{φ ψ : 𝓕.CrAnStates} (h : ¬ crAnTimeOrderRel φ ψ) (a b : 𝓕.CrAnAlgebra) :
|
||||
𝓣ᶠ(a * [ofCrAnState φ, ofCrAnState ψ]ₛca * b) = 0 := by
|
||||
rw [timeOrder_timeOrder_mid,
|
||||
timeOrder_superCommuteF_ofCrAnState_ofCrAnState_not_crAnTimeOrderRel h]
|
||||
rw [timeOrderF_timeOrderF_mid,
|
||||
timeOrderF_superCommuteF_ofCrAnState_ofCrAnState_not_crAnTimeOrderRel h]
|
||||
simp
|
||||
|
||||
lemma timeOrder_superCommuteF_superCommuteF_ofCrAnState_not_crAnTimeOrderRel
|
||||
lemma timeOrderF_superCommuteF_superCommuteF_ofCrAnState_not_crAnTimeOrderRel
|
||||
{φ1 φ2 : 𝓕.CrAnStates} (h : ¬ crAnTimeOrderRel φ1 φ2) (a : 𝓕.CrAnAlgebra) :
|
||||
𝓣ᶠ([a, [ofCrAnState φ1, ofCrAnState φ2]ₛca]ₛca) = 0 := by
|
||||
rw [← bosonicProj_add_fermionicProj a]
|
||||
simp only [map_add, LinearMap.add_apply]
|
||||
rw [bosonic_superCommuteF (Submodule.coe_mem (bosonicProj a))]
|
||||
simp only [map_sub]
|
||||
rw [timeOrder_superCommuteF_ofCrAnState_ofCrAnState_not_crAnTimeOrderRel_left h]
|
||||
rw [timeOrder_superCommuteF_ofCrAnState_ofCrAnState_not_crAnTimeOrderRel_right h]
|
||||
rw [timeOrderF_superCommuteF_ofCrAnState_ofCrAnState_not_crAnTimeOrderRel_left h]
|
||||
rw [timeOrderF_superCommuteF_ofCrAnState_ofCrAnState_not_crAnTimeOrderRel_right h]
|
||||
simp only [sub_self, zero_add]
|
||||
rw [← ofCrAnList_singleton, ← ofCrAnList_singleton]
|
||||
rcases superCommuteF_ofCrAnList_ofCrAnList_bosonic_or_fermionic [φ1] [φ2] with h' | h'
|
||||
· rw [superCommuteF_bonsonic h']
|
||||
simp only [ofCrAnList_singleton, map_sub]
|
||||
rw [timeOrder_superCommuteF_ofCrAnState_ofCrAnState_not_crAnTimeOrderRel_left h]
|
||||
rw [timeOrder_superCommuteF_ofCrAnState_ofCrAnState_not_crAnTimeOrderRel_right h]
|
||||
rw [timeOrderF_superCommuteF_ofCrAnState_ofCrAnState_not_crAnTimeOrderRel_left h]
|
||||
rw [timeOrderF_superCommuteF_ofCrAnState_ofCrAnState_not_crAnTimeOrderRel_right h]
|
||||
simp
|
||||
· rw [superCommuteF_fermionic_fermionic (Submodule.coe_mem (fermionicProj a)) h']
|
||||
simp only [ofCrAnList_singleton, map_add]
|
||||
rw [timeOrder_superCommuteF_ofCrAnState_ofCrAnState_not_crAnTimeOrderRel_left h]
|
||||
rw [timeOrder_superCommuteF_ofCrAnState_ofCrAnState_not_crAnTimeOrderRel_right h]
|
||||
rw [timeOrderF_superCommuteF_ofCrAnState_ofCrAnState_not_crAnTimeOrderRel_left h]
|
||||
rw [timeOrderF_superCommuteF_ofCrAnState_ofCrAnState_not_crAnTimeOrderRel_right h]
|
||||
simp
|
||||
|
||||
lemma timeOrder_superCommuteF_ofCrAnState_superCommuteF_not_crAnTimeOrderRel
|
||||
lemma timeOrderF_superCommuteF_ofCrAnState_superCommuteF_not_crAnTimeOrderRel
|
||||
{φ1 φ2 φ3 : 𝓕.CrAnStates} (h12 : ¬ crAnTimeOrderRel φ1 φ2)
|
||||
(h13 : ¬ crAnTimeOrderRel φ1 φ3) :
|
||||
𝓣ᶠ([ofCrAnState φ1, [ofCrAnState φ2, ofCrAnState φ3]ₛca]ₛca) = 0 := by
|
||||
|
|
@ -213,14 +213,14 @@ lemma timeOrder_superCommuteF_ofCrAnState_superCommuteF_not_crAnTimeOrderRel
|
|||
simp only [instCommGroup.eq_1, ofList_singleton, ofCrAnList_singleton, neg_smul, map_smul,
|
||||
map_sub, map_neg, smul_eq_zero]
|
||||
right
|
||||
rw [timeOrder_superCommuteF_superCommuteF_ofCrAnState_not_crAnTimeOrderRel h12]
|
||||
rw [timeOrderF_superCommuteF_superCommuteF_ofCrAnState_not_crAnTimeOrderRel h12]
|
||||
rw [superCommuteF_ofCrAnState_ofCrAnState_symm φ3]
|
||||
simp only [smul_zero, neg_zero, instCommGroup.eq_1, neg_smul, map_neg, map_smul, smul_neg,
|
||||
sub_neg_eq_add, zero_add, smul_eq_zero]
|
||||
rw [timeOrder_superCommuteF_superCommuteF_ofCrAnState_not_crAnTimeOrderRel h13]
|
||||
rw [timeOrderF_superCommuteF_superCommuteF_ofCrAnState_not_crAnTimeOrderRel h13]
|
||||
simp
|
||||
|
||||
lemma timeOrder_superCommuteF_ofCrAnState_superCommuteF_not_crAnTimeOrderRel'
|
||||
lemma timeOrderF_superCommuteF_ofCrAnState_superCommuteF_not_crAnTimeOrderRel'
|
||||
{φ1 φ2 φ3 : 𝓕.CrAnStates} (h12 : ¬ crAnTimeOrderRel φ2 φ1)
|
||||
(h13 : ¬ crAnTimeOrderRel φ3 φ1) :
|
||||
𝓣ᶠ([ofCrAnState φ1, [ofCrAnState φ2, ofCrAnState φ3]ₛca]ₛca) = 0 := by
|
||||
|
|
@ -231,12 +231,12 @@ lemma timeOrder_superCommuteF_ofCrAnState_superCommuteF_not_crAnTimeOrderRel'
|
|||
right
|
||||
rw [superCommuteF_ofCrAnState_ofCrAnState_symm φ1]
|
||||
simp only [instCommGroup.eq_1, neg_smul, map_neg, map_smul, smul_neg, neg_neg]
|
||||
rw [timeOrder_superCommuteF_superCommuteF_ofCrAnState_not_crAnTimeOrderRel h12]
|
||||
rw [timeOrderF_superCommuteF_superCommuteF_ofCrAnState_not_crAnTimeOrderRel h12]
|
||||
simp only [smul_zero, zero_sub, neg_eq_zero, smul_eq_zero]
|
||||
rw [timeOrder_superCommuteF_superCommuteF_ofCrAnState_not_crAnTimeOrderRel h13]
|
||||
rw [timeOrderF_superCommuteF_superCommuteF_ofCrAnState_not_crAnTimeOrderRel h13]
|
||||
simp
|
||||
|
||||
lemma timeOrder_superCommuteF_ofCrAnState_superCommuteF_all_not_crAnTimeOrderRel
|
||||
lemma timeOrderF_superCommuteF_ofCrAnState_superCommuteF_all_not_crAnTimeOrderRel
|
||||
(φ1 φ2 φ3 : 𝓕.CrAnStates) (h : ¬
|
||||
(crAnTimeOrderRel φ1 φ2 ∧ crAnTimeOrderRel φ1 φ3 ∧
|
||||
crAnTimeOrderRel φ2 φ1 ∧ crAnTimeOrderRel φ2 φ3 ∧
|
||||
|
|
@ -245,13 +245,13 @@ lemma timeOrder_superCommuteF_ofCrAnState_superCommuteF_all_not_crAnTimeOrderRel
|
|||
simp only [not_and] at h
|
||||
by_cases h23 : ¬ crAnTimeOrderRel φ2 φ3
|
||||
· simp_all only [IsEmpty.forall_iff, implies_true]
|
||||
rw [timeOrder_superCommuteF_superCommuteF_ofCrAnState_not_crAnTimeOrderRel h23]
|
||||
rw [timeOrderF_superCommuteF_superCommuteF_ofCrAnState_not_crAnTimeOrderRel h23]
|
||||
simp_all only [Decidable.not_not, forall_const]
|
||||
by_cases h32 : ¬ crAnTimeOrderRel φ3 φ2
|
||||
· simp_all only [not_false_eq_true, implies_true]
|
||||
rw [superCommuteF_ofCrAnState_ofCrAnState_symm]
|
||||
simp only [instCommGroup.eq_1, neg_smul, map_neg, map_smul, neg_eq_zero, smul_eq_zero]
|
||||
rw [timeOrder_superCommuteF_superCommuteF_ofCrAnState_not_crAnTimeOrderRel h32]
|
||||
rw [timeOrderF_superCommuteF_superCommuteF_ofCrAnState_not_crAnTimeOrderRel h32]
|
||||
simp
|
||||
simp_all only [imp_false, Decidable.not_not]
|
||||
by_cases h12 : ¬ crAnTimeOrderRel φ1 φ2
|
||||
|
|
@ -259,7 +259,7 @@ lemma timeOrder_superCommuteF_ofCrAnState_superCommuteF_all_not_crAnTimeOrderRel
|
|||
intro h13
|
||||
apply h12
|
||||
exact IsTrans.trans φ1 φ3 φ2 h13 h32
|
||||
rw [timeOrder_superCommuteF_ofCrAnState_superCommuteF_not_crAnTimeOrderRel h12 h13]
|
||||
rw [timeOrderF_superCommuteF_ofCrAnState_superCommuteF_not_crAnTimeOrderRel h12 h13]
|
||||
simp_all only [Decidable.not_not, forall_const]
|
||||
have h13 : crAnTimeOrderRel φ1 φ3 := IsTrans.trans φ1 φ2 φ3 h12 h23
|
||||
simp_all only [forall_const]
|
||||
|
|
@ -269,18 +269,18 @@ lemma timeOrder_superCommuteF_ofCrAnState_superCommuteF_all_not_crAnTimeOrderRel
|
|||
intro h31
|
||||
apply h21
|
||||
exact IsTrans.trans φ2 φ3 φ1 h23 h31
|
||||
rw [timeOrder_superCommuteF_ofCrAnState_superCommuteF_not_crAnTimeOrderRel' h21 h31]
|
||||
rw [timeOrderF_superCommuteF_ofCrAnState_superCommuteF_not_crAnTimeOrderRel' h21 h31]
|
||||
simp_all only [Decidable.not_not, forall_const]
|
||||
refine False.elim (h ?_)
|
||||
exact IsTrans.trans φ3 φ2 φ1 h32 h21
|
||||
|
||||
lemma timeOrder_superCommuteF_ofCrAnState_ofCrAnState_eq_time
|
||||
lemma timeOrderF_superCommuteF_ofCrAnState_ofCrAnState_eq_time
|
||||
{φ ψ : 𝓕.CrAnStates} (h1 : crAnTimeOrderRel φ ψ) (h2 : crAnTimeOrderRel ψ φ) :
|
||||
𝓣ᶠ([ofCrAnState φ, ofCrAnState ψ]ₛca) = [ofCrAnState φ, ofCrAnState ψ]ₛca := by
|
||||
rw [superCommuteF_ofCrAnState_ofCrAnState]
|
||||
simp only [instCommGroup.eq_1, Algebra.smul_mul_assoc, map_sub, map_smul]
|
||||
rw [← ofCrAnList_singleton, ← ofCrAnList_singleton,
|
||||
← ofCrAnList_append, ← ofCrAnList_append, timeOrder_ofCrAnList, timeOrder_ofCrAnList]
|
||||
← ofCrAnList_append, ← ofCrAnList_append, timeOrderF_ofCrAnList, timeOrderF_ofCrAnList]
|
||||
simp only [List.singleton_append]
|
||||
rw [crAnTimeOrderSign_pair_ordered h1, crAnTimeOrderList_pair_ordered h1,
|
||||
crAnTimeOrderSign_pair_ordered h2, crAnTimeOrderList_pair_ordered h2]
|
||||
|
|
@ -295,12 +295,12 @@ lemma timeOrder_superCommuteF_ofCrAnState_ofCrAnState_eq_time
|
|||
/-- In the state algebra time, ordering obeys `T(φ₀φ₁…φₙ) = s * φᵢ * T(φ₀φ₁…φᵢ₋₁φᵢ₊₁…φₙ)`
|
||||
where `φᵢ` is the state
|
||||
which has maximum time and `s` is the exchange sign of `φᵢ` and `φ₀φ₁…φᵢ₋₁`. -/
|
||||
lemma timeOrder_eq_maxTimeField_mul (φ : 𝓕.States) (φs : List 𝓕.States) :
|
||||
lemma timeOrderF_eq_maxTimeField_mul (φ : 𝓕.States) (φs : List 𝓕.States) :
|
||||
𝓣ᶠ(ofStateList (φ :: φs)) =
|
||||
𝓢(𝓕 |>ₛ maxTimeField φ φs, 𝓕 |>ₛ (φ :: φs).take (maxTimeFieldPos φ φs)) •
|
||||
ofState (maxTimeField φ φs) * 𝓣ᶠ(ofStateList (eraseMaxTimeField φ φs)) := by
|
||||
rw [timeOrder_ofStateList, timeOrderList_eq_maxTimeField_timeOrderList]
|
||||
rw [ofStateList_cons, timeOrder_ofStateList]
|
||||
rw [timeOrderF_ofStateList, timeOrderList_eq_maxTimeField_timeOrderList]
|
||||
rw [ofStateList_cons, timeOrderF_ofStateList]
|
||||
simp only [instCommGroup.eq_1, Algebra.mul_smul_comm, Algebra.smul_mul_assoc, smul_smul]
|
||||
congr
|
||||
rw [timerOrderSign_of_eraseMaxTimeField, mul_assoc]
|
||||
|
|
@ -310,12 +310,12 @@ lemma timeOrder_eq_maxTimeField_mul (φ : 𝓕.States) (φs : List 𝓕.States)
|
|||
where `φᵢ` is the state
|
||||
which has maximum time and `s` is the exchange sign of `φᵢ` and `φ₀φ₁…φᵢ₋₁`.
|
||||
Here `s` is written using finite sets. -/
|
||||
lemma timeOrder_eq_maxTimeField_mul_finset (φ : 𝓕.States) (φs : List 𝓕.States) :
|
||||
lemma timeOrderF_eq_maxTimeField_mul_finset (φ : 𝓕.States) (φs : List 𝓕.States) :
|
||||
𝓣ᶠ(ofStateList (φ :: φs)) = 𝓢(𝓕 |>ₛ maxTimeField φ φs, 𝓕 |>ₛ ⟨(eraseMaxTimeField φ φs).get,
|
||||
(Finset.filter (fun x =>
|
||||
(maxTimeFieldPosFin φ φs).succAbove x < maxTimeFieldPosFin φ φs) Finset.univ)⟩) •
|
||||
ofState (maxTimeField φ φs) * 𝓣ᶠ(ofStateList (eraseMaxTimeField φ φs)) := by
|
||||
rw [timeOrder_eq_maxTimeField_mul]
|
||||
rw [timeOrderF_eq_maxTimeField_mul]
|
||||
congr 3
|
||||
apply FieldStatistic.ofList_perm
|
||||
nth_rewrite 1 [← List.finRange_map_get (φ :: φs)]
|
||||
|
|
|
|||
|
|
@ -19,7 +19,7 @@ open FieldStatistic
|
|||
namespace FieldOpAlgebra
|
||||
variable {𝓕 : FieldSpecification}
|
||||
|
||||
lemma ι_timeOrder_superCommuteF_superCommuteF_eq_time_ofCrAnList {φ1 φ2 φ3 : 𝓕.CrAnStates}
|
||||
lemma ι_timeOrderF_superCommuteF_superCommuteF_eq_time_ofCrAnList {φ1 φ2 φ3 : 𝓕.CrAnStates}
|
||||
(φs1 φs2 : List 𝓕.CrAnStates) (h :
|
||||
crAnTimeOrderRel φ1 φ2 ∧ crAnTimeOrderRel φ1 φ3 ∧
|
||||
crAnTimeOrderRel φ2 φ1 ∧ crAnTimeOrderRel φ2 φ3 ∧
|
||||
|
|
@ -38,7 +38,7 @@ lemma ι_timeOrder_superCommuteF_superCommuteF_eq_time_ofCrAnList {φ1 φ2 φ3 :
|
|||
• (ι (ofCrAnList l1) * ι (ofCrAnList [φ1, φ2, φ3]) * ι (ofCrAnList l2)) := by
|
||||
have h1 := insertionSort_of_eq_list 𝓕.crAnTimeOrderRel φ1 φs1 [φ1, φ2, φ3] φs2
|
||||
(by simp_all)
|
||||
rw [timeOrder_ofCrAnList, show φs1 ++ φ1 :: φ2 :: φ3 :: φs2 = φs1 ++ [φ1, φ2, φ3] ++ φs2
|
||||
rw [timeOrderF_ofCrAnList, show φs1 ++ φ1 :: φ2 :: φ3 :: φs2 = φs1 ++ [φ1, φ2, φ3] ++ φs2
|
||||
by simp, crAnTimeOrderList, h1]
|
||||
simp only [List.append_assoc, List.singleton_append, decide_not,
|
||||
Bool.decide_and, ofCrAnList_append, map_smul, map_mul, l1, l2, mul_assoc]
|
||||
|
|
@ -47,7 +47,7 @@ lemma ι_timeOrder_superCommuteF_superCommuteF_eq_time_ofCrAnList {φ1 φ2 φ3 :
|
|||
• (ι (ofCrAnList l1) * ι (ofCrAnList [φ1, φ3, φ2]) * ι (ofCrAnList l2)) := by
|
||||
have h1 := insertionSort_of_eq_list 𝓕.crAnTimeOrderRel φ1 φs1 [φ1, φ3, φ2] φs2
|
||||
(by simp_all)
|
||||
rw [timeOrder_ofCrAnList, show φs1 ++ φ1 :: φ3 :: φ2 :: φs2 = φs1 ++ [φ1, φ3, φ2] ++ φs2
|
||||
rw [timeOrderF_ofCrAnList, show φs1 ++ φ1 :: φ3 :: φ2 :: φs2 = φs1 ++ [φ1, φ3, φ2] ++ φs2
|
||||
by simp, crAnTimeOrderList, h1]
|
||||
simp only [List.singleton_append, decide_not,
|
||||
Bool.decide_and, ofCrAnList_append, map_smul, map_mul, l1, l2, mul_assoc]
|
||||
|
|
@ -72,7 +72,7 @@ lemma ι_timeOrder_superCommuteF_superCommuteF_eq_time_ofCrAnList {φ1 φ2 φ3 :
|
|||
• (ι (ofCrAnList l1) * ι (ofCrAnList [φ2, φ3, φ1]) * ι (ofCrAnList l2)) := by
|
||||
have h1 := insertionSort_of_eq_list 𝓕.crAnTimeOrderRel φ1 φs1 [φ2, φ3, φ1] φs2
|
||||
(by simp_all)
|
||||
rw [timeOrder_ofCrAnList, show φs1 ++ φ2 :: φ3 :: φ1 :: φs2 = φs1 ++ [φ2, φ3, φ1] ++ φs2
|
||||
rw [timeOrderF_ofCrAnList, show φs1 ++ φ2 :: φ3 :: φ1 :: φs2 = φs1 ++ [φ2, φ3, φ1] ++ φs2
|
||||
by simp, crAnTimeOrderList, h1]
|
||||
simp only [List.singleton_append, decide_not,
|
||||
Bool.decide_and, ofCrAnList_append, map_smul, map_mul, l1, l2, mul_assoc]
|
||||
|
|
@ -90,7 +90,7 @@ lemma ι_timeOrder_superCommuteF_superCommuteF_eq_time_ofCrAnList {φ1 φ2 φ3 :
|
|||
• (ι (ofCrAnList l1) * ι (ofCrAnList [φ3, φ2, φ1]) * ι (ofCrAnList l2)) := by
|
||||
have h1 := insertionSort_of_eq_list 𝓕.crAnTimeOrderRel φ1 φs1 [φ3, φ2, φ1] φs2
|
||||
(by simp_all)
|
||||
rw [timeOrder_ofCrAnList, show φs1 ++ φ3 :: φ2 :: φ1 :: φs2 = φs1 ++ [φ3, φ2, φ1] ++ φs2
|
||||
rw [timeOrderF_ofCrAnList, show φs1 ++ φ3 :: φ2 :: φ1 :: φs2 = φs1 ++ [φ3, φ2, φ1] ++ φs2
|
||||
by simp, crAnTimeOrderList, h1]
|
||||
simp only [List.singleton_append, decide_not,
|
||||
Bool.decide_and, ofCrAnList_append, map_smul, map_mul, l1, l2, mul_assoc]
|
||||
|
|
@ -139,7 +139,7 @@ lemma ι_timeOrder_superCommuteF_superCommuteF_eq_time_ofCrAnList {φ1 φ2 φ3 :
|
|||
map_smul, smul_sub]
|
||||
simp_all
|
||||
|
||||
lemma ι_timeOrder_superCommuteF_superCommuteF_ofCrAnList {φ1 φ2 φ3 : 𝓕.CrAnStates}
|
||||
lemma ι_timeOrderF_superCommuteF_superCommuteF_ofCrAnList {φ1 φ2 φ3 : 𝓕.CrAnStates}
|
||||
(φs1 φs2 : List 𝓕.CrAnStates) :
|
||||
ι 𝓣ᶠ(ofCrAnList φs1 * [ofCrAnState φ1, [ofCrAnState φ2, ofCrAnState φ3]ₛca]ₛca * ofCrAnList φs2)
|
||||
= 0 := by
|
||||
|
|
@ -147,13 +147,13 @@ lemma ι_timeOrder_superCommuteF_superCommuteF_ofCrAnList {φ1 φ2 φ3 : 𝓕.Cr
|
|||
crAnTimeOrderRel φ1 φ2 ∧ crAnTimeOrderRel φ1 φ3 ∧
|
||||
crAnTimeOrderRel φ2 φ1 ∧ crAnTimeOrderRel φ2 φ3 ∧
|
||||
crAnTimeOrderRel φ3 φ1 ∧ crAnTimeOrderRel φ3 φ2
|
||||
· exact ι_timeOrder_superCommuteF_superCommuteF_eq_time_ofCrAnList φs1 φs2 h
|
||||
· rw [timeOrder_timeOrder_mid]
|
||||
rw [timeOrder_superCommuteF_ofCrAnState_superCommuteF_all_not_crAnTimeOrderRel _ _ _ h]
|
||||
· exact ι_timeOrderF_superCommuteF_superCommuteF_eq_time_ofCrAnList φs1 φs2 h
|
||||
· rw [timeOrderF_timeOrderF_mid]
|
||||
rw [timeOrderF_superCommuteF_ofCrAnState_superCommuteF_all_not_crAnTimeOrderRel _ _ _ h]
|
||||
simp
|
||||
|
||||
@[simp]
|
||||
lemma ι_timeOrder_superCommuteF_superCommuteF {φ1 φ2 φ3 : 𝓕.CrAnStates} (a b : 𝓕.CrAnAlgebra) :
|
||||
lemma ι_timeOrderF_superCommuteF_superCommuteF {φ1 φ2 φ3 : 𝓕.CrAnStates} (a b : 𝓕.CrAnAlgebra) :
|
||||
ι 𝓣ᶠ(a * [ofCrAnState φ1, [ofCrAnState φ2, ofCrAnState φ3]ₛca]ₛca * b) = 0 := by
|
||||
let pb (b : 𝓕.CrAnAlgebra) (hc : b ∈ Submodule.span ℂ (Set.range ofCrAnListBasis)) :
|
||||
Prop := ι 𝓣ᶠ(a * [ofCrAnState φ1, [ofCrAnState φ2, ofCrAnState φ3]ₛca]ₛca * b) = 0
|
||||
|
|
@ -169,7 +169,7 @@ lemma ι_timeOrder_superCommuteF_superCommuteF {φ1 φ2 φ3 : 𝓕.CrAnStates} (
|
|||
· intro x hx
|
||||
obtain ⟨φs', rfl⟩ := hx
|
||||
simp only [ofListBasis_eq_ofList, pa]
|
||||
exact ι_timeOrder_superCommuteF_superCommuteF_ofCrAnList φs' φs
|
||||
exact ι_timeOrderF_superCommuteF_superCommuteF_ofCrAnList φs' φs
|
||||
· simp [pa]
|
||||
· intro x y hx hy hpx hpy
|
||||
simp_all [pa,mul_add, add_mul]
|
||||
|
|
@ -181,7 +181,7 @@ lemma ι_timeOrder_superCommuteF_superCommuteF {φ1 φ2 φ3 : 𝓕.CrAnStates} (
|
|||
· intro x hx hpx
|
||||
simp_all [pb, hpx]
|
||||
|
||||
lemma ι_timeOrder_superCommuteF_eq_time {φ ψ : 𝓕.CrAnStates}
|
||||
lemma ι_timeOrderF_superCommuteF_eq_time {φ ψ : 𝓕.CrAnStates}
|
||||
(hφψ : crAnTimeOrderRel φ ψ) (hψφ : crAnTimeOrderRel ψ φ) (a b : 𝓕.CrAnAlgebra) :
|
||||
ι 𝓣ᶠ(a * [ofCrAnState φ, ofCrAnState ψ]ₛca * b) =
|
||||
ι ([ofCrAnState φ, ofCrAnState ψ]ₛca * 𝓣ᶠ(a * b)) := by
|
||||
|
|
@ -204,7 +204,7 @@ lemma ι_timeOrder_superCommuteF_eq_time {φ ψ : 𝓕.CrAnStates}
|
|||
conv_lhs =>
|
||||
rw [← ofCrAnList_singleton, ← ofCrAnList_singleton, superCommuteF_ofCrAnList_ofCrAnList]
|
||||
simp [mul_sub, sub_mul, ← ofCrAnList_append]
|
||||
rw [timeOrder_ofCrAnList, timeOrder_ofCrAnList]
|
||||
rw [timeOrderF_ofCrAnList, timeOrderF_ofCrAnList]
|
||||
have h1 : crAnTimeOrderSign (φs' ++ φ :: ψ :: φs) =
|
||||
crAnTimeOrderSign (φs' ++ ψ :: φ :: φs) := by
|
||||
trans crAnTimeOrderSign (φs' ++ [φ, ψ] ++ φs)
|
||||
|
|
@ -260,7 +260,7 @@ lemma ι_timeOrder_superCommuteF_eq_time {φ ψ : 𝓕.CrAnStates}
|
|||
· rw [ι_superCommuteF_of_diff_statistic hq]
|
||||
simp
|
||||
· rw [crAnTimeOrderSign, Wick.koszulSign_eq_rel_eq_stat _ _, ← crAnTimeOrderSign]
|
||||
rw [timeOrder_ofCrAnList]
|
||||
rw [timeOrderF_ofCrAnList]
|
||||
simp only [map_smul, Algebra.mul_smul_comm]
|
||||
simp only [List.nil_append]
|
||||
exact hψφ
|
||||
|
|
@ -277,30 +277,30 @@ lemma ι_timeOrder_superCommuteF_eq_time {φ ψ : 𝓕.CrAnStates}
|
|||
· intro x hx hpx
|
||||
simp_all [pb, hpx]
|
||||
|
||||
lemma ι_timeOrder_superCommuteF_neq_time {φ ψ : 𝓕.CrAnStates}
|
||||
lemma ι_timeOrderF_superCommuteF_neq_time {φ ψ : 𝓕.CrAnStates}
|
||||
(hφψ : ¬ (crAnTimeOrderRel φ ψ ∧ crAnTimeOrderRel ψ φ)) (a b : 𝓕.CrAnAlgebra) :
|
||||
ι 𝓣ᶠ(a * [ofCrAnState φ, ofCrAnState ψ]ₛca * b) = 0 := by
|
||||
rw [timeOrder_timeOrder_mid]
|
||||
rw [timeOrderF_timeOrderF_mid]
|
||||
have hφψ : ¬ (crAnTimeOrderRel φ ψ) ∨ ¬ (crAnTimeOrderRel ψ φ) := by
|
||||
exact Decidable.not_and_iff_or_not.mp hφψ
|
||||
rcases hφψ with hφψ | hφψ
|
||||
· rw [timeOrder_superCommuteF_ofCrAnState_ofCrAnState_not_crAnTimeOrderRel]
|
||||
· rw [timeOrderF_superCommuteF_ofCrAnState_ofCrAnState_not_crAnTimeOrderRel]
|
||||
simp_all only [false_and, not_false_eq_true, false_or, mul_zero, zero_mul, map_zero]
|
||||
simp_all
|
||||
· rw [superCommuteF_ofCrAnState_ofCrAnState_symm]
|
||||
simp only [instCommGroup.eq_1, neg_smul, map_neg, map_smul, mul_neg, Algebra.mul_smul_comm,
|
||||
neg_mul, Algebra.smul_mul_assoc, neg_eq_zero, smul_eq_zero]
|
||||
rw [timeOrder_superCommuteF_ofCrAnState_ofCrAnState_not_crAnTimeOrderRel]
|
||||
rw [timeOrderF_superCommuteF_ofCrAnState_ofCrAnState_not_crAnTimeOrderRel]
|
||||
simp only [mul_zero, zero_mul, map_zero, or_true]
|
||||
simp_all
|
||||
|
||||
/-!
|
||||
|
||||
## Defining normal order for `FiedOpAlgebra`.
|
||||
## Defining time order for `FiedOpAlgebra`.
|
||||
|
||||
-/
|
||||
|
||||
lemma ι_timeOrder_zero_of_mem_ideal (a : 𝓕.CrAnAlgebra)
|
||||
lemma ι_timeOrderF_zero_of_mem_ideal (a : 𝓕.CrAnAlgebra)
|
||||
(h : a ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet) : ι 𝓣ᶠ(a) = 0 := by
|
||||
rw [TwoSidedIdeal.mem_span_iff_mem_addSubgroup_closure] at h
|
||||
let p {k : Set 𝓕.CrAnAlgebra} (a : CrAnAlgebra 𝓕) (h : a ∈ AddSubgroup.closure k) := ι 𝓣ᶠ(a) = 0
|
||||
|
|
@ -314,11 +314,11 @@ lemma ι_timeOrder_zero_of_mem_ideal (a : 𝓕.CrAnAlgebra)
|
|||
match hc with
|
||||
| Or.inl hc =>
|
||||
obtain ⟨φa, φa', hφa, hφa', rfl⟩ := hc
|
||||
simp only [ι_timeOrder_superCommuteF_superCommuteF]
|
||||
simp only [ι_timeOrderF_superCommuteF_superCommuteF]
|
||||
| Or.inr (Or.inl hc) =>
|
||||
obtain ⟨φa, hφa, φb, hφb, rfl⟩ := hc
|
||||
by_cases heqt : (crAnTimeOrderRel φa φb ∧ crAnTimeOrderRel φb φa)
|
||||
· rw [ι_timeOrder_superCommuteF_eq_time]
|
||||
· rw [ι_timeOrderF_superCommuteF_eq_time]
|
||||
simp only [map_mul]
|
||||
rw [ι_superCommuteF_of_create_create]
|
||||
simp only [zero_mul]
|
||||
|
|
@ -326,11 +326,11 @@ lemma ι_timeOrder_zero_of_mem_ideal (a : 𝓕.CrAnAlgebra)
|
|||
· exact hφb
|
||||
· exact heqt.1
|
||||
· exact heqt.2
|
||||
· rw [ι_timeOrder_superCommuteF_neq_time heqt]
|
||||
· rw [ι_timeOrderF_superCommuteF_neq_time heqt]
|
||||
| Or.inr (Or.inr (Or.inl hc)) =>
|
||||
obtain ⟨φa, hφa, φb, hφb, rfl⟩ := hc
|
||||
by_cases heqt : (crAnTimeOrderRel φa φb ∧ crAnTimeOrderRel φb φa)
|
||||
· rw [ι_timeOrder_superCommuteF_eq_time]
|
||||
· rw [ι_timeOrderF_superCommuteF_eq_time]
|
||||
simp only [map_mul]
|
||||
rw [ι_superCommuteF_of_annihilate_annihilate]
|
||||
simp only [zero_mul]
|
||||
|
|
@ -338,18 +338,18 @@ lemma ι_timeOrder_zero_of_mem_ideal (a : 𝓕.CrAnAlgebra)
|
|||
· exact hφb
|
||||
· exact heqt.1
|
||||
· exact heqt.2
|
||||
· rw [ι_timeOrder_superCommuteF_neq_time heqt]
|
||||
· rw [ι_timeOrderF_superCommuteF_neq_time heqt]
|
||||
| Or.inr (Or.inr (Or.inr hc)) =>
|
||||
obtain ⟨φa, φb, hdiff, rfl⟩ := hc
|
||||
by_cases heqt : (crAnTimeOrderRel φa φb ∧ crAnTimeOrderRel φb φa)
|
||||
· rw [ι_timeOrder_superCommuteF_eq_time]
|
||||
· rw [ι_timeOrderF_superCommuteF_eq_time]
|
||||
simp only [map_mul]
|
||||
rw [ι_superCommuteF_of_diff_statistic]
|
||||
simp only [zero_mul]
|
||||
· exact hdiff
|
||||
· exact heqt.1
|
||||
· exact heqt.2
|
||||
· rw [ι_timeOrder_superCommuteF_neq_time heqt]
|
||||
· rw [ι_timeOrderF_superCommuteF_neq_time heqt]
|
||||
· simp [p]
|
||||
· intro x y hx hy
|
||||
simp only [map_add, p]
|
||||
|
|
@ -358,16 +358,16 @@ lemma ι_timeOrder_zero_of_mem_ideal (a : 𝓕.CrAnAlgebra)
|
|||
· intro x hx
|
||||
simp [p]
|
||||
|
||||
lemma ι_timeOrder_eq_of_equiv (a b : 𝓕.CrAnAlgebra) (h : a ≈ b) :
|
||||
lemma ι_timeOrderF_eq_of_equiv (a b : 𝓕.CrAnAlgebra) (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 ι_timeOrder_zero_of_mem_ideal (a - b) h
|
||||
exact ι_timeOrderF_zero_of_mem_ideal (a - b) h
|
||||
|
||||
/-- Time ordering on `FieldOpAlgebra`. -/
|
||||
noncomputable def timeOrder : FieldOpAlgebra 𝓕 →ₗ[ℂ] FieldOpAlgebra 𝓕 where
|
||||
toFun := Quotient.lift (ι.toLinearMap ∘ₗ CrAnAlgebra.timeOrder) ι_timeOrder_eq_of_equiv
|
||||
toFun := Quotient.lift (ι.toLinearMap ∘ₗ timeOrderF) ι_timeOrderF_eq_of_equiv
|
||||
map_add' x y := by
|
||||
obtain ⟨x, hx⟩ := ι_surjective x
|
||||
obtain ⟨y, hy⟩ := ι_surjective y
|
||||
|
|
|
|||
|
|
@ -40,7 +40,7 @@ lemma timeContract_of_timeOrderRel (φ ψ : 𝓕.States) (h : timeOrderRel φ ψ
|
|||
rw [ofState_eq_crPart_add_anPart]
|
||||
rw [map_add, map_add, crAnF_superCommuteF_anPart_anPart, superCommuteF_anPart_crPart]
|
||||
simp only [timeContract, instCommGroup.eq_1, Algebra.smul_mul_assoc, add_zero]
|
||||
rw [timeOrder_ofState_ofState_ordered h]
|
||||
rw [timeOrderF_ofState_ofState_ordered h]
|
||||
rw [normalOrderF_ofState_mul_ofState]
|
||||
simp only [instCommGroup.eq_1]
|
||||
rw [ofState_eq_crPart_add_anPart, ofState_eq_crPart_add_anPart]
|
||||
|
|
@ -53,7 +53,7 @@ lemma timeContract_of_not_timeOrderRel (φ ψ : 𝓕.States) (h : ¬ timeOrderRe
|
|||
simp only [Int.reduceNeg, one_smul, map_add]
|
||||
rw [map_smul]
|
||||
rw [crAnF_normalOrderF_ofState_ofState_swap]
|
||||
rw [timeOrder_ofState_ofState_not_ordered_eq_timeOrder h]
|
||||
rw [timeOrderF_ofState_ofState_not_ordered_eq_timeOrderF h]
|
||||
rw [timeContract_eq_smul]
|
||||
simp only [instCommGroup.eq_1, map_smul, map_add, smul_add]
|
||||
rw [smul_smul, smul_smul, mul_comm]
|
||||
|
|
|
|||
|
|
@ -319,7 +319,7 @@ lemma wick_term_cons_eq_sum_wick_term (φ : 𝓕.States) (φs : List 𝓕.States
|
|||
lemma wicks_theorem_nil :
|
||||
𝓞.crAnF (𝓣ᶠ(ofStateList [])) = ∑ (nilΛ : WickContraction [].length),
|
||||
(nilΛ.sign • nilΛ.timeContract 𝓞) * 𝓞.crAnF 𝓝ᶠ([nilΛ]ᵘᶜ) := by
|
||||
rw [timeOrder_ofStateList_nil]
|
||||
rw [timeOrderF_ofStateList_nil]
|
||||
simp only [map_one, List.length_nil, Algebra.smul_mul_assoc]
|
||||
rw [sum_WickContraction_nil, uncontractedListGet, nil_zero_uncontractedList]
|
||||
simp only [List.map_nil]
|
||||
|
|
@ -356,7 +356,7 @@ theorem wicks_theorem : (φs : List 𝓕.States) → 𝓞.crAnF (𝓣ᶠ(ofState
|
|||
| [] => wicks_theorem_nil
|
||||
| φ :: φs => by
|
||||
have ih := wicks_theorem (eraseMaxTimeField φ φs)
|
||||
rw [timeOrder_eq_maxTimeField_mul_finset, map_mul, ih, Finset.mul_sum]
|
||||
rw [timeOrderF_eq_maxTimeField_mul_finset, map_mul, ih, Finset.mul_sum]
|
||||
have h1 : φ :: φs =
|
||||
(eraseMaxTimeField φ φs).insertIdx (maxTimeFieldPosFin φ φs) (maxTimeField φ φs) := by
|
||||
simp only [eraseMaxTimeField, insertionSortDropMinPos, List.length_cons, Nat.succ_eq_add_one,
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue