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

refactor: Fix typo

Browse source
This commit is contained in:
jstoobysmith 2025-02-05 10:04:41 +00:00
parent 48b46879c2
commit d61cc2ee4d
4 changed files with 8 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -55,7 +55,7 @@ lemma staticWickTerm_insert_zero_some (φ : 𝓕.FieldOp) (φs : List 𝓕.Field
simp only [← mul_assoc]
rw [← smul_mul_assoc]
congr 1
rw [staticConract_insertAndContract_some_eq_mul_contractStateAtIndex_lt]
rw [staticContract_insertAndContract_some_eq_mul_contractStateAtIndex_lt]
swap
· simp
rw [smul_smul]

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

@ -114,7 +114,7 @@ lemma wickTerm_insert_some (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
rw [wickTerm]
by_cases hg : GradingCompliant φs φsΛ ∧ (𝓕 |>ₛ φ) = (𝓕 |>ₛ φs[k.1])
· by_cases hk : i.succAbove k < i
· rw [WickContraction.timeConract_insertAndContract_some_eq_mul_contractStateAtIndex_not_lt]
· rw [WickContraction.timeContract_insertAndContract_some_eq_mul_contractStateAtIndex_not_lt]
swap
· exact hn _ hk
· rw [normalOrder_uncontracted_some, sign_insert_some_of_lt φ φs φsΛ i k hk hg]
@ -134,7 +134,7 @@ lemma wickTerm_insert_some (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
rw [mul_assoc, mul_assoc, mul_comm, mul_assoc, mul_assoc]
simp
· omega
· rw [timeConract_insertAndContract_some]
· rw [timeContract_insertAndContract_some]
simp only [Fin.getElem_fin, not_and] at hg
by_cases hg' : GradingCompliant φs φsΛ
· have hg := hg hg'

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

@ -66,7 +66,7 @@ lemma staticContract_insertAndContract_some
open FieldStatistic
lemma staticConract_insertAndContract_some_eq_mul_contractStateAtIndex_lt
lemma staticContract_insertAndContract_some_eq_mul_contractStateAtIndex_lt
(φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
(φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (k : φsΛ.uncontracted)
(hik : i < i.succAbove k) :

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

@ -50,7 +50,7 @@ lemma timeContract_insertAndContract_none (φ : 𝓕.FieldOp) (φs : List 𝓕.F
This follows from the fact that `(φsΛ ↩Λ φ i (some j))` has one more contracted pair than `φsΛ`,
corresponding to `φ` contracted with `φⱼ`. The order depends on whether we insert `φ` before
or after `φⱼ`. -/
lemma timeConract_insertAndContract_some
lemma timeContract_insertAndContract_some
(φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
(φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (j : φsΛ.uncontracted) :
(φsΛ ↩Λ φ i (some j)).timeContract =
@ -85,7 +85,7 @@ lemma timeContract_insertAndContract_some_eq_mul_contractStateAtIndex_lt
𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ ⟨φs.get, (φsΛ.uncontracted.filter (fun x => x < k))⟩)
• (contractStateAtIndex φ [φsΛ]ᵘᶜ ((uncontractedFieldOpEquiv φs φsΛ) (some k)) *
φsΛ.timeContract) := by
rw [timeConract_insertAndContract_some]
rw [timeContract_insertAndContract_some]
simp only [Nat.succ_eq_add_one, Fin.getElem_fin, ite_mul, instCommGroup.eq_1,
contractStateAtIndex, uncontractedFieldOpEquiv, Equiv.optionCongr_apply,
Equiv.coe_trans, Option.map_some', Function.comp_apply, finCongr_apply, Fin.coe_cast,
@ -110,7 +110,7 @@ lemma timeContract_insertAndContract_some_eq_mul_contractStateAtIndex_lt
simp only [exchangeSign_mul_self]
· exact ht
lemma timeConract_insertAndContract_some_eq_mul_contractStateAtIndex_not_lt
lemma timeContract_insertAndContract_some_eq_mul_contractStateAtIndex_not_lt
(φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
(φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (k : φsΛ.uncontracted)
(ht : ¬ 𝓕.timeOrderRel φs[k.1] φ) (hik : ¬ i < i.succAbove k) :
@ -118,7 +118,7 @@ lemma timeConract_insertAndContract_some_eq_mul_contractStateAtIndex_not_lt
𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ ⟨φs.get, (φsΛ.uncontracted.filter (fun x => x ≤ k))⟩)
• (contractStateAtIndex φ [φsΛ]ᵘᶜ
((uncontractedFieldOpEquiv φs φsΛ) (some k)) * φsΛ.timeContract) := by
rw [timeConract_insertAndContract_some]
rw [timeContract_insertAndContract_some]
simp only [Nat.succ_eq_add_one, Fin.getElem_fin, ite_mul, instCommGroup.eq_1,
contractStateAtIndex, uncontractedFieldOpEquiv, Equiv.optionCongr_apply,
Equiv.coe_trans, Option.map_some', Function.comp_apply, finCongr_apply, Fin.coe_cast,