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

refactor: Lint

Browse source
This commit is contained in:
jstoobysmith 2025-01-23 14:31:03 +00:00
parent fca75098f1
commit 5a25cd0f5c
6 changed files with 15 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

6
HepLean/PerturbationTheory/Algebras/StateAlgebra/TimeOrder.lean
View file

@ -65,7 +65,8 @@ lemma timeOrder_ofState_ofState_not_ordered_eq_timeOrder {φ ψ : 𝓕.States} (
have hx := IsTotal.total (r := timeOrderRel) ψ φ
simp_all
/-- In the state algebra time, ordering obeys `T(φ₀φ₁…φₙ) = s * φᵢ * T(φ₀φ₁…φᵢ₋₁φᵢ₊₁…φₙ)` where `φᵢ` is the state
/-- In the state algebra time, ordering obeys `T(φ₀φ₁…φₙ) = s * φᵢ * T(φ₀φ₁…φᵢ₋₁φᵢ₊₁…φₙ)`
where `φᵢ` is the state
which has maximum time and `s` is the exchange sign of `φᵢ` and `φ₀φ₁…φᵢ₋₁`. -/
lemma timeOrder_eq_maxTimeField_mul (φ : 𝓕.States) (φs : List 𝓕.States) :
timeOrder (ofList (φ :: φs)) =
@ -78,7 +79,8 @@ lemma timeOrder_eq_maxTimeField_mul (φ : 𝓕.States) (φs : List 𝓕.States)
rw [timerOrderSign_of_eraseMaxTimeField, mul_assoc]
simp
/-- In the state algebra time, ordering obeys `T(φ₀φ₁…φₙ) = s * φᵢ * T(φ₀φ₁…φᵢ₋₁φᵢ₊₁…φₙ)` where `φᵢ` is the state
/-- In the state algebra time, ordering obeys `T(φ₀φ₁…φₙ) = s * φᵢ * T(φ₀φ₁…φᵢ₋₁φᵢ₊₁…φₙ)`
where `φᵢ` is the state
which has maximum time and `s` is the exchange sign of `φᵢ` and `φ₀φ₁…φᵢ₋₁`.
Here `s` is written using finite sets. -/
lemma timeOrder_eq_maxTimeField_mul_finset (φ : 𝓕.States) (φs : List 𝓕.States) :

4
HepLean/PerturbationTheory/WicksTheorem.lean
View file

@ -27,7 +27,7 @@ open FieldStatistic
/--
Let `c` be a Wick Contraction for `φ₀φ₁…φₙ`.
We have (roughly) `N(c.insertList φ φs i none).uncontractedList = s • N(φ * c.uncontractedList)`
We have (roughly) `N(c.insertList φ φs i none).uncontractedList = s • N(φ * c.uncontractedList)`
Where `s` is the exchange sign for `φ` and the uncontracted fields in `φ₀φ₁…φᵢ`.
-/
lemma insertList_none_normalOrder (φ : 𝓕.States) (φs : List 𝓕.States)
@ -324,7 +324,7 @@ remark wicks_theorem_context := "
for all possible Wick contractions `c` of the list of fields `φs := φ₀φ₁…φₙ`, given by
the multiple of:
- The sign corresponding to the number of fermionic-fermionic exchanges one must do
to put elements in contracted pairs of `c` next to each other.
to put elements in contracted pairs of `c` next to each other.
- The product of time-contractions of the contracted pairs of `c`.
- The normal-ordering of the uncontracted fields in `c`.
-/