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-02-07 10:34:48 +00:00
parent cb2f8a30bf
commit cecc75cf46
17 changed files with 36 additions and 43 deletions
Download patch file Download diff file Expand all files Collapse all files

2
HepLean/PerturbationTheory/FieldOpAlgebra/NormalOrder/Basic.lean
View file

@ -226,7 +226,7 @@ lemma ι_normalOrderF_eq_of_equiv (a b : 𝓕.FieldOpFreeAlgebra) (h : a ≈ b)
defined as the decent of `ι ∘ₗ normalOrderF` from `FieldOpFreeAlgebra 𝓕` to `FieldOpAlgebra 𝓕`.
This decent exists because `ι ∘ₗ normalOrderF` is well-defined on equivalence classes.
The notation `𝓝(a)` is used for `normalOrder a`. -/
The notation `𝓝(a)` is used for `normalOrder a`. -/
noncomputable def normalOrder : FieldOpAlgebra 𝓕 →ₗ[ℂ] FieldOpAlgebra 𝓕 where
toFun := Quotient.lift (ι.toLinearMap ∘ₗ normalOrderF) ι_normalOrderF_eq_of_equiv
map_add' x y := by

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

@ -118,7 +118,6 @@ lemma crPart_mul_normalOrder (φ : 𝓕.FieldOp) (a : 𝓕.FieldOpAlgebra) :
-/
/-- For a field specfication `𝓕`, and `a` and `b` in `𝓕.FieldOpAlgebra` the normal ordering
of the super commutator of `a` and `b` vanishes. I.e. `𝓝([a,b]ₛ) = 0`. -/
@[simp]
@ -351,7 +350,7 @@ the following relation holds in the algebra `𝓕.FieldOpAlgebra`,
The proof of ultimetly goes as follows:
- `ofFieldOp_eq_crPart_add_anPart` is used to split `φ` into its creation and annihilation parts.
- The fact that `crPart φ * 𝓝(φ₀φ₁…φₙ) = 𝓝(crPart φ * φ₀φ₁…φₙ)` is used.
- The fact that `crPart φ * 𝓝(φ₀φ₁…φₙ) = 𝓝(crPart φ * φ₀φ₁…φₙ)` is used.
- The fact that `anPart φ * 𝓝(φ₀φ₁…φₙ)` is
`𝓢(φ, φ₀φ₁…φₙ) 𝓝(φ₀φ₁…φₙ) * anPart φ + [anPart φ, 𝓝(φ₀φ₁…φₙ)]` is used
- The fact that `𝓢(φ, φ₀φ₁…φₙ) 𝓝(φ₀φ₁…φₙ) * anPart φ = 𝓝(anPart φ * φ₀φ₁…φₙ)`

4
HepLean/PerturbationTheory/FieldOpAlgebra/NormalOrder/WickContractions.lean
View file

