refactor: rename normalOrder for CrAnAlgebra
This commit is contained in:
jstoobysmith
parent
289050c829
commit
f5e7bbad59
5 changed files with 249 additions and 249 deletions
|
|
@ -32,24 +32,24 @@ noncomputable section
|
|||
a list of CrAnStates to the normal-ordered list of states multiplied by
|
||||
the sign corresponding to the number of fermionic-fermionic
|
||||
exchanges done in ordering. -/
|
||||
def normalOrder : CrAnAlgebra 𝓕 →ₗ[ℂ] CrAnAlgebra 𝓕 :=
|
||||
def normalOrderF : CrAnAlgebra 𝓕 →ₗ[ℂ] CrAnAlgebra 𝓕 :=
|
||||
Basis.constr ofCrAnListBasis ℂ fun φs =>
|
||||
normalOrderSign φs • ofCrAnList (normalOrderList φs)
|
||||
|
||||
@[inherit_doc normalOrder]
|
||||
scoped[FieldSpecification.CrAnAlgebra] notation "𝓝ᶠ(" a ")" => normalOrder a
|
||||
@[inherit_doc normalOrderF]
|
||||
scoped[FieldSpecification.CrAnAlgebra] notation "𝓝ᶠ(" a ")" => normalOrderF a
|
||||
|
||||
lemma normalOrder_ofCrAnList (φs : List 𝓕.CrAnStates) :
|
||||
lemma normalOrderF_ofCrAnList (φs : List 𝓕.CrAnStates) :
|
||||
𝓝ᶠ(ofCrAnList φs) = normalOrderSign φs • ofCrAnList (normalOrderList φs) := by
|
||||
rw [← ofListBasis_eq_ofList, normalOrder, Basis.constr_basis]
|
||||
rw [← ofListBasis_eq_ofList, normalOrderF, Basis.constr_basis]
|
||||
|
||||
lemma ofCrAnList_eq_normalOrder (φs : List 𝓕.CrAnStates) :
|
||||
lemma ofCrAnList_eq_normalOrderF (φs : List 𝓕.CrAnStates) :
|
||||
ofCrAnList (normalOrderList φs) = normalOrderSign φs • 𝓝ᶠ(ofCrAnList φs) := by
|
||||
rw [normalOrder_ofCrAnList, normalOrderList, smul_smul, normalOrderSign, Wick.koszulSign_mul_self,
|
||||
rw [normalOrderF_ofCrAnList, normalOrderList, smul_smul, normalOrderSign, Wick.koszulSign_mul_self,
|
||||
one_smul]
|
||||
|
||||
lemma normalOrder_one : normalOrder (𝓕 := 𝓕) 1 = 1 := by
|
||||
rw [← ofCrAnList_nil, normalOrder_ofCrAnList, normalOrderSign_nil, normalOrderList_nil,
|
||||
lemma normalOrderF_one : normalOrderF (𝓕 := 𝓕) 1 = 1 := by
|
||||
rw [← ofCrAnList_nil, normalOrderF_ofCrAnList, normalOrderSign_nil, normalOrderList_nil,
|
||||
ofCrAnList_nil, one_smul]
|
||||
|
||||
/-!
|
||||
|
|
@ -58,130 +58,130 @@ lemma normalOrder_one : normalOrder (𝓕 := 𝓕) 1 = 1 := by
|
|||
|
||||
-/
|
||||
|
||||
lemma normalOrder_ofCrAnList_cons_create (φ : 𝓕.CrAnStates)
|
||||
lemma normalOrderF_ofCrAnList_cons_create (φ : 𝓕.CrAnStates)
|
||||
(hφ : 𝓕 |>ᶜ φ = CreateAnnihilate.create) (φs : List 𝓕.CrAnStates) :
|
||||
𝓝ᶠ(ofCrAnList (φ :: φs)) = ofCrAnState φ * 𝓝ᶠ(ofCrAnList φs) := by
|
||||
rw [normalOrder_ofCrAnList, normalOrderSign_cons_create φ hφ, normalOrderList_cons_create φ hφ φs]
|
||||
rw [ofCrAnList_cons, normalOrder_ofCrAnList, mul_smul_comm]
|
||||
rw [normalOrderF_ofCrAnList, normalOrderSign_cons_create φ hφ, normalOrderList_cons_create φ hφ φs]
|
||||
rw [ofCrAnList_cons, normalOrderF_ofCrAnList, mul_smul_comm]
|
||||
|
||||
lemma normalOrder_create_mul (φ : 𝓕.CrAnStates)
|
||||
lemma normalOrderF_create_mul (φ : 𝓕.CrAnStates)
|
||||
(hφ : 𝓕 |>ᶜ φ = CreateAnnihilate.create) (a : CrAnAlgebra 𝓕) :
|
||||
𝓝ᶠ(ofCrAnState φ * a) = ofCrAnState φ * 𝓝ᶠ(a) := by
|
||||
change (normalOrder ∘ₗ mulLinearMap (ofCrAnState φ)) a =
|
||||
(mulLinearMap (ofCrAnState φ) ∘ₗ normalOrder) a
|
||||
change (normalOrderF ∘ₗ mulLinearMap (ofCrAnState φ)) a =
|
||||
(mulLinearMap (ofCrAnState φ) ∘ₗ normalOrderF) a
|
||||
refine LinearMap.congr_fun (ofCrAnListBasis.ext fun l ↦ ?_) a
|
||||
simp only [mulLinearMap, LinearMap.coe_mk, AddHom.coe_mk, ofListBasis_eq_ofList,
|
||||
LinearMap.coe_comp, Function.comp_apply]
|
||||
rw [← ofCrAnList_cons, normalOrder_ofCrAnList_cons_create φ hφ]
|
||||
rw [← ofCrAnList_cons, normalOrderF_ofCrAnList_cons_create φ hφ]
|
||||
|
||||
lemma normalOrder_ofCrAnList_append_annihilate (φ : 𝓕.CrAnStates)
|
||||
lemma normalOrderF_ofCrAnList_append_annihilate (φ : 𝓕.CrAnStates)
|
||||
(hφ : 𝓕 |>ᶜ φ = CreateAnnihilate.annihilate) (φs : List 𝓕.CrAnStates) :
|
||||
𝓝ᶠ(ofCrAnList (φs ++ [φ])) = 𝓝ᶠ(ofCrAnList φs) * ofCrAnState φ := by
|
||||
rw [normalOrder_ofCrAnList, normalOrderSign_append_annihlate φ hφ φs,
|
||||
rw [normalOrderF_ofCrAnList, normalOrderSign_append_annihlate φ hφ φs,
|
||||
normalOrderList_append_annihilate φ hφ φs, ofCrAnList_append, ofCrAnList_singleton,
|
||||
normalOrder_ofCrAnList, smul_mul_assoc]
|
||||
normalOrderF_ofCrAnList, smul_mul_assoc]
|
||||
|
||||
lemma normalOrder_mul_annihilate (φ : 𝓕.CrAnStates)
|
||||
lemma normalOrderF_mul_annihilate (φ : 𝓕.CrAnStates)
|
||||
(hφ : 𝓕 |>ᶜ φ = CreateAnnihilate.annihilate)
|
||||
(a : CrAnAlgebra 𝓕) : 𝓝ᶠ(a * ofCrAnState φ) = 𝓝ᶠ(a) * ofCrAnState φ := by
|
||||
change (normalOrder ∘ₗ mulLinearMap.flip (ofCrAnState φ)) a =
|
||||
(mulLinearMap.flip (ofCrAnState φ) ∘ₗ normalOrder) a
|
||||
change (normalOrderF ∘ₗ mulLinearMap.flip (ofCrAnState φ)) a =
|
||||
(mulLinearMap.flip (ofCrAnState φ) ∘ₗ normalOrderF) a
|
||||
refine LinearMap.congr_fun (ofCrAnListBasis.ext fun l ↦ ?_) a
|
||||
simp only [mulLinearMap, ofListBasis_eq_ofList, LinearMap.coe_comp, Function.comp_apply,
|
||||
LinearMap.flip_apply, LinearMap.coe_mk, AddHom.coe_mk]
|
||||
rw [← ofCrAnList_singleton, ← ofCrAnList_append, ofCrAnList_singleton,
|
||||
normalOrder_ofCrAnList_append_annihilate φ hφ]
|
||||
normalOrderF_ofCrAnList_append_annihilate φ hφ]
|
||||
|
||||
lemma normalOrder_crPart_mul (φ : 𝓕.States) (a : CrAnAlgebra 𝓕) :
|
||||
lemma normalOrderF_crPart_mul (φ : 𝓕.States) (a : CrAnAlgebra 𝓕) :
|
||||
𝓝ᶠ(crPart φ * a) =
|
||||
crPart φ * 𝓝ᶠ(a) := by
|
||||
match φ with
|
||||
| .inAsymp φ =>
|
||||
rw [crPart]
|
||||
exact normalOrder_create_mul ⟨States.inAsymp φ, ()⟩ rfl a
|
||||
exact normalOrderF_create_mul ⟨States.inAsymp φ, ()⟩ rfl a
|
||||
| .position φ =>
|
||||
rw [crPart]
|
||||
exact normalOrder_create_mul _ rfl _
|
||||
exact normalOrderF_create_mul _ rfl _
|
||||
| .outAsymp φ => simp
|
||||
|
||||
lemma normalOrder_mul_anPart (φ : 𝓕.States) (a : CrAnAlgebra 𝓕) :
|
||||
lemma normalOrderF_mul_anPart (φ : 𝓕.States) (a : CrAnAlgebra 𝓕) :
|
||||
𝓝ᶠ(a * anPart φ) =
|
||||
𝓝ᶠ(a) * anPart φ := by
|
||||
match φ with
|
||||
| .inAsymp φ => simp
|
||||
| .position φ =>
|
||||
rw [anPart]
|
||||
exact normalOrder_mul_annihilate _ rfl _
|
||||
exact normalOrderF_mul_annihilate _ rfl _
|
||||
| .outAsymp φ =>
|
||||
rw [anPart]
|
||||
refine normalOrder_mul_annihilate _ rfl _
|
||||
refine normalOrderF_mul_annihilate _ rfl _
|
||||
|
||||
/-!
|
||||
|
||||
## Normal ordering for an adjacent creation and annihliation state
|
||||
|
||||
The main result of this section is `normalOrder_superCommuteF_annihilate_create`.
|
||||
The main result of this section is `normalOrderF_superCommuteF_annihilate_create`.
|
||||
-/
|
||||
|
||||
lemma normalOrder_swap_create_annihlate_ofCrAnList_ofCrAnList (φc φa : 𝓕.CrAnStates)
|
||||
lemma normalOrderF_swap_create_annihlate_ofCrAnList_ofCrAnList (φc φa : 𝓕.CrAnStates)
|
||||
(hφc : 𝓕 |>ᶜ φc = CreateAnnihilate.create) (hφa : 𝓕 |>ᶜ φa = CreateAnnihilate.annihilate)
|
||||
(φs φs' : List 𝓕.CrAnStates) :
|
||||
𝓝ᶠ(ofCrAnList φs' * ofCrAnState φc * ofCrAnState φa * ofCrAnList φs) = 𝓢(𝓕 |>ₛ φc, 𝓕 |>ₛ φa) •
|
||||
𝓝ᶠ(ofCrAnList φs' * ofCrAnState φa * ofCrAnState φc * ofCrAnList φs) := by
|
||||
rw [mul_assoc, mul_assoc, ← ofCrAnList_cons, ← ofCrAnList_cons, ← ofCrAnList_append]
|
||||
rw [normalOrder_ofCrAnList, normalOrderSign_swap_create_annihlate φc φa hφc hφa]
|
||||
rw [normalOrderList_swap_create_annihlate φc φa hφc hφa, ← smul_smul, ← normalOrder_ofCrAnList]
|
||||
rw [normalOrderF_ofCrAnList, normalOrderSign_swap_create_annihlate φc φa hφc hφa]
|
||||
rw [normalOrderList_swap_create_annihlate φc φa hφc hφa, ← smul_smul, ← normalOrderF_ofCrAnList]
|
||||
rw [ofCrAnList_append, ofCrAnList_cons, ofCrAnList_cons]
|
||||
noncomm_ring
|
||||
|
||||
lemma normalOrder_swap_create_annihlate_ofCrAnList (φc φa : 𝓕.CrAnStates)
|
||||
lemma normalOrderF_swap_create_annihlate_ofCrAnList (φc φa : 𝓕.CrAnStates)
|
||||
(hφc : 𝓕 |>ᶜ φc = CreateAnnihilate.create) (hφa : 𝓕 |>ᶜ φa = CreateAnnihilate.annihilate)
|
||||
(φs : List 𝓕.CrAnStates) (a : 𝓕.CrAnAlgebra) :
|
||||
𝓝ᶠ(ofCrAnList φs * ofCrAnState φc * ofCrAnState φa * a) = 𝓢(𝓕 |>ₛ φc, 𝓕 |>ₛ φa) •
|
||||
𝓝ᶠ(ofCrAnList φs * ofCrAnState φa * ofCrAnState φc * a) := by
|
||||
change (normalOrder ∘ₗ mulLinearMap (ofCrAnList φs * ofCrAnState φc * ofCrAnState φa)) a =
|
||||
(smulLinearMap _ ∘ₗ normalOrder ∘ₗ
|
||||
change (normalOrderF ∘ₗ mulLinearMap (ofCrAnList φs * ofCrAnState φc * ofCrAnState φa)) a =
|
||||
(smulLinearMap _ ∘ₗ normalOrderF ∘ₗ
|
||||
mulLinearMap (ofCrAnList φs * ofCrAnState φa * ofCrAnState φc)) a
|
||||
refine LinearMap.congr_fun (ofCrAnListBasis.ext fun l ↦ ?_) a
|
||||
simp only [mulLinearMap, LinearMap.coe_mk, AddHom.coe_mk, ofListBasis_eq_ofList,
|
||||
LinearMap.coe_comp, Function.comp_apply, instCommGroup.eq_1]
|
||||
rw [normalOrder_swap_create_annihlate_ofCrAnList_ofCrAnList φc φa hφc hφa]
|
||||
rw [normalOrderF_swap_create_annihlate_ofCrAnList_ofCrAnList φc φa hφc hφa]
|
||||
rfl
|
||||
|
||||
lemma normalOrder_swap_create_annihlate (φc φa : 𝓕.CrAnStates)
|
||||
lemma normalOrderF_swap_create_annihlate (φc φa : 𝓕.CrAnStates)
|
||||
(hφc : 𝓕 |>ᶜ φc = CreateAnnihilate.create) (hφa : 𝓕 |>ᶜ φa = CreateAnnihilate.annihilate)
|
||||
(a b : 𝓕.CrAnAlgebra) :
|
||||
𝓝ᶠ(a * ofCrAnState φc * ofCrAnState φa * b) = 𝓢(𝓕 |>ₛ φc, 𝓕 |>ₛ φa) •
|
||||
𝓝ᶠ(a * ofCrAnState φa * ofCrAnState φc * b) := by
|
||||
rw [mul_assoc, mul_assoc, mul_assoc, mul_assoc]
|
||||
change (normalOrder ∘ₗ mulLinearMap.flip (ofCrAnState φc * (ofCrAnState φa * b))) a =
|
||||
change (normalOrderF ∘ₗ mulLinearMap.flip (ofCrAnState φc * (ofCrAnState φa * b))) a =
|
||||
(smulLinearMap (𝓢(𝓕 |>ₛ φc, 𝓕 |>ₛ φa)) ∘ₗ
|
||||
normalOrder ∘ₗ mulLinearMap.flip (ofCrAnState φa * (ofCrAnState φc * b))) a
|
||||
normalOrderF ∘ₗ mulLinearMap.flip (ofCrAnState φa * (ofCrAnState φc * b))) a
|
||||
refine LinearMap.congr_fun (ofCrAnListBasis.ext fun l ↦ ?_) _
|
||||
simp only [mulLinearMap, ofListBasis_eq_ofList, LinearMap.coe_comp, Function.comp_apply,
|
||||
LinearMap.flip_apply, LinearMap.coe_mk, AddHom.coe_mk, instCommGroup.eq_1, ← mul_assoc,
|
||||
normalOrder_swap_create_annihlate_ofCrAnList φc φa hφc hφa]
|
||||
normalOrderF_swap_create_annihlate_ofCrAnList φc φa hφc hφa]
|
||||
rfl
|
||||
|
||||
lemma normalOrder_superCommuteF_create_annihilate (φc φa : 𝓕.CrAnStates)
|
||||
lemma normalOrderF_superCommuteF_create_annihilate (φc φa : 𝓕.CrAnStates)
|
||||
(hφc : 𝓕 |>ᶜ φc = CreateAnnihilate.create) (hφa : 𝓕 |>ᶜ φa = CreateAnnihilate.annihilate)
|
||||
(a b : 𝓕.CrAnAlgebra) :
|
||||
𝓝ᶠ(a * [ofCrAnState φc, ofCrAnState φa]ₛca * b) = 0 := by
|
||||
simp only [superCommuteF_ofCrAnState_ofCrAnState, instCommGroup.eq_1, Algebra.smul_mul_assoc]
|
||||
rw [mul_sub, sub_mul, map_sub, ← smul_mul_assoc, ← mul_assoc, ← mul_assoc,
|
||||
normalOrder_swap_create_annihlate φc φa hφc hφa]
|
||||
normalOrderF_swap_create_annihlate φc φa hφc hφa]
|
||||
simp
|
||||
|
||||
lemma normalOrder_superCommuteF_annihilate_create (φc φa : 𝓕.CrAnStates)
|
||||
lemma normalOrderF_superCommuteF_annihilate_create (φc φa : 𝓕.CrAnStates)
|
||||
(hφc : 𝓕 |>ᶜ φc = CreateAnnihilate.create) (hφa : 𝓕 |>ᶜ φa = CreateAnnihilate.annihilate)
|
||||
(a b : 𝓕.CrAnAlgebra) :
|
||||
𝓝ᶠ(a * [ofCrAnState φa, ofCrAnState φc]ₛca * b) = 0 := by
|
||||
rw [superCommuteF_ofCrAnState_ofCrAnState_symm]
|
||||
simp only [instCommGroup.eq_1, neg_smul, mul_neg, Algebra.mul_smul_comm, neg_mul,
|
||||
Algebra.smul_mul_assoc, map_neg, map_smul, neg_eq_zero, smul_eq_zero]
|
||||
exact Or.inr (normalOrder_superCommuteF_create_annihilate φc φa hφc hφa ..)
|
||||
exact Or.inr (normalOrderF_superCommuteF_create_annihilate φc φa hφc hφa ..)
|
||||
|
||||
lemma normalOrder_swap_crPart_anPart (φ φ' : 𝓕.States) (a b : CrAnAlgebra 𝓕) :
|
||||
lemma normalOrderF_swap_crPart_anPart (φ φ' : 𝓕.States) (a b : CrAnAlgebra 𝓕) :
|
||||
𝓝ᶠ(a * (crPart φ) * (anPart φ') * b) =
|
||||
𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') •
|
||||
𝓝ᶠ(a * (anPart φ') * (crPart φ) * b) := by
|
||||
|
|
@ -190,22 +190,22 @@ lemma normalOrder_swap_crPart_anPart (φ φ' : 𝓕.States) (a b : CrAnAlgebra
|
|||
| .outAsymp φ, _ => simp
|
||||
| .position φ, .position φ' =>
|
||||
simp only [crPart_position, anPart_position, instCommGroup.eq_1]
|
||||
rw [normalOrder_swap_create_annihlate]
|
||||
rw [normalOrderF_swap_create_annihlate]
|
||||
simp only [instCommGroup.eq_1, crAnStatistics, Function.comp_apply, crAnStatesToStates_prod]
|
||||
rfl; rfl
|
||||
| .inAsymp φ, .outAsymp φ' =>
|
||||
simp only [crPart_negAsymp, anPart_posAsymp, instCommGroup.eq_1]
|
||||
rw [normalOrder_swap_create_annihlate]
|
||||
rw [normalOrderF_swap_create_annihlate]
|
||||
simp only [instCommGroup.eq_1, crAnStatistics, Function.comp_apply, crAnStatesToStates_prod]
|
||||
rfl; rfl
|
||||
| .inAsymp φ, .position φ' =>
|
||||
simp only [crPart_negAsymp, anPart_position, instCommGroup.eq_1]
|
||||
rw [normalOrder_swap_create_annihlate]
|
||||
rw [normalOrderF_swap_create_annihlate]
|
||||
simp only [instCommGroup.eq_1, crAnStatistics, Function.comp_apply, crAnStatesToStates_prod]
|
||||
rfl; rfl
|
||||
| .position φ, .outAsymp φ' =>
|
||||
simp only [crPart_position, anPart_posAsymp, instCommGroup.eq_1]
|
||||
rw [normalOrder_swap_create_annihlate]
|
||||
rw [normalOrderF_swap_create_annihlate]
|
||||
simp only [instCommGroup.eq_1, crAnStatistics, Function.comp_apply, crAnStatesToStates_prod]
|
||||
rfl; rfl
|
||||
|
||||
|
|
@ -217,13 +217,13 @@ Using the results from above.
|
|||
|
||||
-/
|
||||
|
||||
lemma normalOrder_swap_anPart_crPart (φ φ' : 𝓕.States) (a b : CrAnAlgebra 𝓕) :
|
||||
lemma normalOrderF_swap_anPart_crPart (φ φ' : 𝓕.States) (a b : CrAnAlgebra 𝓕) :
|
||||
𝓝ᶠ(a * (anPart φ) * (crPart φ') * b) =
|
||||
𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') • 𝓝ᶠ(a * (crPart φ') *
|
||||
(anPart φ) * b) := by
|
||||
simp [normalOrder_swap_crPart_anPart, smul_smul]
|
||||
simp [normalOrderF_swap_crPart_anPart, smul_smul]
|
||||
|
||||
lemma normalOrder_superCommuteF_crPart_anPart (φ φ' : 𝓕.States) (a b : CrAnAlgebra 𝓕) :
|
||||
lemma normalOrderF_superCommuteF_crPart_anPart (φ φ' : 𝓕.States) (a b : CrAnAlgebra 𝓕) :
|
||||
𝓝ᶠ(a * superCommuteF
|
||||
(crPart φ) (anPart φ') * b) = 0 := by
|
||||
match φ, φ' with
|
||||
|
|
@ -231,18 +231,18 @@ lemma normalOrder_superCommuteF_crPart_anPart (φ φ' : 𝓕.States) (a b : CrAn
|
|||
| .outAsymp φ', _ => simp
|
||||
| .position φ, .position φ' =>
|
||||
rw [crPart_position, anPart_position]
|
||||
exact normalOrder_superCommuteF_create_annihilate _ _ rfl rfl ..
|
||||
exact normalOrderF_superCommuteF_create_annihilate _ _ rfl rfl ..
|
||||
| .inAsymp φ, .outAsymp φ' =>
|
||||
rw [crPart_negAsymp, anPart_posAsymp]
|
||||
exact normalOrder_superCommuteF_create_annihilate _ _ rfl rfl ..
|
||||
exact normalOrderF_superCommuteF_create_annihilate _ _ rfl rfl ..
|
||||
| .inAsymp φ, .position φ' =>
|
||||
rw [crPart_negAsymp, anPart_position]
|
||||
exact normalOrder_superCommuteF_create_annihilate _ _ rfl rfl ..
|
||||
exact normalOrderF_superCommuteF_create_annihilate _ _ rfl rfl ..
|
||||
| .position φ, .outAsymp φ' =>
|
||||
rw [crPart_position, anPart_posAsymp]
|
||||
exact normalOrder_superCommuteF_create_annihilate _ _ rfl rfl ..
|
||||
exact normalOrderF_superCommuteF_create_annihilate _ _ rfl rfl ..
|
||||
|
||||
lemma normalOrder_superCommuteF_anPart_crPart (φ φ' : 𝓕.States) (a b : CrAnAlgebra 𝓕) :
|
||||
lemma normalOrderF_superCommuteF_anPart_crPart (φ φ' : 𝓕.States) (a b : CrAnAlgebra 𝓕) :
|
||||
𝓝ᶠ(a * superCommuteF
|
||||
(anPart φ) (crPart φ') * b) = 0 := by
|
||||
match φ, φ' with
|
||||
|
|
@ -250,16 +250,16 @@ lemma normalOrder_superCommuteF_anPart_crPart (φ φ' : 𝓕.States) (a b : CrAn
|
|||
| _, .outAsymp φ' => simp
|
||||
| .position φ, .position φ' =>
|
||||
rw [anPart_position, crPart_position]
|
||||
exact normalOrder_superCommuteF_annihilate_create _ _ rfl rfl ..
|
||||
exact normalOrderF_superCommuteF_annihilate_create _ _ rfl rfl ..
|
||||
| .outAsymp φ', .inAsymp φ =>
|
||||
simp only [anPart_posAsymp, crPart_negAsymp]
|
||||
exact normalOrder_superCommuteF_annihilate_create _ _ rfl rfl ..
|
||||
exact normalOrderF_superCommuteF_annihilate_create _ _ rfl rfl ..
|
||||
| .position φ', .inAsymp φ =>
|
||||
simp only [anPart_position, crPart_negAsymp]
|
||||
exact normalOrder_superCommuteF_annihilate_create _ _ rfl rfl ..
|
||||
exact normalOrderF_superCommuteF_annihilate_create _ _ rfl rfl ..
|
||||
| .outAsymp φ, .position φ' =>
|
||||
simp only [anPart_posAsymp, crPart_position]
|
||||
exact normalOrder_superCommuteF_annihilate_create _ _ rfl rfl ..
|
||||
exact normalOrderF_superCommuteF_annihilate_create _ _ rfl rfl ..
|
||||
|
||||
/-!
|
||||
|
||||
|
|
@ -268,44 +268,44 @@ lemma normalOrder_superCommuteF_anPart_crPart (φ φ' : 𝓕.States) (a b : CrAn
|
|||
-/
|
||||
|
||||
@[simp]
|
||||
lemma normalOrder_crPart_mul_crPart (φ φ' : 𝓕.States) :
|
||||
lemma normalOrderF_crPart_mul_crPart (φ φ' : 𝓕.States) :
|
||||
𝓝ᶠ(crPart φ * crPart φ') =
|
||||
crPart φ * crPart φ' := by
|
||||
rw [normalOrder_crPart_mul]
|
||||
rw [normalOrderF_crPart_mul]
|
||||
conv_lhs => rw [← mul_one (crPart φ')]
|
||||
rw [normalOrder_crPart_mul, normalOrder_one]
|
||||
rw [normalOrderF_crPart_mul, normalOrderF_one]
|
||||
simp
|
||||
|
||||
@[simp]
|
||||
lemma normalOrder_anPart_mul_anPart (φ φ' : 𝓕.States) :
|
||||
lemma normalOrderF_anPart_mul_anPart (φ φ' : 𝓕.States) :
|
||||
𝓝ᶠ(anPart φ * anPart φ') =
|
||||
anPart φ * anPart φ' := by
|
||||
rw [normalOrder_mul_anPart]
|
||||
rw [normalOrderF_mul_anPart]
|
||||
conv_lhs => rw [← one_mul (anPart φ)]
|
||||
rw [normalOrder_mul_anPart, normalOrder_one]
|
||||
rw [normalOrderF_mul_anPart, normalOrderF_one]
|
||||
simp
|
||||
|
||||
@[simp]
|
||||
lemma normalOrder_crPart_mul_anPart (φ φ' : 𝓕.States) :
|
||||
lemma normalOrderF_crPart_mul_anPart (φ φ' : 𝓕.States) :
|
||||
𝓝ᶠ(crPart φ * anPart φ') =
|
||||
crPart φ * anPart φ' := by
|
||||
rw [normalOrder_crPart_mul]
|
||||
rw [normalOrderF_crPart_mul]
|
||||
conv_lhs => rw [← one_mul (anPart φ')]
|
||||
rw [normalOrder_mul_anPart, normalOrder_one]
|
||||
rw [normalOrderF_mul_anPart, normalOrderF_one]
|
||||
simp
|
||||
|
||||
@[simp]
|
||||
lemma normalOrder_anPart_mul_crPart (φ φ' : 𝓕.States) :
|
||||
lemma normalOrderF_anPart_mul_crPart (φ φ' : 𝓕.States) :
|
||||
𝓝ᶠ(anPart φ * crPart φ') =
|
||||
𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') •
|
||||
(crPart φ' * anPart φ) := by
|
||||
conv_lhs => rw [← one_mul (anPart φ * crPart φ')]
|
||||
conv_lhs => rw [← mul_one (1 * (anPart φ *
|
||||
crPart φ'))]
|
||||
rw [← mul_assoc, normalOrder_swap_anPart_crPart]
|
||||
rw [← mul_assoc, normalOrderF_swap_anPart_crPart]
|
||||
simp
|
||||
|
||||
lemma normalOrder_ofState_mul_ofState (φ φ' : 𝓕.States) :
|
||||
lemma normalOrderF_ofState_mul_ofState (φ φ' : 𝓕.States) :
|
||||
𝓝ᶠ(ofState φ * ofState φ') =
|
||||
crPart φ * crPart φ' +
|
||||
𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') •
|
||||
|
|
@ -313,8 +313,8 @@ lemma normalOrder_ofState_mul_ofState (φ φ' : 𝓕.States) :
|
|||
crPart φ * anPart φ' +
|
||||
anPart φ * anPart φ' := by
|
||||
rw [ofState_eq_crPart_add_anPart, ofState_eq_crPart_add_anPart, mul_add, add_mul, add_mul]
|
||||
simp only [map_add, normalOrder_crPart_mul_crPart, normalOrder_anPart_mul_crPart,
|
||||
instCommGroup.eq_1, normalOrder_crPart_mul_anPart, normalOrder_anPart_mul_anPart]
|
||||
simp only [map_add, normalOrderF_crPart_mul_crPart, normalOrderF_anPart_mul_crPart,
|
||||
instCommGroup.eq_1, normalOrderF_crPart_mul_anPart, normalOrderF_anPart_mul_anPart]
|
||||
abel
|
||||
|
||||
/-!
|
||||
|
|
@ -325,7 +325,7 @@ lemma normalOrder_ofState_mul_ofState (φ φ' : 𝓕.States) :
|
|||
|
||||
TODO "Split the following two lemmas up into smaller parts."
|
||||
|
||||
lemma normalOrder_superCommuteF_ofCrAnList_create_create_ofCrAnList
|
||||
lemma normalOrderF_superCommuteF_ofCrAnList_create_create_ofCrAnList
|
||||
(φc φc' : 𝓕.CrAnStates) (hφc : 𝓕 |>ᶜ φc = CreateAnnihilate.create)
|
||||
(hφc' : 𝓕 |>ᶜ φc' = CreateAnnihilate.create) (φs φs' : List 𝓕.CrAnStates) :
|
||||
(𝓝ᶠ(ofCrAnList φs * [ofCrAnState φc, ofCrAnState φc']ₛca * ofCrAnList φs')) =
|
||||
|
|
@ -339,7 +339,7 @@ lemma normalOrder_superCommuteF_ofCrAnList_create_create_ofCrAnList
|
|||
← ofCrAnList_append]
|
||||
conv_lhs =>
|
||||
lhs
|
||||
rw [normalOrder_ofCrAnList, normalOrderList_eq_createFilter_append_annihilateFilter]
|
||||
rw [normalOrderF_ofCrAnList, normalOrderList_eq_createFilter_append_annihilateFilter]
|
||||
rw [createFilter_append, createFilter_append, createFilter_append,
|
||||
createFilter_singleton_create _ hφc, createFilter_singleton_create _ hφc']
|
||||
rw [annihilateFilter_append, annihilateFilter_append, annihilateFilter_append,
|
||||
|
|
@ -358,7 +358,7 @@ lemma normalOrder_superCommuteF_ofCrAnList_create_create_ofCrAnList
|
|||
rhs
|
||||
rw [map_smul]
|
||||
rhs
|
||||
rw [normalOrder_ofCrAnList, normalOrderList_eq_createFilter_append_annihilateFilter]
|
||||
rw [normalOrderF_ofCrAnList, normalOrderList_eq_createFilter_append_annihilateFilter]
|
||||
rw [createFilter_append, createFilter_append, createFilter_append,
|
||||
createFilter_singleton_create _ hφc, createFilter_singleton_create _ hφc']
|
||||
rw [annihilateFilter_append, annihilateFilter_append, annihilateFilter_append,
|
||||
|
|
@ -384,7 +384,7 @@ lemma normalOrder_superCommuteF_ofCrAnList_create_create_ofCrAnList
|
|||
ofCrAnList_singleton]
|
||||
rw [ofCrAnList_append, ofCrAnList_singleton, ofCrAnList_singleton, smul_mul_assoc]
|
||||
|
||||
lemma normalOrder_superCommuteF_ofCrAnList_annihilate_annihilate_ofCrAnList
|
||||
lemma normalOrderF_superCommuteF_ofCrAnList_annihilate_annihilate_ofCrAnList
|
||||
(φa φa' : 𝓕.CrAnStates)
|
||||
(hφa : 𝓕 |>ᶜ φa = CreateAnnihilate.annihilate)
|
||||
(hφa' : 𝓕 |>ᶜ φa' = CreateAnnihilate.annihilate)
|
||||
|
|
@ -401,7 +401,7 @@ lemma normalOrder_superCommuteF_ofCrAnList_annihilate_annihilate_ofCrAnList
|
|||
← ofCrAnList_append]
|
||||
conv_lhs =>
|
||||
lhs
|
||||
rw [normalOrder_ofCrAnList, normalOrderList_eq_createFilter_append_annihilateFilter]
|
||||
rw [normalOrderF_ofCrAnList, normalOrderList_eq_createFilter_append_annihilateFilter]
|
||||
rw [createFilter_append, createFilter_append, createFilter_append,
|
||||
createFilter_singleton_annihilate _ hφa, createFilter_singleton_annihilate _ hφa']
|
||||
rw [annihilateFilter_append, annihilateFilter_append, annihilateFilter_append,
|
||||
|
|
@ -421,7 +421,7 @@ lemma normalOrder_superCommuteF_ofCrAnList_annihilate_annihilate_ofCrAnList
|
|||
rhs
|
||||
rw [map_smul]
|
||||
rhs
|
||||
rw [normalOrder_ofCrAnList, normalOrderList_eq_createFilter_append_annihilateFilter]
|
||||
rw [normalOrderF_ofCrAnList, normalOrderList_eq_createFilter_append_annihilateFilter]
|
||||
rw [createFilter_append, createFilter_append, createFilter_append,
|
||||
createFilter_singleton_annihilate _ hφa, createFilter_singleton_annihilate _ hφa']
|
||||
rw [annihilateFilter_append, annihilateFilter_append, annihilateFilter_append,
|
||||
|
|
@ -458,14 +458,14 @@ lemma normalOrder_superCommuteF_ofCrAnList_annihilate_annihilate_ofCrAnList
|
|||
|
||||
-/
|
||||
|
||||
lemma ofCrAnList_superCommuteF_normalOrder_ofCrAnList (φs φs' : List 𝓕.CrAnStates) :
|
||||
lemma ofCrAnList_superCommuteF_normalOrderF_ofCrAnList (φs φs' : List 𝓕.CrAnStates) :
|
||||
[ofCrAnList φs, 𝓝ᶠ(ofCrAnList φs')]ₛca =
|
||||
ofCrAnList φs * 𝓝ᶠ(ofCrAnList φs') -
|
||||
𝓢(𝓕 |>ₛ φs, 𝓕 |>ₛ φs') • 𝓝ᶠ(ofCrAnList φs') * ofCrAnList φs := by
|
||||
simp [normalOrder_ofCrAnList, map_smul, superCommuteF_ofCrAnList_ofCrAnList, ofCrAnList_append,
|
||||
simp [normalOrderF_ofCrAnList, map_smul, superCommuteF_ofCrAnList_ofCrAnList, ofCrAnList_append,
|
||||
smul_sub, smul_smul, mul_comm]
|
||||
|
||||
lemma ofCrAnList_superCommuteF_normalOrder_ofStateList (φs : List 𝓕.CrAnStates)
|
||||
lemma ofCrAnList_superCommuteF_normalOrderF_ofStateList (φs : List 𝓕.CrAnStates)
|
||||
(φs' : List 𝓕.States) : [ofCrAnList φs, 𝓝ᶠ(ofStateList φs')]ₛca =
|
||||
ofCrAnList φs * 𝓝ᶠ(ofStateList φs') -
|
||||
𝓢(𝓕 |>ₛ φs, 𝓕 |>ₛ φs') • 𝓝ᶠ(ofStateList φs') * ofCrAnList φs := by
|
||||
|
|
@ -473,7 +473,7 @@ lemma ofCrAnList_superCommuteF_normalOrder_ofStateList (φs : List 𝓕.CrAnStat
|
|||
← Finset.sum_sub_distrib, map_sum]
|
||||
congr
|
||||
funext n
|
||||
rw [ofCrAnList_superCommuteF_normalOrder_ofCrAnList,
|
||||
rw [ofCrAnList_superCommuteF_normalOrderF_ofCrAnList,
|
||||
CrAnSection.statistics_eq_state_statistics]
|
||||
|
||||
/-!
|
||||
|
|
@ -482,29 +482,29 @@ lemma ofCrAnList_superCommuteF_normalOrder_ofStateList (φs : List 𝓕.CrAnStat
|
|||
|
||||
-/
|
||||
|
||||
lemma ofCrAnList_mul_normalOrder_ofStateList_eq_superCommuteF (φs : List 𝓕.CrAnStates)
|
||||
lemma ofCrAnList_mul_normalOrderF_ofStateList_eq_superCommuteF (φs : List 𝓕.CrAnStates)
|
||||
(φs' : List 𝓕.States) :
|
||||
ofCrAnList φs * 𝓝ᶠ(ofStateList φs') =
|
||||
𝓢(𝓕 |>ₛ φs, 𝓕 |>ₛ φs') • 𝓝ᶠ(ofStateList φs') * ofCrAnList φs
|
||||
+ [ofCrAnList φs, 𝓝ᶠ(ofStateList φs')]ₛca := by
|
||||
simp [ofCrAnList_superCommuteF_normalOrder_ofStateList]
|
||||
simp [ofCrAnList_superCommuteF_normalOrderF_ofStateList]
|
||||
|
||||
lemma ofCrAnState_mul_normalOrder_ofStateList_eq_superCommuteF (φ : 𝓕.CrAnStates)
|
||||
lemma ofCrAnState_mul_normalOrderF_ofStateList_eq_superCommuteF (φ : 𝓕.CrAnStates)
|
||||
(φs' : List 𝓕.States) : ofCrAnState φ * 𝓝ᶠ(ofStateList φs') =
|
||||
𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φs') • 𝓝ᶠ(ofStateList φs') * ofCrAnState φ
|
||||
+ [ofCrAnState φ, 𝓝ᶠ(ofStateList φs')]ₛca := by
|
||||
simp [← ofCrAnList_singleton, ofCrAnList_mul_normalOrder_ofStateList_eq_superCommuteF]
|
||||
simp [← ofCrAnList_singleton, ofCrAnList_mul_normalOrderF_ofStateList_eq_superCommuteF]
|
||||
|
||||
lemma anPart_mul_normalOrder_ofStateList_eq_superCommuteF (φ : 𝓕.States)
|
||||
lemma anPart_mul_normalOrderF_ofStateList_eq_superCommuteF (φ : 𝓕.States)
|
||||
(φs' : List 𝓕.States) :
|
||||
anPart φ * 𝓝ᶠ(ofStateList φs') =
|
||||
𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φs') • 𝓝ᶠ(ofStateList φs' * anPart φ)
|
||||
+ [anPart φ, 𝓝ᶠ(ofStateList φs')]ₛca := by
|
||||
rw [normalOrder_mul_anPart]
|
||||
rw [normalOrderF_mul_anPart]
|
||||
match φ with
|
||||
| .inAsymp φ => simp
|
||||
| .position φ => simp [ofCrAnState_mul_normalOrder_ofStateList_eq_superCommuteF, crAnStatistics]
|
||||
| .outAsymp φ => simp [ofCrAnState_mul_normalOrder_ofStateList_eq_superCommuteF, crAnStatistics]
|
||||
| .position φ => simp [ofCrAnState_mul_normalOrderF_ofStateList_eq_superCommuteF, crAnStatistics]
|
||||
| .outAsymp φ => simp [ofCrAnState_mul_normalOrderF_ofStateList_eq_superCommuteF, crAnStatistics]
|
||||
|
||||
end
|
||||
|
||||
|
|
|
|||
|
|
@ -24,53 +24,53 @@ variable {𝓕 : FieldSpecification}
|
|||
## Normal order on super-commutators.
|
||||
|
||||
The main result of this is
|
||||
`ι_normalOrder_superCommuteF_eq_zero_mul`
|
||||
`ι_normalOrderF_superCommuteF_eq_zero_mul`
|
||||
which states that applying `ι` to the normal order of something containing a super-commutator
|
||||
is zero.
|
||||
|
||||
-/
|
||||
|
||||
lemma ι_normalOrder_superCommuteF_ofCrAnList_ofCrAnList_eq_zero
|
||||
lemma ι_normalOrderF_superCommuteF_ofCrAnList_ofCrAnList_eq_zero
|
||||
(φa φa' : 𝓕.CrAnStates) (φs φs' : List 𝓕.CrAnStates) :
|
||||
ι 𝓝ᶠ(ofCrAnList φs * [ofCrAnState φa, ofCrAnState φa']ₛca * ofCrAnList φ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 [normalOrder_superCommuteF_ofCrAnList_create_create_ofCrAnList φa φa' hφa hφa' φs φs']
|
||||
· rw [normalOrderF_superCommuteF_ofCrAnList_create_create_ofCrAnList φ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 [normalOrder_superCommuteF_create_annihilate φa φa' hφa hφa' (ofCrAnList φs)
|
||||
· rw [normalOrderF_superCommuteF_create_annihilate φa φa' hφa hφa' (ofCrAnList φs)
|
||||
(ofCrAnList φs')]
|
||||
simp
|
||||
· rw [normalOrder_superCommuteF_annihilate_create φa' φa hφa' hφa (ofCrAnList φs)
|
||||
· rw [normalOrderF_superCommuteF_annihilate_create φa' φa hφa' hφa (ofCrAnList φs)
|
||||
(ofCrAnList φs')]
|
||||
simp
|
||||
· rw [normalOrder_superCommuteF_ofCrAnList_annihilate_annihilate_ofCrAnList φa φa' hφa hφa' φs φs']
|
||||
· rw [normalOrderF_superCommuteF_ofCrAnList_annihilate_annihilate_ofCrAnList φ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 ι_normalOrder_superCommuteF_ofCrAnList_eq_zero
|
||||
lemma ι_normalOrderF_superCommuteF_ofCrAnList_eq_zero
|
||||
(φa φa' : 𝓕.CrAnStates) (φs : List 𝓕.CrAnStates)
|
||||
(a : 𝓕.CrAnAlgebra) : ι 𝓝ᶠ(ofCrAnList φs * [ofCrAnState φa, ofCrAnState φa']ₛca * a) = 0 := by
|
||||
have hf : ι.toLinearMap ∘ₗ normalOrder ∘ₗ
|
||||
have hf : ι.toLinearMap ∘ₗ normalOrderF ∘ₗ
|
||||
mulLinearMap (ofCrAnList φs * [ofCrAnState φa, ofCrAnState φa']ₛca) = 0 := by
|
||||
apply ofCrAnListBasis.ext
|
||||
intro l
|
||||
simp only [CrAnAlgebra.ofListBasis_eq_ofList, LinearMap.coe_comp, Function.comp_apply,
|
||||
AlgHom.toLinearMap_apply, LinearMap.zero_apply]
|
||||
exact ι_normalOrder_superCommuteF_ofCrAnList_ofCrAnList_eq_zero φa φa' φs l
|
||||
change (ι.toLinearMap ∘ₗ normalOrder ∘ₗ
|
||||
exact ι_normalOrderF_superCommuteF_ofCrAnList_ofCrAnList_eq_zero φa φa' φs l
|
||||
change (ι.toLinearMap ∘ₗ normalOrderF ∘ₗ
|
||||
mulLinearMap ((ofCrAnList φs * [ofCrAnState φa, ofCrAnState φa']ₛca))) a = 0
|
||||
rw [hf]
|
||||
simp
|
||||
|
||||
lemma ι_normalOrder_superCommuteF_ofCrAnState_eq_zero_mul (φa φa' : 𝓕.CrAnStates)
|
||||
lemma ι_normalOrderF_superCommuteF_ofCrAnState_eq_zero_mul (φa φa' : 𝓕.CrAnStates)
|
||||
(a b : 𝓕.CrAnAlgebra) :
|
||||
ι 𝓝ᶠ(a * [ofCrAnState φa, ofCrAnState φa']ₛca * b) = 0 := by
|
||||
rw [mul_assoc]
|
||||
change (ι.toLinearMap ∘ₗ normalOrder ∘ₗ mulLinearMap.flip
|
||||
change (ι.toLinearMap ∘ₗ normalOrderF ∘ₗ mulLinearMap.flip
|
||||
([ofCrAnState φa, ofCrAnState φa']ₛca * b)) a = 0
|
||||
have hf : ι.toLinearMap ∘ₗ normalOrder ∘ₗ mulLinearMap.flip
|
||||
have hf : ι.toLinearMap ∘ₗ normalOrderF ∘ₗ mulLinearMap.flip
|
||||
([ofCrAnState φa, ofCrAnState φa']ₛca * b) = 0 := by
|
||||
apply ofCrAnListBasis.ext
|
||||
intro l
|
||||
|
|
@ -78,11 +78,11 @@ lemma ι_normalOrder_superCommuteF_ofCrAnState_eq_zero_mul (φa φa' : 𝓕.CrAn
|
|||
Function.comp_apply, LinearMap.flip_apply, LinearMap.coe_mk, AddHom.coe_mk,
|
||||
AlgHom.toLinearMap_apply, LinearMap.zero_apply]
|
||||
rw [← mul_assoc]
|
||||
exact ι_normalOrder_superCommuteF_ofCrAnList_eq_zero φa φa' _ _
|
||||
exact ι_normalOrderF_superCommuteF_ofCrAnList_eq_zero φa φa' _ _
|
||||
rw [hf]
|
||||
simp
|
||||
|
||||
lemma ι_normalOrder_superCommuteF_ofCrAnState_ofCrAnList_eq_zero_mul (φa : 𝓕.CrAnStates)
|
||||
lemma ι_normalOrderF_superCommuteF_ofCrAnState_ofCrAnList_eq_zero_mul (φa : 𝓕.CrAnStates)
|
||||
(φs : List 𝓕.CrAnStates)
|
||||
(a b : 𝓕.CrAnAlgebra) :
|
||||
ι 𝓝ᶠ(a * [ofCrAnState φa, ofCrAnList φs]ₛca * b) = 0 := by
|
||||
|
|
@ -93,18 +93,18 @@ lemma ι_normalOrder_superCommuteF_ofCrAnState_ofCrAnList_eq_zero_mul (φa :
|
|||
intro n
|
||||
rw [← mul_assoc, ← mul_assoc]
|
||||
rw [mul_assoc _ _ b, ofCrAnList_singleton]
|
||||
rw [ι_normalOrder_superCommuteF_ofCrAnState_eq_zero_mul]
|
||||
rw [ι_normalOrderF_superCommuteF_ofCrAnState_eq_zero_mul]
|
||||
|
||||
lemma ι_normalOrder_superCommuteF_ofCrAnList_ofCrAnState_eq_zero_mul (φa : 𝓕.CrAnStates)
|
||||
lemma ι_normalOrderF_superCommuteF_ofCrAnList_ofCrAnState_eq_zero_mul (φa : 𝓕.CrAnStates)
|
||||
(φs : List 𝓕.CrAnStates) (a b : 𝓕.CrAnAlgebra) :
|
||||
ι 𝓝ᶠ(a * [ofCrAnList φs, ofCrAnState φa]ₛca * b) = 0 := by
|
||||
rw [← ofCrAnList_singleton, superCommuteF_ofCrAnList_ofCrAnList_symm, ofCrAnList_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 [ι_normalOrder_superCommuteF_ofCrAnState_ofCrAnList_eq_zero_mul]
|
||||
rw [ι_normalOrderF_superCommuteF_ofCrAnState_ofCrAnList_eq_zero_mul]
|
||||
simp
|
||||
|
||||
lemma ι_normalOrder_superCommuteF_ofCrAnList_ofCrAnList_eq_zero_mul
|
||||
lemma ι_normalOrderF_superCommuteF_ofCrAnList_ofCrAnList_eq_zero_mul
|
||||
(φs φs' : List 𝓕.CrAnStates) (a b : 𝓕.CrAnAlgebra) :
|
||||
ι 𝓝ᶠ(a * [ofCrAnList φs, ofCrAnList φs']ₛca * b) = 0 := by
|
||||
rw [superCommuteF_ofCrAnList_ofCrAnList_eq_sum, Finset.mul_sum, Finset.sum_mul]
|
||||
|
|
@ -113,63 +113,63 @@ lemma ι_normalOrder_superCommuteF_ofCrAnList_ofCrAnList_eq_zero_mul
|
|||
intro n
|
||||
rw [← mul_assoc, ← mul_assoc]
|
||||
rw [mul_assoc _ _ b]
|
||||
rw [ι_normalOrder_superCommuteF_ofCrAnList_ofCrAnState_eq_zero_mul]
|
||||
rw [ι_normalOrderF_superCommuteF_ofCrAnList_ofCrAnState_eq_zero_mul]
|
||||
|
||||
lemma ι_normalOrder_superCommuteF_ofCrAnList_eq_zero_mul
|
||||
lemma ι_normalOrderF_superCommuteF_ofCrAnList_eq_zero_mul
|
||||
(φs : List 𝓕.CrAnStates)
|
||||
(a b c : 𝓕.CrAnAlgebra) :
|
||||
ι 𝓝ᶠ(a * [ofCrAnList φs, c]ₛca * b) = 0 := by
|
||||
change (ι.toLinearMap ∘ₗ normalOrder ∘ₗ
|
||||
change (ι.toLinearMap ∘ₗ normalOrderF ∘ₗ
|
||||
mulLinearMap.flip b ∘ₗ mulLinearMap a ∘ₗ superCommuteF (ofCrAnList φs)) c = 0
|
||||
have hf : (ι.toLinearMap ∘ₗ normalOrder ∘ₗ
|
||||
have hf : (ι.toLinearMap ∘ₗ normalOrderF ∘ₗ
|
||||
mulLinearMap.flip b ∘ₗ mulLinearMap a ∘ₗ superCommuteF (ofCrAnList φs)) = 0 := by
|
||||
apply ofCrAnListBasis.ext
|
||||
intro φs'
|
||||
simp only [mulLinearMap, LinearMap.coe_mk, AddHom.coe_mk, CrAnAlgebra.ofListBasis_eq_ofList,
|
||||
LinearMap.coe_comp, Function.comp_apply, LinearMap.flip_apply, AlgHom.toLinearMap_apply,
|
||||
LinearMap.zero_apply]
|
||||
rw [ι_normalOrder_superCommuteF_ofCrAnList_ofCrAnList_eq_zero_mul]
|
||||
rw [ι_normalOrderF_superCommuteF_ofCrAnList_ofCrAnList_eq_zero_mul]
|
||||
rw [hf]
|
||||
simp
|
||||
|
||||
@[simp]
|
||||
lemma ι_normalOrder_superCommuteF_eq_zero_mul
|
||||
lemma ι_normalOrderF_superCommuteF_eq_zero_mul
|
||||
(a b c d : 𝓕.CrAnAlgebra) : ι 𝓝ᶠ(a * [d, c]ₛca * b) = 0 := by
|
||||
change (ι.toLinearMap ∘ₗ normalOrder ∘ₗ
|
||||
change (ι.toLinearMap ∘ₗ normalOrderF ∘ₗ
|
||||
mulLinearMap.flip b ∘ₗ mulLinearMap a ∘ₗ superCommuteF.flip c) d = 0
|
||||
have hf : (ι.toLinearMap ∘ₗ normalOrder ∘ₗ
|
||||
have hf : (ι.toLinearMap ∘ₗ normalOrderF ∘ₗ
|
||||
mulLinearMap.flip b ∘ₗ mulLinearMap a ∘ₗ superCommuteF.flip c) = 0 := by
|
||||
apply ofCrAnListBasis.ext
|
||||
intro φs
|
||||
simp only [mulLinearMap, LinearMap.coe_mk, AddHom.coe_mk, CrAnAlgebra.ofListBasis_eq_ofList,
|
||||
LinearMap.coe_comp, Function.comp_apply, LinearMap.flip_apply, AlgHom.toLinearMap_apply,
|
||||
LinearMap.zero_apply]
|
||||
rw [ι_normalOrder_superCommuteF_ofCrAnList_eq_zero_mul]
|
||||
rw [ι_normalOrderF_superCommuteF_ofCrAnList_eq_zero_mul]
|
||||
rw [hf]
|
||||
simp
|
||||
|
||||
@[simp]
|
||||
lemma ι_normalOrder_superCommuteF_eq_zero_mul_right (b c d : 𝓕.CrAnAlgebra) :
|
||||
ι 𝓝ᶠ([d, c]ₛca * b) = 0 := by
|
||||
rw [← ι_normalOrder_superCommuteF_eq_zero_mul 1 b c d]
|
||||
rw [← ι_normalOrderF_superCommuteF_eq_zero_mul 1 b c d]
|
||||
simp
|
||||
|
||||
@[simp]
|
||||
lemma ι_normalOrder_superCommuteF_eq_zero_mul_left (a c d : 𝓕.CrAnAlgebra) :
|
||||
lemma ι_normalOrderF_superCommuteF_eq_zero_mul_left (a c d : 𝓕.CrAnAlgebra) :
|
||||
ι 𝓝ᶠ(a * [d, c]ₛca) = 0 := by
|
||||
rw [← ι_normalOrder_superCommuteF_eq_zero_mul a 1 c d]
|
||||
rw [← ι_normalOrderF_superCommuteF_eq_zero_mul a 1 c d]
|
||||
simp
|
||||
|
||||
@[simp]
|
||||
lemma ι_normalOrder_superCommuteF_eq_zero_mul_mul_right (a b1 b2 c d: 𝓕.CrAnAlgebra) :
|
||||
lemma ι_normalOrderF_superCommuteF_eq_zero_mul_mul_right (a b1 b2 c d: 𝓕.CrAnAlgebra) :
|
||||
ι 𝓝ᶠ(a * [d, c]ₛca * b1 * b2) = 0 := by
|
||||
rw [← ι_normalOrder_superCommuteF_eq_zero_mul a (b1 * b2) c d]
|
||||
rw [← ι_normalOrderF_superCommuteF_eq_zero_mul a (b1 * b2) c d]
|
||||
congr 2
|
||||
noncomm_ring
|
||||
|
||||
@[simp]
|
||||
lemma ι_normalOrder_superCommuteF_eq_zero (c d : 𝓕.CrAnAlgebra) : ι 𝓝ᶠ([d, c]ₛca) = 0 := by
|
||||
rw [← ι_normalOrder_superCommuteF_eq_zero_mul 1 1 c d]
|
||||
lemma ι_normalOrderF_superCommuteF_eq_zero (c d : 𝓕.CrAnAlgebra) : ι 𝓝ᶠ([d, c]ₛca) = 0 := by
|
||||
rw [← ι_normalOrderF_superCommuteF_eq_zero_mul 1 1 c d]
|
||||
simp
|
||||
|
||||
/-!
|
||||
|
|
@ -178,7 +178,7 @@ lemma ι_normalOrder_superCommuteF_eq_zero (c d : 𝓕.CrAnAlgebra) : ι 𝓝ᶠ
|
|||
|
||||
-/
|
||||
|
||||
lemma ι_normalOrder_zero_of_mem_ideal (a : 𝓕.CrAnAlgebra)
|
||||
lemma ι_normalOrderF_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
|
||||
|
|
@ -210,16 +210,16 @@ lemma ι_normalOrder_zero_of_mem_ideal (a : 𝓕.CrAnAlgebra)
|
|||
· intro x hx
|
||||
simp [p]
|
||||
|
||||
lemma ι_normalOrder_eq_of_equiv (a b : 𝓕.CrAnAlgebra) (h : a ≈ b) :
|
||||
lemma ι_normalOrderF_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 ι_normalOrder_zero_of_mem_ideal (a - b) h
|
||||
exact ι_normalOrderF_zero_of_mem_ideal (a - b) h
|
||||
|
||||
/-- Normal ordering on `FieldOpAlgebra`. -/
|
||||
noncomputable def normalOrder : FieldOpAlgebra 𝓕 →ₗ[ℂ] FieldOpAlgebra 𝓕 where
|
||||
toFun := Quotient.lift (ι.toLinearMap ∘ₗ CrAnAlgebra.normalOrder) ι_normalOrder_eq_of_equiv
|
||||
toFun := Quotient.lift (ι.toLinearMap ∘ₗ normalOrderF) ι_normalOrderF_eq_of_equiv
|
||||
map_add' x y := by
|
||||
obtain ⟨x, rfl⟩ := ι_surjective x
|
||||
obtain ⟨y, rfl⟩ := ι_surjective y
|
||||
|
|
|
|||
|
|
@ -24,68 +24,68 @@ open FieldStatistic
|
|||
## Normal order of super-commutators.
|
||||
|
||||
The main result of this section is
|
||||
`crAnF_normalOrder_superCommuteF_eq_zero_mul`.
|
||||
`crAnF_normalOrderF_superCommuteF_eq_zero_mul`.
|
||||
|
||||
-/
|
||||
|
||||
lemma crAnF_normalOrder_superCommuteF_ofCrAnList_create_create_ofCrAnList
|
||||
lemma crAnF_normalOrderF_superCommuteF_ofCrAnList_create_create_ofCrAnList
|
||||
(φc φc' : 𝓕.CrAnStates) (hφc : 𝓕 |>ᶜ φc = CreateAnnihilate.create)
|
||||
(hφc' : 𝓕 |>ᶜ φc' = CreateAnnihilate.create) (φs φs' : List 𝓕.CrAnStates) :
|
||||
𝓞.crAnF (𝓝ᶠ(ofCrAnList φs * [ofCrAnState φc, ofCrAnState φc']ₛca * ofCrAnList φs')) = 0 := by
|
||||
rw [normalOrder_superCommuteF_ofCrAnList_create_create_ofCrAnList φc φc' hφc hφc' φs φs']
|
||||
rw [normalOrderF_superCommuteF_ofCrAnList_create_create_ofCrAnList φc φc' hφc hφc' φs φs']
|
||||
rw [map_smul, map_mul, map_mul, map_mul, 𝓞.superCommuteF_create_create φc φc' hφc hφc']
|
||||
simp
|
||||
|
||||
lemma crAnF_normalOrder_superCommuteF_ofCrAnList_annihilate_annihilate_ofCrAnList
|
||||
lemma crAnF_normalOrderF_superCommuteF_ofCrAnList_annihilate_annihilate_ofCrAnList
|
||||
(φa φa' : 𝓕.CrAnStates) (hφa : 𝓕 |>ᶜ φa = CreateAnnihilate.annihilate)
|
||||
(hφa' : 𝓕 |>ᶜ φa' = CreateAnnihilate.annihilate) (φs φs' : List 𝓕.CrAnStates) :
|
||||
𝓞.crAnF (𝓝ᶠ(ofCrAnList φs * [ofCrAnState φa, ofCrAnState φa']ₛca * ofCrAnList φs')) = 0 := by
|
||||
rw [normalOrder_superCommuteF_ofCrAnList_annihilate_annihilate_ofCrAnList φa φa' hφa hφa' φs φs']
|
||||
rw [normalOrderF_superCommuteF_ofCrAnList_annihilate_annihilate_ofCrAnList φa φa' hφa hφa' φs φs']
|
||||
rw [map_smul, map_mul, map_mul, map_mul, 𝓞.superCommuteF_annihilate_annihilate φa φa' hφa hφa']
|
||||
simp
|
||||
|
||||
lemma crAnF_normalOrder_superCommuteF_ofCrAnList_ofCrAnList_eq_zero
|
||||
lemma crAnF_normalOrderF_superCommuteF_ofCrAnList_ofCrAnList_eq_zero
|
||||
(φa φa' : 𝓕.CrAnStates) (φs φs' : List 𝓕.CrAnStates) :
|
||||
𝓞.crAnF (normalOrder
|
||||
𝓞.crAnF (normalOrderF
|
||||
(ofCrAnList φs * [ofCrAnState φa, ofCrAnState φa']ₛca * ofCrAnList φ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 [normalOrder_superCommuteF_ofCrAnList_create_create_ofCrAnList φa φa' hφa hφa' φs φs']
|
||||
· rw [normalOrderF_superCommuteF_ofCrAnList_create_create_ofCrAnList φa φa' hφa hφa' φs φs']
|
||||
rw [map_smul, map_mul, map_mul, map_mul, 𝓞.superCommuteF_create_create φa φa' hφa hφa']
|
||||
simp
|
||||
· rw [normalOrder_superCommuteF_create_annihilate φa φa' hφa hφa' (ofCrAnList φs)
|
||||
· rw [normalOrderF_superCommuteF_create_annihilate φa φa' hφa hφa' (ofCrAnList φs)
|
||||
(ofCrAnList φs')]
|
||||
simp
|
||||
· rw [normalOrder_superCommuteF_annihilate_create φa' φa hφa' hφa (ofCrAnList φs)
|
||||
· rw [normalOrderF_superCommuteF_annihilate_create φa' φa hφa' hφa (ofCrAnList φs)
|
||||
(ofCrAnList φs')]
|
||||
simp
|
||||
· rw [normalOrder_superCommuteF_ofCrAnList_annihilate_annihilate_ofCrAnList φa φa' hφa hφa' φs φs']
|
||||
· rw [normalOrderF_superCommuteF_ofCrAnList_annihilate_annihilate_ofCrAnList φa φa' hφa hφa' φs φs']
|
||||
rw [map_smul, map_mul, map_mul, map_mul, 𝓞.superCommuteF_annihilate_annihilate φa φa' hφa hφa']
|
||||
simp
|
||||
|
||||
lemma crAnF_normalOrder_superCommuteF_ofCrAnList_eq_zero
|
||||
lemma crAnF_normalOrderF_superCommuteF_ofCrAnList_eq_zero
|
||||
(φa φa' : 𝓕.CrAnStates) (φs : List 𝓕.CrAnStates)
|
||||
(a : 𝓕.CrAnAlgebra) : 𝓞.crAnF (normalOrder (ofCrAnList φs *
|
||||
(a : 𝓕.CrAnAlgebra) : 𝓞.crAnF (normalOrderF (ofCrAnList φs *
|
||||
[ofCrAnState φa, ofCrAnState φa']ₛca * a)) = 0 := by
|
||||
change (𝓞.crAnF.toLinearMap ∘ₗ normalOrder ∘ₗ
|
||||
change (𝓞.crAnF.toLinearMap ∘ₗ normalOrderF ∘ₗ
|
||||
mulLinearMap ((ofCrAnList φs * [ofCrAnState φa, ofCrAnState φa']ₛca))) a = 0
|
||||
have hf : 𝓞.crAnF.toLinearMap ∘ₗ normalOrder ∘ₗ
|
||||
have hf : 𝓞.crAnF.toLinearMap ∘ₗ normalOrderF ∘ₗ
|
||||
mulLinearMap (ofCrAnList φs * [ofCrAnState φa, ofCrAnState φa']ₛca) = 0 := by
|
||||
apply ofCrAnListBasis.ext
|
||||
intro l
|
||||
simp only [ofListBasis_eq_ofList, LinearMap.coe_comp, Function.comp_apply,
|
||||
AlgHom.toLinearMap_apply, LinearMap.zero_apply]
|
||||
exact crAnF_normalOrder_superCommuteF_ofCrAnList_ofCrAnList_eq_zero φa φa' φs l
|
||||
exact crAnF_normalOrderF_superCommuteF_ofCrAnList_ofCrAnList_eq_zero φa φa' φs l
|
||||
rw [hf]
|
||||
simp
|
||||
|
||||
lemma crAnF_normalOrder_superCommuteF_ofCrAnState_eq_zero_mul (φa φa' : 𝓕.CrAnStates)
|
||||
lemma crAnF_normalOrderF_superCommuteF_ofCrAnState_eq_zero_mul (φa φa' : 𝓕.CrAnStates)
|
||||
(a b : 𝓕.CrAnAlgebra) :
|
||||
𝓞.crAnF (normalOrder (a * [ofCrAnState φa, ofCrAnState φa']ₛca * b)) = 0 := by
|
||||
𝓞.crAnF (normalOrderF (a * [ofCrAnState φa, ofCrAnState φa']ₛca * b)) = 0 := by
|
||||
rw [mul_assoc]
|
||||
change (𝓞.crAnF.toLinearMap ∘ₗ normalOrder ∘ₗ mulLinearMap.flip
|
||||
change (𝓞.crAnF.toLinearMap ∘ₗ normalOrderF ∘ₗ mulLinearMap.flip
|
||||
([ofCrAnState φa, ofCrAnState φa']ₛca * b)) a = 0
|
||||
have hf : 𝓞.crAnF.toLinearMap ∘ₗ normalOrder ∘ₗ mulLinearMap.flip
|
||||
have hf : 𝓞.crAnF.toLinearMap ∘ₗ normalOrderF ∘ₗ mulLinearMap.flip
|
||||
([ofCrAnState φa, ofCrAnState φa']ₛca * b) = 0 := by
|
||||
apply ofCrAnListBasis.ext
|
||||
intro l
|
||||
|
|
@ -93,14 +93,14 @@ lemma crAnF_normalOrder_superCommuteF_ofCrAnState_eq_zero_mul (φa φa' : 𝓕.C
|
|||
LinearMap.flip_apply, LinearMap.coe_mk, AddHom.coe_mk, AlgHom.toLinearMap_apply,
|
||||
LinearMap.zero_apply]
|
||||
rw [← mul_assoc]
|
||||
exact crAnF_normalOrder_superCommuteF_ofCrAnList_eq_zero φa φa' _ _
|
||||
exact crAnF_normalOrderF_superCommuteF_ofCrAnList_eq_zero φa φa' _ _
|
||||
rw [hf]
|
||||
simp
|
||||
|
||||
lemma crAnF_normalOrder_superCommuteF_ofCrAnState_ofCrAnList_eq_zero_mul (φa : 𝓕.CrAnStates)
|
||||
lemma crAnF_normalOrderF_superCommuteF_ofCrAnState_ofCrAnList_eq_zero_mul (φa : 𝓕.CrAnStates)
|
||||
(φs : List 𝓕.CrAnStates)
|
||||
(a b : 𝓕.CrAnAlgebra) :
|
||||
𝓞.crAnF (normalOrder (a * [ofCrAnState φa, ofCrAnList φs]ₛca * b)) = 0 := by
|
||||
𝓞.crAnF (normalOrderF (a * [ofCrAnState φa, ofCrAnList φs]ₛca * b)) = 0 := by
|
||||
rw [← ofCrAnList_singleton, superCommuteF_ofCrAnList_ofCrAnList_eq_sum]
|
||||
rw [Finset.mul_sum, Finset.sum_mul]
|
||||
rw [map_sum, map_sum]
|
||||
|
|
@ -108,79 +108,79 @@ lemma crAnF_normalOrder_superCommuteF_ofCrAnState_ofCrAnList_eq_zero_mul (φa :
|
|||
intro n
|
||||
rw [← mul_assoc, ← mul_assoc]
|
||||
rw [mul_assoc _ _ b, ofCrAnList_singleton]
|
||||
rw [crAnF_normalOrder_superCommuteF_ofCrAnState_eq_zero_mul]
|
||||
rw [crAnF_normalOrderF_superCommuteF_ofCrAnState_eq_zero_mul]
|
||||
|
||||
lemma crAnF_normalOrder_superCommuteF_ofCrAnList_ofCrAnState_eq_zero_mul (φa : 𝓕.CrAnStates)
|
||||
lemma crAnF_normalOrderF_superCommuteF_ofCrAnList_ofCrAnState_eq_zero_mul (φa : 𝓕.CrAnStates)
|
||||
(φs : List 𝓕.CrAnStates)
|
||||
(a b : 𝓕.CrAnAlgebra) :
|
||||
𝓞.crAnF (normalOrder (a * [ofCrAnList φs, ofCrAnState φa]ₛca * b)) = 0 := by
|
||||
𝓞.crAnF (normalOrderF (a * [ofCrAnList φs, ofCrAnState φa]ₛca * b)) = 0 := by
|
||||
rw [← ofCrAnList_singleton, superCommuteF_ofCrAnList_ofCrAnList_symm, ofCrAnList_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 [crAnF_normalOrder_superCommuteF_ofCrAnState_ofCrAnList_eq_zero_mul]
|
||||
rw [crAnF_normalOrderF_superCommuteF_ofCrAnState_ofCrAnList_eq_zero_mul]
|
||||
simp
|
||||
|
||||
lemma crAnF_normalOrder_superCommuteF_ofCrAnList_ofCrAnList_eq_zero_mul
|
||||
lemma crAnF_normalOrderF_superCommuteF_ofCrAnList_ofCrAnList_eq_zero_mul
|
||||
(φs φs' : List 𝓕.CrAnStates)
|
||||
(a b : 𝓕.CrAnAlgebra) :
|
||||
𝓞.crAnF (normalOrder (a * [ofCrAnList φs, ofCrAnList φs']ₛca * b)) = 0 := by
|
||||
𝓞.crAnF (normalOrderF (a * [ofCrAnList φs, ofCrAnList φs']ₛca * b)) = 0 := by
|
||||
rw [superCommuteF_ofCrAnList_ofCrAnList_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 [crAnF_normalOrder_superCommuteF_ofCrAnList_ofCrAnState_eq_zero_mul]
|
||||
rw [crAnF_normalOrderF_superCommuteF_ofCrAnList_ofCrAnState_eq_zero_mul]
|
||||
|
||||
lemma crAnF_normalOrder_superCommuteF_ofCrAnList_eq_zero_mul
|
||||
lemma crAnF_normalOrderF_superCommuteF_ofCrAnList_eq_zero_mul
|
||||
(φs : List 𝓕.CrAnStates)
|
||||
(a b c : 𝓕.CrAnAlgebra) :
|
||||
𝓞.crAnF (normalOrder (a * [ofCrAnList φs, c]ₛca * b)) = 0 := by
|
||||
change (𝓞.crAnF.toLinearMap ∘ₗ normalOrder ∘ₗ
|
||||
𝓞.crAnF (normalOrderF (a * [ofCrAnList φs, c]ₛca * b)) = 0 := by
|
||||
change (𝓞.crAnF.toLinearMap ∘ₗ normalOrderF ∘ₗ
|
||||
mulLinearMap.flip b ∘ₗ mulLinearMap a ∘ₗ superCommuteF (ofCrAnList φs)) c = 0
|
||||
have hf : (𝓞.crAnF.toLinearMap ∘ₗ normalOrder ∘ₗ
|
||||
have hf : (𝓞.crAnF.toLinearMap ∘ₗ normalOrderF ∘ₗ
|
||||
mulLinearMap.flip b ∘ₗ mulLinearMap a ∘ₗ superCommuteF (ofCrAnList φs)) = 0 := by
|
||||
apply ofCrAnListBasis.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 [crAnF_normalOrder_superCommuteF_ofCrAnList_ofCrAnList_eq_zero_mul]
|
||||
rw [crAnF_normalOrderF_superCommuteF_ofCrAnList_ofCrAnList_eq_zero_mul]
|
||||
rw [hf]
|
||||
simp
|
||||
|
||||
@[simp]
|
||||
lemma crAnF_normalOrder_superCommuteF_eq_zero_mul
|
||||
(a b c d : 𝓕.CrAnAlgebra) : 𝓞.crAnF (normalOrder (a * [d, c]ₛca * b)) = 0 := by
|
||||
change (𝓞.crAnF.toLinearMap ∘ₗ normalOrder ∘ₗ
|
||||
lemma crAnF_normalOrderF_superCommuteF_eq_zero_mul
|
||||
(a b c d : 𝓕.CrAnAlgebra) : 𝓞.crAnF (normalOrderF (a * [d, c]ₛca * b)) = 0 := by
|
||||
change (𝓞.crAnF.toLinearMap ∘ₗ normalOrderF ∘ₗ
|
||||
mulLinearMap.flip b ∘ₗ mulLinearMap a ∘ₗ superCommuteF.flip c) d = 0
|
||||
have hf : (𝓞.crAnF.toLinearMap ∘ₗ normalOrder ∘ₗ
|
||||
have hf : (𝓞.crAnF.toLinearMap ∘ₗ normalOrderF ∘ₗ
|
||||
mulLinearMap.flip b ∘ₗ mulLinearMap a ∘ₗ superCommuteF.flip c) = 0 := by
|
||||
apply ofCrAnListBasis.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 [crAnF_normalOrder_superCommuteF_ofCrAnList_eq_zero_mul]
|
||||
rw [crAnF_normalOrderF_superCommuteF_ofCrAnList_eq_zero_mul]
|
||||
rw [hf]
|
||||
simp
|
||||
|
||||
@[simp]
|
||||
lemma crAnF_normalOrder_superCommuteF_eq_zero_mul_right
|
||||
(b c d : 𝓕.CrAnAlgebra) : 𝓞.crAnF (normalOrder ([d, c]ₛca * b)) = 0 := by
|
||||
rw [← crAnF_normalOrder_superCommuteF_eq_zero_mul 1 b c d]
|
||||
lemma crAnF_normalOrderF_superCommuteF_eq_zero_mul_right
|
||||
(b c d : 𝓕.CrAnAlgebra) : 𝓞.crAnF (normalOrderF ([d, c]ₛca * b)) = 0 := by
|
||||
rw [← crAnF_normalOrderF_superCommuteF_eq_zero_mul 1 b c d]
|
||||
simp
|
||||
|
||||
@[simp]
|
||||
lemma crAnF_normalOrder_superCommuteF_eq_zero_mul_left
|
||||
(a c d : 𝓕.CrAnAlgebra) : 𝓞.crAnF (normalOrder (a * [d, c]ₛca)) = 0 := by
|
||||
rw [← crAnF_normalOrder_superCommuteF_eq_zero_mul a 1 c d]
|
||||
lemma crAnF_normalOrderF_superCommuteF_eq_zero_mul_left
|
||||
(a c d : 𝓕.CrAnAlgebra) : 𝓞.crAnF (normalOrderF (a * [d, c]ₛca)) = 0 := by
|
||||
rw [← crAnF_normalOrderF_superCommuteF_eq_zero_mul a 1 c d]
|
||||
simp
|
||||
|
||||
@[simp]
|
||||
lemma crAnF_normalOrder_superCommuteF_eq_zero
|
||||
(c d : 𝓕.CrAnAlgebra) : 𝓞.crAnF (normalOrder [d, c]ₛca) = 0 := by
|
||||
rw [← crAnF_normalOrder_superCommuteF_eq_zero_mul 1 1 c d]
|
||||
lemma crAnF_normalOrderF_superCommuteF_eq_zero
|
||||
(c d : 𝓕.CrAnAlgebra) : 𝓞.crAnF (normalOrderF [d, c]ₛca) = 0 := by
|
||||
rw [← crAnF_normalOrderF_superCommuteF_eq_zero_mul 1 1 c d]
|
||||
simp
|
||||
|
||||
/-!
|
||||
|
|
@ -189,78 +189,78 @@ lemma crAnF_normalOrder_superCommuteF_eq_zero
|
|||
|
||||
-/
|
||||
|
||||
lemma crAnF_normalOrder_ofState_ofState_swap (φ φ' : 𝓕.States) :
|
||||
𝓞.crAnF (normalOrder (ofState φ * ofState φ')) =
|
||||
𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') • 𝓞.crAnF (normalOrder (ofState φ' * ofState φ)) := by
|
||||
lemma crAnF_normalOrderF_ofState_ofState_swap (φ φ' : 𝓕.States) :
|
||||
𝓞.crAnF (normalOrderF (ofState φ * ofState φ')) =
|
||||
𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') • 𝓞.crAnF (normalOrderF (ofState φ' * ofState φ)) := by
|
||||
rw [← ofStateList_singleton, ← ofStateList_singleton,
|
||||
ofStateList_mul_ofStateList_eq_superCommuteF]
|
||||
simp
|
||||
|
||||
lemma crAnF_normalOrder_ofCrAnState_ofCrAnList_swap (φ : 𝓕.CrAnStates)
|
||||
lemma crAnF_normalOrderF_ofCrAnState_ofCrAnList_swap (φ : 𝓕.CrAnStates)
|
||||
(φs : List 𝓕.CrAnStates) :
|
||||
𝓞.crAnF (normalOrder (ofCrAnState φ * ofCrAnList φs)) =
|
||||
𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φs) • 𝓞.crAnF (normalOrder (ofCrAnList φs * ofCrAnState φ)) := by
|
||||
𝓞.crAnF (normalOrderF (ofCrAnState φ * ofCrAnList φs)) =
|
||||
𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φs) • 𝓞.crAnF (normalOrderF (ofCrAnList φs * ofCrAnState φ)) := by
|
||||
rw [← ofCrAnList_singleton, ofCrAnList_mul_ofCrAnList_eq_superCommuteF]
|
||||
simp
|
||||
|
||||
lemma crAnF_normalOrder_ofCrAnState_ofStatesList_swap (φ : 𝓕.CrAnStates)
|
||||
lemma crAnF_normalOrderF_ofCrAnState_ofStatesList_swap (φ : 𝓕.CrAnStates)
|
||||
(φ' : List 𝓕.States) :
|
||||
𝓞.crAnF (normalOrder (ofCrAnState φ * ofStateList φ')) =
|
||||
𝓞.crAnF (normalOrderF (ofCrAnState φ * ofStateList φ')) =
|
||||
𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') •
|
||||
𝓞.crAnF (normalOrder (ofStateList φ' * ofCrAnState φ)) := by
|
||||
𝓞.crAnF (normalOrderF (ofStateList φ' * ofCrAnState φ)) := by
|
||||
rw [← ofCrAnList_singleton, ofCrAnList_mul_ofStateList_eq_superCommuteF]
|
||||
simp
|
||||
|
||||
lemma crAnF_normalOrder_anPart_ofStatesList_swap (φ : 𝓕.States)
|
||||
lemma crAnF_normalOrderF_anPart_ofStatesList_swap (φ : 𝓕.States)
|
||||
(φ' : List 𝓕.States) :
|
||||
𝓞.crAnF (normalOrder (anPart φ * ofStateList φ')) =
|
||||
𝓞.crAnF (normalOrderF (anPart φ * ofStateList φ')) =
|
||||
𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') •
|
||||
𝓞.crAnF (normalOrder (ofStateList φ' * anPart φ)) := by
|
||||
𝓞.crAnF (normalOrderF (ofStateList φ' * anPart φ)) := by
|
||||
match φ with
|
||||
| .inAsymp φ =>
|
||||
simp
|
||||
| .position φ =>
|
||||
simp only [anPart_position, instCommGroup.eq_1]
|
||||
rw [crAnF_normalOrder_ofCrAnState_ofStatesList_swap]
|
||||
rw [crAnF_normalOrderF_ofCrAnState_ofStatesList_swap]
|
||||
rfl
|
||||
| .outAsymp φ =>
|
||||
simp only [anPart_posAsymp, instCommGroup.eq_1]
|
||||
rw [crAnF_normalOrder_ofCrAnState_ofStatesList_swap]
|
||||
rw [crAnF_normalOrderF_ofCrAnState_ofStatesList_swap]
|
||||
rfl
|
||||
|
||||
lemma crAnF_normalOrder_ofStatesList_anPart_swap (φ : 𝓕.States) (φ' : List 𝓕.States) :
|
||||
𝓞.crAnF (normalOrder (ofStateList φ' * anPart φ))
|
||||
lemma crAnF_normalOrderF_ofStatesList_anPart_swap (φ : 𝓕.States) (φ' : List 𝓕.States) :
|
||||
𝓞.crAnF (normalOrderF (ofStateList φ' * anPart φ))
|
||||
= 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') •
|
||||
𝓞.crAnF (normalOrder (anPart φ * ofStateList φ')) := by
|
||||
rw [crAnF_normalOrder_anPart_ofStatesList_swap]
|
||||
𝓞.crAnF (normalOrderF (anPart φ * ofStateList φ')) := by
|
||||
rw [crAnF_normalOrderF_anPart_ofStatesList_swap]
|
||||
simp [smul_smul, FieldStatistic.exchangeSign_mul_self]
|
||||
|
||||
lemma crAnF_normalOrder_ofStatesList_mul_anPart_swap (φ : 𝓕.States)
|
||||
lemma crAnF_normalOrderF_ofStatesList_mul_anPart_swap (φ : 𝓕.States)
|
||||
(φ' : List 𝓕.States) :
|
||||
𝓞.crAnF (normalOrder (ofStateList φ') * anPart φ) =
|
||||
𝓞.crAnF (normalOrderF (ofStateList φ') * anPart φ) =
|
||||
𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') •
|
||||
𝓞.crAnF (normalOrder (anPart φ * ofStateList φ')) := by
|
||||
rw [← normalOrder_mul_anPart]
|
||||
rw [crAnF_normalOrder_ofStatesList_anPart_swap]
|
||||
𝓞.crAnF (normalOrderF (anPart φ * ofStateList φ')) := by
|
||||
rw [← normalOrderF_mul_anPart]
|
||||
rw [crAnF_normalOrderF_ofStatesList_anPart_swap]
|
||||
|
||||
/-!
|
||||
|
||||
## Super commutators with a normal ordered term as sums
|
||||
|
||||
-/
|
||||
lemma crAnF_ofCrAnState_superCommuteF_normalOrder_ofCrAnList_eq_sum (φ : 𝓕.CrAnStates)
|
||||
(φs : List 𝓕.CrAnStates) : 𝓞.crAnF ([ofCrAnState φ, normalOrder (ofCrAnList φs)]ₛca) =
|
||||
lemma crAnF_ofCrAnState_superCommuteF_normalOrderF_ofCrAnList_eq_sum (φ : 𝓕.CrAnStates)
|
||||
(φs : List 𝓕.CrAnStates) : 𝓞.crAnF ([ofCrAnState φ, normalOrderF (ofCrAnList φs)]ₛca) =
|
||||
∑ n : Fin φs.length, 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ (φs.take n)) •
|
||||
𝓞.crAnF ([ofCrAnState φ, ofCrAnState φs[n]]ₛca)
|
||||
* 𝓞.crAnF (normalOrder (ofCrAnList (φs.eraseIdx n))) := by
|
||||
rw [normalOrder_ofCrAnList, map_smul, map_smul]
|
||||
* 𝓞.crAnF (normalOrderF (ofCrAnList (φs.eraseIdx n))) := by
|
||||
rw [normalOrderF_ofCrAnList, map_smul, map_smul]
|
||||
rw [crAnF_superCommuteF_ofCrAnState_ofCrAnList_eq_sum, sum_normalOrderList_length]
|
||||
simp only [instCommGroup.eq_1, List.get_eq_getElem, normalOrderList_get_normalOrderEquiv,
|
||||
normalOrderList_eraseIdx_normalOrderEquiv, Algebra.smul_mul_assoc, map_sum, map_smul, map_mul,
|
||||
Finset.smul_sum, Fin.getElem_fin]
|
||||
congr
|
||||
funext n
|
||||
rw [ofCrAnList_eq_normalOrder, map_smul, mul_smul_comm, smul_smul, smul_smul]
|
||||
rw [ofCrAnList_eq_normalOrderF, map_smul, mul_smul_comm, smul_smul, smul_smul]
|
||||
by_cases hs : (𝓕 |>ₛ φ) = (𝓕 |>ₛ φs[n])
|
||||
· congr
|
||||
erw [normalOrderSign_eraseIdx, ← hs]
|
||||
|
|
@ -275,15 +275,15 @@ lemma crAnF_ofCrAnState_superCommuteF_normalOrder_ofCrAnList_eq_sum (φ : 𝓕.C
|
|||
· erw [𝓞.superCommuteF_different_statistics _ _ hs]
|
||||
simp
|
||||
|
||||
lemma crAnF_ofCrAnState_superCommuteF_normalOrder_ofStateList_eq_sum (φ : 𝓕.CrAnStates)
|
||||
(φs : List 𝓕.States) : 𝓞.crAnF ([ofCrAnState φ, normalOrder (ofStateList φs)]ₛca) =
|
||||
lemma crAnF_ofCrAnState_superCommuteF_normalOrderF_ofStateList_eq_sum (φ : 𝓕.CrAnStates)
|
||||
(φs : List 𝓕.States) : 𝓞.crAnF ([ofCrAnState φ, normalOrderF (ofStateList φs)]ₛca) =
|
||||
∑ n : Fin φs.length, 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ (φs.take n)) •
|
||||
𝓞.crAnF ([ofCrAnState φ, ofState φs[n]]ₛca)
|
||||
* 𝓞.crAnF (normalOrder (ofStateList (φs.eraseIdx n))) := by
|
||||
* 𝓞.crAnF (normalOrderF (ofStateList (φs.eraseIdx n))) := by
|
||||
conv_lhs =>
|
||||
rw [ofStateList_sum, map_sum, map_sum, map_sum]
|
||||
enter [2, s]
|
||||
rw [crAnF_ofCrAnState_superCommuteF_normalOrder_ofCrAnList_eq_sum,
|
||||
rw [crAnF_ofCrAnState_superCommuteF_normalOrderF_ofCrAnList_eq_sum,
|
||||
CrAnSection.sum_over_length]
|
||||
enter [2, n]
|
||||
rw [CrAnSection.take_statistics_eq_take_state_statistics, smul_mul_assoc]
|
||||
|
|
@ -306,7 +306,7 @@ where `sᵢ` is the exchange sign for `φ` and `φ₀…φᵢ₋₁`.
|
|||
The origin of this result is
|
||||
- `superCommuteF_ofCrAnList_ofCrAnList_eq_sum`
|
||||
-/
|
||||
lemma crAnF_anPart_superCommuteF_normalOrder_ofStateList_eq_sum (φ : 𝓕.States) (φs : List 𝓕.States) :
|
||||
lemma crAnF_anPart_superCommuteF_normalOrderF_ofStateList_eq_sum (φ : 𝓕.States) (φs : List 𝓕.States) :
|
||||
𝓞.crAnF ([anPart φ, 𝓝ᶠ(φs)]ₛca) =
|
||||
∑ n : Fin φs.length, 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ (φs.take n)) •
|
||||
𝓞.crAnF ([anPart φ, ofState φs[n]]ₛca) * 𝓞.crAnF 𝓝ᶠ(φs.eraseIdx n) := by
|
||||
|
|
@ -315,11 +315,11 @@ lemma crAnF_anPart_superCommuteF_normalOrder_ofStateList_eq_sum (φ : 𝓕.State
|
|||
simp
|
||||
| .position φ =>
|
||||
simp only [anPart_position, instCommGroup.eq_1, Fin.getElem_fin, Algebra.smul_mul_assoc]
|
||||
rw [crAnF_ofCrAnState_superCommuteF_normalOrder_ofStateList_eq_sum]
|
||||
rw [crAnF_ofCrAnState_superCommuteF_normalOrderF_ofStateList_eq_sum]
|
||||
simp [crAnStatistics]
|
||||
| .outAsymp φ =>
|
||||
simp only [anPart_posAsymp, instCommGroup.eq_1, Fin.getElem_fin, Algebra.smul_mul_assoc]
|
||||
rw [crAnF_ofCrAnState_superCommuteF_normalOrder_ofStateList_eq_sum]
|
||||
rw [crAnF_ofCrAnState_superCommuteF_normalOrderF_ofStateList_eq_sum]
|
||||
simp [crAnStatistics]
|
||||
|
||||
/-!
|
||||
|
|
@ -331,32 +331,32 @@ lemma crAnF_anPart_superCommuteF_normalOrder_ofStateList_eq_sum (φ : 𝓕.State
|
|||
Within a proto-operator algebra we have that
|
||||
`anPart φ * 𝓝ᶠ(φ₀φ₁…φₙ) = 𝓝ᶠ((anPart φ)φ₀φ₁…φₙ) + [anpart φ, 𝓝ᶠ(φ₀φ₁…φₙ)]ₛca`.
|
||||
-/
|
||||
lemma crAnF_anPart_mul_normalOrder_ofStatesList_eq_superCommuteF (φ : 𝓕.States)
|
||||
lemma crAnF_anPart_mul_normalOrderF_ofStatesList_eq_superCommuteF (φ : 𝓕.States)
|
||||
(φ' : List 𝓕.States) :
|
||||
𝓞.crAnF (anPart φ * normalOrder (ofStateList φ')) =
|
||||
𝓞.crAnF (normalOrder (anPart φ * ofStateList φ')) +
|
||||
𝓞.crAnF ([anPart φ, normalOrder (ofStateList φ')]ₛca) := by
|
||||
rw [anPart_mul_normalOrder_ofStateList_eq_superCommuteF]
|
||||
𝓞.crAnF (anPart φ * normalOrderF (ofStateList φ')) =
|
||||
𝓞.crAnF (normalOrderF (anPart φ * ofStateList φ')) +
|
||||
𝓞.crAnF ([anPart φ, normalOrderF (ofStateList φ')]ₛca) := by
|
||||
rw [anPart_mul_normalOrderF_ofStateList_eq_superCommuteF]
|
||||
simp only [instCommGroup.eq_1, map_add, map_smul]
|
||||
congr
|
||||
rw [crAnF_normalOrder_anPart_ofStatesList_swap]
|
||||
rw [crAnF_normalOrderF_anPart_ofStatesList_swap]
|
||||
|
||||
/--
|
||||
Within a proto-operator algebra we have that
|
||||
`φ * 𝓝ᶠ(φ₀φ₁…φₙ) = 𝓝ᶠ(φφ₀φ₁…φₙ) + [anpart φ, 𝓝ᶠ(φ₀φ₁…φₙ)]ₛca`.
|
||||
-/
|
||||
lemma crAnF_ofState_mul_normalOrder_ofStatesList_eq_superCommuteF (φ : 𝓕.States)
|
||||
lemma crAnF_ofState_mul_normalOrderF_ofStatesList_eq_superCommuteF (φ : 𝓕.States)
|
||||
(φs : List 𝓕.States) : 𝓞.crAnF (ofState φ * 𝓝ᶠ(φs)) =
|
||||
𝓞.crAnF (normalOrder (ofState φ * ofStateList φs)) +
|
||||
𝓞.crAnF (normalOrderF (ofState φ * ofStateList φs)) +
|
||||
𝓞.crAnF ([anPart φ, 𝓝ᶠ(φs)]ₛca) := by
|
||||
conv_lhs => rw [ofState_eq_crPart_add_anPart]
|
||||
rw [add_mul, map_add, crAnF_anPart_mul_normalOrder_ofStatesList_eq_superCommuteF, ← add_assoc,
|
||||
← normalOrder_crPart_mul, ← map_add]
|
||||
rw [add_mul, map_add, crAnF_anPart_mul_normalOrderF_ofStatesList_eq_superCommuteF, ← add_assoc,
|
||||
← normalOrderF_crPart_mul, ← map_add]
|
||||
conv_lhs =>
|
||||
lhs
|
||||
rw [← map_add, ← add_mul, ← ofState_eq_crPart_add_anPart]
|
||||
|
||||
/-- In the expansion of `ofState φ * normalOrder (ofStateList φs)` the element
|
||||
/-- In the expansion of `ofState φ * normalOrderF (ofStateList φs)` the element
|
||||
of `𝓞.A` associated with contracting `φ` with the (optional) `n`th element of `φs`. -/
|
||||
noncomputable def contractStateAtIndex (φ : 𝓕.States) (φs : List 𝓕.States)
|
||||
(n : Option (Fin φs.length)) : 𝓞.A :=
|
||||
|
|
@ -370,14 +370,14 @@ Within a proto-operator algebra,
|
|||
`φ * N(φ₀φ₁…φₙ) = N(φφ₀φ₁…φₙ) + ∑ i, (sᵢ • [anPart φ, φᵢ]ₛ) * N(φ₀φ₁…φᵢ₋₁φᵢ₊₁…φₙ)`,
|
||||
where `sₙ` is the exchange sign for `φ` and `φ₀φ₁…φᵢ₋₁`.
|
||||
-/
|
||||
lemma crAnF_ofState_mul_normalOrder_ofStatesList_eq_sum (φ : 𝓕.States)
|
||||
lemma crAnF_ofState_mul_normalOrderF_ofStatesList_eq_sum (φ : 𝓕.States)
|
||||
(φs : List 𝓕.States) :
|
||||
𝓞.crAnF (ofState φ * normalOrder (ofStateList φs)) =
|
||||
𝓞.crAnF (ofState φ * normalOrderF (ofStateList φs)) =
|
||||
∑ n : Option (Fin φs.length),
|
||||
contractStateAtIndex φ φs n *
|
||||
𝓞.crAnF (normalOrder (ofStateList (HepLean.List.optionEraseZ φs φ n))) := by
|
||||
rw [crAnF_ofState_mul_normalOrder_ofStatesList_eq_superCommuteF]
|
||||
rw [crAnF_anPart_superCommuteF_normalOrder_ofStateList_eq_sum]
|
||||
𝓞.crAnF (normalOrderF (ofStateList (HepLean.List.optionEraseZ φs φ n))) := by
|
||||
rw [crAnF_ofState_mul_normalOrderF_ofStatesList_eq_superCommuteF]
|
||||
rw [crAnF_anPart_superCommuteF_normalOrderF_ofStateList_eq_sum]
|
||||
simp only [instCommGroup.eq_1, Fin.getElem_fin, Algebra.smul_mul_assoc, contractStateAtIndex,
|
||||
Fintype.sum_option, one_mul]
|
||||
rfl
|
||||
|
|
@ -392,10 +392,10 @@ lemma crAnF_ofState_mul_normalOrder_ofStatesList_eq_sum (φ : 𝓕.States)
|
|||
Within a proto-operator algebra, `N(φφ₀φ₁…φₙ) = s • N(φ₀…φₖ₋₁φφₖ…φₙ)`, where
|
||||
`s` is the exchange sign for `φ` and `φ₀…φₖ₋₁`.
|
||||
-/
|
||||
lemma crAnF_ofState_normalOrder_insert (φ : 𝓕.States) (φs : List 𝓕.States)
|
||||
lemma crAnF_ofState_normalOrderF_insert (φ : 𝓕.States) (φs : List 𝓕.States)
|
||||
(k : Fin φs.length.succ) :
|
||||
𝓞.crAnF (normalOrder (ofStateList (φ :: φs))) =
|
||||
𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φs.take k) • 𝓞.crAnF (normalOrder (ofStateList (φs.insertIdx k φ))) := by
|
||||
𝓞.crAnF (normalOrderF (ofStateList (φ :: φs))) =
|
||||
𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φs.take k) • 𝓞.crAnF (normalOrderF (ofStateList (φs.insertIdx k φ))) := by
|
||||
have hl : φs.insertIdx k φ = φs.take k ++ [φ] ++ φs.drop k := by
|
||||
rw [HepLean.List.insertIdx_eq_take_drop]
|
||||
simp
|
||||
|
|
@ -403,7 +403,7 @@ lemma crAnF_ofState_normalOrder_insert (φ : 𝓕.States) (φs : List 𝓕.State
|
|||
rw [ofStateList_append, ofStateList_append]
|
||||
rw [ofStateList_mul_ofStateList_eq_superCommuteF, add_mul]
|
||||
simp only [instCommGroup.eq_1, Nat.succ_eq_add_one, ofList_singleton, Algebra.smul_mul_assoc,
|
||||
map_add, map_smul, crAnF_normalOrder_superCommuteF_eq_zero_mul_right, add_zero, smul_smul,
|
||||
map_add, map_smul, crAnF_normalOrderF_superCommuteF_eq_zero_mul_right, add_zero, smul_smul,
|
||||
exchangeSign_mul_self_swap, one_smul]
|
||||
rw [← ofStateList_append, ← ofStateList_append]
|
||||
simp
|
||||
|
|
|
|||
|
|
@ -41,7 +41,7 @@ lemma timeContract_of_timeOrderRel (φ ψ : 𝓕.States) (h : timeOrderRel φ ψ
|
|||
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 [normalOrder_ofState_mul_ofState]
|
||||
rw [normalOrderF_ofState_mul_ofState]
|
||||
simp only [instCommGroup.eq_1]
|
||||
rw [ofState_eq_crPart_add_anPart, ofState_eq_crPart_add_anPart]
|
||||
simp only [mul_add, add_mul]
|
||||
|
|
@ -52,7 +52,7 @@ lemma timeContract_of_not_timeOrderRel (φ ψ : 𝓕.States) (h : ¬ timeOrderRe
|
|||
rw [timeContract_eq_smul]
|
||||
simp only [Int.reduceNeg, one_smul, map_add]
|
||||
rw [map_smul]
|
||||
rw [crAnF_normalOrder_ofState_ofState_swap]
|
||||
rw [crAnF_normalOrderF_ofState_ofState_swap]
|
||||
rw [timeOrder_ofState_ofState_not_ordered_eq_timeOrder h]
|
||||
rw [timeContract_eq_smul]
|
||||
simp only [instCommGroup.eq_1, map_smul, map_add, smul_add]
|
||||
|
|
|
|||
|
|
@ -35,13 +35,13 @@ 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 (φ : 𝓕.States) (φs : List 𝓕.States)
|
||||
lemma normalOrderF_uncontracted_none (φ : 𝓕.States) (φs : List 𝓕.States)
|
||||
(i : Fin φs.length.succ) (φsΛ : WickContraction φs.length) :
|
||||
𝓞.crAnF (𝓝ᶠ([φsΛ ↩Λ φ i none]ᵘᶜ))
|
||||
= 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ ⟨φs.get, φsΛ.uncontracted.filter (fun x => i.succAbove x < i)⟩) •
|
||||
𝓞.crAnF 𝓝ᶠ(φ :: [φsΛ]ᵘᶜ) := by
|
||||
simp only [Nat.succ_eq_add_one, instCommGroup.eq_1]
|
||||
rw [crAnF_ofState_normalOrder_insert φ [φsΛ]ᵘᶜ
|
||||
rw [crAnF_ofState_normalOrderF_insert φ [φsΛ]ᵘᶜ
|
||||
⟨(φsΛ.uncontractedListOrderPos i), by simp [uncontractedListGet]⟩, smul_smul]
|
||||
trans (1 : ℂ) • 𝓞.crAnF (𝓝ᶠ(ofStateList [φsΛ ↩Λ φ i none]ᵘᶜ))
|
||||
· simp
|
||||
|
|
@ -105,7 +105,7 @@ 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 (φ : 𝓕.States) (φs : List 𝓕.States)
|
||||
lemma normalOrderF_uncontracted_some (φ : 𝓕.States) (φs : List 𝓕.States)
|
||||
(i : Fin φs.length.succ) (φsΛ : WickContraction φs.length) (k : φsΛ.uncontracted) :
|
||||
𝓞.crAnF 𝓝ᶠ([φsΛ ↩Λ φ i (some k)]ᵘᶜ)
|
||||
= 𝓞.crAnF 𝓝ᶠ((optionEraseZ [φsΛ]ᵘᶜ φ ((uncontractedStatesEquiv φs φsΛ) k))) := by
|
||||
|
|
@ -143,7 +143,7 @@ is equal to
|
|||
where `s` is the exchange sign of `φ` and the uncontracted fields in `φ₀φ₁…φᵢ₋₁`.
|
||||
|
||||
The proof of this result relies primarily on:
|
||||
- `normalOrder_uncontracted_none` which replaces `𝓝ᶠ([φsΛ ↩Λ φ i none]ᵘᶜ)` with
|
||||
- `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 𝓞`.
|
||||
|
|
@ -157,7 +157,7 @@ lemma wick_term_none_eq_wick_term_cons (φ : 𝓕.States) (φs : List 𝓕.State
|
|||
𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ ⟨φs.get, (Finset.univ.filter (fun k => i.succAbove k < i))⟩)
|
||||
• (φsΛ.sign • φsΛ.timeContract 𝓞 * 𝓞.crAnF 𝓝ᶠ(φ :: [φsΛ]ᵘᶜ)) := by
|
||||
by_cases hg : GradingCompliant φs φsΛ
|
||||
· rw [normalOrder_uncontracted_none, sign_insert_none]
|
||||
· rw [normalOrderF_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
|
||||
|
|
@ -213,7 +213,7 @@ lemma wick_term_some_eq_wick_term_optionEraseZ (φ : 𝓕.States) (φs : List
|
|||
· rw [WickContraction.timeConract_insertAndContract_some_eq_mul_contractStateAtIndex_not_lt]
|
||||
swap
|
||||
· exact hn _ hk
|
||||
rw [normalOrder_uncontracted_some, sign_insert_some]
|
||||
rw [normalOrderF_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]
|
||||
|
|
@ -224,7 +224,7 @@ lemma wick_term_some_eq_wick_term_optionEraseZ (φ : 𝓕.States) (φs : List
|
|||
rw [WickContraction.timeConract_insertAndContract_some_eq_mul_contractStateAtIndex_lt]
|
||||
swap
|
||||
· exact hlt _
|
||||
rw [normalOrder_uncontracted_some]
|
||||
rw [normalOrderF_uncontracted_some]
|
||||
rw [sign_insert_some]
|
||||
simp only [instCommGroup.eq_1, smul_smul, Algebra.smul_mul_assoc]
|
||||
congr 1
|
||||
|
|
@ -270,7 +270,7 @@ is equal to the product of
|
|||
over all `k` in `Option φsΛ.uncontracted`.
|
||||
|
||||
The proof of this result primarily depends on
|
||||
- `crAnF_ofState_mul_normalOrder_ofStatesList_eq_sum` to rewrite `𝓞.crAnF (φ * 𝓝ᶠ([φsΛ]ᵘᶜ))`
|
||||
- `crAnF_ofState_mul_normalOrderF_ofStatesList_eq_sum` to rewrite `𝓞.crAnF (φ * 𝓝ᶠ([φsΛ]ᵘᶜ))`
|
||||
- `wick_term_none_eq_wick_term_cons`
|
||||
- `wick_term_some_eq_wick_term_optionEraseZ`
|
||||
-/
|
||||
|
|
@ -281,7 +281,7 @@ lemma wick_term_cons_eq_sum_wick_term (φ : 𝓕.States) (φs : List 𝓕.States
|
|||
𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ ⟨φs.get, (Finset.univ.filter (fun x => i.succAbove x < i))⟩) •
|
||||
∑ (k : Option φsΛ.uncontracted), ((φsΛ ↩Λ φ i k).sign •
|
||||
(φsΛ ↩Λ φ i k).timeContract 𝓞 * 𝓞.crAnF (𝓝ᶠ([φsΛ ↩Λ φ i k]ᵘᶜ))) := by
|
||||
rw [crAnF_ofState_mul_normalOrder_ofStatesList_eq_sum, Finset.mul_sum,
|
||||
rw [crAnF_ofState_mul_normalOrderF_ofStatesList_eq_sum, Finset.mul_sum,
|
||||
uncontractedStatesEquiv_list_sum, Finset.smul_sum]
|
||||
simp only [instCommGroup.eq_1, Nat.succ_eq_add_one]
|
||||
congr 1
|
||||
|
|
@ -324,7 +324,7 @@ lemma wicks_theorem_nil :
|
|||
rw [sum_WickContraction_nil, uncontractedListGet, nil_zero_uncontractedList]
|
||||
simp only [List.map_nil]
|
||||
have h1 : ofStateList (𝓕 := 𝓕) [] = CrAnAlgebra.ofCrAnList [] := by simp
|
||||
rw [h1, normalOrder_ofCrAnList]
|
||||
rw [h1, normalOrderF_ofCrAnList]
|
||||
simp [WickContraction.timeContract, empty, sign]
|
||||
|
||||
lemma wicks_theorem_congr {φs φs' : List 𝓕.States} (h : φs = φs') :
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue