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

refactor: rename ofCrAnOpList to ofCrAnList

Browse source
This commit is contained in:
jstoobysmith 2025-02-06 10:10:55 +00:00
parent 2d561dd89d
commit 48e3417d5d
6 changed files with 97 additions and 97 deletions
Download patch file Download diff file Expand all files Collapse all files

20
HepLean/PerturbationTheory/FieldOpAlgebra/Basic.lean
View file

@ -485,23 +485,23 @@ lemma ofFieldOp_eq_sum (φ : 𝓕.FieldOp) :
rfl
/-- An element of `FieldOpAlgebra` from a list of `CrAnFieldOp`. -/
def ofCrAnOpList (φs : List 𝓕.CrAnFieldOp) : 𝓕.FieldOpAlgebra := ι (ofCrAnListF φs)
def ofCrAnList (φs : List 𝓕.CrAnFieldOp) : 𝓕.FieldOpAlgebra := ι (ofCrAnListF φs)
lemma ofCrAnOpList_eq_ι_ofCrAnListF (φs : List 𝓕.CrAnFieldOp) :
ofCrAnOpList φs = ι (ofCrAnListF φs) := rfl
lemma ofCrAnList_eq_ι_ofCrAnListF (φs : List 𝓕.CrAnFieldOp) :
ofCrAnList φs = ι (ofCrAnListF φs) := rfl
lemma ofCrAnOpList_append (φs ψs : List 𝓕.CrAnFieldOp) :
ofCrAnOpList (φs ++ ψs) = ofCrAnOpList φs * ofCrAnOpList ψs := by
simp only [ofCrAnOpList]
lemma ofCrAnList_append (φs ψs : List 𝓕.CrAnFieldOp) :
ofCrAnList (φs ++ ψs) = ofCrAnList φs * ofCrAnList ψs := by
simp only [ofCrAnList]
rw [ofCrAnListF_append]
simp
lemma ofCrAnOpList_singleton (φ : 𝓕.CrAnFieldOp) :
ofCrAnOpList [φ] = ofCrAnOp φ := by
simp only [ofCrAnOpList, ofCrAnOp, ofCrAnListF_singleton]
lemma ofCrAnList_singleton (φ : 𝓕.CrAnFieldOp) :
ofCrAnList [φ] = ofCrAnOp φ := by
simp only [ofCrAnList, ofCrAnOp, ofCrAnListF_singleton]
lemma ofFieldOpList_eq_sum (φs : List 𝓕.FieldOp) :
ofFieldOpList φs = ∑ s : CrAnSection φs, ofCrAnOpList s.1 := by
ofFieldOpList φs = ∑ s : CrAnSection φs, ofCrAnList s.1 := by
rw [ofFieldOpList, ofFieldOpListF_sum]
simp only [map_sum]
rfl

26
HepLean/PerturbationTheory/FieldOpAlgebra/Grading.lean
View file