@ -26,7 +26,7 @@ variable {𝓕 : FieldSpecification}
-/
/-- For a list `φs = φ₀…φₙ` of `𝓕.FieldOp`, a Wick contraction `φsΛ` of `φs`, an element `φ` of
`𝓕.FieldOp`, and a `i ≤ φs.length` the following relation holds
`𝓕.FieldOp`, and a `i ≤ φs.length` the following relation holds
`𝓝([φsΛ ↩Λ φ i none]ᵘᶜ) = s • 𝓝(φ :: [φsΛ]ᵘᶜ)`
@ -100,7 +100,7 @@ lemma normalOrder_uncontracted_none (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp
/--
For a list `φs = φ₀…φₙ` of `𝓕.FieldOp`, a Wick contraction `φsΛ` of `φs`, an element `φ` of
`𝓕.FieldOp`, a `i ≤ φs.length` and a `k` in `φsΛ.uncontracted`, then
`𝓕.FieldOp`, a `i ≤ φs.length` and a `k` in `φsΛ.uncontracted`, then
`𝓝([φsΛ ↩Λ φ i (some k)]ᵘᶜ)` is equal to the normal ordering of `[φsΛ]ᵘᶜ` with the `FieldOp`
corresponding to `k` removed.

2
HepLean/PerturbationTheory/FieldOpAlgebra/StaticWickTerm.lean
View file

@ -31,7 +31,7 @@ noncomputable section
def staticWickTerm {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) : 𝓕.FieldOpAlgebra :=
φsΛ.sign • φsΛ.staticContract * 𝓝(ofFieldOpList [φsΛ]ᵘᶜ)
/-- For the empty list `[]` of `𝓕.FieldOp`, the `staticWickTerm` of the empty Wick contraction
/-- For the empty list `[]` of `𝓕.FieldOp`, the `staticWickTerm` of the empty Wick contraction
`empty` of `[]` (its only Wick contraction) is `1`. -/
@[simp]
lemma staticWickTerm_empty_nil :

2
HepLean/PerturbationTheory/FieldOpAlgebra/StaticWickTheorem.lean
View file

@ -33,7 +33,7 @@ The inductive step works as follows:
For the LHS:
1. The proof considers `φ₀…φₙ` as `φ₀(φ₁…φₙ)` and use the induction hypothesis on `φ₁…φₙ`.
2. This gives terms of the form `φ * φsΛ.staticWickTerm` on which
2. This gives terms of the form `φ * φsΛ.staticWickTerm` on which
`mul_staticWickTerm_eq_sum` is used where `φsΛ` is a Wick contraction of `φ₁…φₙ`,
to rewrite terms as a sum over optional uncontracted elements of `φsΛ`

5
HepLean/PerturbationTheory/FieldOpAlgebra/TimeContraction.lean
View file

@ -31,11 +31,10 @@ def timeContract (φ ψ : 𝓕.FieldOp) : 𝓕.FieldOpAlgebra :=
lemma timeContract_eq_smul (φ ψ : 𝓕.FieldOp) : timeContract φ ψ =
𝓣(ofFieldOp φ * ofFieldOp ψ) + (-1 : ℂ) • 𝓝(ofFieldOp φ * ofFieldOp ψ) := by rfl
/-- For a field specification `𝓕`, and `φ` and `ψ` elements of `𝓕.FieldOp`, if
`φ` and `ψ` are time-ordered then
`timeContract φ ψ = [anPart φ, ofFieldOp ψ]ₛ`. -/
`timeContract φ ψ = [anPart φ, ofFieldOp ψ]ₛ`. -/
lemma timeContract_of_timeOrderRel (φ ψ : 𝓕.FieldOp) (h : timeOrderRel φ ψ) :
timeContract φ ψ = [anPart φ, ofFieldOp ψ]ₛ := by
conv_rhs =>
@ -62,7 +61,7 @@ lemma timeContract_of_not_timeOrderRel (φ ψ : 𝓕.FieldOp) (h : ¬ timeOrderR
/-- For a field specification `𝓕`, and `φ` and `ψ` elements of `𝓕.FieldOp`, if
`φ` and `ψ` are not time-ordered then
`timeContract φ ψ = 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ ψ) • [anPart ψ, ofFieldOp φ]ₛ`. -/
`timeContract φ ψ = 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ ψ) • [anPart ψ, ofFieldOp φ]ₛ`. -/
lemma timeContract_of_not_timeOrderRel_expand (φ ψ : 𝓕.FieldOp) (h : ¬ timeOrderRel φ ψ) :
timeContract φ ψ = 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ ψ) • [anPart ψ, ofFieldOp φ]ₛ := by
rw [timeContract_of_not_timeOrderRel _ _ h]

2
HepLean/PerturbationTheory/FieldOpAlgebra/WickTerm.lean
View file

@ -33,7 +33,7 @@ noncomputable section
def wickTerm {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) : 𝓕.FieldOpAlgebra :=
φsΛ.sign • φsΛ.timeContract * 𝓝(ofFieldOpList [φsΛ]ᵘᶜ)
/-- For the empty list `[]` of `𝓕.FieldOp`, the `wickTerm` of the empty Wick contraction
/-- For the empty list `[]` of `𝓕.FieldOp`, the `wickTerm` of the empty Wick contraction
`empty` of `[]` (its only Wick contraction) is `1`. -/
@[simp]
lemma wickTerm_empty_nil :

2
HepLean/PerturbationTheory/FieldOpAlgebra/WicksTheorem.lean
View file

@ -79,7 +79,7 @@ For the LHS:
the maximal time field in `φ₀…φₙ`
2. The induction hypothesis is then used on `𝓣(φ₀…φᵢ₋₁φᵢ₊₁φₙ)` to expand it as a sum over
Wick contractions of `φ₀…φᵢ₋₁φᵢ₊₁φₙ`.
3. This gives terms of the form `φᵢ * φsΛ.timeContract` on which
3. This gives terms of the form `φᵢ * φsΛ.timeContract` on which
`mul_wickTerm_eq_sum` is used where `φsΛ` is a Wick contraction of `φ₀…φᵢ₋₁φᵢ₊₁φ`,
to rewrite terms as a sum over optional uncontracted elements of `φsΛ`

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

@ -30,7 +30,7 @@ where the sum is over all Wick contraction `φsΛ` which only have equal time co
This result follows from
- `static_wick_theorem` to rewrite `𝓣(φs)` on the left hand side as a sum of
`𝓣(φsΛ.staticWickTerm)`.
- `EqTimeOnly.timeOrder_staticContract_of_not_mem` and `timeOrder_timeOrder_mid` to set to
- `EqTimeOnly.timeOrder_staticContract_of_not_mem` and `timeOrder_timeOrder_mid` to set to
zero those terms in which the contracted elements do not have equal time.
- `staticContract_eq_timeContract_of_eqTimeOnly` to rewrite the static contract as a time contract
for those terms which have equal time.
@ -61,7 +61,6 @@ lemma timeOrder_ofFieldOpList_eqTimeOnly (φs : List 𝓕.FieldOp) :
exact x.2
exact x.2
lemma timeOrder_ofFieldOpList_eq_eqTimeOnly_empty (φs : List 𝓕.FieldOp) :
𝓣(ofFieldOpList φs) = 𝓣(𝓝(ofFieldOpList φs)) +
∑ (φsΛ : {φsΛ // φsΛ.EqTimeOnly (φs := φs) ∧ φsΛ ≠ empty}),
@ -112,7 +111,7 @@ For a list `φs` of `𝓕.FieldOp`, then `𝓣(φs)` is equal to the sum of
- `∑ φsΛ, φsΛ.wickTerm` where the sum is over all Wick contraction `φsΛ` which have
no contractions of equal time.
- `∑ φsΛ, sign φs ↑φsΛ • (φsΛ.1).timeContract ∑ φssucΛ, φssucΛ.wickTerm`, where
- `∑ φsΛ, sign φs ↑φsΛ • (φsΛ.1).timeContract ∑ φssucΛ, φssucΛ.wickTerm`, where
the first sum is over all Wick contraction `φsΛ` which only have equal time contractions
and the second sum is over all Wick contraction `φssucΛ` of the uncontracted elements of `φsΛ`
which do not have any equal time contractions.
@ -120,7 +119,7 @@ For a list `φs` of `𝓕.FieldOp`, then `𝓣(φs)` is equal to the sum of
The proof of this result relies on `wicks_theorem` to rewrite `𝓣(φs)` as a sum over
all Wick contractions.
The sum over all Wick contractions is then split additively into two parts using based on having or
not having equal time contractions.
not having equal time contractions.
The sum over Wick contractions which do have equal time contractions is turned into two sums
one over the Wick contractions which only have equal time contractions and the other over the
uncontracted elements of the Wick contraction which do not have equal time contractions using
@ -130,10 +129,9 @@ The properties of `join_sign_timeContract` is then used to equate terms.
lemma timeOrder_haveEqTime_split (φs : List 𝓕.FieldOp) :
𝓣(ofFieldOpList φs) = (∑ (φsΛ : {φsΛ : WickContraction φs.length // ¬ HaveEqTime φsΛ}),
φsΛ.1.sign • φsΛ.1.timeContract.1 * 𝓝(ofFieldOpList [φsΛ.1]ᵘᶜ))
+ ∑ (φsΛ : {φsΛ // φsΛ.EqTimeOnly (φs := φs) ∧ φsΛ ≠ empty}),
sign φs ↑φsΛ • (φsΛ.1).timeContract *
(∑ φssucΛ : { φssucΛ : WickContraction [φsΛ.1]ᵘᶜ.length // ¬ φssucΛ.HaveEqTime },
sign [φsΛ.1]ᵘᶜ φssucΛ • (φssucΛ.1).timeContract * normalOrder (ofFieldOpList [φssucΛ.1]ᵘᶜ)) := by
+ ∑ (φsΛ : {φsΛ // φsΛ.EqTimeOnly (φs := φs) ∧ φsΛ ≠ empty}), φsΛ.1.sign • φsΛ.1.timeContract *
(∑ φssucΛ : { φssucΛ : WickContraction [φsΛ.1]ᵘᶜ.length // ¬ φssucΛ.HaveEqTime },
φssucΛ.1.wickTerm) := by
rw [wicks_theorem]
simp only [wickTerm]
let e1 : WickContraction φs.length ≃ {φsΛ // HaveEqTime φsΛ} ⊕ {φsΛ // ¬ HaveEqTime φsΛ} := by
@ -165,13 +163,12 @@ lemma timeOrder_haveEqTime_split (φs : List 𝓕.FieldOp) :
rw [@join_uncontractedListGet]
lemma normalOrder_timeOrder_ofFieldOpList_eq_not_haveEqTime_sub_inductive (φs : List 𝓕.FieldOp) :
𝓣(𝓝(ofFieldOpList φs)) = (∑ (φsΛ : {φsΛ : WickContraction φs.length // ¬ HaveEqTime φsΛ}),
φsΛ.1.sign • φsΛ.1.timeContract.1 * 𝓝(ofFieldOpList [φsΛ.1]ᵘᶜ))
𝓣(𝓝(ofFieldOpList φs)) =
(∑ (φsΛ : {φsΛ : WickContraction φs.length // ¬ HaveEqTime φsΛ}), φsΛ.1.wickTerm)
+ ∑ (φsΛ : {φsΛ // φsΛ.EqTimeOnly (φs := φs) ∧ φsΛ ≠ empty}),
sign φs ↑φsΛ • (φsΛ.1).timeContract *
(∑ φssucΛ : { φssucΛ : WickContraction [φsΛ.1]ᵘᶜ.length // ¬ φssucΛ.HaveEqTime },
sign [φsΛ.1]ᵘᶜ φssucΛ • (φssucΛ.1).timeContract * normalOrder (ofFieldOpList [φssucΛ.1]ᵘᶜ) -
𝓣(𝓝(ofFieldOpList [φsΛ.1]ᵘᶜ))) := by
φssucΛ.1.wickTerm - 𝓣(𝓝(ofFieldOpList [φsΛ.1]ᵘᶜ))) := by
rw [normalOrder_timeOrder_ofFieldOpList_eq_eqTimeOnly_empty,
timeOrder_haveEqTime_split]
rw [add_sub_assoc]
@ -224,7 +221,7 @@ lemma wicks_theorem_normal_order_empty : 𝓣(𝓝(ofFieldOpList [])) =
where the sum is over all Wick contraction `φsΛ` in which no two contracted elements
have the same time.
The proof of proceeds by induction on `φs`, with the base case `[]` holding by following
The proof of proceeds by induction on `φs`, with the base case `[]` holding by following
through definitions. and the inductive case holding as a result of
- `timeOrder_haveEqTime_split`
- `normalOrder_timeOrder_ofFieldOpList_eq_eqTimeOnly_empty`
@ -236,7 +233,6 @@ theorem wicks_theorem_normal_order : (φs : List 𝓕.FieldOp) →
∑ (φsΛ : {φsΛ : WickContraction φs.length // ¬ HaveEqTime φsΛ}), φsΛ.1.wickTerm
| [] => wicks_theorem_normal_order_empty
| φ :: φs => by
simp only [wickTerm]
rw [normalOrder_timeOrder_ofFieldOpList_eq_not_haveEqTime_sub_inductive]
simp only [Algebra.smul_mul_assoc, ne_eq, add_right_eq_self]
apply Finset.sum_eq_zero

2
HepLean/PerturbationTheory/FieldSpecification/NormalOrder.lean
View file

@ -347,7 +347,7 @@ lemma normalOrderList_eraseIdx_normalOrderEquiv {φs : List 𝓕.CrAnFieldOp} (n
the following relation holds
`normalOrderSign (φ₀…φᵢ₋₁φᵢ₊₁…φₙ)` is equal to the product of
- `normalOrderSign φ₀…φₙ`,
- `𝓢(φᵢ, φ₀…φᵢ₋₁)` i.e. the sign needed to remove `φᵢ` from `φ₀…φₙ`,
- `𝓢(φᵢ, φ₀…φᵢ₋₁)` i.e. the sign needed to remove `φᵢ` from `φ₀…φₙ`,
- `𝓢(φᵢ, _)` where `_` is the list of elements appearing before `φᵢ` after normal ordering. I.e.
the sign needed to insert `φᵢ` back into the normal-ordered list at the correct place. -/
lemma normalOrderSign_eraseIdx (φs : List 𝓕.CrAnFieldOp) (i : Fin φs.length) :

4
HepLean/PerturbationTheory/WickContraction/InsertAndContract.lean
View file

@ -24,7 +24,7 @@ open HepLean.Fin
-/
/-- Given a Wick contraction `φsΛ` for a list `φs` of `𝓕.FieldOp`,
/-- Given a Wick contraction `φsΛ` for a list `φs` of `𝓕.FieldOp`,
a `𝓕.FieldOp` `φ`, an `i ≤ φs.length` and a `j` which is either `none` or
some element of `φsΛ.uncontracted`, the new Wick contraction
`φsΛ.insertAndContract φ i j` is defined by inserting `φ` into `φs` after
@ -285,7 +285,7 @@ lemma insert_fin_eq_self (φ : 𝓕.FieldOp) {φs : List 𝓕.FieldOp}
rfl
/-- For a list `φs` of `𝓕.FieldOp`, a Wick contraction `φsΛ` of `φs`, an element `φ` of
`𝓕.FieldOp`, a `i ≤ φs.length` a sum over
`𝓕.FieldOp`, a `i ≤ φs.length` a sum over
Wick contractions of `φs` with `φ` inserted at `i` is equal to the sum over Wick contractions
`φsΛ` of just `φs` and the sum over optional uncontracted elements of the `φsΛ`.

2
HepLean/PerturbationTheory/WickContraction/Sign/InsertNone.lean
View file

@ -255,7 +255,7 @@ lemma sign_insert_none (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
exact hG
/-- For a list `φs = φ₀…φₙ` of `𝓕.FieldOp`, a graded compliant Wick contraction `φsΛ` of `φs`,
and a `φ` in `𝓕.FieldOp`, the following relation holds
and a `φ` in `𝓕.FieldOp`, the following relation holds
`(φsΛ ↩Λ φ 0 none).sign = φsΛ.sign`.
This is a direct corollary of `sign_insert_none`. -/

6
HepLean/PerturbationTheory/WickContraction/Sign/InsertSome.lean
View file

@ -856,7 +856,7 @@ lemma signInsertSome_mul_filter_contracted_of_not_lt (φ : 𝓕.FieldOp) (φs :
/--
For a list `φs = φ₀…φₙ` of `𝓕.FieldOp`, a Wick contraction `φsΛ` of `φs`, an element `φ` of
`𝓕.FieldOp`, a `i ≤ φs.length` and a `k` in `φsΛ.uncontracted` such that `k<i`,
`𝓕.FieldOp`, a `i ≤ φs.length` and a `k` in `φsΛ.uncontracted` such that `k<i`,
the sign of `φsΛ ↩Λ φ i (some k)` is equal to the product of
- the sign associated with moving `φ` through the `φsΛ`-uncontracted `FieldOp` in `φ₀…φₖ`,
- the sign associated with moving `φ` through all `FieldOp` in `φ₀…φᵢ₋₁`,
@ -881,7 +881,7 @@ lemma sign_insert_some_of_lt (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
/--
For a list `φs = φ₀…φₙ` of `𝓕.FieldOp`, a Wick contraction `φsΛ` of `φs`, an element `φ` of
`𝓕.FieldOp`, a `i ≤ φs.length` and a `k` in `φsΛ.uncontracted` such that `i ≤ k`,
`𝓕.FieldOp`, a `i ≤ φs.length` and a `k` in `φsΛ.uncontracted` such that `i ≤ k`,
the sign of `φsΛ ↩Λ φ i (some k)` is equal to the product of
- the sign associated with moving `φ` through the `φsΛ`-uncontracted `FieldOp` in `φ₀…φₖ₋₁`,
- the sign associated with moving `φ` through all the `FieldOp` in `φ₀…φᵢ₋₁`,
@ -906,7 +906,7 @@ lemma sign_insert_some_of_not_lt (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
/--
For a list `φs = φ₀…φₙ` of `𝓕.FieldOp`, a Wick contraction `φsΛ` of `φs`, an element `φ` of
`𝓕.FieldOp`, and a `k` in `φsΛ.uncontracted`,
`𝓕.FieldOp`, and a `k` in `φsΛ.uncontracted`,
the sign of `φsΛ ↩Λ φ 0 (some k)` is equal to the product of
- the sign associated with moving `φ` through the `φsΛ`-uncontracted `FieldOp` in `φ₀…φₖ₋₁`,
- the sign of `φsΛ`.

2
HepLean/PerturbationTheory/WickContraction/Sign/Join.lean
View file

@ -429,7 +429,7 @@ lemma join_sign {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length)
(join φsΛ φsucΛ).sign = φsΛ.sign * φsucΛ.sign :=
join_sign_induction φsΛ φsucΛ hc (φsΛ).1.card rfl
/-- For a list `φs` of `𝓕.FieldOp`, a Wick contraction `φsΛ` of `φs`,
/-- For a list `φs` of `𝓕.FieldOp`, a Wick contraction `φsΛ` of `φs`,
and a Wick contraction `φsucΛ` of `[φsΛ]ᵘᶜ`,
`(join φsΛ φsucΛ).sign • (join φsΛ φsucΛ).timeContract` is equal to the product of
- `φsΛ.sign • φsΛ.timeContract` and

5
HepLean/PerturbationTheory/WickContraction/StaticContract.lean
View file

@ -31,7 +31,7 @@ noncomputable def staticContract {φs : List 𝓕.FieldOp}
superCommute_anPart_ofFieldOp_mem_center _ _⟩
/-- For a list `φs = φ₀…φₙ` of `𝓕.FieldOp`, a Wick contraction `φsΛ` of `φs`, an element `φ` of
`𝓕.FieldOp`, and a `i ≤ φs.length` the following relation holds
`𝓕.FieldOp`, and a `i ≤ φs.length` the following relation holds
`(φsΛ ↩Λ φ i none).staticContract = φsΛ.staticContract`
@ -46,10 +46,9 @@ lemma staticContract_insert_none (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
ext a
simp
/--
For a list `φs = φ₀…φₙ` of `𝓕.FieldOp`, a Wick contraction `φsΛ` of `φs`, an element `φ` of
`𝓕.FieldOp`, a `i ≤ φs.length` and a `k` in `φsΛ.uncontracted`, then
`𝓕.FieldOp`, a `i ≤ φs.length` and a `k` in `φsΛ.uncontracted`, then
`(φsΛ ↩Λ φ i (some k)).staticContract` is equal to the product of
- `[anPart φ, φs[k]]ₛ` if `i ≤ k` or `[anPart φs[k], φ]ₛ` if `k < i`
- `φsΛ.staticContract`.

10
HepLean/PerturbationTheory/WickContraction/TimeContract.lean
View file

@ -31,7 +31,7 @@ noncomputable def timeContract {φs : List 𝓕.FieldOp}
timeContract_mem_center _ _⟩
/-- For a list `φs = φ₀…φₙ` of `𝓕.FieldOp`, a Wick contraction `φsΛ` of `φs`, an element `φ` of
`𝓕.FieldOp`, and a `i ≤ φs.length` the following relation holds
`𝓕.FieldOp`, and a `i ≤ φs.length` the following relation holds
`(φsΛ ↩Λ φ i none).timeContract = φsΛ.timeContract`
@ -45,8 +45,8 @@ lemma timeContract_insert_none (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
ext a
simp
/-- For a list `φs = φ₀…φₙ` of `𝓕.FieldOp`, a Wick contraction `φsΛ` of `φs`, an element `φ` of
`𝓕.FieldOp`, a `i ≤ φs.length` and a `k` in `φsΛ.uncontracted`, then
/-- For a list `φs = φ₀…φₙ` of `𝓕.FieldOp`, a Wick contraction `φsΛ` of `φs`, an element `φ` of
`𝓕.FieldOp`, a `i ≤ φs.length` and a `k` in `φsΛ.uncontracted`, then
`(φsΛ ↩Λ φ i (some k)).timeContract` is equal to the product of
- `timeContract φ φs[k]` if `i ≤ k` or `timeContract φs[k] φ` if `k < i`
- `φsΛ.timeContract`.
@ -80,7 +80,7 @@ lemma timeContract_empty (φs : List 𝓕.FieldOp) :
open FieldStatistic
/-! For a list `φs = φ₀…φₙ` of `𝓕.FieldOp`, a Wick contraction `φsΛ` of `φs`, an element `φ` of
`𝓕.FieldOp`, a `i ≤ φs.length` and a `k` in `φsΛ.uncontracted` such that `i ≤ k`, with the
`𝓕.FieldOp`, a `i ≤ φs.length` and a `k` in `φsΛ.uncontracted` such that `i ≤ k`, with the
condition that `φ` has greater or equal time to `φs[k]`, then
`(φsΛ ↩Λ φ i (some k)).timeContract` is equal to the product of
- `[anPart φ, φs[k]]ₛ`
@ -124,7 +124,7 @@ lemma timeContract_insert_some_of_lt
· exact ht
/-! For a list `φs = φ₀…φₙ` of `𝓕.FieldOp`, a Wick contraction `φsΛ` of `φs`, an element `φ` of
`𝓕.FieldOp`, a `i ≤ φs.length` and a `k` in `φsΛ.uncontracted` such that `k < i`, with the
`𝓕.FieldOp`, a `i ≤ φs.length` and a `k` in `φsΛ.uncontracted` such that `k < i`, with the
condition that `φs[k]` does not have has greater or equal time to `φ`, then
`(φsΛ ↩Λ φ i (some k)).timeContract` is equal to the product of
- `[anPart φ, φs[k]]ₛ`

2
HepLean/PerturbationTheory/WickContraction/UncontractedList.lean
View file

@ -315,7 +315,7 @@ lemma take_uncontractedIndexEquiv_symm (k : c.uncontracted) :
-/
/-- Given a Wick Contraction `φsΛ` of a list `φs` of `𝓕.FieldOp`. The list
`φsΛ.uncontractedListGet` of `𝓕.FieldOp` is defined as the list `φs` with
`φsΛ.uncontractedListGet` of `𝓕.FieldOp` is defined as the list `φs` with
all contracted positions removed, leaving the uncontracted `𝓕.FieldOp`.
The notation `[φsΛ]ᵘᶜ` is used for `φsΛ.uncontractedListGet`. -/