From fa7536bea9b5acc23e09f201a7765792caebb199 Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Fri, 24 Jan 2025 07:18:48 +0000 Subject: [PATCH] refactor: Rename InsertList and Insert --- HepLean.lean | 4 +- .../Algebras/CrAnAlgebra/Basic.lean | 2 + .../WickContraction/Basic.lean | 4 +- .../WickContraction/ExtractEquiv.lean | 12 +- ...InsertList.lean => InsertAndContract.lean} | 138 +++++++------- ...{Insert.lean => InsertAndContractNat.lean} | 176 +++++++++--------- .../WickContraction/Involutions.lean | 2 +- .../WickContraction/Sign.lean | 142 +++++++------- .../WickContraction/TimeContract.lean | 28 +-- .../WickContraction/UncontractedList.lean | 2 +- HepLean/PerturbationTheory/WicksTheorem.lean | 93 +++++---- 11 files changed, 301 insertions(+), 302 deletions(-) rename HepLean/PerturbationTheory/WickContraction/{InsertList.lean => InsertAndContract.lean} (64%) rename HepLean/PerturbationTheory/WickContraction/{Insert.lean => InsertAndContractNat.lean} (73%) diff --git a/HepLean.lean b/HepLean.lean index bce244c..4207005 100644 --- a/HepLean.lean +++ b/HepLean.lean @@ -149,8 +149,8 @@ import HepLean.PerturbationTheory.Koszul.KoszulSignInsert import HepLean.PerturbationTheory.WickContraction.Basic import HepLean.PerturbationTheory.WickContraction.Erase import HepLean.PerturbationTheory.WickContraction.ExtractEquiv -import HepLean.PerturbationTheory.WickContraction.Insert -import HepLean.PerturbationTheory.WickContraction.InsertList +import HepLean.PerturbationTheory.WickContraction.InsertAndContract +import HepLean.PerturbationTheory.WickContraction.InsertAndContractNat import HepLean.PerturbationTheory.WickContraction.Involutions import HepLean.PerturbationTheory.WickContraction.IsFull import HepLean.PerturbationTheory.WickContraction.Sign diff --git a/HepLean/PerturbationTheory/Algebras/CrAnAlgebra/Basic.lean b/HepLean/PerturbationTheory/Algebras/CrAnAlgebra/Basic.lean index 774cbbc..a1846ea 100644 --- a/HepLean/PerturbationTheory/Algebras/CrAnAlgebra/Basic.lean +++ b/HepLean/PerturbationTheory/Algebras/CrAnAlgebra/Basic.lean @@ -85,6 +85,8 @@ lemma ofStateAlgebra_ofState (φ : 𝓕.States) : Roughly `[φ1, φ2]` gets sent to `(φ1ᶜ+ φ1ᵃ) * (φ2ᶜ+ φ2ᵃ)` etc. -/ def ofStateList (φs : List 𝓕.States) : CrAnAlgebra 𝓕 := (List.map ofState φs).prod +instance : Coe (List 𝓕.States) (CrAnAlgebra 𝓕) := ⟨ofStateList⟩ + @[simp] lemma ofStateList_nil : ofStateList ([] : List 𝓕.States) = 1 := rfl diff --git a/HepLean/PerturbationTheory/WickContraction/Basic.lean b/HepLean/PerturbationTheory/WickContraction/Basic.lean index c6eec58..f937215 100644 --- a/HepLean/PerturbationTheory/WickContraction/Basic.lean +++ b/HepLean/PerturbationTheory/WickContraction/Basic.lean @@ -478,8 +478,8 @@ lemma prod_finset_eq_mul_fst_snd (c : WickContraction n) (a : c.1) /-- A Wick contraction associated with a list of states is said to be `GradingCompliant` if in any contracted pair of states they are either both fermionic or both bosonic. -/ -def GradingCompliant (φs : List 𝓕.States) (c : WickContraction φs.length) := - ∀ (a : c.1), (𝓕 |>ₛ φs[c.fstFieldOfContract a]) = (𝓕 |>ₛ φs[c.sndFieldOfContract a]) +def GradingCompliant (φs : List 𝓕.States) (φsΛ : WickContraction φs.length) := + ∀ (a : φsΛ.1), (𝓕 |>ₛ φs[φsΛ.fstFieldOfContract a]) = (𝓕 |>ₛ φs[φsΛ.sndFieldOfContract a]) /-- An equivalence from the sigma type `(a : c.1) × a` to the subtype of `Fin n` consisting of those positions which are contracted. -/ diff --git a/HepLean/PerturbationTheory/WickContraction/ExtractEquiv.lean b/HepLean/PerturbationTheory/WickContraction/ExtractEquiv.lean index 6af31b0..6e17b3c 100644 --- a/HepLean/PerturbationTheory/WickContraction/ExtractEquiv.lean +++ b/HepLean/PerturbationTheory/WickContraction/ExtractEquiv.lean @@ -3,7 +3,7 @@ Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Joseph Tooby-Smith -/ -import HepLean.PerturbationTheory.WickContraction.Insert +import HepLean.PerturbationTheory.WickContraction.InsertAndContractNat /-! # Equivalence extracting element from contraction @@ -40,20 +40,20 @@ lemma extractEquiv_equiv {c1 c2 : (c : WickContraction n) × Option c.uncontract def extractEquiv (i : Fin n.succ) : WickContraction n.succ ≃ (c : WickContraction n) × Option c.uncontracted where toFun := fun c => ⟨erase c i, getDualErase c i⟩ - invFun := fun ⟨c, j⟩ => insert c i j + invFun := fun ⟨c, j⟩ => insertAndContractNat c i j left_inv f := by simp right_inv f := by refine extractEquiv_equiv ?_ ?_ - simp only [insert_erase] + simp only [insertAndContractNat_erase] simp only [Nat.succ_eq_add_one] - have h1 := insert_getDualErase f.fst i f.snd - exact insert_getDualErase _ i _ + have h1 := insertAndContractNat_getDualErase f.fst i f.snd + exact insertAndContractNat_getDualErase _ i _ lemma extractEquiv_symm_none_uncontracted (i : Fin n.succ) (c : WickContraction n) : ((extractEquiv i).symm ⟨c, none⟩).uncontracted = (Insert.insert i (c.uncontracted.map i.succAboveEmb)) := by - exact insert_none_uncontracted c i + exact insertAndContractNat_none_uncontracted c i @[simp] lemma extractEquiv_apply_congr_symm_apply {n m : ℕ} (k : ℕ) diff --git a/HepLean/PerturbationTheory/WickContraction/InsertList.lean b/HepLean/PerturbationTheory/WickContraction/InsertAndContract.lean similarity index 64% rename from HepLean/PerturbationTheory/WickContraction/InsertList.lean rename to HepLean/PerturbationTheory/WickContraction/InsertAndContract.lean index 28a0aea..9f0786a 100644 --- a/HepLean/PerturbationTheory/WickContraction/InsertList.lean +++ b/HepLean/PerturbationTheory/WickContraction/InsertAndContract.lean @@ -29,39 +29,39 @@ open HepLean.Fin `j : Option (c.uncontracted)` of `c`. The Wick contraction associated with `(φs.insertIdx i φ).length` formed by 'inserting' `φ` into `φs` after the first `i` elements and contracting it optionally with j. -/ -def insertList (φ : 𝓕.States) {φs : List 𝓕.States} (φsΛ : WickContraction φs.length) +def insertAndContract (φ : 𝓕.States) {φs : List 𝓕.States} (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (j : Option φsΛ.uncontracted) : WickContraction (φs.insertIdx i φ).length := - congr (by simp) (φsΛ.insert i j) + congr (by simp) (φsΛ.insertAndContractNat i j) @[simp] -lemma insertList_fstFieldOfContract (φ : 𝓕.States) (φs : List 𝓕.States) +lemma insertAndContract_fstFieldOfContract (φ : 𝓕.States) (φs : List 𝓕.States) (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (j : Option φsΛ.uncontracted) - (a : φsΛ.1) : (φsΛ.insertList φ i j).fstFieldOfContract + (a : φsΛ.1) : (φsΛ.insertAndContract φ i j).fstFieldOfContract (congrLift (insertIdx_length_fin φ φs i).symm (insertLift i j a)) = finCongr (insertIdx_length_fin φ φs i).symm (i.succAbove (φsΛ.fstFieldOfContract a)) := by - simp [insertList] + simp [insertAndContract] @[simp] -lemma insertList_sndFieldOfContract (φ : 𝓕.States) (φs : List 𝓕.States) +lemma insertAndContract_sndFieldOfContract (φ : 𝓕.States) (φs : List 𝓕.States) (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (j : Option (φsΛ.uncontracted)) - (a : φsΛ.1) : (φsΛ.insertList φ i j).sndFieldOfContract + (a : φsΛ.1) : (φsΛ.insertAndContract φ i j).sndFieldOfContract (congrLift (insertIdx_length_fin φ φs i).symm (insertLift i j a)) = finCongr (insertIdx_length_fin φ φs i).symm (i.succAbove (φsΛ.sndFieldOfContract a)) := by - simp [insertList] + simp [insertAndContract] @[simp] -lemma insertList_fstFieldOfContract_some_incl (φ : 𝓕.States) (φs : List 𝓕.States) +lemma insertAndContract_fstFieldOfContract_some_incl (φ : 𝓕.States) (φs : List 𝓕.States) (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (j : φsΛ.uncontracted) : - (insertList φ φsΛ i (some j)).fstFieldOfContract - (congrLift (insertIdx_length_fin φ φs i).symm ⟨{i, i.succAbove j}, by simp [insert]⟩) = + (insertAndContract φ φsΛ i (some j)).fstFieldOfContract + (congrLift (insertIdx_length_fin φ φs i).symm ⟨{i, i.succAbove j}, by simp [insertAndContractNat]⟩) = if i < i.succAbove j.1 then finCongr (insertIdx_length_fin φ φs i).symm i else finCongr (insertIdx_length_fin φ φs i).symm (i.succAbove j.1) := by split · rename_i h - refine (insertList φ φsΛ i (some j)).eq_fstFieldOfContract_of_mem - (a := congrLift (insertIdx_length_fin φ φs i).symm ⟨{i, i.succAbove j}, by simp [insert]⟩) + refine (insertAndContract φ φsΛ i (some j)).eq_fstFieldOfContract_of_mem + (a := congrLift (insertIdx_length_fin φ φs i).symm ⟨{i, i.succAbove j}, by simp [insertAndContractNat]⟩) (i := finCongr (insertIdx_length_fin φ φs i).symm i) (j := finCongr (insertIdx_length_fin φ φs i).symm (i.succAbove j)) ?_ ?_ ?_ · simp [congrLift] @@ -69,8 +69,8 @@ lemma insertList_fstFieldOfContract_some_incl (φ : 𝓕.States) (φs : List · rw [Fin.lt_def] at h ⊢ simp_all · rename_i h - refine (insertList φ φsΛ i (some j)).eq_fstFieldOfContract_of_mem - (a := congrLift (insertIdx_length_fin φ φs i).symm ⟨{i, i.succAbove j}, by simp [insert]⟩) + refine (insertAndContract φ φsΛ i (some j)).eq_fstFieldOfContract_of_mem + (a := congrLift (insertIdx_length_fin φ φs i).symm ⟨{i, i.succAbove j}, by simp [insertAndContractNat]⟩) (i := finCongr (insertIdx_length_fin φ φs i).symm (i.succAbove j)) (j := finCongr (insertIdx_length_fin φ φs i).symm i) ?_ ?_ ?_ · simp [congrLift] @@ -82,41 +82,41 @@ lemma insertList_fstFieldOfContract_some_incl (φ : 𝓕.States) (φs : List /-! -## insertList and getDual? +## insertAndContract and getDual? -/ @[simp] -lemma insertList_none_getDual?_self (φ : 𝓕.States) (φs : List 𝓕.States) +lemma insertAndContract_none_getDual?_self (φ : 𝓕.States) (φs : List 𝓕.States) (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) : - (insertList φ φsΛ i none).getDual? (Fin.cast (insertIdx_length_fin φ φs i).symm i) = none := by - simp only [Nat.succ_eq_add_one, insertList, getDual?_congr, finCongr_apply, Fin.cast_trans, + (insertAndContract φ φsΛ i none).getDual? (Fin.cast (insertIdx_length_fin φ φs i).symm i) = none := by + simp only [Nat.succ_eq_add_one, insertAndContract, getDual?_congr, finCongr_apply, Fin.cast_trans, Fin.cast_eq_self, Option.map_eq_none'] - have h1 := φsΛ.insert_none_getDual?_isNone i + have h1 := φsΛ.insertAndContractNat_none_getDual?_isNone i simpa using h1 -lemma insertList_isSome_getDual?_self (φ : 𝓕.States) (φs : List 𝓕.States) +lemma insertAndContract_isSome_getDual?_self (φ : 𝓕.States) (φs : List 𝓕.States) (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (j : φsΛ.uncontracted) : - ((insertList φ φsΛ i (some j)).getDual? + ((insertAndContract φ φsΛ i (some j)).getDual? (Fin.cast (insertIdx_length_fin φ φs i).symm i)).isSome := by - simp [insertList, getDual?_congr] + simp [insertAndContract, getDual?_congr] -lemma insertList_some_getDual?_self_not_none (φ : 𝓕.States) (φs : List 𝓕.States) +lemma insertAndContract_some_getDual?_self_not_none (φ : 𝓕.States) (φs : List 𝓕.States) (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (j : φsΛ.uncontracted) : - ¬ ((insertList φ φsΛ i (some j)).getDual? + ¬ ((insertAndContract φ φsΛ i (some j)).getDual? (Fin.cast (insertIdx_length_fin φ φs i).symm i)) = none := by - simp [insertList, getDual?_congr] + simp [insertAndContract, getDual?_congr] @[simp] -lemma insertList_some_getDual?_self_eq (φ : 𝓕.States) (φs : List 𝓕.States) +lemma insertAndContract_some_getDual?_self_eq (φ : 𝓕.States) (φs : List 𝓕.States) (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (j : φsΛ.uncontracted) : - ((insertList φ φsΛ i (some j)).getDual? (Fin.cast (insertIdx_length_fin φ φs i).symm i)) + ((insertAndContract φ φsΛ i (some j)).getDual? (Fin.cast (insertIdx_length_fin φ φs i).symm i)) = some (Fin.cast (insertIdx_length_fin φ φs i).symm (i.succAbove j)) := by - simp [insertList, getDual?_congr] + simp [insertAndContract, getDual?_congr] @[simp] -lemma insertList_some_getDual?_some_eq (φ : 𝓕.States) (φs : List 𝓕.States) +lemma insertAndContract_some_getDual?_some_eq (φ : 𝓕.States) (φs : List 𝓕.States) (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (j : φsΛ.uncontracted) : - ((insertList φ φsΛ i (some j)).getDual? + ((insertAndContract φ φsΛ i (some j)).getDual? (Fin.cast (insertIdx_length_fin φ φs i).symm (i.succAbove j))) = some (Fin.cast (insertIdx_length_fin φ φs i).symm i) := by rw [getDual?_eq_some_iff_mem] @@ -125,54 +125,54 @@ lemma insertList_some_getDual?_some_eq (φ : 𝓕.States) (φs : List 𝓕.State simp @[simp] -lemma insertList_none_succAbove_getDual?_eq_none_iff (φ : 𝓕.States) (φs : List 𝓕.States) +lemma insertAndContract_none_succAbove_getDual?_eq_none_iff (φ : 𝓕.States) (φs : List 𝓕.States) (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (j : Fin φs.length) : - (insertList φ φsΛ i none).getDual? (Fin.cast (insertIdx_length_fin φ φs i).symm + (insertAndContract φ φsΛ i none).getDual? (Fin.cast (insertIdx_length_fin φ φs i).symm (i.succAbove j)) = none ↔ φsΛ.getDual? j = none := by - simp [insertList, getDual?_congr] + simp [insertAndContract, getDual?_congr] @[simp] -lemma insertList_some_succAbove_getDual?_eq_option (φ : 𝓕.States) (φs : List 𝓕.States) +lemma insertAndContract_some_succAbove_getDual?_eq_option (φ : 𝓕.States) (φs : List 𝓕.States) (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (j : Fin φs.length) (k : φsΛ.uncontracted) (hkj : j ≠ k.1) : - (insertList φ φsΛ i (some k)).getDual? (Fin.cast (insertIdx_length_fin φ φs i).symm + (insertAndContract φ φsΛ i (some k)).getDual? (Fin.cast (insertIdx_length_fin φ φs i).symm (i.succAbove j)) = Option.map (Fin.cast (insertIdx_length_fin φ φs i).symm ∘ i.succAbove) (φsΛ.getDual? j) := by - simp only [Nat.succ_eq_add_one, insertList, getDual?_congr, finCongr_apply, Fin.cast_trans, - Fin.cast_eq_self, ne_eq, hkj, not_false_eq_true, insert_some_getDual?_of_neq, Option.map_map] + simp only [Nat.succ_eq_add_one, insertAndContract, getDual?_congr, finCongr_apply, Fin.cast_trans, + Fin.cast_eq_self, ne_eq, hkj, not_false_eq_true, insertAndContractNat_some_getDual?_of_neq, Option.map_map] rfl @[simp] -lemma insertList_none_succAbove_getDual?_isSome_iff (φ : 𝓕.States) (φs : List 𝓕.States) +lemma insertAndContract_none_succAbove_getDual?_isSome_iff (φ : 𝓕.States) (φs : List 𝓕.States) (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (j : Fin φs.length) : - ((insertList φ φsΛ i none).getDual? (Fin.cast (insertIdx_length_fin φ φs i).symm + ((insertAndContract φ φsΛ i none).getDual? (Fin.cast (insertIdx_length_fin φ φs i).symm (i.succAbove j))).isSome ↔ (φsΛ.getDual? j).isSome := by rw [← not_iff_not] simp @[simp] -lemma insertList_none_getDual?_get_eq (φ : 𝓕.States) (φs : List 𝓕.States) +lemma insertAndContract_none_getDual?_get_eq (φ : 𝓕.States) (φs : List 𝓕.States) (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (j : Fin φs.length) - (h : ((insertList φ φsΛ i none).getDual? (Fin.cast (insertIdx_length_fin φ φs i).symm + (h : ((insertAndContract φ φsΛ i none).getDual? (Fin.cast (insertIdx_length_fin φ φs i).symm (i.succAbove j))).isSome) : - ((insertList φ φsΛ i none).getDual? (Fin.cast (insertIdx_length_fin φ φs i).symm + ((insertAndContract φ φsΛ i none).getDual? (Fin.cast (insertIdx_length_fin φ φs i).symm (i.succAbove j))).get h = Fin.cast (insertIdx_length_fin φ φs i).symm (i.succAbove ((φsΛ.getDual? j).get (by simpa using h))) := by - simp [insertList, getDual?_congr_get] + simp [insertAndContract, getDual?_congr_get] /-........................................... -/ @[simp] -lemma insertList_sndFieldOfContract_some_incl (φ : 𝓕.States) (φs : List 𝓕.States) +lemma insertAndContract_sndFieldOfContract_some_incl (φ : 𝓕.States) (φs : List 𝓕.States) (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (j : φsΛ.uncontracted) : - (insertList φ φsΛ i (some j)).sndFieldOfContract - (congrLift (insertIdx_length_fin φ φs i).symm ⟨{i, i.succAbove j}, by simp [insert]⟩) = + (insertAndContract φ φsΛ i (some j)).sndFieldOfContract + (congrLift (insertIdx_length_fin φ φs i).symm ⟨{i, i.succAbove j}, by simp [insertAndContractNat]⟩) = if i < i.succAbove j.1 then finCongr (insertIdx_length_fin φ φs i).symm (i.succAbove j.1) else finCongr (insertIdx_length_fin φ φs i).symm i := by split · rename_i h - refine (insertList φ φsΛ i (some j)).eq_sndFieldOfContract_of_mem - (a := congrLift (insertIdx_length_fin φ φs i).symm ⟨{i, i.succAbove j}, by simp [insert]⟩) + refine (insertAndContract φ φsΛ i (some j)).eq_sndFieldOfContract_of_mem + (a := congrLift (insertIdx_length_fin φ φs i).symm ⟨{i, i.succAbove j}, by simp [insertAndContractNat]⟩) (i := finCongr (insertIdx_length_fin φ φs i).symm i) (j := finCongr (insertIdx_length_fin φ φs i).symm (i.succAbove j)) ?_ ?_ ?_ · simp [congrLift] @@ -180,8 +180,8 @@ lemma insertList_sndFieldOfContract_some_incl (φ : 𝓕.States) (φs : List · rw [Fin.lt_def] at h ⊢ simp_all · rename_i h - refine (insertList φ φsΛ i (some j)).eq_sndFieldOfContract_of_mem - (a := congrLift (insertIdx_length_fin φ φs i).symm ⟨{i, i.succAbove j}, by simp [insert]⟩) + refine (insertAndContract φ φsΛ i (some j)).eq_sndFieldOfContract_of_mem + (a := congrLift (insertIdx_length_fin φ φs i).symm ⟨{i, i.succAbove j}, by simp [insertAndContractNat]⟩) (i := finCongr (insertIdx_length_fin φ φs i).symm (i.succAbove j)) (j := finCongr (insertIdx_length_fin φ φs i).symm i) ?_ ?_ ?_ · simp [congrLift] @@ -191,26 +191,26 @@ lemma insertList_sndFieldOfContract_some_incl (φ : 𝓕.States) (φs : List have hi : i.succAbove j ≠ i := Fin.succAbove_ne i j omega -lemma insertList_none_prod_contractions (φ : 𝓕.States) (φs : List 𝓕.States) +lemma insertAndContract_none_prod_contractions (φ : 𝓕.States) (φs : List 𝓕.States) (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) - (f : (φsΛ.insertList φ i none).1 → M) [CommMonoid M] : + (f : (φsΛ.insertAndContract φ i none).1 → M) [CommMonoid M] : ∏ a, f a = ∏ (a : φsΛ.1), f (congrLift (insertIdx_length_fin φ φs i).symm (insertLift i none a)) := by let e1 := Equiv.ofBijective (φsΛ.insertLift i none) (insertLift_none_bijective i) let e2 := Equiv.ofBijective (congrLift (insertIdx_length_fin φ φs i).symm) - ((φsΛ.insert i none).congrLift_bijective ((insertIdx_length_fin φ φs i).symm)) + ((φsΛ.insertAndContractNat i none).congrLift_bijective ((insertIdx_length_fin φ φs i).symm)) erw [← e2.prod_comp] erw [← e1.prod_comp] rfl -lemma insertList_some_prod_contractions (φ : 𝓕.States) (φs : List 𝓕.States) +lemma insertAndContract_some_prod_contractions (φ : 𝓕.States) (φs : List 𝓕.States) (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (j : φsΛ.uncontracted) - (f : (φsΛ.insertList φ i (some j)).1 → M) [CommMonoid M] : + (f : (φsΛ.insertAndContract φ i (some j)).1 → M) [CommMonoid M] : ∏ a, f a = f (congrLift (insertIdx_length_fin φ φs i).symm - ⟨{i, i.succAbove j}, by simp [insert]⟩) * + ⟨{i, i.succAbove j}, by simp [insertAndContractNat]⟩) * ∏ (a : φsΛ.1), f (congrLift (insertIdx_length_fin φ φs i).symm (insertLift i (some j) a)) := by let e2 := Equiv.ofBijective (congrLift (insertIdx_length_fin φ φs i).symm) - ((φsΛ.insert i (some j)).congrLift_bijective ((insertIdx_length_fin φ φs i).symm)) + ((φsΛ.insertAndContractNat i (some j)).congrLift_bijective ((insertIdx_length_fin φ φs i).symm)) erw [← e2.prod_comp] let e1 := Equiv.ofBijective (φsΛ.insertLiftSome i j) (insertLiftSome_bijective i j) erw [← e1.prod_comp] @@ -221,26 +221,26 @@ lemma insertList_some_prod_contractions (φ : 𝓕.States) (φs : List 𝓕.Stat /-- Given a finite set of `Fin φs.length` the finite set of `(φs.insertIdx i φ).length` formed by mapping elements using `i.succAboveEmb` and `finCongr`. -/ -def insertListLiftFinset (φ : 𝓕.States) {φs : List 𝓕.States} +def insertAndContractLiftFinset (φ : 𝓕.States) {φs : List 𝓕.States} (i : Fin φs.length.succ) (a : Finset (Fin φs.length)) : Finset (Fin (φs.insertIdx i φ).length) := (a.map i.succAboveEmb).map (finCongr (insertIdx_length_fin φ φs i).symm).toEmbedding @[simp] -lemma self_not_mem_insertListLiftFinset (φ : 𝓕.States) {φs : List 𝓕.States} +lemma self_not_mem_insertAndContractLiftFinset (φ : 𝓕.States) {φs : List 𝓕.States} (i : Fin φs.length.succ) (a : Finset (Fin φs.length)) : - Fin.cast (insertIdx_length_fin φ φs i).symm i ∉ insertListLiftFinset φ i a := by - simp only [Nat.succ_eq_add_one, insertListLiftFinset, Finset.mem_map_equiv, finCongr_symm, + Fin.cast (insertIdx_length_fin φ φs i).symm i ∉ insertAndContractLiftFinset φ i a := by + simp only [Nat.succ_eq_add_one, insertAndContractLiftFinset, Finset.mem_map_equiv, finCongr_symm, finCongr_apply, Fin.cast_trans, Fin.cast_eq_self] simp only [Finset.mem_map, Fin.succAboveEmb_apply, not_exists, not_and] intro x exact fun a => Fin.succAbove_ne i x -lemma succAbove_mem_insertListLiftFinset (φ : 𝓕.States) {φs : List 𝓕.States} +lemma succAbove_mem_insertAndContractLiftFinset (φ : 𝓕.States) {φs : List 𝓕.States} (i : Fin φs.length.succ) (a : Finset (Fin φs.length)) (j : Fin φs.length) : - Fin.cast (insertIdx_length_fin φ φs i).symm (i.succAbove j) ∈ insertListLiftFinset φ i a ↔ + Fin.cast (insertIdx_length_fin φ φs i).symm (i.succAbove j) ∈ insertAndContractLiftFinset φ i a ↔ j ∈ a := by - simp only [insertListLiftFinset, Finset.mem_map_equiv, finCongr_symm, finCongr_apply, + simp only [insertAndContractLiftFinset, Finset.mem_map_equiv, finCongr_symm, finCongr_apply, Fin.cast_trans, Fin.cast_eq_self] simp only [Finset.mem_map, Fin.succAboveEmb_apply] apply Iff.intro @@ -266,10 +266,10 @@ lemma insert_fin_eq_self (φ : 𝓕.States) {φs : List 𝓕.States} use z rfl -lemma insertList_uncontractedList_none_map (φ : 𝓕.States) {φs : List 𝓕.States} +lemma insertAndContract_uncontractedList_none_map (φ : 𝓕.States) {φs : List 𝓕.States} (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) : - [φsΛ.insertList φ i none]ᵘᶜ = List.insertIdx (φsΛ.uncontractedListOrderPos i) φ [φsΛ]ᵘᶜ := by - simp only [Nat.succ_eq_add_one, insertList, uncontractedListGet] + [φsΛ.insertAndContract φ i none]ᵘᶜ = List.insertIdx (φsΛ.uncontractedListOrderPos i) φ [φsΛ]ᵘᶜ := by + simp only [Nat.succ_eq_add_one, insertAndContract, uncontractedListGet] rw [congr_uncontractedList] erw [uncontractedList_extractEquiv_symm_none] rw [orderedInsert_succAboveEmb_uncontractedList_eq_insertIdx] @@ -284,7 +284,7 @@ lemma insertList_uncontractedList_none_map (φ : 𝓕.States) {φs : List 𝓕.S lemma insertLift_sum (φ : 𝓕.States) {φs : List 𝓕.States} (i : Fin φs.length.succ) [AddCommMonoid M] (f : WickContraction (φs.insertIdx i φ).length → M) : ∑ c, f c = ∑ (φsΛ : WickContraction φs.length), ∑ (k : Option φsΛ.uncontracted), - f (φsΛ.insertList φ i k) := by + f (φsΛ.insertAndContract φ i k) := by rw [sum_extractEquiv_congr (finCongr (insertIdx_length_fin φ φs i).symm i) f (insertIdx_length_fin φ φs i)] rfl diff --git a/HepLean/PerturbationTheory/WickContraction/Insert.lean b/HepLean/PerturbationTheory/WickContraction/InsertAndContractNat.lean similarity index 73% rename from HepLean/PerturbationTheory/WickContraction/Insert.lean rename to HepLean/PerturbationTheory/WickContraction/InsertAndContractNat.lean index c4a9a26..f93eb45 100644 --- a/HepLean/PerturbationTheory/WickContraction/Insert.lean +++ b/HepLean/PerturbationTheory/WickContraction/InsertAndContractNat.lean @@ -28,7 +28,7 @@ open HepLean.Fin an optional uncontracted element `j : Option (c.uncontracted)` of `c`. The Wick contraction for `n.succ` formed by 'inserting' `i` into `Fin n` and contracting it optionally with `j`. -/ -def insert (c : WickContraction n) (i : Fin n.succ) (j : Option (c.uncontracted)) : +def insertAndContractNat (c : WickContraction n) (i : Fin n.succ) (j : Option (c.uncontracted)) : WickContraction n.succ := by let f := Finset.map (Finset.mapEmbedding i.succAboveEmb).toEmbedding c.1 let f' := match j with | none => f | some j => Insert.insert {i, i.succAbove j} f @@ -123,21 +123,21 @@ def insert (c : WickContraction n) (i : Fin n.succ) (j : Option (c.uncontracted) rw [Finset.mapEmbedding_apply, Finset.mapEmbedding_apply, Finset.disjoint_map] exact c.2.2 a' ha' b' hb' -lemma insert_of_isSome (c : WickContraction n) (i : Fin n.succ) (j : Option c.uncontracted) - (hj : j.isSome) : (insert c i j).1 = Insert.insert {i, i.succAbove (j.get hj)} +lemma insertAndContractNat_of_isSome (c : WickContraction n) (i : Fin n.succ) (j : Option c.uncontracted) + (hj : j.isSome) : (insertAndContractNat c i j).1 = Insert.insert {i, i.succAbove (j.get hj)} (Finset.map (Finset.mapEmbedding i.succAboveEmb).toEmbedding c.1) := by - simp only [Nat.succ_eq_add_one, insert, Finset.le_eq_subset] + simp only [Nat.succ_eq_add_one, insertAndContractNat, Finset.le_eq_subset] rw [@Option.isSome_iff_exists] at hj obtain ⟨j, hj⟩ := hj subst hj simp @[simp] -lemma self_mem_uncontracted_of_insert_none (c : WickContraction n) (i : Fin n.succ) : - i ∈ (insert c i none).uncontracted := by +lemma self_mem_uncontracted_of_insertAndContractNat_none (c : WickContraction n) (i : Fin n.succ) : + i ∈ (insertAndContractNat c i none).uncontracted := by rw [mem_uncontracted_iff_not_contracted] intro p hp - simp only [Nat.succ_eq_add_one, insert, Finset.le_eq_subset, Finset.mem_map, + simp only [Nat.succ_eq_add_one, insertAndContractNat, Finset.le_eq_subset, Finset.mem_map, RelEmbedding.coe_toEmbedding] at hp obtain ⟨a, ha, ha'⟩ := hp have hc := c.2.1 a ha @@ -153,15 +153,15 @@ lemma self_mem_uncontracted_of_insert_none (c : WickContraction n) (i : Fin n.su · exact Fin.ne_succAbove i y @[simp] -lemma self_not_mem_uncontracted_of_insert_some (c : WickContraction n) (i : Fin n.succ) - (j : c.uncontracted) : i ∉ (insert c i (some j)).uncontracted := by +lemma self_not_mem_uncontracted_of_insertAndContractNat_some (c : WickContraction n) (i : Fin n.succ) + (j : c.uncontracted) : i ∉ (insertAndContractNat c i (some j)).uncontracted := by rw [mem_uncontracted_iff_not_contracted] - simp [insert] + simp [insertAndContractNat] -lemma insert_succAbove_mem_uncontracted_iff (c : WickContraction n) (i : Fin n.succ) (j : Fin n) : - (i.succAbove j) ∈ (insert c i none).uncontracted ↔ j ∈ c.uncontracted := by +lemma insertAndContractNat_succAbove_mem_uncontracted_iff (c : WickContraction n) (i : Fin n.succ) (j : Fin n) : + (i.succAbove j) ∈ (insertAndContractNat c i none).uncontracted ↔ j ∈ c.uncontracted := by rw [mem_uncontracted_iff_not_contracted, mem_uncontracted_iff_not_contracted] - simp only [Nat.succ_eq_add_one, insert, Finset.le_eq_subset, Finset.mem_map, + simp only [Nat.succ_eq_add_one, insertAndContractNat, Finset.le_eq_subset, Finset.mem_map, RelEmbedding.coe_toEmbedding, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂] apply Iff.intro · intro h p hp @@ -191,8 +191,8 @@ lemma insert_succAbove_mem_uncontracted_iff (c : WickContraction n) (i : Fin n.s (fun a => hp'.2 (i.succAbove_right_injective a)) @[simp] -lemma mem_uncontracted_insert_none_iff (c : WickContraction n) (i : Fin n.succ) (k : Fin n.succ) : - k ∈ (insert c i none).uncontracted ↔ +lemma mem_uncontracted_insertAndContractNat_none_iff (c : WickContraction n) (i : Fin n.succ) (k : Fin n.succ) : + k ∈ (insertAndContractNat c i none).uncontracted ↔ k = i ∨ ∃ j, k = i.succAbove j ∧ j ∈ c.uncontracted := by by_cases hi : k = i · subst hi @@ -201,7 +201,7 @@ lemma mem_uncontracted_insert_none_iff (c : WickContraction n) (i : Fin n.succ) obtain ⟨z, hk⟩ := hi subst hk have hn : ¬ i.succAbove z = i := Fin.succAbove_ne i z - simp only [Nat.succ_eq_add_one, insert_succAbove_mem_uncontracted_iff, hn, false_or] + simp only [Nat.succ_eq_add_one, insertAndContractNat_succAbove_mem_uncontracted_iff, hn, false_or] apply Iff.intro · intro h exact ⟨z, rfl, h⟩ @@ -211,10 +211,10 @@ lemma mem_uncontracted_insert_none_iff (c : WickContraction n) (i : Fin n.succ) subst hjk exact hk.2 -lemma insert_none_uncontracted (c : WickContraction n) (i : Fin n.succ) : - (insert c i none).uncontracted = Insert.insert i (c.uncontracted.map i.succAboveEmb) := by +lemma insertAndContractNat_none_uncontracted (c : WickContraction n) (i : Fin n.succ) : + (insertAndContractNat c i none).uncontracted = Insert.insert i (c.uncontracted.map i.succAboveEmb) := by ext a - simp only [Nat.succ_eq_add_one, mem_uncontracted_insert_none_iff, Finset.mem_insert, + simp only [Nat.succ_eq_add_one, mem_uncontracted_insertAndContractNat_none_iff, Finset.mem_insert, Finset.mem_map, Fin.succAboveEmb_apply] apply Iff.intro · intro a_1 @@ -249,13 +249,13 @@ lemma insert_none_uncontracted (c : WickContraction n) (i : Fin n.succ) : · simp_all only @[simp] -lemma mem_uncontracted_insert_some_iff (c : WickContraction n) (i : Fin n.succ) +lemma mem_uncontracted_insertAndContractNat_some_iff (c : WickContraction n) (i : Fin n.succ) (k : Fin n.succ) (j : c.uncontracted) : - k ∈ (insert c i (some j)).uncontracted ↔ + k ∈ (insertAndContractNat c i (some j)).uncontracted ↔ ∃ z, k = i.succAbove z ∧ z ∈ c.uncontracted ∧ z ≠ j := by by_cases hki : k = i · subst hki - simp only [Nat.succ_eq_add_one, self_not_mem_uncontracted_of_insert_some, ne_eq, false_iff, + simp only [Nat.succ_eq_add_one, self_not_mem_uncontracted_of_insertAndContractNat_some, ne_eq, false_iff, not_exists, not_and, Decidable.not_not] exact fun x hx => False.elim (Fin.ne_succAbove k x hx) · simp only [Nat.succ_eq_add_one, ← Fin.exists_succAbove_eq_iff] at hki @@ -264,7 +264,7 @@ lemma mem_uncontracted_insert_some_iff (c : WickContraction n) (i : Fin n.succ) by_cases hjz : j = z · subst hjz rw [mem_uncontracted_iff_not_contracted] - simp only [Nat.succ_eq_add_one, insert, Finset.le_eq_subset, Finset.mem_insert, + simp only [Nat.succ_eq_add_one, insertAndContractNat, Finset.le_eq_subset, Finset.mem_insert, Finset.mem_map, RelEmbedding.coe_toEmbedding, forall_eq_or_imp, Finset.mem_singleton, or_true, not_true_eq_false, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂, false_and, ne_eq, false_iff, not_exists, not_and, Decidable.not_not] @@ -279,7 +279,7 @@ lemma mem_uncontracted_insert_some_iff (c : WickContraction n) (i : Fin n.succ) rw [mem_uncontracted_iff_not_contracted] intro p hp rw [mem_uncontracted_iff_not_contracted] at h - simp only [Nat.succ_eq_add_one, insert, Finset.le_eq_subset, Finset.mem_insert, + simp only [Nat.succ_eq_add_one, insertAndContractNat, Finset.le_eq_subset, Finset.mem_insert, Finset.mem_map, RelEmbedding.coe_toEmbedding, forall_eq_or_imp, Finset.mem_singleton, not_or, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂] at h have hc := h.2 p hp @@ -290,7 +290,7 @@ lemma mem_uncontracted_insert_some_iff (c : WickContraction n) (i : Fin n.succ) rw [Function.Injective.eq_iff (Fin.succAbove_right_injective)] at hz'1 subst hz'1 rw [mem_uncontracted_iff_not_contracted] - simp only [Nat.succ_eq_add_one, insert, Finset.le_eq_subset, Finset.mem_insert, + simp only [Nat.succ_eq_add_one, insertAndContractNat, Finset.le_eq_subset, Finset.mem_insert, Finset.mem_map, RelEmbedding.coe_toEmbedding, forall_eq_or_imp, Finset.mem_singleton, not_or, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂] apply And.intro @@ -299,10 +299,10 @@ lemma mem_uncontracted_insert_some_iff (c : WickContraction n) (i : Fin n.succ) · rw [mem_uncontracted_iff_not_contracted] at hz' exact fun a ha hc => hz'.1 a ha ((Finset.mem_map' (i.succAboveEmb)).mp hc) -lemma insert_some_uncontracted (c : WickContraction n) (i : Fin n.succ) (j : c.uncontracted) : - (insert c i (some j)).uncontracted = (c.uncontracted.erase j).map i.succAboveEmb := by +lemma insertAndContractNat_some_uncontracted (c : WickContraction n) (i : Fin n.succ) (j : c.uncontracted) : + (insertAndContractNat c i (some j)).uncontracted = (c.uncontracted.erase j).map i.succAboveEmb := by ext a - simp only [Nat.succ_eq_add_one, mem_uncontracted_insert_some_iff, ne_eq, Finset.map_erase, + simp only [Nat.succ_eq_add_one, mem_uncontracted_insertAndContractNat_some_iff, ne_eq, Finset.map_erase, Fin.succAboveEmb_apply, Finset.mem_erase, Finset.mem_map] apply Iff.intro · intro h @@ -329,35 +329,35 @@ lemma insert_some_uncontracted (c : WickContraction n) (i : Fin n.succ) (j : c.u -/ -lemma insert_none_getDual?_isNone (c : WickContraction n) (i : Fin n.succ) : - ((insert c i none).getDual? i).isNone := by - have hi : i ∈ (insert c i none).uncontracted := by +lemma insertAndContractNat_none_getDual?_isNone (c : WickContraction n) (i : Fin n.succ) : + ((insertAndContractNat c i none).getDual? i).isNone := by + have hi : i ∈ (insertAndContractNat c i none).uncontracted := by simp simp only [Nat.succ_eq_add_one, uncontracted, Finset.mem_filter, Finset.mem_univ, true_and] at hi rw [hi] simp @[simp] -lemma insert_succAbove_getDual?_eq_none_iff (c : WickContraction n) (i : Fin n.succ) (j : Fin n) : - (insert c i none).getDual? (i.succAbove j) = none ↔ c.getDual? j = none := by - have h1 := insert_succAbove_mem_uncontracted_iff c i j +lemma insertAndContractNat_succAbove_getDual?_eq_none_iff (c : WickContraction n) (i : Fin n.succ) (j : Fin n) : + (insertAndContractNat c i none).getDual? (i.succAbove j) = none ↔ c.getDual? j = none := by + have h1 := insertAndContractNat_succAbove_mem_uncontracted_iff c i j simpa [uncontracted] using h1 @[simp] -lemma insert_succAbove_getDual?_isSome_iff (c : WickContraction n) (i : Fin n.succ) (j : Fin n) : - ((insert c i none).getDual? (i.succAbove j)).isSome ↔ (c.getDual? j).isSome := by +lemma insertAndContractNat_succAbove_getDual?_isSome_iff (c : WickContraction n) (i : Fin n.succ) (j : Fin n) : + ((insertAndContractNat c i none).getDual? (i.succAbove j)).isSome ↔ (c.getDual? j).isSome := by rw [← not_iff_not] simp @[simp] -lemma insert_succAbove_getDual?_get (c : WickContraction n) (i : Fin n.succ) (j : Fin n) - (h : ((insert c i none).getDual? (i.succAbove j)).isSome) : - ((insert c i none).getDual? (i.succAbove j)).get h = +lemma insertAndContractNat_succAbove_getDual?_get (c : WickContraction n) (i : Fin n.succ) (j : Fin n) + (h : ((insertAndContractNat c i none).getDual? (i.succAbove j)).isSome) : + ((insertAndContractNat c i none).getDual? (i.succAbove j)).get h = i.succAbove ((c.getDual? j).get (by simpa using h)) := by - have h1 : (insert c i none).getDual? (i.succAbove j) = some + have h1 : (insertAndContractNat c i none).getDual? (i.succAbove j) = some (i.succAbove ((c.getDual? j).get (by simpa using h))) := by rw [getDual?_eq_some_iff_mem] - simp only [Nat.succ_eq_add_one, insert, Finset.le_eq_subset, Finset.mem_map, + simp only [Nat.succ_eq_add_one, insertAndContractNat, Finset.le_eq_subset, Finset.mem_map, RelEmbedding.coe_toEmbedding] use {j, ((c.getDual? j).get (by simpa using h))} simp only [self_getDual?_get_mem, true_and] @@ -366,50 +366,50 @@ lemma insert_succAbove_getDual?_get (c : WickContraction n) (i : Fin n.succ) (j exact Option.get_of_mem h h1 @[simp] -lemma insert_some_getDual?_eq (c : WickContraction n) (i : Fin n.succ) (j : c.uncontracted) : - (insert c i (some j)).getDual? i = some (i.succAbove j) := by +lemma insertAndContractNat_some_getDual?_eq (c : WickContraction n) (i : Fin n.succ) (j : c.uncontracted) : + (insertAndContractNat c i (some j)).getDual? i = some (i.succAbove j) := by rw [getDual?_eq_some_iff_mem] - simp [insert] + simp [insertAndContractNat] @[simp] -lemma insert_some_getDual?_neq_none (c : WickContraction n) (i : Fin n.succ) (j : c.uncontracted) +lemma insertAndContractNat_some_getDual?_neq_none (c : WickContraction n) (i : Fin n.succ) (j : c.uncontracted) (k : Fin n) (hkj : k ≠ j.1) : - (insert c i (some j)).getDual? (i.succAbove k) = none ↔ c.getDual? k = none := by + (insertAndContractNat c i (some j)).getDual? (i.succAbove k) = none ↔ c.getDual? k = none := by apply Iff.intro · intro h - have hk : (i.succAbove k) ∈ (insert c i (some j)).uncontracted := by + have hk : (i.succAbove k) ∈ (insertAndContractNat c i (some j)).uncontracted := by simp only [Nat.succ_eq_add_one, uncontracted, Finset.mem_filter, Finset.mem_univ, true_and] exact h - simp only [Nat.succ_eq_add_one, mem_uncontracted_insert_some_iff, ne_eq] at hk + simp only [Nat.succ_eq_add_one, mem_uncontracted_insertAndContractNat_some_iff, ne_eq] at hk obtain ⟨z, hz1, hz2, hz3⟩ := hk rw [Function.Injective.eq_iff (Fin.succAbove_right_injective)] at hz1 subst hz1 simpa [uncontracted] using hz2 · intro h - have hk : (i.succAbove k) ∈ (insert c i (some j)).uncontracted := by - simp only [Nat.succ_eq_add_one, mem_uncontracted_insert_some_iff, ne_eq] + have hk : (i.succAbove k) ∈ (insertAndContractNat c i (some j)).uncontracted := by + simp only [Nat.succ_eq_add_one, mem_uncontracted_insertAndContractNat_some_iff, ne_eq] use k simp only [hkj, not_false_eq_true, and_true, true_and] simpa [uncontracted] using h - simpa [uncontracted, -mem_uncontracted_insert_some_iff, ne_eq] using hk + simpa [uncontracted, -mem_uncontracted_insertAndContractNat_some_iff, ne_eq] using hk @[simp] -lemma insert_some_getDual?_neq_isSome (c : WickContraction n) (i : Fin n.succ) (j : c.uncontracted) +lemma insertAndContractNat_some_getDual?_neq_isSome (c : WickContraction n) (i : Fin n.succ) (j : c.uncontracted) (k : Fin n) (hkj : k ≠ j.1) : - ((insert c i (some j)).getDual? (i.succAbove k)).isSome ↔ (c.getDual? k).isSome := by + ((insertAndContractNat c i (some j)).getDual? (i.succAbove k)).isSome ↔ (c.getDual? k).isSome := by rw [← not_iff_not] simp [hkj] @[simp] -lemma insert_some_getDual?_neq_isSome_get (c : WickContraction n) (i : Fin n.succ) +lemma insertAndContractNat_some_getDual?_neq_isSome_get (c : WickContraction n) (i : Fin n.succ) (j : c.uncontracted) (k : Fin n) (hkj : k ≠ j.1) - (h : ((insert c i (some j)).getDual? (i.succAbove k)).isSome) : - ((insert c i (some j)).getDual? (i.succAbove k)).get h = + (h : ((insertAndContractNat c i (some j)).getDual? (i.succAbove k)).isSome) : + ((insertAndContractNat c i (some j)).getDual? (i.succAbove k)).get h = i.succAbove ((c.getDual? k).get (by simpa [hkj] using h)) := by - have h1 : ((insert c i (some j)).getDual? (i.succAbove k)) + have h1 : ((insertAndContractNat c i (some j)).getDual? (i.succAbove k)) = some (i.succAbove ((c.getDual? k).get (by simpa [hkj] using h))) := by rw [getDual?_eq_some_iff_mem] - simp only [Nat.succ_eq_add_one, insert, Finset.le_eq_subset, Finset.mem_insert, Finset.mem_map, + simp only [Nat.succ_eq_add_one, insertAndContractNat, Finset.le_eq_subset, Finset.mem_insert, Finset.mem_map, RelEmbedding.coe_toEmbedding] apply Or.inr use { k, ((c.getDual? k).get (by simpa [hkj] using h))} @@ -419,14 +419,14 @@ lemma insert_some_getDual?_neq_isSome_get (c : WickContraction n) (i : Fin n.suc exact Option.get_of_mem h h1 @[simp] -lemma insert_some_getDual?_of_neq (c : WickContraction n) (i : Fin n.succ) (j : c.uncontracted) +lemma insertAndContractNat_some_getDual?_of_neq (c : WickContraction n) (i : Fin n.succ) (j : c.uncontracted) (k : Fin n) (hkj : k ≠ j.1) : - (insert c i (some j)).getDual? (i.succAbove k) = + (insertAndContractNat c i (some j)).getDual? (i.succAbove k) = Option.map i.succAbove (c.getDual? k) := by by_cases h : (c.getDual? k).isSome - · have h1 : (c.insert i (some j)).getDual? (i.succAbove k) = + · have h1 : (c.insertAndContractNat i (some j)).getDual? (i.succAbove k) = some (i.succAbove ((c.getDual? k).get h)) := by - rw [← insert_some_getDual?_neq_isSome_get c i j k hkj] + rw [← insertAndContractNat_some_getDual?_neq_isSome_get c i j k hkj] refine Eq.symm (Option.some_get ?_) simpa [hkj] using h rw [h1] @@ -435,7 +435,7 @@ lemma insert_some_getDual?_of_neq (c : WickContraction n) (i : Fin n.succ) (j : rw [@Option.map_coe'] · simp only [Bool.not_eq_true, Option.not_isSome, Option.isNone_iff_eq_none] at h simp only [Nat.succ_eq_add_one, h, Option.map_none'] - simp only [ne_eq, hkj, not_false_eq_true, insert_some_getDual?_neq_none] + simp only [ne_eq, hkj, not_false_eq_true, insertAndContractNat_some_getDual?_neq_none] exact h /-! @@ -444,10 +444,10 @@ lemma insert_some_getDual?_of_neq (c : WickContraction n) (i : Fin n.succ) (j : -/ @[simp] -lemma insert_erase (c : WickContraction n) (i : Fin n.succ) (j : Option (c.uncontracted)) : - erase (insert c i j) i = c := by +lemma insertAndContractNat_erase (c : WickContraction n) (i : Fin n.succ) (j : Option (c.uncontracted)) : + erase (insertAndContractNat c i j) i = c := by refine Subtype.eq ?_ - simp only [erase, Nat.succ_eq_add_one, insert, Finset.le_eq_subset] + simp only [erase, Nat.succ_eq_add_one, insertAndContractNat, Finset.le_eq_subset] conv_rhs => rw [c.eq_filter_mem_self] refine Finset.filter_inj'.mpr ?_ intro a _ @@ -489,31 +489,31 @@ lemma insert_erase (c : WickContraction n) (i : Fin n.succ) (j : Option (c.uncon simp only [ha, true_and] rw [Finset.mapEmbedding_apply] -lemma insert_getDualErase (c : WickContraction n) (i : Fin n.succ) (j : Option c.uncontracted) : - (insert c i j).getDualErase i = - uncontractedCongr (c := c) (c' := (c.insert i j).erase i) (by simp) j := by +lemma insertAndContractNat_getDualErase (c : WickContraction n) (i : Fin n.succ) (j : Option c.uncontracted) : + (insertAndContractNat c i j).getDualErase i = + uncontractedCongr (c := c) (c' := (c.insertAndContractNat i j).erase i) (by simp) j := by match n with | 0 => - simp only [insert, Nat.succ_eq_add_one, Nat.reduceAdd, Finset.le_eq_subset, getDualErase] + simp only [insertAndContractNat, Nat.succ_eq_add_one, Nat.reduceAdd, Finset.le_eq_subset, getDualErase] fin_cases j simp | Nat.succ n => match j with | none => - have hi := insert_none_getDual?_isNone c i + have hi := insertAndContractNat_none_getDual?_isNone c i simp [getDualErase, hi] | some j => - simp only [Nat.succ_eq_add_one, getDualErase, insert_some_getDual?_eq, Option.isSome_some, + simp only [Nat.succ_eq_add_one, getDualErase, insertAndContractNat_some_getDual?_eq, Option.isSome_some, ↓reduceDIte, Option.get_some, predAboveI_succAbove, uncontractedCongr_some, Option.some.injEq] rfl @[simp] lemma erase_insert (c : WickContraction n.succ) (i : Fin n.succ) : - insert (erase c i) i (getDualErase c i) = c := by + insertAndContractNat (erase c i) i (getDualErase c i) = c := by match n with | 0 => apply Subtype.eq - simp only [Nat.succ_eq_add_one, Nat.reduceAdd, insert, getDualErase, Finset.le_eq_subset] + simp only [Nat.succ_eq_add_one, Nat.reduceAdd, insertAndContractNat, getDualErase, Finset.le_eq_subset] ext a simp only [Finset.mem_map, RelEmbedding.coe_toEmbedding] apply Iff.intro @@ -536,7 +536,7 @@ lemma erase_insert (c : WickContraction n.succ) (i : Fin n.succ) : | Nat.succ n => apply Subtype.eq by_cases hi : (c.getDual? i).isSome - · rw [insert_of_isSome] + · rw [insertAndContractNat_of_isSome] simp only [Nat.succ_eq_add_one, getDualErase, hi, ↓reduceDIte, Option.get_some, Finset.le_eq_subset] rw [succsAbove_predAboveI] @@ -565,7 +565,7 @@ lemma erase_insert (c : WickContraction n.succ) (i : Fin n.succ) : rfl simp only [Nat.succ_eq_add_one, ne_eq, self_neq_getDual?_get, not_false_eq_true] exact (getDualErase_isSome_iff_getDual?_isSome c i).mpr hi - · simp only [Nat.succ_eq_add_one, insert, getDualErase, hi, Bool.false_eq_true, ↓reduceDIte, + · simp only [Nat.succ_eq_add_one, insertAndContractNat, getDualErase, hi, Bool.false_eq_true, ↓reduceDIte, Finset.le_eq_subset] ext a simp only [Finset.mem_map, RelEmbedding.coe_toEmbedding] @@ -589,8 +589,8 @@ lemma erase_insert (c : WickContraction n.succ) (i : Fin n.succ) : /-- Lifts a contraction in `c` to a contraction in `(c.insert i j)`. -/ def insertLift {c : WickContraction n} (i : Fin n.succ) (j : Option (c.uncontracted)) - (a : c.1) : (c.insert i j).1 := ⟨a.1.map (Fin.succAboveEmb i), by - simp only [Nat.succ_eq_add_one, insert, Finset.le_eq_subset] + (a : c.1) : (c.insertAndContractNat i j).1 := ⟨a.1.map (Fin.succAboveEmb i), by + simp only [Nat.succ_eq_add_one, insertAndContractNat, Finset.le_eq_subset] match j with | none => simp only [Finset.mem_map, RelEmbedding.coe_toEmbedding] @@ -614,7 +614,7 @@ lemma insertLift_none_surjective {c : WickContraction n} (i : Fin n.succ) : Function.Surjective (c.insertLift i none) := by intro a have ha := a.2 - simp only [Nat.succ_eq_add_one, insert, Finset.le_eq_subset, Finset.mem_map, + simp only [Nat.succ_eq_add_one, insertAndContractNat, Finset.le_eq_subset, Finset.mem_map, RelEmbedding.coe_toEmbedding] at ha obtain ⟨a', ha', ha''⟩ := ha use ⟨a', ha'⟩ @@ -625,10 +625,10 @@ lemma insertLift_none_bijective {c : WickContraction n} (i : Fin n.succ) : exact ⟨insertLift_injective i none, insertLift_none_surjective i⟩ @[simp] -lemma insert_fstFieldOfContract (c : WickContraction n) (i : Fin n.succ) - (j : Option (c.uncontracted)) (a : c.1) : (c.insert i j).fstFieldOfContract (insertLift i j a) = +lemma insertAndContractNat_fstFieldOfContract (c : WickContraction n) (i : Fin n.succ) + (j : Option (c.uncontracted)) (a : c.1) : (c.insertAndContractNat i j).fstFieldOfContract (insertLift i j a) = i.succAbove (c.fstFieldOfContract a) := by - refine (c.insert i j).eq_fstFieldOfContract_of_mem (a := (insertLift i j a)) + refine (c.insertAndContractNat i j).eq_fstFieldOfContract_of_mem (a := (insertLift i j a)) (i := i.succAbove (c.fstFieldOfContract a)) (j := i.succAbove (c.sndFieldOfContract a)) ?_ ?_ ?_ · simp only [Nat.succ_eq_add_one, insertLift, Finset.mem_map, Fin.succAboveEmb_apply] use (c.fstFieldOfContract a) @@ -640,10 +640,10 @@ lemma insert_fstFieldOfContract (c : WickContraction n) (i : Fin n.succ) exact fstFieldOfContract_lt_sndFieldOfContract c a @[simp] -lemma insert_sndFieldOfContract (c : WickContraction n) (i : Fin n.succ) - (j : Option (c.uncontracted)) (a : c.1) : (c.insert i j).sndFieldOfContract (insertLift i j a) = +lemma insertAndContractNat_sndFieldOfContract (c : WickContraction n) (i : Fin n.succ) + (j : Option (c.uncontracted)) (a : c.1) : (c.insertAndContractNat i j).sndFieldOfContract (insertLift i j a) = i.succAbove (c.sndFieldOfContract a) := by - refine (c.insert i j).eq_sndFieldOfContract_of_mem (a := (insertLift i j a)) + refine (c.insertAndContractNat i j).eq_sndFieldOfContract_of_mem (a := (insertLift i j a)) (i := i.succAbove (c.fstFieldOfContract a)) (j := i.succAbove (c.sndFieldOfContract a)) ?_ ?_ ?_ · simp only [Nat.succ_eq_add_one, insertLift, Finset.mem_map, Fin.succAboveEmb_apply] use (c.fstFieldOfContract a) @@ -658,10 +658,10 @@ lemma insert_sndFieldOfContract (c : WickContraction n) (i : Fin n.succ) corresponding contracted pair of a wick contraction `(c.insert i (some j))` formed by inserting an element `i` into the contraction. -/ def insertLiftSome {c : WickContraction n} (i : Fin n.succ) (j : c.uncontracted) - (a : Unit ⊕ c.1) : (c.insert i (some j)).1 := + (a : Unit ⊕ c.1) : (c.insertAndContractNat i (some j)).1 := match a with | Sum.inl () => ⟨{i, i.succAbove j}, by - simp [insert]⟩ + simp [insertAndContractNat]⟩ | Sum.inr a => c.insertLift i j a lemma insertLiftSome_injective {c : WickContraction n} (i : Fin n.succ) (j : c.uncontracted) : @@ -701,7 +701,7 @@ lemma insertLiftSome_surjective {c : WickContraction n} (i : Fin n.succ) (j : c. Function.Surjective (insertLiftSome i j) := by intro a have ha := a.2 - simp only [Nat.succ_eq_add_one, insert, Finset.le_eq_subset, Finset.mem_insert, Finset.mem_map, + simp only [Nat.succ_eq_add_one, insertAndContractNat, Finset.le_eq_subset, Finset.mem_insert, Finset.mem_map, RelEmbedding.coe_toEmbedding] at ha rcases ha with ha | ha · use Sum.inl () diff --git a/HepLean/PerturbationTheory/WickContraction/Involutions.lean b/HepLean/PerturbationTheory/WickContraction/Involutions.lean index e5961ee..a08d06b 100644 --- a/HepLean/PerturbationTheory/WickContraction/Involutions.lean +++ b/HepLean/PerturbationTheory/WickContraction/Involutions.lean @@ -6,7 +6,7 @@ Authors: Joseph Tooby-Smith import HepLean.PerturbationTheory.WickContraction.Uncontracted import HepLean.PerturbationTheory.Algebras.StateAlgebra.TimeOrder import HepLean.PerturbationTheory.Algebras.ProtoOperatorAlgebra.TimeContraction -import HepLean.PerturbationTheory.WickContraction.InsertList +import HepLean.PerturbationTheory.WickContraction.InsertAndContract /-! # Involution associated with a contraction diff --git a/HepLean/PerturbationTheory/WickContraction/Sign.lean b/HepLean/PerturbationTheory/WickContraction/Sign.lean index 0bcd9bd..211a5b2 100644 --- a/HepLean/PerturbationTheory/WickContraction/Sign.lean +++ b/HepLean/PerturbationTheory/WickContraction/Sign.lean @@ -3,7 +3,7 @@ Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Joseph Tooby-Smith -/ -import HepLean.PerturbationTheory.WickContraction.InsertList +import HepLean.PerturbationTheory.WickContraction.InsertAndContract /-! @@ -27,26 +27,26 @@ def signFinset (c : WickContraction n) (i1 i2 : Fin n) : Finset (Fin n) := Finset.univ.filter (fun i => i1 < i ∧ i < i2 ∧ (c.getDual? i = none ∨ ∀ (h : (c.getDual? i).isSome), i1 < (c.getDual? i).get h)) -lemma signFinset_insertList_none (φ : 𝓕.States) (φs : List 𝓕.States) +lemma signFinset_insertAndContract_none (φ : 𝓕.States) (φs : List 𝓕.States) (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (i1 i2 : Fin φs.length) : - (φsΛ.insertList φ i none).signFinset (finCongr (insertIdx_length_fin φ φs i).symm + (φsΛ.insertAndContract φ i none).signFinset (finCongr (insertIdx_length_fin φ φs i).symm (i.succAbove i1)) (finCongr (insertIdx_length_fin φ φs i).symm (i.succAbove i2)) = if i.succAbove i1 < i ∧ i < i.succAbove i2 then Insert.insert (finCongr (insertIdx_length_fin φ φs i).symm i) - (insertListLiftFinset φ i (φsΛ.signFinset i1 i2)) + (insertAndContractLiftFinset φ i (φsΛ.signFinset i1 i2)) else - (insertListLiftFinset φ i (φsΛ.signFinset i1 i2)) := by + (insertAndContractLiftFinset φ i (φsΛ.signFinset i1 i2)) := by ext k rcases insert_fin_eq_self φ i k with hk | hk · subst hk conv_lhs => simp only [Nat.succ_eq_add_one, signFinset, finCongr_apply, Finset.mem_filter, Finset.mem_univ, - insertList_none_getDual?_self, Option.isSome_none, Bool.false_eq_true, IsEmpty.forall_iff, + insertAndContract_none_getDual?_self, Option.isSome_none, Bool.false_eq_true, IsEmpty.forall_iff, or_self, and_true, true_and] by_cases h : i.succAbove i1 < i ∧ i < i.succAbove i2 · simp [h, Fin.lt_def] - · simp only [Nat.succ_eq_add_one, h, ↓reduceIte, self_not_mem_insertListLiftFinset, iff_false] + · simp only [Nat.succ_eq_add_one, h, ↓reduceIte, self_not_mem_insertAndContractLiftFinset, iff_false] rw [Fin.lt_def, Fin.lt_def] at h ⊢ simp_all · obtain ⟨k, hk⟩ := hk @@ -54,10 +54,10 @@ lemma signFinset_insertList_none (φ : 𝓕.States) (φs : List 𝓕.States) have h1 : Fin.cast (insertIdx_length_fin φ φs i).symm (i.succAbove k) ∈ (if i.succAbove i1 < i ∧ i < i.succAbove i2 then Insert.insert ((finCongr (insertIdx_length_fin φ φs i).symm) i) - (insertListLiftFinset φ i (φsΛ.signFinset i1 i2)) - else insertListLiftFinset φ i (φsΛ.signFinset i1 i2)) ↔ + (insertAndContractLiftFinset φ i (φsΛ.signFinset i1 i2)) + else insertAndContractLiftFinset φ i (φsΛ.signFinset i1 i2)) ↔ Fin.cast (insertIdx_length_fin φ φs i).symm (i.succAbove k) ∈ - insertListLiftFinset φ i (φsΛ.signFinset i1 i2) := by + insertAndContractLiftFinset φ i (φsΛ.signFinset i1 i2) := by split · simp only [Nat.succ_eq_add_one, finCongr_apply, Finset.mem_insert, Fin.ext_iff, Fin.coe_cast, or_iff_right_iff_imp] @@ -67,10 +67,10 @@ lemma signFinset_insertList_none (φ : 𝓕.States) (φs : List 𝓕.States) omega · simp rw [h1] - rw [succAbove_mem_insertListLiftFinset] + rw [succAbove_mem_insertAndContractLiftFinset] simp only [Nat.succ_eq_add_one, signFinset, finCongr_apply, Finset.mem_filter, Finset.mem_univ, - insertList_none_succAbove_getDual?_eq_none_iff, insertList_none_succAbove_getDual?_isSome_iff, - insertList_none_getDual?_get_eq, true_and] + insertAndContract_none_succAbove_getDual?_eq_none_iff, insertAndContract_none_succAbove_getDual?_isSome_iff, + insertAndContract_none_getDual?_get_eq, true_and] rw [Fin.lt_def, Fin.lt_def, Fin.lt_def, Fin.lt_def] simp only [Fin.coe_cast, Fin.val_fin_lt] rw [Fin.succAbove_lt_succAbove_iff, Fin.succAbove_lt_succAbove_iff] @@ -83,9 +83,9 @@ lemma signFinset_insertList_none (φ : 𝓕.States) (φs : List 𝓕.States) simp only [Fin.coe_cast, Fin.val_fin_lt] rw [Fin.succAbove_lt_succAbove_iff] -lemma stat_ofFinset_of_insertListLiftFinset (φ : 𝓕.States) (φs : List 𝓕.States) +lemma stat_ofFinset_of_insertAndContractLiftFinset (φ : 𝓕.States) (φs : List 𝓕.States) (i : Fin φs.length.succ) (a : Finset (Fin φs.length)) : - (𝓕 |>ₛ ⟨(φs.insertIdx i φ).get, insertListLiftFinset φ i a⟩) = 𝓕 |>ₛ ⟨φs.get, a⟩ := by + (𝓕 |>ₛ ⟨(φs.insertIdx i φ).get, insertAndContractLiftFinset φ i a⟩) = 𝓕 |>ₛ ⟨φs.get, a⟩ := by simp only [ofFinset, Nat.succ_eq_add_one] congr 1 rw [get_eq_insertIdx_succAbove φ _ i] @@ -109,13 +109,13 @@ lemma stat_ofFinset_of_insertListLiftFinset (φ : 𝓕.States) (φs : List 𝓕. exact Finset.sort_nodup (fun x1 x2 => x1 ≤ x2) a have h3 : (List.map (⇑(finCongr (insertIdx_length_fin φ φs i).symm)) (List.map i.succAbove (Finset.sort (fun x1 x2 => x1 ≤ x2) a))).toFinset - = (insertListLiftFinset φ i a) := by + = (insertAndContractLiftFinset φ i a) := by ext b simp only [Nat.succ_eq_add_one, List.map_map, List.mem_toFinset, List.mem_map, Finset.mem_sort, Function.comp_apply, finCongr_apply] rcases insert_fin_eq_self φ i b with hk | hk · subst hk - simp only [Nat.succ_eq_add_one, self_not_mem_insertListLiftFinset, iff_false, not_exists, + simp only [Nat.succ_eq_add_one, self_not_mem_insertAndContractLiftFinset, iff_false, not_exists, not_and] intro x hx refine Fin.ne_of_val_ne ?h.inl.h @@ -125,7 +125,7 @@ lemma stat_ofFinset_of_insertListLiftFinset (φ : 𝓕.States) (φs : List 𝓕. · obtain ⟨k, hk⟩ := hk subst hk simp only [Nat.succ_eq_add_one] - rw [succAbove_mem_insertListLiftFinset] + rw [succAbove_mem_insertAndContractLiftFinset] apply Iff.intro · intro h obtain ⟨x, hx⟩ := h @@ -177,46 +177,46 @@ lemma stat_ofFinset_eq_one_of_gradingCompliant (φs : List 𝓕.States) exact False.elim (h1 hsom') rfl -lemma signFinset_insertList_some (φ : 𝓕.States) (φs : List 𝓕.States) +lemma signFinset_insertAndContract_some (φ : 𝓕.States) (φs : List 𝓕.States) (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (i1 i2 : Fin φs.length) (j : φsΛ.uncontracted) : - (φsΛ.insertList φ i (some j)).signFinset (finCongr (insertIdx_length_fin φ φs i).symm + (φsΛ.insertAndContract φ i (some j)).signFinset (finCongr (insertIdx_length_fin φ φs i).symm (i.succAbove i1)) (finCongr (insertIdx_length_fin φ φs i).symm (i.succAbove i2)) = if i.succAbove i1 < i ∧ i < i.succAbove i2 ∧ (i1 < j) then Insert.insert (finCongr (insertIdx_length_fin φ φs i).symm i) - (insertListLiftFinset φ i (φsΛ.signFinset i1 i2)) + (insertAndContractLiftFinset φ i (φsΛ.signFinset i1 i2)) else if i1 < j ∧ j < i2 ∧ ¬ i.succAbove i1 < i then - (insertListLiftFinset φ i (φsΛ.signFinset i1 i2)).erase + (insertAndContractLiftFinset φ i (φsΛ.signFinset i1 i2)).erase (finCongr (insertIdx_length_fin φ φs i).symm (i.succAbove j)) else - (insertListLiftFinset φ i (φsΛ.signFinset i1 i2)) := by + (insertAndContractLiftFinset φ i (φsΛ.signFinset i1 i2)) := by ext k rcases insert_fin_eq_self φ i k with hk | hk · subst hk have h1 : Fin.cast (insertIdx_length_fin φ φs i).symm i ∈ (if i.succAbove i1 < i ∧ i < i.succAbove i2 ∧ (i1 < j) then Insert.insert (finCongr (insertIdx_length_fin φ φs i).symm i) - (insertListLiftFinset φ i (φsΛ.signFinset i1 i2)) + (insertAndContractLiftFinset φ i (φsΛ.signFinset i1 i2)) else if i1 < j ∧ j < i2 ∧ ¬ i.succAbove i1 < i then - (insertListLiftFinset φ i (φsΛ.signFinset i1 i2)).erase + (insertAndContractLiftFinset φ i (φsΛ.signFinset i1 i2)).erase (finCongr (insertIdx_length_fin φ φs i).symm (i.succAbove j)) else - (insertListLiftFinset φ i (φsΛ.signFinset i1 i2))) ↔ + (insertAndContractLiftFinset φ i (φsΛ.signFinset i1 i2))) ↔ i.succAbove i1 < i ∧ i < i.succAbove i2 ∧ (i1 < j) := by split simp_all only [Nat.succ_eq_add_one, finCongr_apply, Finset.mem_insert, - self_not_mem_insertListLiftFinset, or_false, and_self] + self_not_mem_insertAndContractLiftFinset, or_false, and_self] rename_i h simp only [Nat.succ_eq_add_one, not_lt, finCongr_apply, h, iff_false] split - simp only [Finset.mem_erase, ne_eq, self_not_mem_insertListLiftFinset, and_false, + simp only [Finset.mem_erase, ne_eq, self_not_mem_insertAndContractLiftFinset, and_false, not_false_eq_true] simp rw [h1] simp only [Nat.succ_eq_add_one, signFinset, finCongr_apply, Finset.mem_filter, Finset.mem_univ, - insertList_some_getDual?_self_eq, reduceCtorEq, Option.isSome_some, Option.get_some, + insertAndContract_some_getDual?_self_eq, reduceCtorEq, Option.isSome_some, Option.get_some, forall_const, false_or, true_and] rw [Fin.lt_def, Fin.lt_def, Fin.lt_def, Fin.lt_def] simp only [Fin.coe_cast, Fin.val_fin_lt, and_congr_right_iff] @@ -227,7 +227,7 @@ lemma signFinset_insertList_some (φ : 𝓕.States) (φs : List 𝓕.States) by_cases hkj : k = j.1 · subst hkj conv_lhs=> simp only [Nat.succ_eq_add_one, signFinset, finCongr_apply, Finset.mem_filter, - Finset.mem_univ, insertList_some_getDual?_some_eq, reduceCtorEq, Option.isSome_some, + Finset.mem_univ, insertAndContract_some_getDual?_some_eq, reduceCtorEq, Option.isSome_some, Option.get_some, forall_const, false_or, true_and, not_lt] rw [Fin.lt_def, Fin.lt_def] simp only [Fin.coe_cast, Fin.val_fin_lt, Nat.succ_eq_add_one, finCongr_apply, not_lt] @@ -238,7 +238,7 @@ lemma signFinset_insertList_some (φ : 𝓕.States) (φs : List 𝓕.States) split · rename_i h simp_all only [and_true, Finset.mem_insert] - rw [succAbove_mem_insertListLiftFinset] + rw [succAbove_mem_insertAndContractLiftFinset] simp only [Fin.ext_iff, Fin.coe_cast] have h1 : ¬ (i.succAbove ↑j) = i := Fin.succAbove_ne i ↑j simp only [Fin.val_eq_val, h1, signFinset, Finset.mem_filter, Finset.mem_univ, true_and, @@ -259,7 +259,7 @@ lemma signFinset_insertList_some (φ : 𝓕.States) (φs : List 𝓕.States) intro h1 h2 omega · rename_i h1 - rw [succAbove_mem_insertListLiftFinset] + rw [succAbove_mem_insertAndContractLiftFinset] simp only [signFinset, Finset.mem_filter, Finset.mem_univ, true_and, and_congr_right_iff] intro h1 h2 have hj:= j.2 @@ -270,15 +270,15 @@ lemma signFinset_insertList_some (φ : 𝓕.States) (φs : List 𝓕.States) · have h1 : Fin.cast (insertIdx_length_fin φ φs i).symm (i.succAbove k) ∈ (if i.succAbove i1 < i ∧ i < i.succAbove i2 ∧ (i1 < j) then Insert.insert (finCongr (insertIdx_length_fin φ φs i).symm i) - (insertListLiftFinset φ i (φsΛ.signFinset i1 i2)) + (insertAndContractLiftFinset φ i (φsΛ.signFinset i1 i2)) else if i1 < j ∧ j < i2 ∧ ¬ i.succAbove i1 < i then - (insertListLiftFinset φ i (φsΛ.signFinset i1 i2)).erase + (insertAndContractLiftFinset φ i (φsΛ.signFinset i1 i2)).erase (finCongr (insertIdx_length_fin φ φs i).symm (i.succAbove j)) else - (insertListLiftFinset φ i (φsΛ.signFinset i1 i2))) ↔ + (insertAndContractLiftFinset φ i (φsΛ.signFinset i1 i2))) ↔ Fin.cast (insertIdx_length_fin φ φs i).symm (i.succAbove k) ∈ - (insertListLiftFinset φ i (φsΛ.signFinset i1 i2)) := by + (insertAndContractLiftFinset φ i (φsΛ.signFinset i1 i2)) := by split · simp only [Nat.succ_eq_add_one, finCongr_apply, Finset.mem_insert, or_iff_right_iff_imp] intro h @@ -297,7 +297,7 @@ lemma signFinset_insertList_some (φ : 𝓕.States) (φs : List 𝓕.States) exact Fin.succAbove_right_injective · simp rw [h1] - rw [succAbove_mem_insertListLiftFinset] + rw [succAbove_mem_insertAndContractLiftFinset] simp only [Nat.succ_eq_add_one, signFinset, finCongr_apply, Finset.mem_filter, Finset.mem_univ, true_and] rw [Fin.lt_def, Fin.lt_def, Fin.lt_def, Fin.lt_def] @@ -305,7 +305,7 @@ lemma signFinset_insertList_some (φ : 𝓕.States) (φs : List 𝓕.States) rw [Fin.succAbove_lt_succAbove_iff, Fin.succAbove_lt_succAbove_iff] simp only [and_congr_right_iff] intro h1 h2 - simp only [ne_eq, hkj, not_false_eq_true, insertList_some_succAbove_getDual?_eq_option, + simp only [ne_eq, hkj, not_false_eq_true, insertAndContract_some_succAbove_getDual?_eq_option, Nat.succ_eq_add_one, Option.map_eq_none', Option.isSome_map'] conv_lhs => rhs @@ -341,24 +341,24 @@ def signInsertNone (φ : 𝓕.States) (φs : List 𝓕.States) (φsΛ : WickCont lemma sign_insert_none (φ : 𝓕.States) (φs : List 𝓕.States) (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) : - (φsΛ.insertList φ i none).sign = (φsΛ.signInsertNone φ φs i) * φsΛ.sign := by + (φsΛ.insertAndContract φ i none).sign = (φsΛ.signInsertNone φ φs i) * φsΛ.sign := by rw [sign] rw [signInsertNone, sign, ← Finset.prod_mul_distrib] - rw [insertList_none_prod_contractions] + rw [insertAndContract_none_prod_contractions] congr funext a - simp only [instCommGroup.eq_1, Nat.succ_eq_add_one, insertList_sndFieldOfContract, finCongr_apply, - Fin.getElem_fin, Fin.coe_cast, insertIdx_getElem_fin, insertList_fstFieldOfContract, ite_mul, + simp only [instCommGroup.eq_1, Nat.succ_eq_add_one, insertAndContract_sndFieldOfContract, finCongr_apply, + Fin.getElem_fin, Fin.coe_cast, insertIdx_getElem_fin, insertAndContract_fstFieldOfContract, ite_mul, one_mul] - erw [signFinset_insertList_none] + erw [signFinset_insertAndContract_none] split · rw [ofFinset_insert] simp only [instCommGroup, Nat.succ_eq_add_one, finCongr_apply, Fin.getElem_fin, Fin.coe_cast, List.getElem_insertIdx_self, map_mul] - rw [stat_ofFinset_of_insertListLiftFinset] + rw [stat_ofFinset_of_insertAndContractLiftFinset] simp only [exchangeSign_symm, instCommGroup.eq_1] simp - · rw [stat_ofFinset_of_insertListLiftFinset] + · rw [stat_ofFinset_of_insertAndContractLiftFinset] lemma signInsertNone_eq_mul_fst_snd (φ : 𝓕.States) (φs : List 𝓕.States) (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) : @@ -508,13 +508,13 @@ def signInsertSomeProd (φ : 𝓕.States) (φs : List 𝓕.States) (φsΛ : Wick coming from putting `i` next to `j`. -/ def signInsertSomeCoef (φ : 𝓕.States) (φs : List 𝓕.States) (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (j : φsΛ.uncontracted) : ℂ := - let a : (φsΛ.insertList φ i (some j)).1 := + let a : (φsΛ.insertAndContract φ i (some j)).1 := congrLift (insertIdx_length_fin φ φs i).symm - ⟨{i, i.succAbove j}, by simp [insert]⟩; - 𝓢(𝓕 |>ₛ (φs.insertIdx i φ)[(φsΛ.insertList φ i (some j)).sndFieldOfContract a], + ⟨{i, i.succAbove j}, by simp [insertAndContractNat]⟩; + 𝓢(𝓕 |>ₛ (φs.insertIdx i φ)[(φsΛ.insertAndContract φ i (some j)).sndFieldOfContract a], 𝓕 |>ₛ ⟨(φs.insertIdx i φ).get, signFinset - (φsΛ.insertList φ i (some j)) ((φsΛ.insertList φ i (some j)).fstFieldOfContract a) - ((φsΛ.insertList φ i (some j)).sndFieldOfContract a)⟩) + (φsΛ.insertAndContract φ i (some j)) ((φsΛ.insertAndContract φ i (some j)).fstFieldOfContract a) + ((φsΛ.insertAndContract φ i (some j)).sndFieldOfContract a)⟩) /-- Given a Wick contraction `c` associated with a list of states `φs` and an `i : Fin φs.length.succ`, the change in sign of the contraction associated with @@ -525,22 +525,22 @@ def signInsertSome (φ : 𝓕.States) (φs : List 𝓕.States) (φsΛ : WickCont lemma sign_insert_some (φ : 𝓕.States) (φs : List 𝓕.States) (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (j : φsΛ.uncontracted) : - (φsΛ.insertList φ i (some j)).sign = (φsΛ.signInsertSome φ φs i j) * φsΛ.sign := by + (φsΛ.insertAndContract φ i (some j)).sign = (φsΛ.signInsertSome φ φs i j) * φsΛ.sign := by rw [sign] rw [signInsertSome, signInsertSomeProd, sign, mul_assoc, ← Finset.prod_mul_distrib] - rw [insertList_some_prod_contractions] + rw [insertAndContract_some_prod_contractions] congr funext a - simp only [instCommGroup.eq_1, Nat.succ_eq_add_one, insertList_sndFieldOfContract, finCongr_apply, - Fin.getElem_fin, Fin.coe_cast, insertIdx_getElem_fin, insertList_fstFieldOfContract, not_lt, + simp only [instCommGroup.eq_1, Nat.succ_eq_add_one, insertAndContract_sndFieldOfContract, finCongr_apply, + Fin.getElem_fin, Fin.coe_cast, insertIdx_getElem_fin, insertAndContract_fstFieldOfContract, not_lt, ite_mul, one_mul] - erw [signFinset_insertList_some] + erw [signFinset_insertAndContract_some] split · rename_i h simp only [Nat.succ_eq_add_one, finCongr_apply] rw [ofFinset_insert] simp only [instCommGroup, Fin.getElem_fin, Fin.coe_cast, List.getElem_insertIdx_self, map_mul] - rw [stat_ofFinset_of_insertListLiftFinset] + rw [stat_ofFinset_of_insertAndContractLiftFinset] simp only [exchangeSign_symm, instCommGroup.eq_1] simp · rename_i h @@ -550,9 +550,9 @@ lemma sign_insert_some (φ : 𝓕.States) (φs : List 𝓕.States) (φsΛ : Wick rw [if_pos] rw [ofFinset_erase] simp only [instCommGroup, Fin.getElem_fin, Fin.coe_cast, insertIdx_getElem_fin, map_mul] - rw [stat_ofFinset_of_insertListLiftFinset] + rw [stat_ofFinset_of_insertAndContractLiftFinset] simp only [exchangeSign_symm, instCommGroup.eq_1] - · rw [succAbove_mem_insertListLiftFinset] + · rw [succAbove_mem_insertAndContractLiftFinset] simp only [signFinset, Finset.mem_filter, Finset.mem_univ, true_and] simp_all only [Nat.succ_eq_add_one, and_true, false_and, not_false_eq_true, not_lt, true_and] @@ -561,7 +561,7 @@ lemma sign_insert_some (φ : 𝓕.States) (φs : List 𝓕.States) (φsΛ : Wick · simp_all · rename_i h1 rw [if_neg] - rw [stat_ofFinset_of_insertListLiftFinset] + rw [stat_ofFinset_of_insertAndContractLiftFinset] simp_all lemma signInsertSomeProd_eq_one_if (φ : 𝓕.States) (φs : List 𝓕.States) @@ -731,16 +731,16 @@ lemma signInsertSomeCoef_if (φ : 𝓕.States) (φs : List 𝓕.States) (φsΛ : φsΛ.signInsertSomeCoef φ φs i j = if i < i.succAbove j then 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ ⟨(φs.insertIdx i φ).get, - (signFinset (φsΛ.insertList φ i (some j)) (finCongr (insertIdx_length_fin φ φs i).symm i) + (signFinset (φsΛ.insertAndContract φ i (some j)) (finCongr (insertIdx_length_fin φ φs i).symm i) (finCongr (insertIdx_length_fin φ φs i).symm (i.succAbove j)))⟩) else 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ ⟨(φs.insertIdx i φ).get, - signFinset (φsΛ.insertList φ i (some j)) + signFinset (φsΛ.insertAndContract φ i (some j)) (finCongr (insertIdx_length_fin φ φs i).symm (i.succAbove j)) (finCongr (insertIdx_length_fin φ φs i).symm i)⟩) := by simp only [signInsertSomeCoef, instCommGroup.eq_1, Nat.succ_eq_add_one, - insertList_sndFieldOfContract_some_incl, finCongr_apply, Fin.getElem_fin, - insertList_fstFieldOfContract_some_incl] + insertAndContract_sndFieldOfContract_some_incl, finCongr_apply, Fin.getElem_fin, + insertAndContract_fstFieldOfContract_some_incl] split · simp [hφj] · simp [hφj] @@ -749,7 +749,7 @@ lemma stat_signFinset_insert_some_self_fst (φ : 𝓕.States) (φs : List 𝓕.States) (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (j : φsΛ.uncontracted) : (𝓕 |>ₛ ⟨(φs.insertIdx i φ).get, - (signFinset (φsΛ.insertList φ i (some j)) (finCongr (insertIdx_length_fin φ φs i).symm i) + (signFinset (φsΛ.insertAndContract φ i (some j)) (finCongr (insertIdx_length_fin φ φs i).symm i) (finCongr (insertIdx_length_fin φ φs i).symm (i.succAbove j)))⟩) = 𝓕 |>ₛ ⟨φs.get, (Finset.univ.filter (fun x => i < i.succAbove x ∧ x < j ∧ ((φsΛ.getDual? x = none) ∨ @@ -766,7 +766,7 @@ lemma stat_signFinset_insert_some_self_fst true_and, Finset.mem_map, Function.Embedding.coeFn_mk, Function.comp_apply] rcases insert_fin_eq_self φ i x with hx | hx · subst hx - simp only [Nat.succ_eq_add_one, lt_self_iff_false, insertList_some_getDual?_self_eq, + simp only [Nat.succ_eq_add_one, lt_self_iff_false, insertAndContract_some_getDual?_self_eq, reduceCtorEq, Option.isSome_some, Option.get_some, forall_const, false_or, and_self, false_and, false_iff, not_exists, not_and, and_imp] intro x hi hx @@ -778,7 +778,7 @@ lemma stat_signFinset_insert_some_self_fst subst hx by_cases h : x = j.1 · subst h - simp only [Nat.succ_eq_add_one, lt_self_iff_false, insertList_some_getDual?_some_eq, + simp only [Nat.succ_eq_add_one, lt_self_iff_false, insertAndContract_some_getDual?_some_eq, reduceCtorEq, Option.isSome_some, Option.get_some, imp_false, not_true_eq_false, or_self, and_self, and_false, false_iff, not_exists, not_and, and_imp] intro x hi hx h0 @@ -788,7 +788,7 @@ lemma stat_signFinset_insert_some_self_fst omega exact Fin.succAbove_right_injective · simp only [Nat.succ_eq_add_one, ne_eq, h, not_false_eq_true, - insertList_some_succAbove_getDual?_eq_option, Option.map_eq_none', Option.isSome_map'] + insertAndContract_some_succAbove_getDual?_eq_option, Option.map_eq_none', Option.isSome_map'] rw [Fin.lt_def, Fin.lt_def] simp only [Fin.coe_cast, Fin.val_fin_lt] apply Iff.intro @@ -825,7 +825,7 @@ lemma stat_signFinset_insert_some_self_fst lemma stat_signFinset_insert_some_self_snd (φ : 𝓕.States) (φs : List 𝓕.States) (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (j : φsΛ.uncontracted) : (𝓕 |>ₛ ⟨(φs.insertIdx i φ).get, - (signFinset (φsΛ.insertList φ i (some j)) + (signFinset (φsΛ.insertAndContract φ i (some j)) (finCongr (insertIdx_length_fin φ φs i).symm (i.succAbove j)) (finCongr (insertIdx_length_fin φ φs i).symm i))⟩) = 𝓕 |>ₛ ⟨φs.get, @@ -842,7 +842,7 @@ lemma stat_signFinset_insert_some_self_snd (φ : 𝓕.States) (φs : List 𝓕.S true_and, Finset.mem_map, Function.Embedding.coeFn_mk, Function.comp_apply] rcases insert_fin_eq_self φ i x with hx | hx · subst hx - simp only [Nat.succ_eq_add_one, lt_self_iff_false, insertList_some_getDual?_self_eq, + simp only [Nat.succ_eq_add_one, lt_self_iff_false, insertAndContract_some_getDual?_self_eq, reduceCtorEq, Option.isSome_some, Option.get_some, imp_false, not_true_eq_false, or_self, and_self, and_false, false_iff, not_exists, not_and, and_imp] intro x hi hx @@ -854,7 +854,7 @@ lemma stat_signFinset_insert_some_self_snd (φ : 𝓕.States) (φs : List 𝓕.S subst hx by_cases h : x = j.1 · subst h - simp only [Nat.succ_eq_add_one, lt_self_iff_false, insertList_some_getDual?_some_eq, + simp only [Nat.succ_eq_add_one, lt_self_iff_false, insertAndContract_some_getDual?_some_eq, reduceCtorEq, Option.isSome_some, Option.get_some, forall_const, false_or, and_self, false_and, false_iff, not_exists, not_and, and_imp] intro x hi hx h0 @@ -864,7 +864,7 @@ lemma stat_signFinset_insert_some_self_snd (φ : 𝓕.States) (φs : List 𝓕.S omega exact Fin.succAbove_right_injective · simp only [Nat.succ_eq_add_one, ne_eq, h, not_false_eq_true, - insertList_some_succAbove_getDual?_eq_option, Option.map_eq_none', Option.isSome_map'] + insertAndContract_some_succAbove_getDual?_eq_option, Option.map_eq_none', Option.isSome_map'] rw [Fin.lt_def, Fin.lt_def] simp only [Fin.coe_cast, Fin.val_fin_lt] apply Iff.intro diff --git a/HepLean/PerturbationTheory/WickContraction/TimeContract.lean b/HepLean/PerturbationTheory/WickContraction/TimeContract.lean index 924e965..1d75e55 100644 --- a/HepLean/PerturbationTheory/WickContraction/TimeContract.lean +++ b/HepLean/PerturbationTheory/WickContraction/TimeContract.lean @@ -29,24 +29,24 @@ noncomputable def timeContract (𝓞 : 𝓕.ProtoOperatorAlgebra) {φs : List 𝓞.timeContract_mem_center _ _⟩ @[simp] -lemma timeContract_insertList_none (𝓞 : 𝓕.ProtoOperatorAlgebra) (φ : 𝓕.States) (φs : List 𝓕.States) +lemma timeContract_insertAndContract_none (𝓞 : 𝓕.ProtoOperatorAlgebra) (φ : 𝓕.States) (φs : List 𝓕.States) (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) : - (φsΛ.insertList φ i none).timeContract 𝓞 = φsΛ.timeContract 𝓞 := by - rw [timeContract, insertList_none_prod_contractions] + (φsΛ.insertAndContract φ i none).timeContract 𝓞 = φsΛ.timeContract 𝓞 := by + rw [timeContract, insertAndContract_none_prod_contractions] congr ext a simp -lemma timeConract_insertList_some (𝓞 : 𝓕.ProtoOperatorAlgebra) (φ : 𝓕.States) (φs : List 𝓕.States) +lemma timeConract_insertAndContract_some (𝓞 : 𝓕.ProtoOperatorAlgebra) (φ : 𝓕.States) (φs : List 𝓕.States) (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (j : φsΛ.uncontracted) : - (φsΛ.insertList φ i (some j)).timeContract 𝓞 = + (φsΛ.insertAndContract φ i (some j)).timeContract 𝓞 = (if i < i.succAbove j then ⟨𝓞.timeContract φ φs[j.1], 𝓞.timeContract_mem_center _ _⟩ else ⟨𝓞.timeContract φs[j.1] φ, 𝓞.timeContract_mem_center _ _⟩) * φsΛ.timeContract 𝓞 := by - rw [timeContract, insertList_some_prod_contractions] + rw [timeContract, insertAndContract_some_prod_contractions] congr 1 - · simp only [Nat.succ_eq_add_one, insertList_fstFieldOfContract_some_incl, finCongr_apply, - List.get_eq_getElem, insertList_sndFieldOfContract_some_incl, Fin.getElem_fin] + · simp only [Nat.succ_eq_add_one, insertAndContract_fstFieldOfContract_some_incl, finCongr_apply, + List.get_eq_getElem, insertAndContract_sndFieldOfContract_some_incl, Fin.getElem_fin] split · simp · simp @@ -56,15 +56,15 @@ lemma timeConract_insertList_some (𝓞 : 𝓕.ProtoOperatorAlgebra) (φ : 𝓕. open FieldStatistic -lemma timeConract_insertList_some_eq_mul_contractStateAtIndex_lt +lemma timeConract_insertAndContract_some_eq_mul_contractStateAtIndex_lt (𝓞 : 𝓕.ProtoOperatorAlgebra) (φ : 𝓕.States) (φs : List 𝓕.States) (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (k : φsΛ.uncontracted) (ht : 𝓕.timeOrderRel φ φs[k.1]) (hik : i < i.succAbove k) : - (φsΛ.insertList φ i (some k)).timeContract 𝓞 = + (φsΛ.insertAndContract φ i (some k)).timeContract 𝓞 = 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ ⟨φs.get, (φsΛ.uncontracted.filter (fun x => x < k))⟩) • (𝓞.contractStateAtIndex φ [φsΛ]ᵘᶜ ((uncontractedStatesEquiv φs φsΛ) (some k)) * φsΛ.timeContract 𝓞) := by - rw [timeConract_insertList_some] + rw [timeConract_insertAndContract_some] simp only [Nat.succ_eq_add_one, Fin.getElem_fin, ite_mul, instCommGroup.eq_1, ProtoOperatorAlgebra.contractStateAtIndex, uncontractedStatesEquiv, Equiv.optionCongr_apply, Equiv.coe_trans, Option.map_some', Function.comp_apply, finCongr_apply, Fin.coe_cast, @@ -91,15 +91,15 @@ lemma timeConract_insertList_some_eq_mul_contractStateAtIndex_lt simp only [exchangeSign_mul_self] · exact ht -lemma timeConract_insertList_some_eq_mul_contractStateAtIndex_not_lt +lemma timeConract_insertAndContract_some_eq_mul_contractStateAtIndex_not_lt (𝓞 : 𝓕.ProtoOperatorAlgebra) (φ : 𝓕.States) (φs : List 𝓕.States) (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (k : φsΛ.uncontracted) (ht : ¬ 𝓕.timeOrderRel φs[k.1] φ) (hik : ¬ i < i.succAbove k) : - (φsΛ.insertList φ i (some k)).timeContract 𝓞 = + (φsΛ.insertAndContract φ i (some k)).timeContract 𝓞 = 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ ⟨φs.get, (φsΛ.uncontracted.filter (fun x => x ≤ k))⟩) • (𝓞.contractStateAtIndex φ [φsΛ]ᵘᶜ ((uncontractedStatesEquiv φs φsΛ) (some k)) * φsΛ.timeContract 𝓞) := by - rw [timeConract_insertList_some] + rw [timeConract_insertAndContract_some] simp only [Nat.succ_eq_add_one, Fin.getElem_fin, ite_mul, instCommGroup.eq_1, ProtoOperatorAlgebra.contractStateAtIndex, uncontractedStatesEquiv, Equiv.optionCongr_apply, Equiv.coe_trans, Option.map_some', Function.comp_apply, finCongr_apply, Fin.coe_cast, diff --git a/HepLean/PerturbationTheory/WickContraction/UncontractedList.lean b/HepLean/PerturbationTheory/WickContraction/UncontractedList.lean index 37f8c90..89ac4be 100644 --- a/HepLean/PerturbationTheory/WickContraction/UncontractedList.lean +++ b/HepLean/PerturbationTheory/WickContraction/UncontractedList.lean @@ -441,7 +441,7 @@ lemma uncontractedList_extractEquiv_symm_some (c : WickContraction n) (i : Fin n congr simp only [Nat.succ_eq_add_one, extractEquiv, Equiv.coe_fn_symm_mk, uncontractedList_getElem_uncontractedIndexEquiv_symm, Fin.succAboveEmb_apply] - rw [insert_some_uncontracted] + rw [insertAndContractNat_some_uncontracted] ext a simp diff --git a/HepLean/PerturbationTheory/WicksTheorem.lean b/HepLean/PerturbationTheory/WicksTheorem.lean index d9e099e..1f4c45b 100644 --- a/HepLean/PerturbationTheory/WicksTheorem.lean +++ b/HepLean/PerturbationTheory/WicksTheorem.lean @@ -26,19 +26,19 @@ open WickContraction open FieldStatistic /-- -Let `c` be a Wick Contraction for `φ₀φ₁…φₙ`. -We have (roughly) `N(c.insertList φ i none).uncontractedList = s • N(φ * c.uncontractedList)` -Where `s` is the exchange sign for `φ` and the uncontracted fields in `φ₀φ₁…φᵢ`. +Let `c` be a Wick Contraction for `φs := φ₀φ₁…φₙ`. +We have (roughly) `𝓝([φsΛ.insertAndContract φ i none]ᵘᶜ) = s • 𝓝(φ :: [φsΛ]ᵘᶜ)` +Where `s` is the exchange sign for `φ` and the uncontracted fields in `φ₀φ₁…φᵢ₋₁`. -/ -lemma insertList_none_normalOrder (φ : 𝓕.States) (φs : List 𝓕.States) +lemma insertAndContract_none_normalOrder (φ : 𝓕.States) (φs : List 𝓕.States) (i : Fin φs.length.succ) (φsΛ : WickContraction φs.length) : - 𝓞.crAnF (𝓝(ofStateList [φsΛ.insertList φ i none]ᵘᶜ)) + 𝓞.crAnF (𝓝([φsΛ.insertAndContract φ i none]ᵘᶜ)) = 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ ⟨φs.get, φsΛ.uncontracted.filter (fun x => i.succAbove x < i)⟩) • - 𝓞.crAnF 𝓝(ofStateList (φ :: [φsΛ]ᵘᶜ)) := by + 𝓞.crAnF 𝓝(φ :: [φsΛ]ᵘᶜ) := by simp only [Nat.succ_eq_add_one, instCommGroup.eq_1] rw [crAnF_ofState_normalOrder_insert φ [φsΛ]ᵘᶜ ⟨(φsΛ.uncontractedListOrderPos i), by simp [uncontractedListGet]⟩, smul_smul] - trans (1 : ℂ) • 𝓞.crAnF (𝓝(ofStateList [φsΛ.insertList φ i none]ᵘᶜ)) + trans (1 : ℂ) • 𝓞.crAnF (𝓝(ofStateList [φsΛ.insertAndContract φ i none]ᵘᶜ)) · simp congr 1 simp only [instCommGroup.eq_1, uncontractedListGet] @@ -92,19 +92,19 @@ lemma insertList_none_normalOrder (φ : 𝓕.States) (φs : List 𝓕.States) simp only [exchangeSign_mul_self] congr simp only [Nat.succ_eq_add_one] - rw [insertList_uncontractedList_none_map] + rw [insertAndContract_uncontractedList_none_map] /-- Let `c` be a Wick Contraction for `φ₀φ₁…φₙ`. -We have (roughly) `N(c.insertList φ i k).uncontractedList` +We have (roughly) `N(c.insertAndContract φ i k).uncontractedList` is equal to `N((c.uncontractedList).eraseIdx k')` where `k'` is the position in `c.uncontractedList` corresponding to `k`. -/ -lemma insertList_some_normalOrder (φ : 𝓕.States) (φs : List 𝓕.States) +lemma insertAndContract_some_normalOrder (φ : 𝓕.States) (φs : List 𝓕.States) (i : Fin φs.length.succ) (φsΛ : WickContraction φs.length) (k : φsΛ.uncontracted) : - 𝓞.crAnF 𝓝(ofStateList [φsΛ.insertList φ i (some k)]ᵘᶜ) - = 𝓞.crAnF 𝓝(ofStateList (optionEraseZ [φsΛ]ᵘᶜ φ ((uncontractedStatesEquiv φs φsΛ) k))) := by - simp only [Nat.succ_eq_add_one, insertList, optionEraseZ, uncontractedStatesEquiv, + 𝓞.crAnF 𝓝([φsΛ.insertAndContract φ i (some k)]ᵘᶜ) + = 𝓞.crAnF 𝓝((optionEraseZ [φsΛ]ᵘᶜ φ ((uncontractedStatesEquiv φs φsΛ) k))) := by + simp only [Nat.succ_eq_add_one, insertAndContract, optionEraseZ, uncontractedStatesEquiv, Equiv.optionCongr_apply, Equiv.coe_trans, Option.map_some', Function.comp_apply, finCongr_apply, Fin.coe_cast, uncontractedListGet] congr @@ -117,18 +117,18 @@ lemma insertList_some_normalOrder (φ : 𝓕.States) (φs : List 𝓕.States) /-- Let `c` be a Wick Contraction for `φ₀φ₁…φₙ`. This lemma states that `(c.sign • c.timeContract 𝓞) * N(c.uncontracted)` -for `c` equal to `c.insertList φ i none` is equal to that for just `c` +for `c` equal to `c.insertAndContract φ i none` is equal to that for just `c` mulitiplied by the exchange sign of `φ` and `φ₀φ₁…φᵢ₋₁`. -/ -lemma sign_timeContract_normalOrder_insertList_none (φ : 𝓕.States) (φs : List 𝓕.States) +lemma sign_timeContract_normalOrder_insertAndContract_none (φ : 𝓕.States) (φs : List 𝓕.States) (i : Fin φs.length.succ) (φsΛ : WickContraction φs.length) : - (φsΛ.insertList φ i none).sign • (φsΛ.insertList φ i none).timeContract 𝓞 - * 𝓞.crAnF 𝓝(ofStateList [φsΛ.insertList φ i none]ᵘᶜ) = + (φsΛ.insertAndContract φ i none).sign • (φsΛ.insertAndContract φ i none).timeContract 𝓞 + * 𝓞.crAnF 𝓝([φsΛ.insertAndContract φ i none]ᵘᶜ) = 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ ⟨φs.get, (Finset.univ.filter (fun k => i.succAbove k < i))⟩) - • (φsΛ.sign • φsΛ.timeContract 𝓞 * 𝓞.crAnF 𝓝(ofStateList (φ :: [φsΛ]ᵘᶜ))) := by + • (φsΛ.sign • φsΛ.timeContract 𝓞 * 𝓞.crAnF 𝓝(φ :: [φsΛ]ᵘᶜ)) := by by_cases hg : GradingCompliant φs φsΛ - · rw [insertList_none_normalOrder, sign_insert_none] - simp only [Nat.succ_eq_add_one, timeContract_insertList_none, instCommGroup.eq_1, + · rw [insertAndContract_none_normalOrder, 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 rw [← mul_assoc] @@ -155,7 +155,7 @@ lemma sign_timeContract_normalOrder_insertList_none (φ : 𝓕.States) (φs : Li simp only [Bool.not_eq_true, Bool.eq_false_or_eq_true_self, true_and] intro h1 h2 simp_all - · simp only [Nat.succ_eq_add_one, timeContract_insertList_none, Algebra.smul_mul_assoc, + · simp only [Nat.succ_eq_add_one, timeContract_insertAndContract_none, Algebra.smul_mul_assoc, instCommGroup.eq_1] rw [timeContract_of_not_gradingCompliant] simp only [ZeroMemClass.coe_zero, zero_mul, smul_zero] @@ -165,26 +165,25 @@ lemma sign_timeContract_normalOrder_insertList_none (φ : 𝓕.States) (φs : Li Let `c` be a Wick Contraction for `φ₀φ₁…φₙ`. This lemma states that `(c.sign • c.timeContract 𝓞) * N(c.uncontracted)` -for `c` equal to `c.insertList φ i (some k)` is equal to that for just `c` +for `c` equal to `c.insertAndContract φ i (some k)` is equal to that for just `c` mulitiplied by the exchange sign of `φ` and `φ₀φ₁…φᵢ₋₁`. -/ -lemma sign_timeContract_normalOrder_insertList_some (φ : 𝓕.States) (φs : List 𝓕.States) +lemma sign_timeContract_normalOrder_insertAndContract_some (φ : 𝓕.States) (φs : List 𝓕.States) (i : Fin φs.length.succ) (φsΛ : WickContraction φs.length) (k : φsΛ.uncontracted) (hlt : ∀ (k : Fin φs.length), timeOrderRel φ φs[k]) (hn : ∀ (k : Fin φs.length), i.succAbove k < i → ¬ timeOrderRel φs[k] φ) : - (φsΛ.insertList φ i (some k)).sign • (φsΛ.insertList φ i (some k)).timeContract 𝓞 - * 𝓞.crAnF 𝓝(ofStateList [φsΛ.insertList φ i (some k)]ᵘᶜ) = + (φsΛ.insertAndContract φ i (some k)).sign • (φsΛ.insertAndContract φ i (some k)).timeContract 𝓞 + * 𝓞.crAnF 𝓝([φsΛ.insertAndContract φ i (some k)]ᵘᶜ) = 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ ⟨φs.get, (Finset.univ.filter (fun x => i.succAbove x < i))⟩) • (φsΛ.sign • (𝓞.contractStateAtIndex φ [φsΛ]ᵘᶜ ((uncontractedStatesEquiv φs φsΛ) (some k)) * φsΛ.timeContract 𝓞) - * 𝓞.crAnF 𝓝(ofStateList (optionEraseZ [φsΛ]ᵘᶜ φ - ((uncontractedStatesEquiv φs φsΛ) k)))) := by + * 𝓞.crAnF 𝓝((optionEraseZ [φsΛ]ᵘᶜ φ (uncontractedStatesEquiv φs φsΛ k)))) := by by_cases hg : GradingCompliant φs φsΛ ∧ (𝓕 |>ₛ φ) = (𝓕 |>ₛ φs[k.1]) · by_cases hk : i.succAbove k < i - · rw [WickContraction.timeConract_insertList_some_eq_mul_contractStateAtIndex_not_lt] + · rw [WickContraction.timeConract_insertAndContract_some_eq_mul_contractStateAtIndex_not_lt] swap · exact hn _ hk - rw [insertList_some_normalOrder, sign_insert_some] + rw [insertAndContract_some_normalOrder, 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] @@ -192,10 +191,10 @@ lemma sign_timeContract_normalOrder_insertList_some (φ : 𝓕.States) (φs : Li exact signInsertSome_mul_filter_contracted_of_lt φ φs φsΛ i k hk hg · omega · have hik : i.succAbove ↑k ≠ i := Fin.succAbove_ne i ↑k - rw [WickContraction.timeConract_insertList_some_eq_mul_contractStateAtIndex_lt] + rw [WickContraction.timeConract_insertAndContract_some_eq_mul_contractStateAtIndex_lt] swap · exact hlt _ - rw [insertList_some_normalOrder] + rw [insertAndContract_some_normalOrder] rw [sign_insert_some] simp only [instCommGroup.eq_1, smul_smul, Algebra.smul_mul_assoc] congr 1 @@ -203,7 +202,7 @@ lemma sign_timeContract_normalOrder_insertList_some (φ : 𝓕.States) (φs : Li congr 1 exact signInsertSome_mul_filter_contracted_of_not_lt φ φs φsΛ i k hk hg · omega - · rw [timeConract_insertList_some] + · rw [timeConract_insertAndContract_some] simp only [Fin.getElem_fin, not_and] at hg by_cases hg' : GradingCompliant φs φsΛ · have hg := hg hg' @@ -238,16 +237,16 @@ This lemma states that `(c.sign • c.timeContract 𝓞) * N(c.uncontracted)` is equal to the sum of `(c'.sign • c'.timeContract 𝓞) * N(c'.uncontracted)` -for all `c' = (c.insertList φ i k)` for `k : Option (c.uncontracted)`, multiplied by +for all `c' = (c.insertAndContract φ i k)` for `k : Option c.uncontracted`, multiplied by the exchange sign of `φ` and `φ₀φ₁…φᵢ₋₁`. -/ lemma mul_sum_contractions (φ : 𝓕.States) (φs : List 𝓕.States) (i : Fin φs.length.succ) (φsΛ : WickContraction φs.length) (hlt : ∀ (k : Fin φs.length), timeOrderRel φ φs[k]) (hn : ∀ (k : Fin φs.length), i.succAbove k < i → ¬timeOrderRel φs[k] φ) : - (φsΛ.sign • φsΛ.timeContract 𝓞) * 𝓞.crAnF ((CrAnAlgebra.ofState φ) * 𝓝(ofStateList [φsΛ]ᵘᶜ)) = + (φsΛ.sign • φsΛ.timeContract 𝓞) * 𝓞.crAnF ((CrAnAlgebra.ofState φ) * 𝓝([φsΛ]ᵘᶜ)) = 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ ⟨φs.get, (Finset.univ.filter (fun x => i.succAbove x < i))⟩) • - ∑ (k : Option φsΛ.uncontracted), ((φsΛ.insertList φ i k).sign • - (φsΛ.insertList φ i k).timeContract 𝓞 * 𝓞.crAnF (𝓝(ofStateList [φsΛ.insertList φ i k]ᵘᶜ))) := by + ∑ (k : Option φsΛ.uncontracted), ((φsΛ.insertAndContract φ i k).sign • + (φsΛ.insertAndContract φ i k).timeContract 𝓞 * 𝓞.crAnF (𝓝(ofStateList [φsΛ.insertAndContract φ i k]ᵘᶜ))) := by rw [crAnF_ofState_mul_normalOrder_ofStatesList_eq_sum, Finset.mul_sum, uncontractedStatesEquiv_list_sum, Finset.smul_sum] simp only [instCommGroup.eq_1, Nat.succ_eq_add_one] @@ -255,7 +254,7 @@ lemma mul_sum_contractions (φ : 𝓕.States) (φs : List 𝓕.States) (i : Fin funext n match n with | none => - rw [sign_timeContract_normalOrder_insertList_none] + rw [sign_timeContract_normalOrder_insertAndContract_none] simp only [contractStateAtIndex, uncontractedStatesEquiv, Equiv.optionCongr_apply, Equiv.coe_trans, Option.map_none', one_mul, Algebra.smul_mul_assoc, instCommGroup.eq_1, smul_smul] @@ -263,7 +262,7 @@ lemma mul_sum_contractions (φ : 𝓕.States) (φs : List 𝓕.States) (i : Fin rw [← mul_assoc, exchangeSign_mul_self] simp | some n => - rw [sign_timeContract_normalOrder_insertList_some _ _ _ _ _ + rw [sign_timeContract_normalOrder_insertAndContract_some _ _ _ _ _ (fun k => hlt k) (fun k a => hn k a)] simp only [uncontractedStatesEquiv, Equiv.optionCongr_apply, Equiv.coe_trans, Option.map_some', Function.comp_apply, finCongr_apply, Algebra.smul_mul_assoc, instCommGroup.eq_1, smul_smul] @@ -278,9 +277,9 @@ lemma mul_sum_contractions (φ : 𝓕.States) (φs : List 𝓕.States) (i : Fin lemma wicks_theorem_congr {φs φs' : List 𝓕.States} (h : φs = φs') : ∑ (φsΛ : WickContraction φs.length), (φsΛ.sign • φsΛ.timeContract 𝓞) * - 𝓞.crAnF 𝓝(ofStateList [φsΛ]ᵘᶜ) + 𝓞.crAnF 𝓝([φsΛ]ᵘᶜ) = ∑ (φs'Λ : WickContraction φs'.length), (φs'Λ.sign • φs'Λ.timeContract 𝓞) * - 𝓞.crAnF 𝓝(ofStateList [φs'Λ]ᵘᶜ) := by + 𝓞.crAnF 𝓝([φs'Λ]ᵘᶜ) := by subst h simp @@ -293,8 +292,7 @@ lemma wicks_theorem_congr {φs φs' : List 𝓕.States} (h : φs = φs') : /-- Wick's theorem for the empty list. -/ lemma wicks_theorem_nil : 𝓞.crAnF (ofStateAlgebra (timeOrder (ofList []))) = ∑ (nilΛ : WickContraction [].length), - (nilΛ.sign • nilΛ.timeContract 𝓞) * - 𝓞.crAnF 𝓝(ofStateList [nilΛ]ᵘᶜ) := by + (nilΛ.sign • nilΛ.timeContract 𝓞) * 𝓞.crAnF 𝓝([nilΛ]ᵘᶜ) := by rw [timeOrder_ofList_nil] simp only [map_one, List.length_nil, Algebra.smul_mul_assoc] rw [sum_WickContraction_nil, uncontractedListGet, nil_zero_uncontractedList] @@ -320,8 +318,7 @@ remark wicks_theorem_context := " - The normal-ordering of the uncontracted fields in `c`. -/ theorem wicks_theorem : (φs : List 𝓕.States) → 𝓞.crAnF (ofStateAlgebra (timeOrder (ofList φs))) = - ∑ (φsΛ : WickContraction φs.length), (φsΛ.sign • φsΛ.timeContract 𝓞) * - 𝓞.crAnF 𝓝(ofStateList [φsΛ]ᵘᶜ) + ∑ (φsΛ : WickContraction φs.length), (φsΛ.sign • φsΛ.timeContract 𝓞) * 𝓞.crAnF 𝓝([φsΛ]ᵘᶜ) | [] => wicks_theorem_nil | φ :: φs => by have ih := wicks_theorem (eraseMaxTimeField φ φs) @@ -342,17 +339,17 @@ theorem wicks_theorem : (φs : List 𝓕.States) → 𝓞.crAnF (ofStateAlgebra (maxTimeField φ φs) (eraseMaxTimeField φ φs) (maxTimeFieldPosFin φ φs) c] trans (1 : ℂ) • ∑ k : Option { x // x ∈ c.uncontracted }, sign (List.insertIdx (↑(maxTimeFieldPosFin φ φs)) (maxTimeField φ φs) (eraseMaxTimeField φ φs)) - (insertList (maxTimeField φ φs) c (maxTimeFieldPosFin φ φs) k) • - ↑((c.insertList (maxTimeField φ φs) (maxTimeFieldPosFin φ φs) k).timeContract 𝓞) * + (insertAndContract (maxTimeField φ φs) c (maxTimeFieldPosFin φ φs) k) • + ↑((c.insertAndContract (maxTimeField φ φs) (maxTimeFieldPosFin φ φs) k).timeContract 𝓞) * 𝓞.crAnF 𝓝(ofStateList (List.map (List.insertIdx (↑(maxTimeFieldPosFin φ φs)) (maxTimeField φ φs) (eraseMaxTimeField φ φs)).get - (insertList (maxTimeField φ φs) c + (insertAndContract (maxTimeField φ φs) c (maxTimeFieldPosFin φ φs) k).uncontractedList)) swap · simp [uncontractedListGet] rw [smul_smul] simp only [instCommGroup.eq_1, exchangeSign_mul_self, Nat.succ_eq_add_one, - Algebra.smul_mul_assoc, Fintype.sum_option, timeContract_insertList_none, + Algebra.smul_mul_assoc, Fintype.sum_option, timeContract_insertAndContract_none, Finset.univ_eq_attach, smul_add, one_smul, uncontractedListGet] · exact fun k => timeOrder_maxTimeField _ _ k · exact fun k => lt_maxTimeFieldPosFin_not_timeOrder _ _ k