@ -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 = ofCrAnOpList φs ∧ (𝓕 |>ₛ φs) = f}
Submodule.span ℂ {a | ∃ φs, a = ofCrAnList φs ∧ (𝓕 |>ₛ φs) = f}
lemma ofCrAnOpList_mem_statSubmodule_of_eq (φs : List 𝓕.CrAnFieldOp) (f : FieldStatistic)
(h : (𝓕 |>ₛ φs) = f) : ofCrAnOpList φs ∈ statSubmodule f :=
lemma ofCrAnList_mem_statSubmodule_of_eq (φs : List 𝓕.CrAnFieldOp) (f : FieldStatistic)
(h : (𝓕 |>ₛ φs) = f) : ofCrAnList φs ∈ statSubmodule f :=
Submodule.mem_span.mpr fun _ a => a ⟨φs, ⟨rfl, h⟩⟩
lemma ofCrAnOpList_mem_statSubmodule (φs : List 𝓕.CrAnFieldOp) :
ofCrAnOpList φs ∈ statSubmodule (𝓕 |>ₛ φs) :=
lemma ofCrAnList_mem_statSubmodule (φs : List 𝓕.CrAnFieldOp) :
ofCrAnList φ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 ofCrAnOpList_mem_statSubmodule_of_eq
apply ofCrAnList_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 ofCrAnOpList_mem_statSubmodule_of_eq
apply ofCrAnList_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 [ofCrAnOpList]
rw [ofCrAnList]
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 [ofCrAnOpList]
rw [ofCrAnList]
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 `ofCrAnOpList φs` for which `φs` has `bosonic` statistics span one part of the grading,
Those `ofCrAnList φ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 [ofCrAnOpList, ofCrAnListF_nil, map_one, ofList_empty, true_and]
simp only [ofCrAnList, 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 * ofCrAnOpList φs ∈ statSubmodule (f1 + f2)
a1 * ofCrAnList φ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 [← ofCrAnOpList_append]
rw [← ofCrAnList_append]
refine Submodule.mem_span.mpr fun p a => a ?_
simp only [Set.mem_setOf_eq]
use φs' ++ φs

46
HepLean/PerturbationTheory/FieldOpAlgebra/NormalOrder/Lemmas.lean
View file

@ -27,16 +27,16 @@ variable {𝓕 : FieldSpecification}
lemma normalOrder_eq_ι_normalOrderF (a : 𝓕.FieldOpFreeAlgebra) :
𝓝(ι a) = ι 𝓝ᶠ(a) := rfl
lemma normalOrder_ofCrAnOpList (φs : List 𝓕.CrAnFieldOp) :
𝓝(ofCrAnOpList φs) = normalOrderSign φs • ofCrAnOpList (normalOrderList φs) := by
rw [ofCrAnOpList, normalOrder_eq_ι_normalOrderF, normalOrderF_ofCrAnListF]
lemma normalOrder_ofCrAnList (φs : List 𝓕.CrAnFieldOp) :
𝓝(ofCrAnList φs) = normalOrderSign φs • ofCrAnList (normalOrderList φs) := by
rw [ofCrAnList, normalOrder_eq_ι_normalOrderF, normalOrderF_ofCrAnListF]
rfl
@[simp]
lemma normalOrder_one_eq_one : normalOrder (𝓕 := 𝓕) 1 = 1 := by
have h1 : 1 = ofCrAnOpList (𝓕 := 𝓕) [] := by simp [ofCrAnOpList]
have h1 : 1 = ofCrAnList (𝓕 := 𝓕) [] := by simp [ofCrAnList]
rw [h1]
rw [normalOrder_ofCrAnOpList]
rw [normalOrder_ofCrAnList]
simp
@[simp]
@ -48,14 +48,14 @@ lemma normalOrder_ofFieldOpList_nil : normalOrder (𝓕 := 𝓕) (ofFieldOpList
simp
@[simp]
lemma normalOrder_ofCrAnOpList_nil : normalOrder (𝓕 := 𝓕) (ofCrAnOpList []) = 1 := by
rw [normalOrder_ofCrAnOpList]
lemma normalOrder_ofCrAnList_nil : normalOrder (𝓕 := 𝓕) (ofCrAnList []) = 1 := by
rw [normalOrder_ofCrAnList]
simp only [normalOrderSign_nil, normalOrderList_nil, one_smul]
rfl
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,
lemma ofCrAnList_eq_normalOrder (φs : List 𝓕.CrAnFieldOp) :
ofCrAnList (normalOrderList φs) = normalOrderSign φs • 𝓝(ofCrAnList φs) := by
rw [normalOrder_ofCrAnList, 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_ofCrAnOp_ofCrAnOpList (φ : 𝓕.CrAnFieldOp)
(φs : List 𝓕.CrAnFieldOp) : 𝓝(ofCrAnOp φ * ofCrAnOpList φs) =
𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φs) • 𝓝(ofCrAnOpList φs * ofCrAnOp φ) := by
rw [← ofCrAnOpList_singleton, ofCrAnOpList_mul_ofCrAnOpList_eq_superCommute]
lemma normalOrder_ofCrAnOp_ofCrAnList (φ : 𝓕.CrAnFieldOp)
(φs : List 𝓕.CrAnFieldOp) : 𝓝(ofCrAnOp φ * ofCrAnList φs) =
𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φs) • 𝓝(ofCrAnList φs * ofCrAnOp φ) := by
rw [← ofCrAnList_singleton, ofCrAnList_mul_ofCrAnList_eq_superCommute]
simp
lemma normalOrder_ofCrAnOp_ofFieldOpList_swap (φ : 𝓕.CrAnFieldOp) (φ' : List 𝓕.FieldOp) :
𝓝(ofCrAnOp φ * ofFieldOpList φ') = 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') •
𝓝(ofFieldOpList φ' * ofCrAnOp φ) := by
rw [← ofCrAnOpList_singleton, ofCrAnOpList_mul_ofFieldOpList_eq_superCommute]
rw [← ofCrAnList_singleton, ofCrAnList_mul_ofFieldOpList_eq_superCommute]
simp
lemma normalOrder_anPart_ofFieldOpList_swap (φ : 𝓕.FieldOp) (φ' : List 𝓕.FieldOp) :
@ -224,18 +224,18 @@ The proof of this result ultimetly depends on
- `superCommuteF_ofCrAnListF_ofFieldOpListF_eq_sum`
- `normalOrderSign_eraseIdx`
-/
lemma ofCrAnOp_superCommute_normalOrder_ofCrAnOpList_sum (φ : 𝓕.CrAnFieldOp)
(φs : List 𝓕.CrAnFieldOp) : [ofCrAnOp φ, 𝓝(ofCrAnOpList φs)]ₛ = ∑ n : Fin φs.length,
lemma ofCrAnOp_superCommute_normalOrder_ofCrAnList_sum (φ : 𝓕.CrAnFieldOp)
(φs : List 𝓕.CrAnFieldOp) : [ofCrAnOp φ, 𝓝(ofCrAnList φ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,
* 𝓝(ofCrAnList (φs.eraseIdx n)) := by
rw [normalOrder_ofCrAnList, map_smul]
rw [superCommute_ofCrAnOp_ofCrAnList_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 [ofCrAnOpList_eq_normalOrder, mul_smul_comm, smul_smul, smul_smul]
rw [ofCrAnList_eq_normalOrder, mul_smul_comm, smul_smul, smul_smul]
by_cases hs : (𝓕 |>ₛ φ) = (𝓕 |>ₛ φs[n])
· congr
erw [normalOrderSign_eraseIdx, ← hs]
@ -257,7 +257,7 @@ lemma ofCrAnOp_superCommute_normalOrder_ofFieldOpList_sum (φ : 𝓕.CrAnFieldOp
conv_lhs =>
rw [ofFieldOpList_eq_sum, map_sum, map_sum]
enter [2, s]
rw [ofCrAnOp_superCommute_normalOrder_ofCrAnOpList_sum, CrAnSection.sum_over_length]
rw [ofCrAnOp_superCommute_normalOrder_ofCrAnList_sum, CrAnSection.sum_over_length]
enter [2, n]
rw [CrAnSection.take_statistics_eq_take_state_statistics, smul_mul_assoc]
rw [Finset.sum_comm]
@ -339,7 +339,7 @@ For a field specification `𝓕`, the following relation holds in the algebra `
`φ * 𝓝(φ₀φ₁…φₙ) = 𝓝(φφ₀φ₁…φₙ) + ∑ i, (𝓢(φ,φ₀φ₁…φᵢ₋₁) • [anPartF φ, φᵢ]ₛ) * 𝓝(φ₀φ₁…φᵢ₋₁φᵢ₊₁…φₙ)`.
The proof of this ultimently depends on :
- `ofCrAnOp_superCommute_normalOrder_ofCrAnOpList_sum`
- `ofCrAnOp_superCommute_normalOrder_ofCrAnList_sum`
-/
lemma ofFieldOp_mul_normalOrder_ofFieldOpList_eq_sum (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) :
ofFieldOp φ * 𝓝(ofFieldOpList φs) =

