From 8434334bbfbf99e266d8f5c6762fc3b623a99e9d Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Wed, 5 Feb 2025 11:52:55 +0000 Subject: [PATCH] docs: More docs related to Wicks theorem --- .../FieldOpAlgebra/StaticWickTerm.lean | 57 ++++++++++++++----- .../FieldOpAlgebra/WickTerm.lean | 54 +++++++++--------- .../FieldOpAlgebra/WicksTheorem.lean | 2 +- .../WickContraction/InsertAndContract.lean | 14 +++-- .../WickContraction/Sign/InsertNone.lean | 10 ++-- .../WickContraction/Sign/InsertSome.lean | 11 ++++ .../WickContraction/Sign/Join.lean | 5 ++ .../WickContraction/StaticContract.lean | 4 +- .../WickContraction/TimeContract.lean | 6 +- scripts/MetaPrograms/notes.lean | 22 +++++-- 10 files changed, 124 insertions(+), 61 deletions(-) diff --git a/HepLean/PerturbationTheory/FieldOpAlgebra/StaticWickTerm.lean b/HepLean/PerturbationTheory/FieldOpAlgebra/StaticWickTerm.lean index 9a4e16d..ac98b03 100644 --- a/HepLean/PerturbationTheory/FieldOpAlgebra/StaticWickTerm.lean +++ b/HepLean/PerturbationTheory/FieldOpAlgebra/StaticWickTerm.lean @@ -12,8 +12,6 @@ import HepLean.PerturbationTheory.WickContraction.StaticContract # Static Wick's terms -/ - - open FieldSpecification variable {𝓕 : FieldSpecification} @@ -29,21 +27,45 @@ noncomputable section def staticWickTerm {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) : 𝓕.FieldOpAlgebra := φsΛ.sign • φsΛ.staticContract * 𝓝(ofFieldOpList [φsΛ]ᵘᶜ) +/-- The static Wick term for the empty contraction of the empty list is `1`. -/ @[simp] lemma staticWickTerm_empty_nil : staticWickTerm (empty (n := ([] : List 𝓕.FieldOp).length)) = 1 := by rw [staticWickTerm, uncontractedListGet, nil_zero_uncontractedList] simp [sign, empty, staticContract] +/-- +Let `φsΛ` be a Wick Contraction for `φs = φ₀φ₁…φₙ`. Then the following holds +`(φsΛ ↩Λ φ 0 none).staticWickTerm = φsΛ.sign • φsΛ.staticWickTerm * 𝓝(φ :: [φsΛ]ᵘᶜ)` + +The proof of this result relies on +- `staticContract_insert_none` to rewrite the static contract. +- `sign_insert_none_zero` to rewrite the sign. +-/ lemma staticWickTerm_insert_zero_none (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) (φsΛ : WickContraction φs.length) : (φsΛ ↩Λ φ 0 none).staticWickTerm = φsΛ.sign • φsΛ.staticContract * 𝓝(ofFieldOpList (φ :: [φsΛ]ᵘᶜ)) := by symm erw [staticWickTerm, sign_insert_none_zero] - simp only [staticContract_insertAndContract_none, insertAndContract_uncontractedList_none_zero, + simp only [staticContract_insert_none, insertAndContract_uncontractedList_none_zero, Algebra.smul_mul_assoc] +/-- Let `φsΛ` be a Wick contraction for `φs = φ₀φ₁…φₙ`. Then`(φsΛ ↩Λ φ 0 (some k)).wickTerm` +is equal the product of +- the sign `𝓢(φ, φ₀…φᵢ₋₁) ` +- the sign `φsΛ.sign` +- `φsΛ.staticContract` +- `s • [anPart φ, ofFieldOp φs[k]]ₛ` where `s` is the sign associated with moving `φ` through + uncontracted fields in `φ₀…φₖ₋₁` +- the normal ordering `𝓝([φsΛ]ᵘᶜ.erase (uncontractedFieldOpEquiv φs φsΛ k))`. + +The proof of this result relies on +- `staticContract_insert_some_of_lt` to rewrite static + contractions. +- `normalOrder_uncontracted_some` to rewrite normal orderings. +- `sign_insert_some_zero` to rewrite signs. +-/ lemma staticWickTerm_insert_zero_some (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) (φsΛ : WickContraction φs.length) (k : { x // x ∈ φsΛ.uncontracted }) : (φsΛ ↩Λ φ 0 k).staticWickTerm = @@ -55,23 +77,16 @@ lemma staticWickTerm_insert_zero_some (φ : 𝓕.FieldOp) (φs : List 𝓕.Field simp only [← mul_assoc] rw [← smul_mul_assoc] congr 1 - rw [staticContract_insertAndContract_some_eq_mul_contractStateAtIndex_lt] + rw [staticContract_insert_some_of_lt] swap · simp rw [smul_smul] by_cases hn : GradingCompliant φs φsΛ ∧ (𝓕|>ₛφ) = (𝓕|>ₛ φs[k.1]) · congr 1 swap - · have h1 := φsΛ.staticContract.2 - rw [@Subalgebra.mem_center_iff] at h1 - rw [h1] - erw [sign_insert_some] - rw [mul_assoc, mul_comm φsΛ.sign, ← mul_assoc] - rw [signInsertSome_mul_filter_contracted_of_not_lt] - simp only [instCommGroup.eq_1, Fin.zero_succAbove, Fin.not_lt_zero, Finset.filter_False, - ofFinset_empty, map_one, one_mul] - simp only [Fin.zero_succAbove, Fin.not_lt_zero, not_false_eq_true] - exact hn + · rw [Subalgebra.mem_center_iff.mp φsΛ.staticContract.2] + · rw [sign_insert_some_zero _ _ _ _ hn, mul_comm, ← mul_assoc] + simp · simp only [Fin.getElem_fin, not_and] at hn by_cases h0 : ¬ GradingCompliant φs φsΛ · rw [staticContract_of_not_gradingCompliant] @@ -90,6 +105,18 @@ lemma staticWickTerm_insert_zero_some (φ : 𝓕.FieldOp) (φs : List 𝓕.Field rw [h1] simp + +/-- +Let `φsΛ` be a Wick contraction for `φs = φ₀φ₁…φₙ`. Then +`φ * φsΛ.staticWickTerm = ∑ k, (φsΛ ↩Λ φ i k).wickTerm` +where the sum is over all `k` in `Option φsΛ.uncontracted` (so either `none` or `some k`). + +The proof of proceeds as follows: +- `ofFieldOp_mul_normalOrder_ofFieldOpList_eq_sum` is used to expand `φ 𝓝([φsΛ]ᵘᶜ)` as + a sum over `k` in `Option φsΛ.uncontracted` of terms involving `[φ, φs[k]]` etc. +- Then `staticWickTerm_insert_zero_none` and `staticWickTerm_insert_zero_some` are + used to equate terms. +-/ lemma mul_staticWickTerm_eq_sum (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) (φsΛ : WickContraction φs.length) : ofFieldOp φ * φsΛ.staticWickTerm = @@ -107,7 +134,7 @@ lemma mul_staticWickTerm_eq_sum (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) | none => simp only [contractStateAtIndex, uncontractedFieldOpEquiv, Equiv.optionCongr_apply, Equiv.coe_trans, Option.map_none', one_mul, Algebra.smul_mul_assoc, Nat.succ_eq_add_one, - Fin.zero_eta, Fin.val_zero, List.insertIdx_zero, staticContract_insertAndContract_none, + Fin.zero_eta, Fin.val_zero, List.insertIdx_zero, staticContract_insert_none, insertAndContract_uncontractedList_none_zero] rw [staticWickTerm_insert_zero_none] simp only [Algebra.smul_mul_assoc] diff --git a/HepLean/PerturbationTheory/FieldOpAlgebra/WickTerm.lean b/HepLean/PerturbationTheory/FieldOpAlgebra/WickTerm.lean index 5b0532a..63dc4e2 100644 --- a/HepLean/PerturbationTheory/FieldOpAlgebra/WickTerm.lean +++ b/HepLean/PerturbationTheory/FieldOpAlgebra/WickTerm.lean @@ -29,6 +29,7 @@ noncomputable section def wickTerm {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) : 𝓕.FieldOpAlgebra := φsΛ.sign • φsΛ.timeContract * 𝓝(ofFieldOpList [φsΛ]ᵘᶜ) +/-- The Wick term for the empty contraction of the empty list is `1`. -/ @[simp] lemma wickTerm_empty_nil : wickTerm (empty (n := ([] : List 𝓕.FieldOp).length)) = 1 := by @@ -36,23 +37,13 @@ lemma wickTerm_empty_nil : simp [sign_empty] /-- -Let `φsΛ` be a Wick Contraction for `φs = φ₀φ₁…φₙ`. Then the wick-term of ` (φsΛ ↩Λ φ i none)` +Let `φsΛ` be a Wick Contraction for `φs = φ₀φ₁…φₙ`. Then the following holds +`(φsΛ ↩Λ φ i none).wickTerm = 𝓢(φ, φ₀…φᵢ₋₁) φsΛ.sign • φsΛ.timeContract * 𝓝(φ :: [φsΛ]ᵘᶜ)` -```(φsΛ ↩Λ φ i none).sign • (φsΛ ↩Λ φ i none).timeContract 𝓞 * 𝓞.crAnF 𝓝ᶠ([φsΛ ↩Λ φ i none]ᵘᶜ)``` - -is equal to - -`s • (φsΛ.sign • φsΛ.timeContract 𝓞 * 𝓞.crAnF 𝓝ᶠ(φ :: [φsΛ]ᵘᶜ))` - -where `s` is the exchange sign of `φ` and the uncontracted fields in `φ₀φ₁…φᵢ₋₁`. - -The proof of this result relies primarily on: -- `normalOrderF_uncontracted_none` which replaces `𝓝ᶠ([φsΛ ↩Λ φ i none]ᵘᶜ)` with - `𝓝ᶠ(φ :: [φsΛ]ᵘᶜ)` up to a sign. -- `timeContract_insertAndContract_none` which replaces `(φsΛ ↩Λ φ i none).timeContract 𝓞` with - `φsΛ.timeContract 𝓞`. -- `sign_insert_none` and `signInsertNone_eq_filterset` which are used to take account of - signs. +The proof of this result relies on +- `normalOrder_uncontracted_none` to rewrite normal orderings. +- `timeContract_insert_none` to rewrite the time contract. +- `sign_insert_none` to rewrite the sign. -/ lemma wickTerm_insert_none (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) (i : Fin φs.length.succ) (φsΛ : WickContraction φs.length) : @@ -62,7 +53,7 @@ lemma wickTerm_insert_none (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) rw [wickTerm] by_cases hg : GradingCompliant φs φsΛ · rw [normalOrder_uncontracted_none, sign_insert_none _ _ _ _ hg] - simp only [Nat.succ_eq_add_one, timeContract_insertAndContract_none, instCommGroup.eq_1, + simp only [Nat.succ_eq_add_one, timeContract_insert_none, instCommGroup.eq_1, Algebra.mul_smul_comm, Algebra.smul_mul_assoc, smul_smul] congr 1 rw [← mul_assoc] @@ -89,18 +80,29 @@ lemma wickTerm_insert_none (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) 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_insertAndContract_none, Algebra.smul_mul_assoc, + · simp only [Nat.succ_eq_add_one, timeContract_insert_none, Algebra.smul_mul_assoc, instCommGroup.eq_1] rw [timeContract_of_not_gradingCompliant] simp only [ZeroMemClass.coe_zero, zero_mul, smul_zero] exact hg -/-- -Let `c` be a Wick Contraction for `φ₀φ₁…φₙ`. -This lemma states that -`(c.sign • c.timeContract 𝓞) * N(c.uncontracted)` -for `c` equal to `c ↩Λ φ i (some k)` is equal to that for just `c` -mulitiplied by the exchange sign of `φ` and `φ₀φ₁…φᵢ₋₁`. +/-- Let `φsΛ` be a Wick contraction for `φs = φ₀φ₁…φₙ`. Let `φ` be a field with time +greater then or equal to all the fields in `φs`. Let `i` be a in `Fin φs.length.succ` such that +all files in `φ₀…φᵢ₋₁` have time strictly less then `φ`. Then`(φsΛ ↩Λ φ i (some k)).wickTerm` +is equal the product of +- the sign `𝓢(φ, φ₀…φᵢ₋₁) ` +- the sign `φsΛ.sign` +- `φsΛ.timeContract` +- `s • [anPart φ, ofFieldOp φs[k]]ₛ` where `s` is the sign associated with moving `φ` through + uncontracted fields in `φ₀…φₖ₋₁` +- the normal ordering `𝓝([φsΛ]ᵘᶜ.erase (uncontractedFieldOpEquiv φs φsΛ k))`. + +The proof of this result relies on +- `timeContract_insert_some_of_not_lt` + and `timeContract_insert_some_of_lt` to rewrite time + contractions. +- `normalOrder_uncontracted_some` to rewrite normal orderings. +- `sign_insert_some_of_not_lt` and `sign_insert_some_of_lt` to rewrite signs. -/ lemma wickTerm_insert_some (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) (i : Fin φs.length.succ) (φsΛ : WickContraction φs.length) (k : φsΛ.uncontracted) @@ -114,7 +116,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.timeContract_insertAndContract_some_eq_mul_contractStateAtIndex_not_lt] + · rw [WickContraction.timeContract_insert_some_of_not_lt] swap · exact hn _ hk · rw [normalOrder_uncontracted_some, sign_insert_some_of_lt φ φs φsΛ i k hk hg] @@ -124,7 +126,7 @@ lemma wickTerm_insert_some (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) simp · omega · have hik : i.succAbove ↑k ≠ i := Fin.succAbove_ne i ↑k - rw [timeContract_insertAndContract_some_eq_mul_contractStateAtIndex_lt] + rw [timeContract_insert_some_of_lt] swap · exact hlt _ · rw [normalOrder_uncontracted_some] diff --git a/HepLean/PerturbationTheory/FieldOpAlgebra/WicksTheorem.lean b/HepLean/PerturbationTheory/FieldOpAlgebra/WicksTheorem.lean index 007eb77..5999214 100644 --- a/HepLean/PerturbationTheory/FieldOpAlgebra/WicksTheorem.lean +++ b/HepLean/PerturbationTheory/FieldOpAlgebra/WicksTheorem.lean @@ -101,7 +101,7 @@ theorem wicks_theorem : (φs : List 𝓕.FieldOp) → 𝓣(ofFieldOpList φs) = · 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_insertAndContract_none, + Algebra.smul_mul_assoc, Fintype.sum_option, timeContract_insert_none, Finset.univ_eq_attach, smul_add, one_smul, uncontractedListGet] · exact fun k => timeOrder_maxTimeField _ _ k · exact fun k => lt_maxTimeFieldPosFin_not_timeOrder _ _ k diff --git a/HepLean/PerturbationTheory/WickContraction/InsertAndContract.lean b/HepLean/PerturbationTheory/WickContraction/InsertAndContract.lean index ab29413..0fc3546 100644 --- a/HepLean/PerturbationTheory/WickContraction/InsertAndContract.lean +++ b/HepLean/PerturbationTheory/WickContraction/InsertAndContract.lean @@ -24,11 +24,15 @@ open HepLean.Fin -/ -/-- Given a Wick contraction `c` associated to a list `φs`, - a position `i : Fin n.succ`, an element `φ`, and an optional uncontracted element - `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. -/ +/-- Given a Wick contraction `φsΛ` associated to a list `φs`, + a position `i : Fin φs.lengthsucc`, an element `φ`, and an optional uncontracted element + `j : Option (φsΛ.uncontracted)` of `φsΛ`. + The Wick contraction `φsΛ.insertAndContract φ i j` is defined to be the Wick contraction + associated with `(φs.insertIdx i φ)` formed by 'inserting' `φ` into `φs` after the first `i` + elements and contracting `φ` optionally with `j`. + + The notation `φsΛ ↩Λ φ i j` is used to denote `φsΛ.insertAndContract φ i j`. Thus, + `φsΛ ↩Λ φ i none` indicates the case when we insert `φ` into `φs` but do not contract it. -/ def insertAndContract {φs : List 𝓕.FieldOp} (φ : 𝓕.FieldOp) (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (j : Option φsΛ.uncontracted) : WickContraction (φs.insertIdx i φ).length := diff --git a/HepLean/PerturbationTheory/WickContraction/Sign/InsertNone.lean b/HepLean/PerturbationTheory/WickContraction/Sign/InsertNone.lean index dbd61a1..9323984 100644 --- a/HepLean/PerturbationTheory/WickContraction/Sign/InsertNone.lean +++ b/HepLean/PerturbationTheory/WickContraction/Sign/InsertNone.lean @@ -157,11 +157,6 @@ lemma signInsertNone_eq_prod_prod (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) erw [hG a] rfl -lemma sign_insert_none_zero (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) - (φsΛ : WickContraction φs.length) : (φsΛ ↩Λ φ 0 none).sign = φsΛ.sign := by - rw [sign_insert_none_eq_signInsertNone_mul_sign] - simp [signInsertNone] - lemma signInsertNone_eq_prod_getDual?_Some (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (hG : GradingCompliant φs φsΛ) : φsΛ.signInsertNone φ φs i = ∏ (x : Fin φs.length), @@ -255,4 +250,9 @@ lemma sign_insert_none (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) rw [signInsertNone_eq_filterset] exact hG +lemma sign_insert_none_zero (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) + (φsΛ : WickContraction φs.length) : (φsΛ ↩Λ φ 0 none).sign = φsΛ.sign := by + rw [sign_insert_none_eq_signInsertNone_mul_sign] + simp [signInsertNone] + end WickContraction diff --git a/HepLean/PerturbationTheory/WickContraction/Sign/InsertSome.lean b/HepLean/PerturbationTheory/WickContraction/Sign/InsertSome.lean index 9d4ff99..f5c78d2 100644 --- a/HepLean/PerturbationTheory/WickContraction/Sign/InsertSome.lean +++ b/HepLean/PerturbationTheory/WickContraction/Sign/InsertSome.lean @@ -901,4 +901,15 @@ lemma sign_insert_some_of_not_lt (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) rw [mul_comm, ← mul_assoc] simp +lemma sign_insert_some_zero (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) + (φsΛ : WickContraction φs.length) (k : φsΛ.uncontracted) + (hn : GradingCompliant φs φsΛ ∧ (𝓕|>ₛφ) = 𝓕|>ₛφs[k.1]): + (φsΛ ↩Λ φ 0 k).sign = 𝓢(𝓕|>ₛφ, 𝓕 |>ₛ ⟨φs.get, (φsΛ.uncontracted.filter (fun x => x < ↑k))⟩) * + φsΛ.sign := by + rw [sign_insert_some_of_not_lt] + · simp + · simp + · exact hn + + end WickContraction diff --git a/HepLean/PerturbationTheory/WickContraction/Sign/Join.lean b/HepLean/PerturbationTheory/WickContraction/Sign/Join.lean index 67944ff..08f51f0 100644 --- a/HepLean/PerturbationTheory/WickContraction/Sign/Join.lean +++ b/HepLean/PerturbationTheory/WickContraction/Sign/Join.lean @@ -417,6 +417,11 @@ lemma join_sign_induction {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs apply sign_congr exact join_uncontractedListGet (singleton hij) φsucΛ' +/-- Let `φsΛ` be a grading compliant Wick contraction for `φs` and + `φsucΛ` a Wick contraction for `[φsΛ]ᵘᶜ`. Then `(join φsΛ φsucΛ).sign = φsΛ.sign * φsucΛ.sign`. + + This lemma manifests the fact that it does not matter which order contracted pairs are brought + together when defining the sign of a contraction. -/ lemma join_sign {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) (φsucΛ : WickContraction [φsΛ]ᵘᶜ.length) (hc : φsΛ.GradingCompliant) : (join φsΛ φsucΛ).sign = φsΛ.sign * φsucΛ.sign := by diff --git a/HepLean/PerturbationTheory/WickContraction/StaticContract.lean b/HepLean/PerturbationTheory/WickContraction/StaticContract.lean index c98be1a..acfd884 100644 --- a/HepLean/PerturbationTheory/WickContraction/StaticContract.lean +++ b/HepLean/PerturbationTheory/WickContraction/StaticContract.lean @@ -29,7 +29,7 @@ noncomputable def staticContract {φs : List 𝓕.FieldOp} superCommute_anPart_ofFieldOp_mem_center _ _⟩ @[simp] -lemma staticContract_insertAndContract_none (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) +lemma staticContract_insert_none (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) : (φsΛ ↩Λ φ i none).staticContract = φsΛ.staticContract := by rw [staticContract, insertAndContract_none_prod_contractions] @@ -66,7 +66,7 @@ lemma staticContract_insertAndContract_some open FieldStatistic -lemma staticContract_insertAndContract_some_eq_mul_contractStateAtIndex_lt +lemma staticContract_insert_some_of_lt (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (k : φsΛ.uncontracted) (hik : i < i.succAbove k) : diff --git a/HepLean/PerturbationTheory/WickContraction/TimeContract.lean b/HepLean/PerturbationTheory/WickContraction/TimeContract.lean index 58941be..00e0088 100644 --- a/HepLean/PerturbationTheory/WickContraction/TimeContract.lean +++ b/HepLean/PerturbationTheory/WickContraction/TimeContract.lean @@ -34,7 +34,7 @@ noncomputable def timeContract {φs : List 𝓕.FieldOp} This result follows from the fact that `timeContract` only depends on contracted pairs, and `(φsΛ ↩Λ φ i none)` has the 'same' contracted pairs as `φsΛ`. -/ @[simp] -lemma timeContract_insertAndContract_none (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) +lemma timeContract_insert_none (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) : (φsΛ ↩Λ φ i none).timeContract = φsΛ.timeContract := by rw [timeContract, insertAndContract_none_prod_contractions] @@ -77,7 +77,7 @@ lemma timeContract_empty (φs : List 𝓕.FieldOp) : open FieldStatistic -lemma timeContract_insertAndContract_some_eq_mul_contractStateAtIndex_lt +lemma timeContract_insert_some_of_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) : @@ -110,7 +110,7 @@ lemma timeContract_insertAndContract_some_eq_mul_contractStateAtIndex_lt simp only [exchangeSign_mul_self] · exact ht -lemma timeContract_insertAndContract_some_eq_mul_contractStateAtIndex_not_lt +lemma timeContract_insert_some_of_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) : diff --git a/scripts/MetaPrograms/notes.lean b/scripts/MetaPrograms/notes.lean index 1db6e49..63b828b 100644 --- a/scripts/MetaPrograms/notes.lean +++ b/scripts/MetaPrograms/notes.lean @@ -117,7 +117,8 @@ def perturbationTheory : Note where title := "Proof of Wick's theorem" curators := ["Joseph Tooby-Smith"] parts := [ - .warning "This note is a work in progress and is not finished. Use with caution.", + .warning "This note is a work in progress and is not finished. Use with caution. + (5th Feb 2025)", .h1 "Introduction", .name `FieldSpecification.wicks_theorem_context, .p "In this note we walk through the important parts of the proof of Wick's theorem @@ -167,21 +168,34 @@ def perturbationTheory : Note where .h2 "Definition", .name `WickContraction, .name `WickContraction.GradingCompliant, - .h2 "Cardinality", + .h2 "Aside: Cardinality", .name `WickContraction.card_eq_cardFun, .h2 "Constructors", .p "There are a number of ways to construct a Wick contraction from other Wick contractions or single contractions.", .name `WickContraction.insertAndContract, - .name `WickContraction.erase, .name `WickContraction.join, .h2 "Sign", .name `WickContraction.sign, .name `WickContraction.join_sign, .name `WickContraction.sign_insert_none, + .name `WickContraction.sign_insert_none_zero, .name `WickContraction.sign_insert_some_of_not_lt, .name `WickContraction.sign_insert_some_of_lt, - .h1 "Time and static contractions", + .name `WickContraction.sign_insert_some_zero, + .h2 "Normal order", + .name `FieldSpecification.FieldOpAlgebra.normalOrder_uncontracted_none, + .name `FieldSpecification.FieldOpAlgebra.normalOrder_uncontracted_some, + .h1 "Static contractions", + .name `WickContraction.staticContract, + .name `WickContraction.staticContract_insert_some_of_lt, + .name `WickContraction.staticContract_insert_none, + .h1 "Time contractions", + .name `FieldSpecification.FieldOpAlgebra.timeContract, + .name `WickContraction.timeContract, + .name `WickContraction.timeContract_insert_none, + .name `WickContraction.timeContract_insert_some_of_not_lt, + .name `WickContraction.timeContract_insert_some_of_lt, .h1 "Wick terms", .name `WickContraction.wickTerm, .name `WickContraction.wickTerm_empty_nil,