From 2d561dd89dd003d7ec1637c7454e9a2fe9ae05e4 Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Thu, 6 Feb 2025 10:09:30 +0000 Subject: [PATCH] refactor: Rename ofCrAnFieldOp to ofCrAnOp --- .../FieldOpAlgebra/Basic.lean | 44 ++--- .../FieldOpAlgebra/Grading.lean | 26 +-- .../FieldOpAlgebra/NormalOrder/Lemmas.lean | 68 ++++---- .../FieldOpAlgebra/SuperCommute.lean | 162 +++++++++--------- .../FieldOpAlgebra/TimeOrder.lean | 16 +- .../FieldOpAlgebra/WicksTheoremNormal.lean | 6 +- scripts/MetaPrograms/notes.lean | 8 +- 7 files changed, 165 insertions(+), 165 deletions(-) diff --git a/HepLean/PerturbationTheory/FieldOpAlgebra/Basic.lean b/HepLean/PerturbationTheory/FieldOpAlgebra/Basic.lean index cb5208a..98cfbb0 100644 --- a/HepLean/PerturbationTheory/FieldOpAlgebra/Basic.lean +++ b/HepLean/PerturbationTheory/FieldOpAlgebra/Basic.lean @@ -473,35 +473,35 @@ lemma ofFieldOpList_singleton (Ο† : 𝓕.FieldOp) : simp only [ofFieldOpList, ofFieldOp, ofFieldOpListF_singleton] /-- An element of `FieldOpAlgebra` from a `CrAnFieldOp`. -/ -def ofCrAnFieldOp (Ο† : 𝓕.CrAnFieldOp) : 𝓕.FieldOpAlgebra := ΞΉ (ofCrAnOpF Ο†) +def ofCrAnOp (Ο† : 𝓕.CrAnFieldOp) : 𝓕.FieldOpAlgebra := ΞΉ (ofCrAnOpF Ο†) -lemma ofCrAnFieldOp_eq_ΞΉ_ofCrAnOpF (Ο† : 𝓕.CrAnFieldOp) : - ofCrAnFieldOp Ο† = ΞΉ (ofCrAnOpF Ο†) := rfl +lemma ofCrAnOp_eq_ΞΉ_ofCrAnOpF (Ο† : 𝓕.CrAnFieldOp) : + ofCrAnOp Ο† = ΞΉ (ofCrAnOpF Ο†) := rfl lemma ofFieldOp_eq_sum (Ο† : 𝓕.FieldOp) : - ofFieldOp Ο† = (βˆ‘ i : 𝓕.fieldOpToCrAnType Ο†, ofCrAnFieldOp βŸ¨Ο†, i⟩) := by + ofFieldOp Ο† = (βˆ‘ i : 𝓕.fieldOpToCrAnType Ο†, ofCrAnOp βŸ¨Ο†, i⟩) := by rw [ofFieldOp, ofFieldOpF] simp only [map_sum] rfl /-- An element of `FieldOpAlgebra` from a list of `CrAnFieldOp`. -/ -def ofCrAnFieldOpList (Ο†s : List 𝓕.CrAnFieldOp) : 𝓕.FieldOpAlgebra := ΞΉ (ofCrAnListF Ο†s) +def ofCrAnOpList (Ο†s : List 𝓕.CrAnFieldOp) : 𝓕.FieldOpAlgebra := ΞΉ (ofCrAnListF Ο†s) -lemma ofCrAnFieldOpList_eq_ΞΉ_ofCrAnListF (Ο†s : List 𝓕.CrAnFieldOp) : - ofCrAnFieldOpList Ο†s = ΞΉ (ofCrAnListF Ο†s) := rfl +lemma ofCrAnOpList_eq_ΞΉ_ofCrAnListF (Ο†s : List 𝓕.CrAnFieldOp) : + ofCrAnOpList Ο†s = ΞΉ (ofCrAnListF Ο†s) := rfl -lemma ofCrAnFieldOpList_append (Ο†s ψs : List 𝓕.CrAnFieldOp) : - ofCrAnFieldOpList (Ο†s ++ ψs) = ofCrAnFieldOpList Ο†s * ofCrAnFieldOpList ψs := by - simp only [ofCrAnFieldOpList] +lemma ofCrAnOpList_append (Ο†s ψs : List 𝓕.CrAnFieldOp) : + ofCrAnOpList (Ο†s ++ ψs) = ofCrAnOpList Ο†s * ofCrAnOpList ψs := by + simp only [ofCrAnOpList] rw [ofCrAnListF_append] simp -lemma ofCrAnFieldOpList_singleton (Ο† : 𝓕.CrAnFieldOp) : - ofCrAnFieldOpList [Ο†] = ofCrAnFieldOp Ο† := by - simp only [ofCrAnFieldOpList, ofCrAnFieldOp, ofCrAnListF_singleton] +lemma ofCrAnOpList_singleton (Ο† : 𝓕.CrAnFieldOp) : + ofCrAnOpList [Ο†] = ofCrAnOp Ο† := by + simp only [ofCrAnOpList, ofCrAnOp, ofCrAnListF_singleton] lemma ofFieldOpList_eq_sum (Ο†s : List 𝓕.FieldOp) : - ofFieldOpList Ο†s = βˆ‘ s : CrAnSection Ο†s, ofCrAnFieldOpList s.1 := by + ofFieldOpList Ο†s = βˆ‘ s : CrAnSection Ο†s, ofCrAnOpList s.1 := by rw [ofFieldOpList, ofFieldOpListF_sum] simp only [map_sum] rfl @@ -519,13 +519,13 @@ lemma anPart_negAsymp (Ο† : (Ξ£ f, 𝓕.AsymptoticLabel f) Γ— (Fin 3 β†’ ℝ)) : @[simp] lemma anPart_position (Ο† : (Ξ£ f, 𝓕.PositionLabel f) Γ— SpaceTime) : anPart (FieldOp.position Ο†) = - ofCrAnFieldOp ⟨FieldOp.position Ο†, CreateAnnihilate.annihilate⟩ := by - simp [anPart, ofCrAnFieldOp] + ofCrAnOp ⟨FieldOp.position Ο†, CreateAnnihilate.annihilate⟩ := by + simp [anPart, ofCrAnOp] @[simp] lemma anPart_posAsymp (Ο† : (Ξ£ f, 𝓕.AsymptoticLabel f) Γ— (Fin 3 β†’ ℝ)) : - anPart (FieldOp.outAsymp Ο†) = ofCrAnFieldOp ⟨FieldOp.outAsymp Ο†, ()⟩ := by - simp [anPart, ofCrAnFieldOp] + anPart (FieldOp.outAsymp Ο†) = ofCrAnOp ⟨FieldOp.outAsymp Ο†, ()⟩ := by + simp [anPart, ofCrAnOp] /-- The creation part of a state. -/ def crPart (Ο† : 𝓕.FieldOp) : 𝓕.FieldOpAlgebra := ΞΉ (crPartF Ο†) @@ -534,14 +534,14 @@ lemma crPart_eq_ΞΉ_crPartF (Ο† : 𝓕.FieldOp) : crPart Ο† = ΞΉ (crPartF Ο†) := @[simp] lemma crPart_negAsymp (Ο† : (Ξ£ f, 𝓕.AsymptoticLabel f) Γ— (Fin 3 β†’ ℝ)) : - crPart (FieldOp.inAsymp Ο†) = ofCrAnFieldOp ⟨FieldOp.inAsymp Ο†, ()⟩ := by - simp [crPart, ofCrAnFieldOp] + crPart (FieldOp.inAsymp Ο†) = ofCrAnOp ⟨FieldOp.inAsymp Ο†, ()⟩ := by + simp [crPart, ofCrAnOp] @[simp] lemma crPart_position (Ο† : (Ξ£ f, 𝓕.PositionLabel f) Γ— SpaceTime) : crPart (FieldOp.position Ο†) = - ofCrAnFieldOp ⟨FieldOp.position Ο†, CreateAnnihilate.create⟩ := by - simp [crPart, ofCrAnFieldOp] + ofCrAnOp ⟨FieldOp.position Ο†, CreateAnnihilate.create⟩ := by + simp [crPart, ofCrAnOp] @[simp] lemma crPart_posAsymp (Ο† : (Ξ£ f, 𝓕.AsymptoticLabel f) Γ— (Fin 3 β†’ ℝ)) : diff --git a/HepLean/PerturbationTheory/FieldOpAlgebra/Grading.lean b/HepLean/PerturbationTheory/FieldOpAlgebra/Grading.lean index eb3a19b..6082303 100644 --- a/HepLean/PerturbationTheory/FieldOpAlgebra/Grading.lean +++ b/HepLean/PerturbationTheory/FieldOpAlgebra/Grading.lean @@ -20,14 +20,14 @@ variable {𝓕 : FieldSpecification} /-- The submodule of `𝓕.FieldOpAlgebra` spanned by lists of field statistic `f`. -/ def statSubmodule (f : FieldStatistic) : Submodule β„‚ 𝓕.FieldOpAlgebra := - Submodule.span β„‚ {a | βˆƒ Ο†s, a = ofCrAnFieldOpList Ο†s ∧ (𝓕 |>β‚› Ο†s) = f} + Submodule.span β„‚ {a | βˆƒ Ο†s, a = ofCrAnOpList Ο†s ∧ (𝓕 |>β‚› Ο†s) = f} -lemma ofCrAnFieldOpList_mem_statSubmodule_of_eq (Ο†s : List 𝓕.CrAnFieldOp) (f : FieldStatistic) - (h : (𝓕 |>β‚› Ο†s) = f) : ofCrAnFieldOpList Ο†s ∈ statSubmodule f := +lemma ofCrAnOpList_mem_statSubmodule_of_eq (Ο†s : List 𝓕.CrAnFieldOp) (f : FieldStatistic) + (h : (𝓕 |>β‚› Ο†s) = f) : ofCrAnOpList Ο†s ∈ statSubmodule f := Submodule.mem_span.mpr fun _ a => a βŸ¨Ο†s, ⟨rfl, h⟩⟩ -lemma ofCrAnFieldOpList_mem_statSubmodule (Ο†s : List 𝓕.CrAnFieldOp) : - ofCrAnFieldOpList Ο†s ∈ statSubmodule (𝓕 |>β‚› Ο†s) := +lemma ofCrAnOpList_mem_statSubmodule (Ο†s : List 𝓕.CrAnFieldOp) : + ofCrAnOpList Ο†s ∈ statSubmodule (𝓕 |>β‚› Ο†s) := Submodule.mem_span.mpr fun _ a => a βŸ¨Ο†s, ⟨rfl, rfl⟩⟩ lemma mem_bosonic_of_mem_free_bosonic (a : 𝓕.FieldOpFreeAlgebra) @@ -40,7 +40,7 @@ lemma mem_bosonic_of_mem_free_bosonic (a : 𝓕.FieldOpFreeAlgebra) simp only [Set.mem_setOf_eq] at hx obtain βŸ¨Ο†s, rfl, h⟩ := hx simp [p] - apply ofCrAnFieldOpList_mem_statSubmodule_of_eq + apply ofCrAnOpList_mem_statSubmodule_of_eq exact h Β· simp only [map_zero, p] exact Submodule.zero_mem (statSubmodule bosonic) @@ -61,7 +61,7 @@ lemma mem_fermionic_of_mem_free_fermionic (a : 𝓕.FieldOpFreeAlgebra) simp only [Set.mem_setOf_eq] at hx obtain βŸ¨Ο†s, rfl, h⟩ := hx simp [p] - apply ofCrAnFieldOpList_mem_statSubmodule_of_eq + apply ofCrAnOpList_mem_statSubmodule_of_eq exact h Β· simp only [map_zero, p] exact Submodule.zero_mem (statSubmodule fermionic) @@ -204,7 +204,7 @@ lemma bosonicProj_mem_bosonic (a : 𝓕.FieldOpAlgebra) (ha : a ∈ statSubmodul simp only [p] apply Subtype.eq simp only - rw [ofCrAnFieldOpList] + rw [ofCrAnOpList] rw [bosonicProj_eq_bosonicProjFree] rw [bosonicProjFree_eq_ΞΉ_bosonicProjF] rw [bosonicProjF_of_mem_bosonic] @@ -227,7 +227,7 @@ lemma fermionicProj_mem_fermionic (a : 𝓕.FieldOpAlgebra) (ha : a ∈ statSubm simp only [p] apply Subtype.eq simp only - rw [ofCrAnFieldOpList] + rw [ofCrAnOpList] rw [fermionicProj_eq_fermionicProjFree] rw [fermionicProjFree_eq_ΞΉ_fermionicProjF] rw [fermionicProjF_of_mem_fermionic] @@ -384,7 +384,7 @@ lemma directSum_eq_bosonic_plus_fermionic abel /-- For a field statistic `𝓕`, the algebra `𝓕.FieldOpAlgebra` is graded by `FieldStatistic`. - Those `ofCrAnFieldOpList Ο†s` for which `Ο†s` has `bosonic` statistics span one part of the grading, + Those `ofCrAnOpList Ο†s` for which `Ο†s` has `bosonic` statistics span one part of the grading, whilst those where `Ο†s` has `fermionic` statistics span the other part of the grading. -/ instance fieldOpAlgebraGrade : GradedAlgebra (A := 𝓕.FieldOpAlgebra) statSubmodule where one_mem := by @@ -392,7 +392,7 @@ instance fieldOpAlgebraGrade : GradedAlgebra (A := 𝓕.FieldOpAlgebra) statSubm refine Submodule.mem_span.mpr fun p a => a ?_ simp only [Set.mem_setOf_eq] use [] - simp only [ofCrAnFieldOpList, ofCrAnListF_nil, map_one, ofList_empty, true_and] + simp only [ofCrAnOpList, ofCrAnListF_nil, map_one, ofList_empty, true_and] rfl mul_mem f1 f2 a1 a2 h1 h2 := by let p (a2 : 𝓕.FieldOpAlgebra) (hx : a2 ∈ statSubmodule f2) : Prop := @@ -404,13 +404,13 @@ instance fieldOpAlgebraGrade : GradedAlgebra (A := 𝓕.FieldOpAlgebra) statSubm obtain βŸ¨Ο†s, rfl, h⟩ := hx simp only [p] let p (a1 : 𝓕.FieldOpAlgebra) (hx : a1 ∈ statSubmodule f1) : Prop := - a1 * ofCrAnFieldOpList Ο†s ∈ statSubmodule (f1 + f2) + a1 * ofCrAnOpList Ο†s ∈ statSubmodule (f1 + f2) change p a1 h1 apply Submodule.span_induction (p := p) Β· intro y hy obtain βŸ¨Ο†s', rfl, h'⟩ := hy simp only [p] - rw [← ofCrAnFieldOpList_append] + rw [← ofCrAnOpList_append] refine Submodule.mem_span.mpr fun p a => a ?_ simp only [Set.mem_setOf_eq] use Ο†s' ++ Ο†s diff --git a/HepLean/PerturbationTheory/FieldOpAlgebra/NormalOrder/Lemmas.lean b/HepLean/PerturbationTheory/FieldOpAlgebra/NormalOrder/Lemmas.lean index 0f8f466..ddf02a6 100644 --- a/HepLean/PerturbationTheory/FieldOpAlgebra/NormalOrder/Lemmas.lean +++ b/HepLean/PerturbationTheory/FieldOpAlgebra/NormalOrder/Lemmas.lean @@ -27,16 +27,16 @@ variable {𝓕 : FieldSpecification} lemma normalOrder_eq_ΞΉ_normalOrderF (a : 𝓕.FieldOpFreeAlgebra) : 𝓝(ΞΉ a) = ΞΉ 𝓝ᢠ(a) := rfl -lemma normalOrder_ofCrAnFieldOpList (Ο†s : List 𝓕.CrAnFieldOp) : - 𝓝(ofCrAnFieldOpList Ο†s) = normalOrderSign Ο†s β€’ ofCrAnFieldOpList (normalOrderList Ο†s) := by - rw [ofCrAnFieldOpList, normalOrder_eq_ΞΉ_normalOrderF, normalOrderF_ofCrAnListF] +lemma normalOrder_ofCrAnOpList (Ο†s : List 𝓕.CrAnFieldOp) : + 𝓝(ofCrAnOpList Ο†s) = normalOrderSign Ο†s β€’ ofCrAnOpList (normalOrderList Ο†s) := by + rw [ofCrAnOpList, normalOrder_eq_ΞΉ_normalOrderF, normalOrderF_ofCrAnListF] rfl @[simp] lemma normalOrder_one_eq_one : normalOrder (𝓕 := 𝓕) 1 = 1 := by - have h1 : 1 = ofCrAnFieldOpList (𝓕 := 𝓕) [] := by simp [ofCrAnFieldOpList] + have h1 : 1 = ofCrAnOpList (𝓕 := 𝓕) [] := by simp [ofCrAnOpList] rw [h1] - rw [normalOrder_ofCrAnFieldOpList] + rw [normalOrder_ofCrAnOpList] simp @[simp] @@ -48,14 +48,14 @@ lemma normalOrder_ofFieldOpList_nil : normalOrder (𝓕 := 𝓕) (ofFieldOpList simp @[simp] -lemma normalOrder_ofCrAnFieldOpList_nil : normalOrder (𝓕 := 𝓕) (ofCrAnFieldOpList []) = 1 := by - rw [normalOrder_ofCrAnFieldOpList] +lemma normalOrder_ofCrAnOpList_nil : normalOrder (𝓕 := 𝓕) (ofCrAnOpList []) = 1 := by + rw [normalOrder_ofCrAnOpList] simp only [normalOrderSign_nil, normalOrderList_nil, one_smul] rfl -lemma ofCrAnFieldOpList_eq_normalOrder (Ο†s : List 𝓕.CrAnFieldOp) : - ofCrAnFieldOpList (normalOrderList Ο†s) = normalOrderSign Ο†s β€’ 𝓝(ofCrAnFieldOpList Ο†s) := by - rw [normalOrder_ofCrAnFieldOpList, smul_smul, normalOrderSign, Wick.koszulSign_mul_self, +lemma ofCrAnOpList_eq_normalOrder (Ο†s : List 𝓕.CrAnFieldOp) : + ofCrAnOpList (normalOrderList Ο†s) = normalOrderSign Ο†s β€’ 𝓝(ofCrAnOpList Ο†s) := by + rw [normalOrder_ofCrAnOpList, smul_smul, normalOrderSign, Wick.koszulSign_mul_self, one_smul] lemma normalOrder_normalOrder_mid (a b c : 𝓕.FieldOpAlgebra) : @@ -165,16 +165,16 @@ lemma normalOrder_ofFieldOp_ofFieldOp_swap (Ο† Ο†' : 𝓕.FieldOp) : rw [ofFieldOp_mul_ofFieldOp_eq_superCommute] simp -lemma normalOrder_ofCrAnFieldOp_ofCrAnFieldOpList (Ο† : 𝓕.CrAnFieldOp) - (Ο†s : List 𝓕.CrAnFieldOp) : 𝓝(ofCrAnFieldOp Ο† * ofCrAnFieldOpList Ο†s) = - 𝓒(𝓕 |>β‚› Ο†, 𝓕 |>β‚› Ο†s) β€’ 𝓝(ofCrAnFieldOpList Ο†s * ofCrAnFieldOp Ο†) := by - rw [← ofCrAnFieldOpList_singleton, ofCrAnFieldOpList_mul_ofCrAnFieldOpList_eq_superCommute] +lemma normalOrder_ofCrAnOp_ofCrAnOpList (Ο† : 𝓕.CrAnFieldOp) + (Ο†s : List 𝓕.CrAnFieldOp) : 𝓝(ofCrAnOp Ο† * ofCrAnOpList Ο†s) = + 𝓒(𝓕 |>β‚› Ο†, 𝓕 |>β‚› Ο†s) β€’ 𝓝(ofCrAnOpList Ο†s * ofCrAnOp Ο†) := by + rw [← ofCrAnOpList_singleton, ofCrAnOpList_mul_ofCrAnOpList_eq_superCommute] simp -lemma normalOrder_ofCrAnFieldOp_ofFieldOpList_swap (Ο† : 𝓕.CrAnFieldOp) (Ο†' : List 𝓕.FieldOp) : - 𝓝(ofCrAnFieldOp Ο† * ofFieldOpList Ο†') = 𝓒(𝓕 |>β‚› Ο†, 𝓕 |>β‚› Ο†') β€’ - 𝓝(ofFieldOpList Ο†' * ofCrAnFieldOp Ο†) := by - rw [← ofCrAnFieldOpList_singleton, ofCrAnFieldOpList_mul_ofFieldOpList_eq_superCommute] +lemma normalOrder_ofCrAnOp_ofFieldOpList_swap (Ο† : 𝓕.CrAnFieldOp) (Ο†' : List 𝓕.FieldOp) : + 𝓝(ofCrAnOp Ο† * ofFieldOpList Ο†') = 𝓒(𝓕 |>β‚› Ο†, 𝓕 |>β‚› Ο†') β€’ + 𝓝(ofFieldOpList Ο†' * ofCrAnOp Ο†) := by + rw [← ofCrAnOpList_singleton, ofCrAnOpList_mul_ofFieldOpList_eq_superCommute] simp lemma normalOrder_anPart_ofFieldOpList_swap (Ο† : 𝓕.FieldOp) (Ο†' : List 𝓕.FieldOp) : @@ -184,11 +184,11 @@ lemma normalOrder_anPart_ofFieldOpList_swap (Ο† : 𝓕.FieldOp) (Ο†' : List 𝓕 simp | .position Ο† => simp only [anPart_position, instCommGroup.eq_1] - rw [normalOrder_ofCrAnFieldOp_ofFieldOpList_swap] + rw [normalOrder_ofCrAnOp_ofFieldOpList_swap] rfl | .outAsymp Ο† => simp only [anPart_posAsymp, instCommGroup.eq_1] - rw [normalOrder_ofCrAnFieldOp_ofFieldOpList_swap] + rw [normalOrder_ofCrAnOp_ofFieldOpList_swap] rfl lemma normalOrder_ofFieldOpList_anPart_swap (Ο† : 𝓕.FieldOp) (Ο†' : List 𝓕.FieldOp) : @@ -224,18 +224,18 @@ The proof of this result ultimetly depends on - `superCommuteF_ofCrAnListF_ofFieldOpListF_eq_sum` - `normalOrderSign_eraseIdx` -/ -lemma ofCrAnFieldOp_superCommute_normalOrder_ofCrAnFieldOpList_sum (Ο† : 𝓕.CrAnFieldOp) - (Ο†s : List 𝓕.CrAnFieldOp) : [ofCrAnFieldOp Ο†, 𝓝(ofCrAnFieldOpList Ο†s)]β‚› = βˆ‘ n : Fin Ο†s.length, - 𝓒(𝓕 |>β‚› Ο†, 𝓕 |>β‚› (Ο†s.take n)) β€’ [ofCrAnFieldOp Ο†, ofCrAnFieldOp Ο†s[n]]β‚› - * 𝓝(ofCrAnFieldOpList (Ο†s.eraseIdx n)) := by - rw [normalOrder_ofCrAnFieldOpList, map_smul] - rw [superCommute_ofCrAnFieldOp_ofCrAnFieldOpList_eq_sum, Finset.smul_sum, +lemma ofCrAnOp_superCommute_normalOrder_ofCrAnOpList_sum (Ο† : 𝓕.CrAnFieldOp) + (Ο†s : List 𝓕.CrAnFieldOp) : [ofCrAnOp Ο†, 𝓝(ofCrAnOpList Ο†s)]β‚› = βˆ‘ n : Fin Ο†s.length, + 𝓒(𝓕 |>β‚› Ο†, 𝓕 |>β‚› (Ο†s.take n)) β€’ [ofCrAnOp Ο†, ofCrAnOp Ο†s[n]]β‚› + * 𝓝(ofCrAnOpList (Ο†s.eraseIdx n)) := by + rw [normalOrder_ofCrAnOpList, map_smul] + rw [superCommute_ofCrAnOp_ofCrAnOpList_eq_sum, Finset.smul_sum, sum_normalOrderList_length] congr funext n simp only [instCommGroup.eq_1, List.get_eq_getElem, normalOrderList_get_normalOrderEquiv, normalOrderList_eraseIdx_normalOrderEquiv, Algebra.smul_mul_assoc, Fin.getElem_fin] - rw [ofCrAnFieldOpList_eq_normalOrder, mul_smul_comm, smul_smul, smul_smul] + rw [ofCrAnOpList_eq_normalOrder, mul_smul_comm, smul_smul, smul_smul] by_cases hs : (𝓕 |>β‚› Ο†) = (𝓕 |>β‚› Ο†s[n]) Β· congr erw [normalOrderSign_eraseIdx, ← hs] @@ -250,14 +250,14 @@ lemma ofCrAnFieldOp_superCommute_normalOrder_ofCrAnFieldOpList_sum (Ο† : 𝓕.Cr Β· erw [superCommute_diff_statistic hs] simp -lemma ofCrAnFieldOp_superCommute_normalOrder_ofFieldOpList_sum (Ο† : 𝓕.CrAnFieldOp) +lemma ofCrAnOp_superCommute_normalOrder_ofFieldOpList_sum (Ο† : 𝓕.CrAnFieldOp) (Ο†s : List 𝓕.FieldOp) : - [ofCrAnFieldOp Ο†, 𝓝(ofFieldOpList Ο†s)]β‚› = βˆ‘ n : Fin Ο†s.length, 𝓒(𝓕 |>β‚› Ο†, 𝓕 |>β‚› (Ο†s.take n)) β€’ - [ofCrAnFieldOp Ο†, ofFieldOp Ο†s[n]]β‚› * 𝓝(ofFieldOpList (Ο†s.eraseIdx n)) := by + [ofCrAnOp Ο†, 𝓝(ofFieldOpList Ο†s)]β‚› = βˆ‘ n : Fin Ο†s.length, 𝓒(𝓕 |>β‚› Ο†, 𝓕 |>β‚› (Ο†s.take n)) β€’ + [ofCrAnOp Ο†, ofFieldOp Ο†s[n]]β‚› * 𝓝(ofFieldOpList (Ο†s.eraseIdx n)) := by conv_lhs => rw [ofFieldOpList_eq_sum, map_sum, map_sum] enter [2, s] - rw [ofCrAnFieldOp_superCommute_normalOrder_ofCrAnFieldOpList_sum, CrAnSection.sum_over_length] + rw [ofCrAnOp_superCommute_normalOrder_ofCrAnOpList_sum, CrAnSection.sum_over_length] enter [2, n] rw [CrAnSection.take_statistics_eq_take_state_statistics, smul_mul_assoc] rw [Finset.sum_comm] @@ -285,13 +285,13 @@ lemma anPart_superCommute_normalOrder_ofFieldOpList_sum (Ο† : 𝓕.FieldOp) (Ο†s simp | .position Ο† => simp only [anPart_position, instCommGroup.eq_1, Fin.getElem_fin, Algebra.smul_mul_assoc] - rw [ofCrAnFieldOp_superCommute_normalOrder_ofFieldOpList_sum] + rw [ofCrAnOp_superCommute_normalOrder_ofFieldOpList_sum] simp only [instCommGroup.eq_1, crAnStatistics, Function.comp_apply, crAnFieldOpToFieldOp_prod, Fin.getElem_fin, Algebra.smul_mul_assoc] rfl | .outAsymp Ο† => simp only [anPart_posAsymp, instCommGroup.eq_1, Fin.getElem_fin, Algebra.smul_mul_assoc] - rw [ofCrAnFieldOp_superCommute_normalOrder_ofFieldOpList_sum] + rw [ofCrAnOp_superCommute_normalOrder_ofFieldOpList_sum] simp only [instCommGroup.eq_1, crAnStatistics, Function.comp_apply, crAnFieldOpToFieldOp_prod, Fin.getElem_fin, Algebra.smul_mul_assoc] rfl @@ -339,7 +339,7 @@ For a field specification `𝓕`, the following relation holds in the algebra ` `Ο† * 𝓝(φ₀φ₁…φₙ) = 𝓝(φφ₀φ₁…φₙ) + βˆ‘ i, (𝓒(Ο†,φ₀φ₁…φᡒ₋₁) β€’ [anPartF Ο†, Ο†α΅’]β‚›) * 𝓝(Ο†β‚€Ο†β‚β€¦Ο†α΅’β‚‹β‚Ο†α΅’β‚Šβ‚β€¦Ο†β‚™)`. The proof of this ultimently depends on : -- `ofCrAnFieldOp_superCommute_normalOrder_ofCrAnFieldOpList_sum` +- `ofCrAnOp_superCommute_normalOrder_ofCrAnOpList_sum` -/ lemma ofFieldOp_mul_normalOrder_ofFieldOpList_eq_sum (Ο† : 𝓕.FieldOp) (Ο†s : List 𝓕.FieldOp) : ofFieldOp Ο† * 𝓝(ofFieldOpList Ο†s) = diff --git a/HepLean/PerturbationTheory/FieldOpAlgebra/SuperCommute.lean b/HepLean/PerturbationTheory/FieldOpAlgebra/SuperCommute.lean index ed1c418..0a5f56d 100644 --- a/HepLean/PerturbationTheory/FieldOpAlgebra/SuperCommute.lean +++ b/HepLean/PerturbationTheory/FieldOpAlgebra/SuperCommute.lean @@ -131,23 +131,23 @@ lemma superCommute_eq_ΞΉ_superCommuteF (a b : 𝓕.FieldOpFreeAlgebra) : lemma superCommute_create_create {Ο† Ο†' : 𝓕.CrAnFieldOp} (h : 𝓕 |>ᢜ Ο† = .create) (h' : 𝓕 |>ᢜ Ο†' = .create) : - [ofCrAnFieldOp Ο†, ofCrAnFieldOp Ο†']β‚› = 0 := by - rw [ofCrAnFieldOp, ofCrAnFieldOp] + [ofCrAnOp Ο†, ofCrAnOp Ο†']β‚› = 0 := by + rw [ofCrAnOp, ofCrAnOp] rw [superCommute_eq_ΞΉ_superCommuteF, ΞΉ_superCommuteF_of_create_create _ _ h h'] lemma superCommute_annihilate_annihilate {Ο† Ο†' : 𝓕.CrAnFieldOp} (h : 𝓕 |>ᢜ Ο† = .annihilate) (h' : 𝓕 |>ᢜ Ο†' = .annihilate) : - [ofCrAnFieldOp Ο†, ofCrAnFieldOp Ο†']β‚› = 0 := by - rw [ofCrAnFieldOp, ofCrAnFieldOp] + [ofCrAnOp Ο†, ofCrAnOp Ο†']β‚› = 0 := by + rw [ofCrAnOp, ofCrAnOp] rw [superCommute_eq_ΞΉ_superCommuteF, ΞΉ_superCommuteF_of_annihilate_annihilate _ _ h h'] lemma superCommute_diff_statistic {Ο† Ο†' : 𝓕.CrAnFieldOp} (h : (𝓕 |>β‚› Ο†) β‰  𝓕 |>β‚› Ο†') : - [ofCrAnFieldOp Ο†, ofCrAnFieldOp Ο†']β‚› = 0 := by - rw [ofCrAnFieldOp, ofCrAnFieldOp] + [ofCrAnOp Ο†, ofCrAnOp Ο†']β‚› = 0 := by + rw [ofCrAnOp, ofCrAnOp] rw [superCommute_eq_ΞΉ_superCommuteF, ΞΉ_superCommuteF_of_diff_statistic h] -lemma superCommute_ofCrAnFieldOp_ofFieldOp_diff_stat_zero (Ο† : 𝓕.CrAnFieldOp) (ψ : 𝓕.FieldOp) - (h : (𝓕 |>β‚› Ο†) β‰  (𝓕 |>β‚› ψ)) : [ofCrAnFieldOp Ο†, ofFieldOp ψ]β‚› = 0 := by +lemma superCommute_ofCrAnOp_ofFieldOp_diff_stat_zero (Ο† : 𝓕.CrAnFieldOp) (ψ : 𝓕.FieldOp) + (h : (𝓕 |>β‚› Ο†) β‰  (𝓕 |>β‚› ψ)) : [ofCrAnOp Ο†, ofFieldOp ψ]β‚› = 0 := by rw [ofFieldOp_eq_sum, map_sum] rw [Finset.sum_eq_zero] intro x hx @@ -161,37 +161,37 @@ lemma superCommute_anPart_ofFieldOpF_diff_grade_zero (Ο† ψ : 𝓕.FieldOp) simp | FieldOp.position Ο† => simp only [anPartF_position] - apply superCommute_ofCrAnFieldOp_ofFieldOp_diff_stat_zero _ _ _ + apply superCommute_ofCrAnOp_ofFieldOp_diff_stat_zero _ _ _ simpa [crAnStatistics] using h | FieldOp.outAsymp _ => simp only [anPartF_posAsymp] - apply superCommute_ofCrAnFieldOp_ofFieldOp_diff_stat_zero _ _ + apply superCommute_ofCrAnOp_ofFieldOp_diff_stat_zero _ _ simpa [crAnStatistics] using h -lemma superCommute_ofCrAnFieldOp_ofCrAnFieldOp_mem_center (Ο† Ο†' : 𝓕.CrAnFieldOp) : - [ofCrAnFieldOp Ο†, ofCrAnFieldOp Ο†']β‚› ∈ Subalgebra.center β„‚ (FieldOpAlgebra 𝓕) := by - rw [ofCrAnFieldOp, ofCrAnFieldOp, superCommute_eq_ΞΉ_superCommuteF] +lemma superCommute_ofCrAnOp_ofCrAnOp_mem_center (Ο† Ο†' : 𝓕.CrAnFieldOp) : + [ofCrAnOp Ο†, ofCrAnOp Ο†']β‚› ∈ Subalgebra.center β„‚ (FieldOpAlgebra 𝓕) := by + rw [ofCrAnOp, ofCrAnOp, superCommute_eq_ΞΉ_superCommuteF] exact ΞΉ_superCommuteF_ofCrAnOpF_ofCrAnOpF_mem_center Ο† Ο†' -lemma superCommute_ofCrAnFieldOp_ofCrAnFieldOp_commute (Ο† Ο†' : 𝓕.CrAnFieldOp) +lemma superCommute_ofCrAnOp_ofCrAnOp_commute (Ο† Ο†' : 𝓕.CrAnFieldOp) (a : FieldOpAlgebra 𝓕) : - a * [ofCrAnFieldOp Ο†, ofCrAnFieldOp Ο†']β‚› = [ofCrAnFieldOp Ο†, ofCrAnFieldOp Ο†']β‚› * a := by - have h1 := superCommute_ofCrAnFieldOp_ofCrAnFieldOp_mem_center Ο† Ο†' + a * [ofCrAnOp Ο†, ofCrAnOp Ο†']β‚› = [ofCrAnOp Ο†, ofCrAnOp Ο†']β‚› * a := by + have h1 := superCommute_ofCrAnOp_ofCrAnOp_mem_center Ο† Ο†' rw [@Subalgebra.mem_center_iff] at h1 exact h1 a -lemma superCommute_ofCrAnFieldOp_ofFieldOp_mem_center (Ο† : 𝓕.CrAnFieldOp) (Ο†' : 𝓕.FieldOp) : - [ofCrAnFieldOp Ο†, ofFieldOp Ο†']β‚› ∈ Subalgebra.center β„‚ (FieldOpAlgebra 𝓕) := by +lemma superCommute_ofCrAnOp_ofFieldOp_mem_center (Ο† : 𝓕.CrAnFieldOp) (Ο†' : 𝓕.FieldOp) : + [ofCrAnOp Ο†, ofFieldOp Ο†']β‚› ∈ Subalgebra.center β„‚ (FieldOpAlgebra 𝓕) := by rw [ofFieldOp_eq_sum] simp only [map_sum] refine Subalgebra.sum_mem (Subalgebra.center β„‚ 𝓕.FieldOpAlgebra) ?_ intro x hx - exact superCommute_ofCrAnFieldOp_ofCrAnFieldOp_mem_center Ο† βŸ¨Ο†', x⟩ + exact superCommute_ofCrAnOp_ofCrAnOp_mem_center Ο† βŸ¨Ο†', x⟩ -lemma superCommute_ofCrAnFieldOp_ofFieldOp_commute (Ο† : 𝓕.CrAnFieldOp) (Ο†' : 𝓕.FieldOp) - (a : FieldOpAlgebra 𝓕) : a * [ofCrAnFieldOp Ο†, ofFieldOp Ο†']β‚› = - [ofCrAnFieldOp Ο†, ofFieldOp Ο†']β‚› * a := by - have h1 := superCommute_ofCrAnFieldOp_ofFieldOp_mem_center Ο† Ο†' +lemma superCommute_ofCrAnOp_ofFieldOp_commute (Ο† : 𝓕.CrAnFieldOp) (Ο†' : 𝓕.FieldOp) + (a : FieldOpAlgebra 𝓕) : a * [ofCrAnOp Ο†, ofFieldOp Ο†']β‚› = + [ofCrAnOp Ο†, ofFieldOp Ο†']β‚› * a := by + have h1 := superCommute_ofCrAnOp_ofFieldOp_mem_center Ο† Ο†' rw [@Subalgebra.mem_center_iff] at h1 exact h1 a @@ -202,9 +202,9 @@ lemma superCommute_anPart_ofFieldOp_mem_center (Ο† Ο†' : 𝓕.FieldOp) : simp only [anPart_negAsymp, map_zero, LinearMap.zero_apply] exact Subalgebra.zero_mem (Subalgebra.center β„‚ _) | FieldOp.position Ο† => - exact superCommute_ofCrAnFieldOp_ofFieldOp_mem_center _ _ + exact superCommute_ofCrAnOp_ofFieldOp_mem_center _ _ | FieldOp.outAsymp _ => - exact superCommute_ofCrAnFieldOp_ofFieldOp_mem_center _ _ + exact superCommute_ofCrAnOp_ofFieldOp_mem_center _ _ /-! @@ -212,25 +212,25 @@ lemma superCommute_anPart_ofFieldOp_mem_center (Ο† Ο†' : 𝓕.FieldOp) : -/ -lemma superCommute_ofCrAnFieldOpList_ofCrAnFieldOpList (Ο†s Ο†s' : List 𝓕.CrAnFieldOp) : - [ofCrAnFieldOpList Ο†s, ofCrAnFieldOpList Ο†s']β‚› = - ofCrAnFieldOpList (Ο†s ++ Ο†s') - 𝓒(𝓕 |>β‚› Ο†s, 𝓕 |>β‚› Ο†s') β€’ ofCrAnFieldOpList (Ο†s' ++ Ο†s) := by - rw [ofCrAnFieldOpList_eq_ΞΉ_ofCrAnListF, ofCrAnFieldOpList_eq_ΞΉ_ofCrAnListF] +lemma superCommute_ofCrAnOpList_ofCrAnOpList (Ο†s Ο†s' : List 𝓕.CrAnFieldOp) : + [ofCrAnOpList Ο†s, ofCrAnOpList Ο†s']β‚› = + ofCrAnOpList (Ο†s ++ Ο†s') - 𝓒(𝓕 |>β‚› Ο†s, 𝓕 |>β‚› Ο†s') β€’ ofCrAnOpList (Ο†s' ++ Ο†s) := by + rw [ofCrAnOpList_eq_ΞΉ_ofCrAnListF, ofCrAnOpList_eq_ΞΉ_ofCrAnListF] rw [superCommute_eq_ΞΉ_superCommuteF, superCommuteF_ofCrAnListF_ofCrAnListF] rfl -lemma superCommute_ofCrAnFieldOp_ofCrAnFieldOp (Ο† Ο†' : 𝓕.CrAnFieldOp) : - [ofCrAnFieldOp Ο†, ofCrAnFieldOp Ο†']β‚› = ofCrAnFieldOp Ο† * ofCrAnFieldOp Ο†' - - 𝓒(𝓕 |>β‚› Ο†, 𝓕 |>β‚› Ο†') β€’ ofCrAnFieldOp Ο†' * ofCrAnFieldOp Ο† := by - rw [ofCrAnFieldOp, ofCrAnFieldOp] +lemma superCommute_ofCrAnOp_ofCrAnOp (Ο† Ο†' : 𝓕.CrAnFieldOp) : + [ofCrAnOp Ο†, ofCrAnOp Ο†']β‚› = ofCrAnOp Ο† * ofCrAnOp Ο†' - + 𝓒(𝓕 |>β‚› Ο†, 𝓕 |>β‚› Ο†') β€’ ofCrAnOp Ο†' * ofCrAnOp Ο† := by + rw [ofCrAnOp, ofCrAnOp] rw [superCommute_eq_ΞΉ_superCommuteF, superCommuteF_ofCrAnOpF_ofCrAnOpF] rfl -lemma superCommute_ofCrAnFieldOpList_ofFieldOpList (Ο†cas : List 𝓕.CrAnFieldOp) +lemma superCommute_ofCrAnOpList_ofFieldOpList (Ο†cas : List 𝓕.CrAnFieldOp) (Ο†s : List 𝓕.FieldOp) : - [ofCrAnFieldOpList Ο†cas, ofFieldOpList Ο†s]β‚› = ofCrAnFieldOpList Ο†cas * ofFieldOpList Ο†s - - 𝓒(𝓕 |>β‚› Ο†cas, 𝓕 |>β‚› Ο†s) β€’ ofFieldOpList Ο†s * ofCrAnFieldOpList Ο†cas := by - rw [ofCrAnFieldOpList, ofFieldOpList] + [ofCrAnOpList Ο†cas, ofFieldOpList Ο†s]β‚› = ofCrAnOpList Ο†cas * ofFieldOpList Ο†s - + 𝓒(𝓕 |>β‚› Ο†cas, 𝓕 |>β‚› Ο†s) β€’ ofFieldOpList Ο†s * ofCrAnOpList Ο†cas := by + rw [ofCrAnOpList, ofFieldOpList] rw [superCommute_eq_ΞΉ_superCommuteF, superCommuteF_ofCrAnListF_ofFieldOpFsList] rfl @@ -362,18 +362,18 @@ multiplication with a sign plus the super commutor. -/ -lemma ofCrAnFieldOpList_mul_ofCrAnFieldOpList_eq_superCommute (Ο†s Ο†s' : List 𝓕.CrAnFieldOp) : - ofCrAnFieldOpList Ο†s * ofCrAnFieldOpList Ο†s' = - 𝓒(𝓕 |>β‚› Ο†s, 𝓕 |>β‚› Ο†s') β€’ ofCrAnFieldOpList Ο†s' * ofCrAnFieldOpList Ο†s - + [ofCrAnFieldOpList Ο†s, ofCrAnFieldOpList Ο†s']β‚› := by - rw [superCommute_ofCrAnFieldOpList_ofCrAnFieldOpList] - simp [ofCrAnFieldOpList_append] +lemma ofCrAnOpList_mul_ofCrAnOpList_eq_superCommute (Ο†s Ο†s' : List 𝓕.CrAnFieldOp) : + ofCrAnOpList Ο†s * ofCrAnOpList Ο†s' = + 𝓒(𝓕 |>β‚› Ο†s, 𝓕 |>β‚› Ο†s') β€’ ofCrAnOpList Ο†s' * ofCrAnOpList Ο†s + + [ofCrAnOpList Ο†s, ofCrAnOpList Ο†s']β‚› := by + rw [superCommute_ofCrAnOpList_ofCrAnOpList] + simp [ofCrAnOpList_append] -lemma ofCrAnFieldOp_mul_ofCrAnFieldOpList_eq_superCommute (Ο† : 𝓕.CrAnFieldOp) - (Ο†s' : List 𝓕.CrAnFieldOp) : ofCrAnFieldOp Ο† * ofCrAnFieldOpList Ο†s' = - 𝓒(𝓕 |>β‚› Ο†, 𝓕 |>β‚› Ο†s') β€’ ofCrAnFieldOpList Ο†s' * ofCrAnFieldOp Ο† - + [ofCrAnFieldOp Ο†, ofCrAnFieldOpList Ο†s']β‚› := by - rw [← ofCrAnFieldOpList_singleton, ofCrAnFieldOpList_mul_ofCrAnFieldOpList_eq_superCommute] +lemma ofCrAnOp_mul_ofCrAnOpList_eq_superCommute (Ο† : 𝓕.CrAnFieldOp) + (Ο†s' : List 𝓕.CrAnFieldOp) : ofCrAnOp Ο† * ofCrAnOpList Ο†s' = + 𝓒(𝓕 |>β‚› Ο†, 𝓕 |>β‚› Ο†s') β€’ ofCrAnOpList Ο†s' * ofCrAnOp Ο† + + [ofCrAnOp Ο†, ofCrAnOpList Ο†s']β‚› := by + rw [← ofCrAnOpList_singleton, ofCrAnOpList_mul_ofCrAnOpList_eq_superCommute] simp lemma ofFieldOpList_mul_ofFieldOpList_eq_superCommute (Ο†s Ο†s' : List 𝓕.FieldOp) : @@ -402,11 +402,11 @@ lemma ofFieldOpList_mul_ofFieldOp_eq_superCommute (Ο†s : List 𝓕.FieldOp) (Ο† rw [superCommute_ofFieldOpList_ofFieldOp] simp -lemma ofCrAnFieldOpList_mul_ofFieldOpList_eq_superCommute (Ο†s : List 𝓕.CrAnFieldOp) - (Ο†s' : List 𝓕.FieldOp) : ofCrAnFieldOpList Ο†s * ofFieldOpList Ο†s' = - 𝓒(𝓕 |>β‚› Ο†s, 𝓕 |>β‚› Ο†s') β€’ ofFieldOpList Ο†s' * ofCrAnFieldOpList Ο†s - + [ofCrAnFieldOpList Ο†s, ofFieldOpList Ο†s']β‚› := by - rw [superCommute_ofCrAnFieldOpList_ofFieldOpList] +lemma ofCrAnOpList_mul_ofFieldOpList_eq_superCommute (Ο†s : List 𝓕.CrAnFieldOp) + (Ο†s' : List 𝓕.FieldOp) : ofCrAnOpList Ο†s * ofFieldOpList Ο†s' = + 𝓒(𝓕 |>β‚› Ο†s, 𝓕 |>β‚› Ο†s') β€’ ofFieldOpList Ο†s' * ofCrAnOpList Ο†s + + [ofCrAnOpList Ο†s, ofFieldOpList Ο†s']β‚› := by + rw [superCommute_ofCrAnOpList_ofFieldOpList] simp lemma crPart_mul_anPart_eq_superCommute (Ο† Ο†' : 𝓕.FieldOp) : @@ -441,17 +441,17 @@ lemma anPart_mul_anPart_swap (Ο† Ο†' : 𝓕.FieldOp) : -/ -lemma superCommute_ofCrAnFieldOpList_ofCrAnFieldOpList_symm (Ο†s Ο†s' : List 𝓕.CrAnFieldOp) : - [ofCrAnFieldOpList Ο†s, ofCrAnFieldOpList Ο†s']β‚› = - (- 𝓒(𝓕 |>β‚› Ο†s, 𝓕 |>β‚› Ο†s')) β€’ [ofCrAnFieldOpList Ο†s', ofCrAnFieldOpList Ο†s]β‚› := by - rw [ofCrAnFieldOpList, ofCrAnFieldOpList, superCommute_eq_ΞΉ_superCommuteF, +lemma superCommute_ofCrAnOpList_ofCrAnOpList_symm (Ο†s Ο†s' : List 𝓕.CrAnFieldOp) : + [ofCrAnOpList Ο†s, ofCrAnOpList Ο†s']β‚› = + (- 𝓒(𝓕 |>β‚› Ο†s, 𝓕 |>β‚› Ο†s')) β€’ [ofCrAnOpList Ο†s', ofCrAnOpList Ο†s]β‚› := by + rw [ofCrAnOpList, ofCrAnOpList, superCommute_eq_ΞΉ_superCommuteF, superCommuteF_ofCrAnListF_ofCrAnListF_symm] rfl -lemma superCommute_ofCrAnFieldOp_ofCrAnFieldOp_symm (Ο† Ο†' : 𝓕.CrAnFieldOp) : - [ofCrAnFieldOp Ο†, ofCrAnFieldOp Ο†']β‚› = - (- 𝓒(𝓕 |>β‚› Ο†, 𝓕 |>β‚› Ο†')) β€’ [ofCrAnFieldOp Ο†', ofCrAnFieldOp Ο†]β‚› := by - rw [ofCrAnFieldOp, ofCrAnFieldOp, superCommute_eq_ΞΉ_superCommuteF, +lemma superCommute_ofCrAnOp_ofCrAnOp_symm (Ο† Ο†' : 𝓕.CrAnFieldOp) : + [ofCrAnOp Ο†, ofCrAnOp Ο†']β‚› = + (- 𝓒(𝓕 |>β‚› Ο†, 𝓕 |>β‚› Ο†')) β€’ [ofCrAnOp Ο†', ofCrAnOp Ο†]β‚› := by + rw [ofCrAnOp, ofCrAnOp, superCommute_eq_ΞΉ_superCommuteF, superCommuteF_ofCrAnOpF_ofCrAnOpF_symm] rfl @@ -461,54 +461,54 @@ lemma superCommute_ofCrAnFieldOp_ofCrAnFieldOp_symm (Ο† Ο†' : 𝓕.CrAnFieldOp) -/ -lemma superCommute_ofCrAnFieldOpList_ofCrAnFieldOpList_eq_sum (Ο†s Ο†s' : List 𝓕.CrAnFieldOp) : - [ofCrAnFieldOpList Ο†s, ofCrAnFieldOpList Ο†s']β‚› = +lemma superCommute_ofCrAnOpList_ofCrAnOpList_eq_sum (Ο†s Ο†s' : List 𝓕.CrAnFieldOp) : + [ofCrAnOpList Ο†s, ofCrAnOpList Ο†s']β‚› = βˆ‘ (n : Fin Ο†s'.length), 𝓒(𝓕 |>β‚› Ο†s, 𝓕 |>β‚› Ο†s'.take n) β€’ - ofCrAnFieldOpList (Ο†s'.take n) * [ofCrAnFieldOpList Ο†s, ofCrAnFieldOp (Ο†s'.get n)]β‚› * - ofCrAnFieldOpList (Ο†s'.drop (n + 1)) := by + ofCrAnOpList (Ο†s'.take n) * [ofCrAnOpList Ο†s, ofCrAnOp (Ο†s'.get n)]β‚› * + ofCrAnOpList (Ο†s'.drop (n + 1)) := by conv_lhs => - rw [ofCrAnFieldOpList, ofCrAnFieldOpList, superCommute_eq_ΞΉ_superCommuteF, + rw [ofCrAnOpList, ofCrAnOpList, superCommute_eq_ΞΉ_superCommuteF, superCommuteF_ofCrAnListF_ofCrAnListF_eq_sum] rw [map_sum] rfl -lemma superCommute_ofCrAnFieldOp_ofCrAnFieldOpList_eq_sum (Ο† : 𝓕.CrAnFieldOp) - (Ο†s' : List 𝓕.CrAnFieldOp) : [ofCrAnFieldOp Ο†, ofCrAnFieldOpList Ο†s']β‚› = +lemma superCommute_ofCrAnOp_ofCrAnOpList_eq_sum (Ο† : 𝓕.CrAnFieldOp) + (Ο†s' : List 𝓕.CrAnFieldOp) : [ofCrAnOp Ο†, ofCrAnOpList Ο†s']β‚› = βˆ‘ (n : Fin Ο†s'.length), 𝓒(𝓕 |>β‚› Ο†, 𝓕 |>β‚› Ο†s'.take n) β€’ - [ofCrAnFieldOp Ο†, ofCrAnFieldOp (Ο†s'.get n)]β‚› * ofCrAnFieldOpList (Ο†s'.eraseIdx n) := by + [ofCrAnOp Ο†, ofCrAnOp (Ο†s'.get n)]β‚› * ofCrAnOpList (Ο†s'.eraseIdx n) := by conv_lhs => - rw [← ofCrAnFieldOpList_singleton, superCommute_ofCrAnFieldOpList_ofCrAnFieldOpList_eq_sum] + rw [← ofCrAnOpList_singleton, superCommute_ofCrAnOpList_ofCrAnOpList_eq_sum] congr funext n simp only [instCommGroup.eq_1, ofList_singleton, List.get_eq_getElem, Algebra.smul_mul_assoc] congr 1 - rw [ofCrAnFieldOpList_singleton, superCommute_ofCrAnFieldOp_ofCrAnFieldOp_commute] - rw [mul_assoc, ← ofCrAnFieldOpList_append] + rw [ofCrAnOpList_singleton, superCommute_ofCrAnOp_ofCrAnOp_commute] + rw [mul_assoc, ← ofCrAnOpList_append] congr exact Eq.symm (List.eraseIdx_eq_take_drop_succ Ο†s' ↑n) -lemma superCommute_ofCrAnFieldOpList_ofFieldOpList_eq_sum (Ο†s : List 𝓕.CrAnFieldOp) - (Ο†s' : List 𝓕.FieldOp) : [ofCrAnFieldOpList Ο†s, ofFieldOpList Ο†s']β‚› = +lemma superCommute_ofCrAnOpList_ofFieldOpList_eq_sum (Ο†s : List 𝓕.CrAnFieldOp) + (Ο†s' : List 𝓕.FieldOp) : [ofCrAnOpList Ο†s, ofFieldOpList Ο†s']β‚› = βˆ‘ (n : Fin Ο†s'.length), 𝓒(𝓕 |>β‚› Ο†s, 𝓕 |>β‚› Ο†s'.take n) β€’ - ofFieldOpList (Ο†s'.take n) * [ofCrAnFieldOpList Ο†s, ofFieldOp (Ο†s'.get n)]β‚› * + ofFieldOpList (Ο†s'.take n) * [ofCrAnOpList Ο†s, ofFieldOp (Ο†s'.get n)]β‚› * ofFieldOpList (Ο†s'.drop (n + 1)) := by conv_lhs => - rw [ofCrAnFieldOpList, ofFieldOpList, superCommute_eq_ΞΉ_superCommuteF, + rw [ofCrAnOpList, ofFieldOpList, superCommute_eq_ΞΉ_superCommuteF, superCommuteF_ofCrAnListF_ofFieldOpListF_eq_sum] rw [map_sum] rfl -lemma superCommute_ofCrAnFieldOp_ofFieldOpList_eq_sum (Ο† : 𝓕.CrAnFieldOp) (Ο†s' : List 𝓕.FieldOp) : - [ofCrAnFieldOp Ο†, ofFieldOpList Ο†s']β‚› = +lemma superCommute_ofCrAnOp_ofFieldOpList_eq_sum (Ο† : 𝓕.CrAnFieldOp) (Ο†s' : List 𝓕.FieldOp) : + [ofCrAnOp Ο†, ofFieldOpList Ο†s']β‚› = βˆ‘ (n : Fin Ο†s'.length), 𝓒(𝓕 |>β‚› Ο†, 𝓕 |>β‚› Ο†s'.take n) β€’ - [ofCrAnFieldOp Ο†, ofFieldOp (Ο†s'.get n)]β‚› * ofFieldOpList (Ο†s'.eraseIdx n) := by + [ofCrAnOp Ο†, ofFieldOp (Ο†s'.get n)]β‚› * ofFieldOpList (Ο†s'.eraseIdx n) := by conv_lhs => - rw [← ofCrAnFieldOpList_singleton, superCommute_ofCrAnFieldOpList_ofFieldOpList_eq_sum] + rw [← ofCrAnOpList_singleton, superCommute_ofCrAnOpList_ofFieldOpList_eq_sum] congr funext n simp only [instCommGroup.eq_1, ofList_singleton, List.get_eq_getElem, Algebra.smul_mul_assoc] congr 1 - rw [ofCrAnFieldOpList_singleton, superCommute_ofCrAnFieldOp_ofFieldOp_commute] + rw [ofCrAnOpList_singleton, superCommute_ofCrAnOp_ofFieldOp_commute] rw [mul_assoc, ← ofFieldOpList_append] congr exact Eq.symm (List.eraseIdx_eq_take_drop_succ Ο†s' ↑n) diff --git a/HepLean/PerturbationTheory/FieldOpAlgebra/TimeOrder.lean b/HepLean/PerturbationTheory/FieldOpAlgebra/TimeOrder.lean index f02df74..98cec2d 100644 --- a/HepLean/PerturbationTheory/FieldOpAlgebra/TimeOrder.lean +++ b/HepLean/PerturbationTheory/FieldOpAlgebra/TimeOrder.lean @@ -435,9 +435,9 @@ lemma timeOrder_eq_maxTimeField_mul_finset (Ο† : 𝓕.FieldOp) (Ο†s : List 𝓕. lemma timeOrder_superCommute_eq_time_mid {Ο† ψ : 𝓕.CrAnFieldOp} (hΟ†Οˆ : crAnTimeOrderRel Ο† ψ) (hΟˆΟ† : crAnTimeOrderRel ψ Ο†) (a b : 𝓕.FieldOpAlgebra) : - 𝓣(a * [ofCrAnFieldOp Ο†, ofCrAnFieldOp ψ]β‚› * b) = - [ofCrAnFieldOp Ο†, ofCrAnFieldOp ψ]β‚› * 𝓣(a * b) := by - rw [ofCrAnFieldOp, ofCrAnFieldOp] + 𝓣(a * [ofCrAnOp Ο†, ofCrAnOp ψ]β‚› * b) = + [ofCrAnOp Ο†, ofCrAnOp ψ]β‚› * 𝓣(a * b) := by + rw [ofCrAnOp, ofCrAnOp] rw [superCommute_eq_ΞΉ_superCommuteF] obtain ⟨a, rfl⟩ := ΞΉ_surjective a obtain ⟨b, rfl⟩ := ΞΉ_surjective b @@ -449,17 +449,17 @@ lemma timeOrder_superCommute_eq_time_mid {Ο† ψ : 𝓕.CrAnFieldOp} lemma timeOrder_superCommute_eq_time_left {Ο† ψ : 𝓕.CrAnFieldOp} (hΟ†Οˆ : crAnTimeOrderRel Ο† ψ) (hΟˆΟ† : crAnTimeOrderRel ψ Ο†) (b : 𝓕.FieldOpAlgebra) : - 𝓣([ofCrAnFieldOp Ο†, ofCrAnFieldOp ψ]β‚› * b) = - [ofCrAnFieldOp Ο†, ofCrAnFieldOp ψ]β‚› * 𝓣(b) := by - trans 𝓣(1 * [ofCrAnFieldOp Ο†, ofCrAnFieldOp ψ]β‚› * b) + 𝓣([ofCrAnOp Ο†, ofCrAnOp ψ]β‚› * b) = + [ofCrAnOp Ο†, ofCrAnOp ψ]β‚› * 𝓣(b) := by + trans 𝓣(1 * [ofCrAnOp Ο†, ofCrAnOp ψ]β‚› * b) simp only [one_mul] rw [timeOrder_superCommute_eq_time_mid hΟ†Οˆ hΟˆΟ†] simp lemma timeOrder_superCommute_neq_time {Ο† ψ : 𝓕.CrAnFieldOp} (hΟ†Οˆ : Β¬ (crAnTimeOrderRel Ο† ψ ∧ crAnTimeOrderRel ψ Ο†)) : - 𝓣([ofCrAnFieldOp Ο†, ofCrAnFieldOp ψ]β‚›) = 0 := by - rw [ofCrAnFieldOp, ofCrAnFieldOp] + 𝓣([ofCrAnOp Ο†, ofCrAnOp ψ]β‚›) = 0 := by + rw [ofCrAnOp, ofCrAnOp] rw [superCommute_eq_ΞΉ_superCommuteF] rw [timeOrder_eq_ΞΉ_timeOrderF] trans ΞΉ (timeOrderF (1 * (superCommuteF (ofCrAnOpF Ο†)) (ofCrAnOpF ψ) * 1)) diff --git a/HepLean/PerturbationTheory/FieldOpAlgebra/WicksTheoremNormal.lean b/HepLean/PerturbationTheory/FieldOpAlgebra/WicksTheoremNormal.lean index 67ea1f6..0b24d0d 100644 --- a/HepLean/PerturbationTheory/FieldOpAlgebra/WicksTheoremNormal.lean +++ b/HepLean/PerturbationTheory/FieldOpAlgebra/WicksTheoremNormal.lean @@ -169,11 +169,11 @@ lemma wicks_theorem_normal_order_empty : 𝓣(𝓝(ofFieldOpList [])) = simp only [Finset.univ_unique, PUnit.default_eq_unit, List.length_nil, Equiv.coe_fn_symm_mk, sign_empty, timeContract_empty, OneMemClass.coe_one, one_smul, uncontractedListGet_empty, one_mul, Finset.sum_const, Finset.card_singleton, e2] - have h1' : ofFieldOpList (𝓕 := 𝓕) [] = ofCrAnFieldOpList [] := by rfl + have h1' : ofFieldOpList (𝓕 := 𝓕) [] = ofCrAnOpList [] := by rfl rw [h1'] - rw [normalOrder_ofCrAnFieldOpList] + rw [normalOrder_ofCrAnOpList] simp only [normalOrderSign_nil, normalOrderList_nil, one_smul] - rw [ofCrAnFieldOpList, timeOrder_eq_ΞΉ_timeOrderF] + rw [ofCrAnOpList, timeOrder_eq_ΞΉ_timeOrderF] rw [timeOrderF_ofCrAnListF] simp diff --git a/scripts/MetaPrograms/notes.lean b/scripts/MetaPrograms/notes.lean index e3a29d2..a35910b 100644 --- a/scripts/MetaPrograms/notes.lean +++ b/scripts/MetaPrograms/notes.lean @@ -164,10 +164,10 @@ def perturbationTheory : Note where .name ``FieldSpecification.FieldOpFreeAlgebra.superCommuteF_ofCrAnListF_ofFieldOpListF_eq_sum .incomplete, .h2 "Field-operator algebra", .name ``FieldSpecification.FieldOpAlgebra .incomplete, - .name ``FieldSpecification.FieldOpAlgebra.ofCrAnFieldOp .incomplete, - .name ``FieldSpecification.FieldOpAlgebra.ofCrAnFieldOpList .incomplete, + .name ``FieldSpecification.FieldOpAlgebra.ofCrAnOp .incomplete, + .name ``FieldSpecification.FieldOpAlgebra.ofCrAnOpList .incomplete, .name ``FieldSpecification.FieldOpAlgebra.ofFieldOp .incomplete, - .name ``FieldSpecification.FieldOpAlgebra.ofCrAnFieldOpList .incomplete, + .name ``FieldSpecification.FieldOpAlgebra.ofCrAnOpList .incomplete, .name ``FieldSpecification.FieldOpAlgebra.anPart .incomplete, .name ``FieldSpecification.FieldOpAlgebra.crPart .incomplete, .name ``FieldSpecification.FieldOpAlgebra.ofFieldOp_eq_crPart_add_anPart .incomplete, @@ -186,7 +186,7 @@ def perturbationTheory : Note where .name ``FieldSpecification.FieldOpAlgebra.normalOrder .incomplete, .h2 "Some lemmas", .name ``FieldSpecification.normalOrderSign_eraseIdx .incomplete, - .name ``FieldSpecification.FieldOpAlgebra.ofCrAnFieldOp_superCommute_normalOrder_ofCrAnFieldOpList_sum .incomplete, + .name ``FieldSpecification.FieldOpAlgebra.ofCrAnOp_superCommute_normalOrder_ofCrAnOpList_sum .incomplete, .name ``FieldSpecification.FieldOpAlgebra.ofFieldOp_mul_normalOrder_ofFieldOpList_eq_sum .incomplete, .h1 "Wick Contractions", .h2 "Definition",