90
HepLean/PerturbationTheory/FieldOpAlgebra/SuperCommute.lean
View file

@ -212,10 +212,10 @@ lemma superCommute_anPart_ofFieldOp_mem_center (φ φ' : 𝓕.FieldOp) :
-/
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]
lemma superCommute_ofCrAnList_ofCrAnList (φs φs' : List 𝓕.CrAnFieldOp) :
[ofCrAnList φs, ofCrAnList φs']ₛ =
ofCrAnList (φs ++ φs') - 𝓢(𝓕 |>ₛ φs, 𝓕 |>ₛ φs') • ofCrAnList (φs' ++ φs) := by
rw [ofCrAnList_eq_ι_ofCrAnListF, ofCrAnList_eq_ι_ofCrAnListF]
rw [superCommute_eq_ι_superCommuteF, superCommuteF_ofCrAnListF_ofCrAnListF]
rfl
@ -226,11 +226,11 @@ lemma superCommute_ofCrAnOp_ofCrAnOp (φ φ' : 𝓕.CrAnFieldOp) :
rw [superCommute_eq_ι_superCommuteF, superCommuteF_ofCrAnOpF_ofCrAnOpF]
rfl
lemma superCommute_ofCrAnOpList_ofFieldOpList (φcas : List 𝓕.CrAnFieldOp)
lemma superCommute_ofCrAnList_ofFieldOpList (φcas : List 𝓕.CrAnFieldOp)
(φs : List 𝓕.FieldOp) :
[ofCrAnOpList φcas, ofFieldOpList φs]ₛ = ofCrAnOpList φcas * ofFieldOpList φs -
𝓢(𝓕 |>ₛ φcas, 𝓕 |>ₛ φs) • ofFieldOpList φs * ofCrAnOpList φcas := by
rw [ofCrAnOpList, ofFieldOpList]
[ofCrAnList φcas, ofFieldOpList φs]ₛ = ofCrAnList φcas * ofFieldOpList φs -
𝓢(𝓕 |>ₛ φcas, 𝓕 |>ₛ φs) • ofFieldOpList φs * ofCrAnList φcas := by
rw [ofCrAnList, ofFieldOpList]
rw [superCommute_eq_ι_superCommuteF, superCommuteF_ofCrAnListF_ofFieldOpFsList]
rfl
@ -362,18 +362,18 @@ multiplication with a sign plus the super commutor.
-/
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 ofCrAnList_mul_ofCrAnList_eq_superCommute (φs φs' : List 𝓕.CrAnFieldOp) :
ofCrAnList φs * ofCrAnList φs' =
𝓢(𝓕 |>ₛ φs, 𝓕 |>ₛ φs') • ofCrAnList φs' * ofCrAnList φs
+ [ofCrAnList φs, ofCrAnList φs']ₛ := by
rw [superCommute_ofCrAnList_ofCrAnList]
simp [ofCrAnList_append]
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]
lemma ofCrAnOp_mul_ofCrAnList_eq_superCommute (φ : 𝓕.CrAnFieldOp)
(φs' : List 𝓕.CrAnFieldOp) : ofCrAnOp φ * ofCrAnList φs' =
𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φs') • ofCrAnList φs' * ofCrAnOp φ
+ [ofCrAnOp φ, ofCrAnList φs']ₛ := by
rw [← ofCrAnList_singleton, ofCrAnList_mul_ofCrAnList_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 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]
lemma ofCrAnList_mul_ofFieldOpList_eq_superCommute (φs : List 𝓕.CrAnFieldOp)
(φs' : List 𝓕.FieldOp) : ofCrAnList φs * ofFieldOpList φs' =
𝓢(𝓕 |>ₛ φs, 𝓕 |>ₛ φs') • ofFieldOpList φs' * ofCrAnList φs
+ [ofCrAnList φs, ofFieldOpList φs']ₛ := by
rw [superCommute_ofCrAnList_ofFieldOpList]
simp
lemma crPart_mul_anPart_eq_superCommute (φ φ' : 𝓕.FieldOp) :
@ -441,10 +441,10 @@ lemma anPart_mul_anPart_swap (φ φ' : 𝓕.FieldOp) :
-/
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,
lemma superCommute_ofCrAnList_ofCrAnList_symm (φs φs' : List 𝓕.CrAnFieldOp) :
[ofCrAnList φs, ofCrAnList φs']ₛ =
(- 𝓢(𝓕 |>ₛ φs, 𝓕 |>ₛ φs')) • [ofCrAnList φs', ofCrAnList φs]ₛ := by
rw [ofCrAnList, ofCrAnList, superCommute_eq_ι_superCommuteF,
superCommuteF_ofCrAnListF_ofCrAnListF_symm]
rfl
@ -461,39 +461,39 @@ lemma superCommute_ofCrAnOp_ofCrAnOp_symm (φ φ' : 𝓕.CrAnFieldOp) :
-/
lemma superCommute_ofCrAnOpList_ofCrAnOpList_eq_sum (φs φs' : List 𝓕.CrAnFieldOp) :
[ofCrAnOpList φs, ofCrAnOpList φs']ₛ =
lemma superCommute_ofCrAnList_ofCrAnList_eq_sum (φs φs' : List 𝓕.CrAnFieldOp) :
[ofCrAnList φs, ofCrAnList φs']ₛ =
∑ (n : Fin φs'.length), 𝓢(𝓕 |>ₛ φs, 𝓕 |>ₛ φs'.take n) •
ofCrAnOpList (φs'.take n) * [ofCrAnOpList φs, ofCrAnOp (φs'.get n)]ₛ *
ofCrAnOpList (φs'.drop (n + 1)) := by
ofCrAnList (φs'.take n) * [ofCrAnList φs, ofCrAnOp (φs'.get n)]ₛ *
ofCrAnList (φs'.drop (n + 1)) := by
conv_lhs =>
rw [ofCrAnOpList, ofCrAnOpList, superCommute_eq_ι_superCommuteF,
rw [ofCrAnList, ofCrAnList, superCommute_eq_ι_superCommuteF,
superCommuteF_ofCrAnListF_ofCrAnListF_eq_sum]
rw [map_sum]
rfl
lemma superCommute_ofCrAnOp_ofCrAnOpList_eq_sum (φ : 𝓕.CrAnFieldOp)
(φs' : List 𝓕.CrAnFieldOp) : [ofCrAnOp φ, ofCrAnOpList φs']ₛ =
lemma superCommute_ofCrAnOp_ofCrAnList_eq_sum (φ : 𝓕.CrAnFieldOp)
(φs' : List 𝓕.CrAnFieldOp) : [ofCrAnOp φ, ofCrAnList φs']ₛ =
∑ (n : Fin φs'.length), 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φs'.take n) •
[ofCrAnOp φ, ofCrAnOp (φs'.get n)]ₛ * ofCrAnOpList (φs'.eraseIdx n) := by
[ofCrAnOp φ, ofCrAnOp (φs'.get n)]ₛ * ofCrAnList (φs'.eraseIdx n) := by
conv_lhs =>
rw [← ofCrAnOpList_singleton, superCommute_ofCrAnOpList_ofCrAnOpList_eq_sum]
rw [← ofCrAnList_singleton, superCommute_ofCrAnList_ofCrAnList_eq_sum]
congr
funext n
simp only [instCommGroup.eq_1, ofList_singleton, List.get_eq_getElem, Algebra.smul_mul_assoc]
congr 1
rw [ofCrAnOpList_singleton, superCommute_ofCrAnOp_ofCrAnOp_commute]
rw [mul_assoc, ← ofCrAnOpList_append]
rw [ofCrAnList_singleton, superCommute_ofCrAnOp_ofCrAnOp_commute]
rw [mul_assoc, ← ofCrAnList_append]
congr
exact Eq.symm (List.eraseIdx_eq_take_drop_succ φs' ↑n)
lemma superCommute_ofCrAnOpList_ofFieldOpList_eq_sum (φs : List 𝓕.CrAnFieldOp)
(φs' : List 𝓕.FieldOp) : [ofCrAnOpList φs, ofFieldOpList φs']ₛ =
lemma superCommute_ofCrAnList_ofFieldOpList_eq_sum (φs : List 𝓕.CrAnFieldOp)
(φs' : List 𝓕.FieldOp) : [ofCrAnList φs, ofFieldOpList φs']ₛ =
∑ (n : Fin φs'.length), 𝓢(𝓕 |>ₛ φs, 𝓕 |>ₛ φs'.take n) •
ofFieldOpList (φs'.take n) * [ofCrAnOpList φs, ofFieldOp (φs'.get n)]ₛ *
ofFieldOpList (φs'.take n) * [ofCrAnList φs, ofFieldOp (φs'.get n)]ₛ *
ofFieldOpList (φs'.drop (n + 1)) := by
conv_lhs =>
rw [ofCrAnOpList, ofFieldOpList, superCommute_eq_ι_superCommuteF,
rw [ofCrAnList, ofFieldOpList, superCommute_eq_ι_superCommuteF,
superCommuteF_ofCrAnListF_ofFieldOpListF_eq_sum]
rw [map_sum]
rfl
@ -503,12 +503,12 @@ lemma superCommute_ofCrAnOp_ofFieldOpList_eq_sum (φ : 𝓕.CrAnFieldOp) (φs' :
∑ (n : Fin φs'.length), 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φs'.take n) •
[ofCrAnOp φ, ofFieldOp (φs'.get n)]ₛ * ofFieldOpList (φs'.eraseIdx n) := by
conv_lhs =>
rw [← ofCrAnOpList_singleton, superCommute_ofCrAnOpList_ofFieldOpList_eq_sum]
rw [← ofCrAnList_singleton, superCommute_ofCrAnList_ofFieldOpList_eq_sum]
congr
funext n
simp only [instCommGroup.eq_1, ofList_singleton, List.get_eq_getElem, Algebra.smul_mul_assoc]
congr 1
rw [ofCrAnOpList_singleton, superCommute_ofCrAnOp_ofFieldOp_commute]
rw [ofCrAnList_singleton, superCommute_ofCrAnOp_ofFieldOp_commute]
rw [mul_assoc, ← ofFieldOpList_append]
congr
exact Eq.symm (List.eraseIdx_eq_take_drop_succ φs' ↑n)

6
HepLean/PerturbationTheory/FieldOpAlgebra/WicksTheoremNormal.lean
View file

@ -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 (𝓕 := 𝓕) [] = ofCrAnOpList [] := by rfl
have h1' : ofFieldOpList (𝓕 := 𝓕) [] = ofCrAnList [] := by rfl
rw [h1']
rw [normalOrder_ofCrAnOpList]
rw [normalOrder_ofCrAnList]
simp only [normalOrderSign_nil, normalOrderList_nil, one_smul]
rw [ofCrAnOpList, timeOrder_eq_ι_timeOrderF]
rw [ofCrAnList, timeOrder_eq_ι_timeOrderF]
rw [timeOrderF_ofCrAnListF]
simp