diff --git a/HepLean.lean b/HepLean.lean index 7084beaa..62aaef2e 100644 --- a/HepLean.lean +++ b/HepLean.lean @@ -133,6 +133,7 @@ import HepLean.PerturbationTheory.Algebras.FieldOpAlgebra.StaticWickTheorem import HepLean.PerturbationTheory.Algebras.FieldOpAlgebra.SuperCommute import HepLean.PerturbationTheory.Algebras.FieldOpAlgebra.TimeContraction import HepLean.PerturbationTheory.Algebras.FieldOpAlgebra.TimeOrder +import HepLean.PerturbationTheory.Algebras.FieldOpAlgebra.WicksTheoremNormal import HepLean.PerturbationTheory.CreateAnnihilate import HepLean.PerturbationTheory.FeynmanDiagrams.Basic import HepLean.PerturbationTheory.FeynmanDiagrams.Instances.ComplexScalar @@ -157,8 +158,12 @@ import HepLean.PerturbationTheory.WickContraction.InsertAndContract import HepLean.PerturbationTheory.WickContraction.InsertAndContractNat import HepLean.PerturbationTheory.WickContraction.Involutions import HepLean.PerturbationTheory.WickContraction.IsFull +import HepLean.PerturbationTheory.WickContraction.Join import HepLean.PerturbationTheory.WickContraction.Sign +import HepLean.PerturbationTheory.WickContraction.Singleton import HepLean.PerturbationTheory.WickContraction.StaticContract +import HepLean.PerturbationTheory.WickContraction.SubContraction +import HepLean.PerturbationTheory.WickContraction.TimeCond import HepLean.PerturbationTheory.WickContraction.TimeContract import HepLean.PerturbationTheory.WickContraction.Uncontracted import HepLean.PerturbationTheory.WickContraction.UncontractedList diff --git a/HepLean/PerturbationTheory/Algebras/CrAnAlgebra/NormalOrder.lean b/HepLean/PerturbationTheory/Algebras/CrAnAlgebra/NormalOrder.lean index dc530b0c..7d07da27 100644 --- a/HepLean/PerturbationTheory/Algebras/CrAnAlgebra/NormalOrder.lean +++ b/HepLean/PerturbationTheory/Algebras/CrAnAlgebra/NormalOrder.lean @@ -52,6 +52,67 @@ lemma normalOrderF_one : normalOrderF (𝓕 := 𝓕) 1 = 1 := by rw [← ofCrAnList_nil, normalOrderF_ofCrAnList, normalOrderSign_nil, normalOrderList_nil, ofCrAnList_nil, one_smul] +lemma normalOrderF_normalOrderF_mid (a b c : 𝓕.CrAnAlgebra) : + 𝓝ᶠ(a * b * c) = 𝓝ᶠ(a * 𝓝ᶠ(b) * c) := by + let pc (c : 𝓕.CrAnAlgebra) (hc : c ∈ Submodule.span ℂ (Set.range ofCrAnListBasis)) : + Prop := 𝓝ᶠ(a * b * c) = 𝓝ᶠ(a * 𝓝ᶠ(b) * c) + change pc c (Basis.mem_span _ c) + apply Submodule.span_induction + · intro x hx + obtain ⟨φs, rfl⟩ := hx + simp only [ofListBasis_eq_ofList, pc] + let pb (b : 𝓕.CrAnAlgebra) (hb : b ∈ Submodule.span ℂ (Set.range ofCrAnListBasis)) : + Prop := 𝓝ᶠ(a * b * ofCrAnList φs) = 𝓝ᶠ(a * 𝓝ᶠ(b) * ofCrAnList φs) + change pb b (Basis.mem_span _ b) + apply Submodule.span_induction + · intro x hx + obtain ⟨φs', rfl⟩ := hx + simp only [ofListBasis_eq_ofList, pb] + let pa (a : 𝓕.CrAnAlgebra) (ha : a ∈ Submodule.span ℂ (Set.range ofCrAnListBasis)) : + Prop := 𝓝ᶠ(a * ofCrAnList φs' * ofCrAnList φs) = 𝓝ᶠ(a * 𝓝ᶠ(ofCrAnList φs') * ofCrAnList φs) + change pa a (Basis.mem_span _ a) + apply Submodule.span_induction + · intro x hx + obtain ⟨φs'', rfl⟩ := hx + simp only [ofListBasis_eq_ofList, pa] + rw [normalOrderF_ofCrAnList] + simp only [← ofCrAnList_append, Algebra.mul_smul_comm, + Algebra.smul_mul_assoc, map_smul] + rw [normalOrderF_ofCrAnList, normalOrderF_ofCrAnList, smul_smul] + congr 1 + · simp only [normalOrderSign, normalOrderList] + rw [Wick.koszulSign_of_append_eq_insertionSort, mul_comm] + · congr 1 + simp only [normalOrderList] + rw [HepLean.List.insertionSort_append_insertionSort_append] + · simp [pa] + · intro x y hx hy h1 h2 + simp_all [pa, add_mul] + · intro x hx h + simp_all [pa] + · simp [pb] + · intro x y hx hy h1 h2 + simp_all [pb, mul_add, add_mul] + · intro x hx h + simp_all [pb] + · simp [pc] + · intro x y hx hy h1 h2 + simp_all [pc, mul_add] + · intro x hx h hp + simp_all [pc] + +lemma normalOrderF_normalOrderF_right (a b : 𝓕.CrAnAlgebra) : 𝓝ᶠ(a * b) = 𝓝ᶠ(a * 𝓝ᶠ(b)) := by + trans 𝓝ᶠ(a * b * 1) + · simp + · rw [normalOrderF_normalOrderF_mid] + simp + +lemma normalOrderF_normalOrderF_left (a b : 𝓕.CrAnAlgebra) : 𝓝ᶠ(a * b) = 𝓝ᶠ(𝓝ᶠ(a) * b) := by + trans 𝓝ᶠ(1 * a * b) + · simp + · rw [normalOrderF_normalOrderF_mid] + simp + /-! ## Normal ordering with a creation operator on the left or annihilation on the right diff --git a/HepLean/PerturbationTheory/Algebras/FieldOpAlgebra/NormalOrder.lean b/HepLean/PerturbationTheory/Algebras/FieldOpAlgebra/NormalOrder.lean index 2d83839d..118765e3 100644 --- a/HepLean/PerturbationTheory/Algebras/FieldOpAlgebra/NormalOrder.lean +++ b/HepLean/PerturbationTheory/Algebras/FieldOpAlgebra/NormalOrder.lean @@ -261,6 +261,43 @@ lemma ofCrAnFieldOpList_eq_normalOrder (φs : List 𝓕.CrAnStates) : rw [normalOrder_ofCrAnFieldOpList, smul_smul, normalOrderSign, Wick.koszulSign_mul_self, one_smul] +lemma normalOrder_normalOrder_mid (a b c : 𝓕.FieldOpAlgebra) : + 𝓝(a * b * c) = 𝓝(a * 𝓝(b) * c) := by + obtain ⟨a, rfl⟩ := ι_surjective a + obtain ⟨b, rfl⟩ := ι_surjective b + obtain ⟨c, rfl⟩ := ι_surjective c + rw [normalOrder_eq_ι_normalOrderF] + simp only [← map_mul] + rw [normalOrder_eq_ι_normalOrderF] + rw [normalOrderF_normalOrderF_mid] + rfl + +lemma normalOrder_normalOrder_left (a b : 𝓕.FieldOpAlgebra) : + 𝓝(a * b) = 𝓝(𝓝(a) * b) := by + obtain ⟨a, rfl⟩ := ι_surjective a + obtain ⟨b, rfl⟩ := ι_surjective b + rw [normalOrder_eq_ι_normalOrderF] + simp only [← map_mul] + rw [normalOrder_eq_ι_normalOrderF] + rw [normalOrderF_normalOrderF_left] + rfl + +lemma normalOrder_normalOrder_right (a b : 𝓕.FieldOpAlgebra) : + 𝓝(a * b) = 𝓝(a * 𝓝(b)) := by + obtain ⟨a, rfl⟩ := ι_surjective a + obtain ⟨b, rfl⟩ := ι_surjective b + rw [normalOrder_eq_ι_normalOrderF] + simp only [← map_mul] + rw [normalOrder_eq_ι_normalOrderF] + rw [normalOrderF_normalOrderF_right] + rfl + +lemma normalOrder_normalOrder (a : 𝓕.FieldOpAlgebra) : 𝓝(𝓝(a)) = 𝓝(a) := by + trans 𝓝(𝓝(a) * 1) + · simp + · rw [← normalOrder_normalOrder_left] + simp + /-! ## mul anpart and crpart @@ -466,7 +503,7 @@ lemma anPart_mul_normalOrder_ofFieldOpList_eq_superCommute_reorder (φ : 𝓕.St (φs : List 𝓕.States) : anPart φ * 𝓝(ofFieldOpList φs) = 𝓝(anPart φ * ofFieldOpList φs) + [anPart φ, 𝓝(ofFieldOpList φs)]ₛ := by rw [anPart_mul_normalOrder_ofFieldOpList_eq_superCommute] - simp [instCommGroup.eq_1, map_add, map_smul] + simp only [instCommGroup.eq_1, add_left_inj] rw [normalOrder_anPart_ofFieldOpList_swap] /-- @@ -525,8 +562,8 @@ lemma ofFieldOpList_normalOrder_insert (φ : 𝓕.States) (φs : List 𝓕.State rw [hl] rw [ofFieldOpList_append, ofFieldOpList_append] rw [ofFieldOpList_mul_ofFieldOpList_eq_superCommute, add_mul] - simp [instCommGroup.eq_1, Nat.succ_eq_add_one, ofList_singleton, Algebra.smul_mul_assoc, - map_add, map_smul, add_zero, smul_smul, + simp only [instCommGroup.eq_1, Nat.succ_eq_add_one, ofList_singleton, Algebra.smul_mul_assoc, + map_add, map_smul, normalOrder_superCommute_left_eq_zero, add_zero, smul_smul, exchangeSign_mul_self_swap, one_smul] rw [← ofFieldOpList_append, ← ofFieldOpList_append] simp diff --git a/HepLean/PerturbationTheory/Algebras/FieldOpAlgebra/StaticWickTheorem.lean b/HepLean/PerturbationTheory/Algebras/FieldOpAlgebra/StaticWickTheorem.lean index b9b6d418..efdc6bbd 100644 --- a/HepLean/PerturbationTheory/Algebras/FieldOpAlgebra/StaticWickTheorem.lean +++ b/HepLean/PerturbationTheory/Algebras/FieldOpAlgebra/StaticWickTheorem.lean @@ -34,15 +34,15 @@ theorem static_wick_theorem : (φs : List 𝓕.States) → | φ :: φs => by rw [ofFieldOpList_cons] rw [static_wick_theorem φs] - rw [show (φ :: φs) = φs.insertIdx (⟨0, Nat.zero_lt_succ φs.length⟩ : Fin φs.length.succ) φ + rw [show (φ :: φs) = φs.insertIdx (⟨0, Nat.zero_lt_succ φs.length⟩ : Fin φs.length.succ) φ from rfl] - conv_rhs => rw [insertLift_sum ] + conv_rhs => rw [insertLift_sum] rw [Finset.mul_sum] apply Finset.sum_congr rfl intro c _ - trans (sign φs c • ↑c.staticContract * (ofFieldOp φ * normalOrder (ofFieldOpList [c]ᵘᶜ))) + trans (sign φs c • ↑c.staticContract * (ofFieldOp φ * normalOrder (ofFieldOpList [c]ᵘᶜ))) · have ht := Subalgebra.mem_center_iff.mp (Subalgebra.smul_mem (Subalgebra.center ℂ _) - (c.staticContract).2 c.sign ) + (c.staticContract).2 c.sign) conv_rhs => rw [← mul_assoc, ← ht] simp [mul_assoc] rw [ofFieldOp_mul_normalOrder_ofFieldOpList_eq_sum] @@ -61,7 +61,7 @@ theorem static_wick_theorem : (φs : List 𝓕.States) → simp only [Algebra.smul_mul_assoc, Nat.succ_eq_add_one, Fin.zero_eta, Fin.val_zero, List.insertIdx_zero] rw [normalOrder_uncontracted_some] - simp [← mul_assoc] + simp only [← mul_assoc] rw [← smul_mul_assoc] conv_rhs => rw [← smul_mul_assoc] congr 1 @@ -69,7 +69,7 @@ theorem static_wick_theorem : (φs : List 𝓕.States) → swap · simp rw [smul_smul] - by_cases hn : GradingCompliant φs c ∧ (𝓕|>ₛφ) = (𝓕|>ₛ φs[n.1]) + by_cases hn : GradingCompliant φs c ∧ (𝓕|>ₛφ) = (𝓕|>ₛ φs[n.1]) · congr 1 swap · have h1 := c.staticContract.2 @@ -82,19 +82,20 @@ theorem static_wick_theorem : (φs : List 𝓕.States) → ofFinset_empty, map_one, one_mul] simp only [Fin.zero_succAbove, Fin.not_lt_zero, not_false_eq_true] exact hn - · simp at hn + · simp only [Fin.getElem_fin, not_and] at hn by_cases h0 : ¬ GradingCompliant φs c · rw [staticContract_of_not_gradingCompliant] simp only [ZeroMemClass.coe_zero, zero_mul, smul_zero, instCommGroup.eq_1, mul_zero] exact h0 - · simp_all - have h1 : contractStateAtIndex φ [c]ᵘᶜ + · simp_all only [Finset.mem_univ, not_not, instCommGroup.eq_1, forall_const] + have h1 : contractStateAtIndex φ [c]ᵘᶜ ((uncontractedStatesEquiv φs c) (some n)) = 0 := by simp only [contractStateAtIndex, uncontractedStatesEquiv, Equiv.optionCongr_apply, Equiv.coe_trans, Option.map_some', Function.comp_apply, finCongr_apply, instCommGroup.eq_1, Fin.coe_cast, Fin.getElem_fin, smul_eq_zero] right - simp [uncontractedListGet] + simp only [uncontractedListGet, List.getElem_map, + uncontractedList_getElem_uncontractedIndexEquiv_symm, List.get_eq_getElem] rw [superCommute_anPart_ofState_diff_grade_zero] exact hn rw [h1] diff --git a/HepLean/PerturbationTheory/Algebras/FieldOpAlgebra/TimeContraction.lean b/HepLean/PerturbationTheory/Algebras/FieldOpAlgebra/TimeContraction.lean index 360ec938..92028653 100644 --- a/HepLean/PerturbationTheory/Algebras/FieldOpAlgebra/TimeContraction.lean +++ b/HepLean/PerturbationTheory/Algebras/FieldOpAlgebra/TimeContraction.lean @@ -55,6 +55,13 @@ lemma timeContract_of_not_timeOrderRel (φ ψ : 𝓕.States) (h : ¬ timeOrderRe simp only [instCommGroup.eq_1, map_smul, map_add, smul_add] rw [smul_smul, smul_smul, mul_comm] +lemma timeContract_of_not_timeOrderRel_expand (φ ψ : 𝓕.States) (h : ¬ timeOrderRel φ ψ) : + timeContract φ ψ = 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ ψ) • [anPart ψ, ofFieldOp φ]ₛ := by + rw [timeContract_of_not_timeOrderRel _ _ h] + rw [timeContract_of_timeOrderRel _ _ _] + have h1 := IsTotal.total (r := 𝓕.timeOrderRel) φ ψ + simp_all + lemma timeContract_mem_center (φ ψ : 𝓕.States) : timeContract φ ψ ∈ Subalgebra.center ℂ 𝓕.FieldOpAlgebra := by by_cases h : timeOrderRel φ ψ @@ -81,6 +88,90 @@ lemma timeContract_zero_of_diff_grade (φ ψ : 𝓕.States) (h : (𝓕 |>ₛ φ) have ht := IsTotal.total (r := 𝓕.timeOrderRel) φ ψ simp_all +lemma normalOrder_timeContract (φ ψ : 𝓕.States) : + 𝓝(timeContract φ ψ) = 0 := by + by_cases h : timeOrderRel φ ψ + · rw [timeContract_of_timeOrderRel _ _ h] + simp + · rw [timeContract_of_not_timeOrderRel _ _ h] + simp only [instCommGroup.eq_1, map_smul, smul_eq_zero] + have h1 : timeOrderRel ψ φ := by + have ht : timeOrderRel φ ψ ∨ timeOrderRel ψ φ := IsTotal.total (r := 𝓕.timeOrderRel) φ ψ + simp_all + rw [timeContract_of_timeOrderRel _ _ h1] + simp + +lemma timeOrder_timeContract_eq_time_mid {φ ψ : 𝓕.States} + (h1 : timeOrderRel φ ψ) (h2 : timeOrderRel ψ φ) (a b : 𝓕.FieldOpAlgebra) : + 𝓣(a * timeContract φ ψ * b) = timeContract φ ψ * 𝓣(a * b) := by + rw [timeContract_of_timeOrderRel _ _ h1] + rw [ofFieldOp_eq_sum] + simp only [map_sum, Finset.mul_sum, Finset.sum_mul] + congr + funext x + match φ with + | .inAsymp φ => + simp + | .position φ => + simp only [anPart_position, instCommGroup.eq_1] + apply timeOrder_superCommute_eq_time_mid _ _ + simp only [crAnTimeOrderRel, h1] + simp [crAnTimeOrderRel, h2] + | .outAsymp φ => + simp only [anPart_posAsymp, instCommGroup.eq_1] + apply timeOrder_superCommute_eq_time_mid _ _ + simp only [crAnTimeOrderRel, h1] + simp [crAnTimeOrderRel, h2] + +lemma timeOrder_timeContract_eq_time_left {φ ψ : 𝓕.States} + (h1 : timeOrderRel φ ψ) (h2 : timeOrderRel ψ φ) (b : 𝓕.FieldOpAlgebra) : + 𝓣(timeContract φ ψ * b) = timeContract φ ψ * 𝓣(b) := by + trans 𝓣(1 * timeContract φ ψ * b) + simp only [one_mul] + rw [timeOrder_timeContract_eq_time_mid h1 h2] + simp + +lemma timeOrder_timeContract_neq_time {φ ψ : 𝓕.States} + (h1 : ¬ (timeOrderRel φ ψ ∧ timeOrderRel ψ φ)) : + 𝓣(timeContract φ ψ) = 0 := by + by_cases h2 : timeOrderRel φ ψ + · simp_all only [true_and] + rw [timeContract_of_timeOrderRel _ _ h2] + simp only + rw [ofFieldOp_eq_sum] + simp only [map_sum] + apply Finset.sum_eq_zero + intro x hx + match φ with + | .inAsymp φ => + simp + | .position φ => + simp only [anPart_position, instCommGroup.eq_1] + apply timeOrder_superCommute_neq_time + simp_all [crAnTimeOrderRel] + | .outAsymp φ => + simp only [anPart_posAsymp, instCommGroup.eq_1] + apply timeOrder_superCommute_neq_time + simp_all [crAnTimeOrderRel] + · rw [timeContract_of_not_timeOrderRel_expand _ _ h2] + simp only [instCommGroup.eq_1, map_smul, smul_eq_zero] + right + rw [ofFieldOp_eq_sum] + simp only [map_sum] + apply Finset.sum_eq_zero + intro x hx + match ψ with + | .inAsymp ψ => + simp + | .position ψ => + simp only [anPart_position, instCommGroup.eq_1] + apply timeOrder_superCommute_neq_time + simp_all [crAnTimeOrderRel] + | .outAsymp ψ => + simp only [anPart_posAsymp, instCommGroup.eq_1] + apply timeOrder_superCommute_neq_time + simp_all [crAnTimeOrderRel] + end FieldOpAlgebra end diff --git a/HepLean/PerturbationTheory/Algebras/FieldOpAlgebra/TimeOrder.lean b/HepLean/PerturbationTheory/Algebras/FieldOpAlgebra/TimeOrder.lean index 04825929..14d7f71f 100644 --- a/HepLean/PerturbationTheory/Algebras/FieldOpAlgebra/TimeOrder.lean +++ b/HepLean/PerturbationTheory/Algebras/FieldOpAlgebra/TimeOrder.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Joseph Tooby-Smith -/ import HepLean.PerturbationTheory.Algebras.CrAnAlgebra.TimeOrder -import HepLean.PerturbationTheory.Algebras.FieldOpAlgebra.Basic +import HepLean.PerturbationTheory.Algebras.FieldOpAlgebra.SuperCommute /-! # Time Ordering on Field operator algebra @@ -429,5 +429,80 @@ lemma timeOrder_eq_maxTimeField_mul_finset (φ : 𝓕.States) (φs : List 𝓕.S rw [ofFieldOpList, timeOrder_eq_ι_timeOrderF, timeOrderF_eq_maxTimeField_mul_finset] rfl +lemma timeOrder_superCommute_eq_time_mid {φ ψ : 𝓕.CrAnStates} + (hφψ : crAnTimeOrderRel φ ψ) (hψφ : crAnTimeOrderRel ψ φ) (a b : 𝓕.FieldOpAlgebra) : + 𝓣(a * [ofCrAnFieldOp φ, ofCrAnFieldOp ψ]ₛ * b) = + [ofCrAnFieldOp φ, ofCrAnFieldOp ψ]ₛ * 𝓣(a * b) := by + rw [ofCrAnFieldOp, ofCrAnFieldOp] + rw [superCommute_eq_ι_superCommuteF] + obtain ⟨a, rfl⟩ := ι_surjective a + obtain ⟨b, rfl⟩ := ι_surjective b + rw [← map_mul, ← map_mul, timeOrder_eq_ι_timeOrderF] + rw [ι_timeOrderF_superCommuteF_eq_time] + rfl + · simp_all + · simp_all + +lemma timeOrder_superCommute_eq_time_left {φ ψ : 𝓕.CrAnStates} + (hφψ : crAnTimeOrderRel φ ψ) (hψφ : crAnTimeOrderRel ψ φ) (b : 𝓕.FieldOpAlgebra) : + 𝓣([ofCrAnFieldOp φ, ofCrAnFieldOp ψ]ₛ * b) = + [ofCrAnFieldOp φ, ofCrAnFieldOp ψ]ₛ * 𝓣(b) := by + trans 𝓣(1 * [ofCrAnFieldOp φ, ofCrAnFieldOp ψ]ₛ * b) + simp only [one_mul] + rw [timeOrder_superCommute_eq_time_mid hφψ hψφ] + simp + +lemma timeOrder_superCommute_neq_time {φ ψ : 𝓕.CrAnStates} + (hφψ : ¬ (crAnTimeOrderRel φ ψ ∧ crAnTimeOrderRel ψ φ)) : + 𝓣([ofCrAnFieldOp φ, ofCrAnFieldOp ψ]ₛ) = 0 := by + rw [ofCrAnFieldOp, ofCrAnFieldOp] + rw [superCommute_eq_ι_superCommuteF] + rw [timeOrder_eq_ι_timeOrderF] + trans ι (timeOrderF (1 * (superCommuteF (ofCrAnState φ)) (ofCrAnState ψ) * 1)) + simp only [one_mul, mul_one] + rw [ι_timeOrderF_superCommuteF_neq_time] + exact hφψ + +lemma timeOrder_superCommute_anPart_ofFieldOp_neq_time {φ ψ : 𝓕.States} + (hφψ : ¬ (timeOrderRel φ ψ ∧ timeOrderRel ψ φ)) : + 𝓣([anPart φ,ofFieldOp ψ]ₛ) = 0 := by + rw [ofFieldOp_eq_sum] + simp only [map_sum] + apply Finset.sum_eq_zero + intro a ha + match φ with + | .inAsymp φ => + simp + | .position φ => + simp only [anPart_position, instCommGroup.eq_1] + apply timeOrder_superCommute_neq_time + simp_all [crAnTimeOrderRel] + | .outAsymp φ => + simp only [anPart_posAsymp, instCommGroup.eq_1] + apply timeOrder_superCommute_neq_time + simp_all [crAnTimeOrderRel] + +lemma timeOrder_timeOrder_mid (a b c : 𝓕.FieldOpAlgebra) : + 𝓣(a * b * c) = 𝓣(a * 𝓣(b) * c) := by + obtain ⟨a, rfl⟩ := ι_surjective a + obtain ⟨b, rfl⟩ := ι_surjective b + obtain ⟨c, rfl⟩ := ι_surjective c + rw [← map_mul, ← map_mul, timeOrder_eq_ι_timeOrderF, timeOrder_eq_ι_timeOrderF, + ← map_mul, ← map_mul, timeOrder_eq_ι_timeOrderF, timeOrderF_timeOrderF_mid] + +lemma timeOrder_timeOrder_left (b c : 𝓕.FieldOpAlgebra) : + 𝓣(b * c) = 𝓣(𝓣(b) * c) := by + trans 𝓣(1 * b * c) + simp only [one_mul] + rw [timeOrder_timeOrder_mid] + simp + +lemma timeOrder_timeOrder_right (a b : 𝓕.FieldOpAlgebra) : + 𝓣(a * b) = 𝓣(a * 𝓣(b)) := by + trans 𝓣(a * b * 1) + simp only [mul_one] + rw [timeOrder_timeOrder_mid] + simp + end FieldOpAlgebra end FieldSpecification diff --git a/HepLean/PerturbationTheory/Algebras/FieldOpAlgebra/WicksTheoremNormal.lean b/HepLean/PerturbationTheory/Algebras/FieldOpAlgebra/WicksTheoremNormal.lean new file mode 100644 index 00000000..721f3e0e --- /dev/null +++ b/HepLean/PerturbationTheory/Algebras/FieldOpAlgebra/WicksTheoremNormal.lean @@ -0,0 +1,201 @@ +/- +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.TimeCond +import HepLean.PerturbationTheory.Algebras.FieldOpAlgebra.StaticWickTheorem +import HepLean.Meta.Remark.Basic +/-! + +# Wick's theorem for normal ordered lists + +-/ + +namespace FieldSpecification +variable {𝓕 : FieldSpecification} +open CrAnAlgebra +namespace FieldOpAlgebra +open WickContraction +open EqTimeOnly + +lemma timeOrder_ofFieldOpList_eqTimeOnly (φs : List 𝓕.States) : + timeOrder (ofFieldOpList φs) = ∑ (φsΛ : {φsΛ // φsΛ.EqTimeOnly (φs := φs)}), + φsΛ.1.sign • φsΛ.1.timeContract.1 * 𝓣(𝓝(ofFieldOpList [φsΛ.1]ᵘᶜ)) := by + rw [static_wick_theorem φs] + let e2 : WickContraction φs.length ≃ + {φsΛ : WickContraction φs.length // φsΛ.EqTimeOnly} ⊕ + {φsΛ : WickContraction φs.length // ¬ φsΛ.EqTimeOnly} := + (Equiv.sumCompl _).symm + rw [← e2.symm.sum_comp] + simp only [Equiv.symm_symm, Algebra.smul_mul_assoc, Fintype.sum_sum_type, + Equiv.sumCompl_apply_inl, Equiv.sumCompl_apply_inr, map_add, map_sum, map_smul, e2] + conv_lhs => + enter [2, 2, x] + rw [timeOrder_timeOrder_left] + rw [timeOrder_staticContract_of_not_mem _ x.2] + simp only [Finset.univ_eq_attach, zero_mul, map_zero, smul_zero, Finset.sum_const_zero, add_zero] + congr + funext x + rw [staticContract_eq_timeContract_of_eqTimeOnly] + rw [timeOrder_timeContract_mul_of_eqTimeOnly_left] + exact x.2 + exact x.2 + +lemma timeOrder_ofFieldOpList_eq_eqTimeOnly_empty (φs : List 𝓕.States) : + timeOrder (ofFieldOpList φs) = 𝓣(𝓝(ofFieldOpList φs)) + + ∑ (φsΛ : {φsΛ // φsΛ.EqTimeOnly (φs := φs) ∧ φsΛ ≠ empty}), + φsΛ.1.sign • φsΛ.1.timeContract.1 * 𝓣(𝓝(ofFieldOpList [φsΛ.1]ᵘᶜ)) := by + let e1 : {φsΛ : WickContraction φs.length // φsΛ.EqTimeOnly} ≃ + {φsΛ : {φsΛ : WickContraction φs.length // φsΛ.EqTimeOnly} // φsΛ.1 = empty} ⊕ + {φsΛ : {φsΛ : WickContraction φs.length // φsΛ.EqTimeOnly} // ¬ φsΛ.1 = empty} := + (Equiv.sumCompl _).symm + rw [timeOrder_ofFieldOpList_eqTimeOnly, ← e1.symm.sum_comp] + simp only [Equiv.symm_symm, Algebra.smul_mul_assoc, Fintype.sum_sum_type, + Equiv.sumCompl_apply_inl, Equiv.sumCompl_apply_inr, ne_eq, e1] + congr 1 + · let e2 : {φsΛ : {φsΛ : WickContraction φs.length // φsΛ.EqTimeOnly} // φsΛ.1 = empty } ≃ + Unit := { + toFun := fun x => (), invFun := fun x => ⟨⟨empty, by simp⟩, rfl⟩, + left_inv a := by + ext + simp [a.2], right_inv a := by simp} + rw [← e2.symm.sum_comp] + simp [e2, sign_empty] + · let e2 : { φsΛ : {φsΛ : WickContraction φs.length // φsΛ.EqTimeOnly} // ¬ φsΛ.1 = empty } ≃ + {φsΛ // φsΛ.EqTimeOnly ∧ φsΛ ≠ empty} := { + toFun := fun x => ⟨x, ⟨x.1.2, x.2⟩⟩, invFun := fun x => ⟨⟨x.1, x.2.1⟩, x.2.2⟩, + left_inv a := by rfl, right_inv a := by rfl } + rw [← e2.symm.sum_comp] + rfl + +lemma normalOrder_timeOrder_ofFieldOpList_eq_eqTimeOnly_empty (φs : List 𝓕.States) : + 𝓣(𝓝(ofFieldOpList φs)) = 𝓣(ofFieldOpList φs) - + ∑ (φsΛ : {φsΛ // φsΛ.EqTimeOnly (φs := φs) ∧ φsΛ ≠ empty}), + φsΛ.1.sign • φsΛ.1.timeContract.1 * 𝓣(𝓝(ofFieldOpList [φsΛ.1]ᵘᶜ)) := by + rw [timeOrder_ofFieldOpList_eq_eqTimeOnly_empty] + simp + +lemma normalOrder_timeOrder_ofFieldOpList_eq_haveEqTime_sum_not_haveEqTime (φs : List 𝓕.States) : + 𝓣(𝓝(ofFieldOpList φs)) = (∑ (φsΛ : {φsΛ : WickContraction φs.length // ¬ HaveEqTime φsΛ}), + φsΛ.1.sign • φsΛ.1.timeContract.1 * 𝓝(ofFieldOpList [φsΛ.1]ᵘᶜ)) + + (∑ (φsΛ : {φsΛ : WickContraction φs.length // HaveEqTime φsΛ}), + φsΛ.1.sign • φsΛ.1.timeContract.1 * 𝓝(ofFieldOpList [φsΛ.1]ᵘᶜ)) + - ∑ (φsΛ : {φsΛ // φsΛ.EqTimeOnly (φs := φs) ∧ φsΛ ≠ empty}), + φsΛ.1.sign • φsΛ.1.timeContract.1 * 𝓣(𝓝(ofFieldOpList [φsΛ.1]ᵘᶜ)) := by + rw [normalOrder_timeOrder_ofFieldOpList_eq_eqTimeOnly_empty] + rw [wicks_theorem] + let e1 : WickContraction φs.length ≃ {φsΛ // HaveEqTime φsΛ} ⊕ {φsΛ // ¬ HaveEqTime φsΛ} := by + exact (Equiv.sumCompl HaveEqTime).symm + rw [← e1.symm.sum_comp] + simp only [Equiv.symm_symm, Algebra.smul_mul_assoc, Fintype.sum_sum_type, + Equiv.sumCompl_apply_inl, Equiv.sumCompl_apply_inr, ne_eq, sub_left_inj, e1] + rw [add_comm] + +lemma haveEqTime_wick_sum_eq_split (φs : List 𝓕.States) : + (∑ (φsΛ : {φsΛ : WickContraction φs.length // HaveEqTime φsΛ}), + φsΛ.1.sign • φsΛ.1.timeContract.1 * 𝓝(ofFieldOpList [φsΛ.1]ᵘᶜ)) = + ∑ (φsΛ : {φsΛ // φsΛ.EqTimeOnly (φs := φs) ∧ φsΛ ≠ empty}), + (sign φs ↑φsΛ • (φsΛ.1).timeContract * + ∑ φssucΛ : { φssucΛ : WickContraction [φsΛ.1]ᵘᶜ.length // ¬φssucΛ.HaveEqTime }, + sign [φsΛ.1]ᵘᶜ φssucΛ • + (φssucΛ.1).timeContract * normalOrder (ofFieldOpList [φssucΛ.1]ᵘᶜ)) := by + let f : WickContraction φs.length → 𝓕.FieldOpAlgebra := fun φsΛ => + φsΛ.sign • φsΛ.timeContract.1 * 𝓝(ofFieldOpList [φsΛ]ᵘᶜ) + change ∑ (φsΛ : {φsΛ : WickContraction φs.length // HaveEqTime φsΛ}), f φsΛ.1 = _ + rw [sum_haveEqTime] + congr + funext φsΛ + simp only [f] + conv_lhs => + enter [2, φsucΛ] + enter [1] + rw [join_sign_timeContract φsΛ.1 φsucΛ.1] + conv_lhs => + enter [2, φsucΛ] + rw [mul_assoc] + rw [← Finset.mul_sum] + congr + funext φsΛ' + simp only [ne_eq, Algebra.smul_mul_assoc] + congr 1 + rw [@join_uncontractedListGet] + +lemma normalOrder_timeOrder_ofFieldOpList_eq_not_haveEqTime_sub_inductive (φs : List 𝓕.States) : + 𝓣(𝓝(ofFieldOpList φs)) = (∑ (φsΛ : {φsΛ : WickContraction φs.length // ¬ HaveEqTime φsΛ}), + φsΛ.1.sign • φsΛ.1.timeContract.1 * 𝓝(ofFieldOpList [φsΛ.1]ᵘᶜ)) + + ∑ (φsΛ : {φsΛ // φsΛ.EqTimeOnly (φs := φs) ∧ φsΛ ≠ empty}), + sign φs ↑φsΛ • (φsΛ.1).timeContract * + (∑ φssucΛ : { φssucΛ : WickContraction [φsΛ.1]ᵘᶜ.length // ¬ φssucΛ.HaveEqTime }, + sign [φsΛ.1]ᵘᶜ φssucΛ • (φssucΛ.1).timeContract * normalOrder (ofFieldOpList [φssucΛ.1]ᵘᶜ) - + 𝓣(𝓝(ofFieldOpList [φsΛ.1]ᵘᶜ))) := by + rw [normalOrder_timeOrder_ofFieldOpList_eq_haveEqTime_sum_not_haveEqTime] + rw [add_sub_assoc] + congr 1 + rw [haveEqTime_wick_sum_eq_split] + simp only [ne_eq, Algebra.smul_mul_assoc] + rw [← Finset.sum_sub_distrib] + congr 1 + funext x + simp only + rw [← smul_sub, ← mul_sub] + +lemma wicks_theorem_normal_order_empty : 𝓣(𝓝(ofFieldOpList [])) = + ∑ (φsΛ : {φsΛ : WickContraction ([] : List 𝓕.States).length // ¬ HaveEqTime φsΛ}), + φsΛ.1.sign • φsΛ.1.timeContract.1 * 𝓝(ofFieldOpList [φsΛ.1]ᵘᶜ) := by + let e2 : {φsΛ : WickContraction ([] : List 𝓕.States).length // ¬ HaveEqTime φsΛ} ≃ Unit := + { + toFun := fun x => (), + invFun := fun x => ⟨empty, by simp⟩, + left_inv := by + intro a + simp only [List.length_nil] + apply Subtype.eq + apply Subtype.eq + simp only [empty] + ext i + simp only [Finset.not_mem_empty, false_iff] + by_contra hn + have h2 := a.1.2.1 i hn + rw [@Finset.card_eq_two] at h2 + obtain ⟨a, b, ha, hb, hab⟩ := h2 + exact Fin.elim0 a, + right_inv := by intro a; simp} + rw [← e2.symm.sum_comp] + simp only [Finset.univ_unique, PUnit.default_eq_unit, List.length_nil, Equiv.coe_fn_symm_mk, + sign_empty, timeContract_empty, OneMemClass.coe_one, one_smul, uncontractedListGet_empty, + one_mul, Finset.sum_const, Finset.card_singleton, e2] + have h1' : ofFieldOpList (𝓕 := 𝓕) [] = ofCrAnFieldOpList [] := by rfl + rw [h1'] + rw [normalOrder_ofCrAnFieldOpList] + simp only [normalOrderSign_nil, normalOrderList_nil, one_smul] + rw [ofCrAnFieldOpList, timeOrder_eq_ι_timeOrderF] + rw [timeOrderF_ofCrAnList] + simp + +theorem wicks_theorem_normal_order : (φs : List 𝓕.States) → + 𝓣(𝓝(ofFieldOpList φs)) = ∑ (φsΛ : {φsΛ : WickContraction φs.length // ¬ HaveEqTime φsΛ}), + φsΛ.1.sign • φsΛ.1.timeContract.1 * 𝓝(ofFieldOpList [φsΛ.1]ᵘᶜ) + | [] => wicks_theorem_normal_order_empty + | φ :: φs => by + rw [normalOrder_timeOrder_ofFieldOpList_eq_not_haveEqTime_sub_inductive] + simp only [Algebra.smul_mul_assoc, ne_eq, add_right_eq_self] + apply Finset.sum_eq_zero + intro φsΛ hφsΛ + simp only [smul_eq_zero] + right + have ih := wicks_theorem_normal_order [φsΛ.1]ᵘᶜ + rw [ih] + simp +termination_by φs => φs.length +decreasing_by + simp only [uncontractedListGet, List.length_cons, List.length_map, gt_iff_lt] + rw [uncontractedList_length_eq_card] + have hc := uncontracted_card_eq_iff φsΛ.1 + simp only [List.length_cons, φsΛ.2.2, iff_false] at hc + have hc' := uncontracted_card_le φsΛ.1 + simp_all only [Algebra.smul_mul_assoc, List.length_cons, Finset.mem_univ, gt_iff_lt] + omega + +end FieldOpAlgebra +end FieldSpecification diff --git a/HepLean/PerturbationTheory/FieldStatistics/OfFinset.lean b/HepLean/PerturbationTheory/FieldStatistics/OfFinset.lean index 4bbac9c5..30141262 100644 --- a/HepLean/PerturbationTheory/FieldStatistics/OfFinset.lean +++ b/HepLean/PerturbationTheory/FieldStatistics/OfFinset.lean @@ -106,4 +106,24 @@ lemma ofFinset_union_disjoint (q : 𝓕 → FieldStatistic) (φs : List 𝓕) (a rw [ofFinset_union, Finset.disjoint_iff_inter_eq_empty.mp h] simp +lemma ofFinset_filter_mul_neg (q : 𝓕 → FieldStatistic) (φs : List 𝓕) (a : Finset (Fin φs.length)) + (p : Fin φs.length → Prop) [DecidablePred p] : + ofFinset q φs.get (Finset.filter p a) * + ofFinset q φs.get (Finset.filter (fun i => ¬ p i) a) = ofFinset q φs.get a := by + rw [ofFinset_union_disjoint] + congr + exact Finset.filter_union_filter_neg_eq p a + exact Finset.disjoint_filter_filter_neg a a p + +lemma ofFinset_filter (q : 𝓕 → FieldStatistic) (φs : List 𝓕) (a : Finset (Fin φs.length)) + (p : Fin φs.length → Prop) [DecidablePred p] : + ofFinset q φs.get (Finset.filter p a) = ofFinset q φs.get (Finset.filter (fun i => ¬ p i) a) * + ofFinset q φs.get a := by + rw [← ofFinset_filter_mul_neg q φs a p] + conv_rhs => + rhs + rw [mul_comm] + rw [← mul_assoc] + simp + end FieldStatistic diff --git a/HepLean/PerturbationTheory/WickContraction/Basic.lean b/HepLean/PerturbationTheory/WickContraction/Basic.lean index 5859c464..c18c1937 100644 --- a/HepLean/PerturbationTheory/WickContraction/Basic.lean +++ b/HepLean/PerturbationTheory/WickContraction/Basic.lean @@ -38,9 +38,32 @@ namespace WickContraction variable {n : ℕ} (c : WickContraction n) open HepLean.List +/-- Wick contractions are decidable. -/ +instance : DecidableEq (WickContraction n) := Subtype.instDecidableEq + /-- The contraction consisting of no contracted pairs. -/ def empty : WickContraction n := ⟨∅, by simp, by simp⟩ +lemma card_zero_iff_empty (c : WickContraction n) : c.1.card = 0 ↔ c = empty := by + rw [Subtype.eq_iff] + simp [empty] + +lemma exists_pair_of_not_eq_empty (c : WickContraction n) (h : c ≠ empty) : + ∃ i j, {i, j} ∈ c.1 := by + by_contra hn + simp only [not_exists] at hn + have hc : c.1 = ∅ := by + ext a + simp only [Finset.not_mem_empty, iff_false] + by_contra hn' + have hc := c.2.1 a hn' + rw [@Finset.card_eq_two] at hc + obtain ⟨x, y, hx, rfl⟩ := hc + exact hn x y hn' + apply h + apply Subtype.eq + simp [empty, hc] + /-- The equivalence between `WickContraction n` and `WickContraction m` derived from a propositional equality of `n` and `m`. -/ def congr : {n m : ℕ} → (h : n = m) → WickContraction n ≃ WickContraction m @@ -48,9 +71,14 @@ def congr : {n m : ℕ} → (h : n = m) → WickContraction n ≃ WickContractio @[simp] lemma congr_refl : c.congr rfl = c := by - cases c rfl +@[simp] +lemma card_congr {n m : ℕ} (h : n = m) (c : WickContraction n) : + (congr h c).1.card = c.1.card := by + subst h + simp + lemma congr_contractions {n m : ℕ} (h : n = m) (c : WickContraction n) : ((congr h) c).1 = Finset.map (Finset.mapEmbedding (finCongr h)).toEmbedding c.1 := by subst h @@ -83,6 +111,11 @@ lemma congr_trans_apply {n m o : ℕ} (h1 : n = m) (h2 : m = o) (c : WickContrac subst h1 h2 simp +lemma mem_congr_iff {n m : ℕ} (h : n = m) {c : WickContraction n } {a : Finset (Fin m)} : + a ∈ (congr h c).1 ↔ Finset.map (finCongr h.symm).toEmbedding a ∈ c.1 := by + subst h + simp + /-- Given a contracted pair in `c : WickContraction n` the contracted pair in `congr h c`. -/ def congrLift {n m : ℕ} (h : n = m) {c : WickContraction n} (a : c.1) : (congr h c).1 := @@ -112,6 +145,18 @@ lemma congrLift_bijective {n m : ℕ} {c : WickContraction n} (h : n = m) : Function.Bijective (c.congrLift h) := by exact ⟨c.congrLift_injective h, c.congrLift_surjective h⟩ +/-- Given a contracted pair in `c : WickContraction n` the contracted pair + in `congr h c`. -/ +def congrLiftInv {n m : ℕ} (h : n = m) {c : WickContraction n} (a : (congr h c).1) : c.1 := + ⟨a.1.map (finCongr h.symm).toEmbedding, by + subst h + simp⟩ + +lemma congrLiftInv_rfl {n : ℕ} {c : WickContraction n} : + c.congrLiftInv rfl = id := by + funext a + simp [congrLiftInv] + lemma eq_filter_mem_self : c.1 = Finset.filter (fun x => x ∈ c.1) Finset.univ := by exact Eq.symm (Finset.filter_univ_mem c.1) @@ -481,6 +526,12 @@ lemma prod_finset_eq_mul_fst_snd (c : WickContraction n) (a : c.1) def GradingCompliant (φs : List 𝓕.States) (φsΛ : WickContraction φs.length) := ∀ (a : φsΛ.1), (𝓕 |>ₛ φs[φsΛ.fstFieldOfContract a]) = (𝓕 |>ₛ φs[φsΛ.sndFieldOfContract a]) +lemma gradingCompliant_congr {φs φs' : List 𝓕.States} (h : φs = φs') + (φsΛ : WickContraction φs.length) : + GradingCompliant φs φsΛ ↔ GradingCompliant φs' (congr (by simp [h]) φsΛ) := by + subst h + rfl + /-- An equivalence from the sigma type `(a : c.1) × a` to the subtype of `Fin n` consisting of those positions which are contracted. -/ def sigmaContractedEquiv : (a : c.1) × a ≃ {x : Fin n // (c.getDual? x).isSome} where diff --git a/HepLean/PerturbationTheory/WickContraction/Join.lean b/HepLean/PerturbationTheory/WickContraction/Join.lean new file mode 100644 index 00000000..28321db7 --- /dev/null +++ b/HepLean/PerturbationTheory/WickContraction/Join.lean @@ -0,0 +1,1081 @@ +/- +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.TimeContract +import HepLean.PerturbationTheory.WickContraction.StaticContract +import HepLean.PerturbationTheory.Algebras.FieldOpAlgebra.TimeContraction +import HepLean.PerturbationTheory.WickContraction.SubContraction +import HepLean.PerturbationTheory.WickContraction.Singleton + +/-! + +# Join of contractions + +-/ + +open FieldSpecification +variable {𝓕 : FieldSpecification} + +namespace WickContraction +variable {n : ℕ} (c : WickContraction n) +open HepLean.List +open FieldOpAlgebra + +/-- Given a Wick contraction `φsΛ` on `φs` and a Wick contraction `φsucΛ` on the uncontracted fields +within `φsΛ`, a Wick contraction on `φs`consisting of the contractins in `φsΛ` and +the contractions in `φsucΛ`. -/ +def join {φs : List 𝓕.States} (φsΛ : WickContraction φs.length) + (φsucΛ : WickContraction [φsΛ]ᵘᶜ.length) : WickContraction φs.length := + ⟨φsΛ.1 ∪ φsucΛ.1.map (Finset.mapEmbedding uncontractedListEmd).toEmbedding, by + intro a ha + simp only [Finset.le_eq_subset, Finset.mem_union, Finset.mem_map, + RelEmbedding.coe_toEmbedding] at ha + rcases ha with ha | ha + · exact φsΛ.2.1 a ha + · obtain ⟨a, ha, rfl⟩ := ha + rw [Finset.mapEmbedding_apply] + simp only [Finset.card_map] + exact φsucΛ.2.1 a ha, by + intro a ha b hb + simp only [Finset.le_eq_subset, Finset.mem_union, Finset.mem_map, + RelEmbedding.coe_toEmbedding] at ha hb + rcases ha with ha | ha <;> rcases hb with hb | hb + · exact φsΛ.2.2 a ha b hb + · obtain ⟨b, hb, rfl⟩ := hb + right + symm + rw [Finset.mapEmbedding_apply] + apply uncontractedListEmd_finset_disjoint_left + exact ha + · obtain ⟨a, ha, rfl⟩ := ha + right + rw [Finset.mapEmbedding_apply] + apply uncontractedListEmd_finset_disjoint_left + exact hb + · obtain ⟨a, ha, rfl⟩ := ha + obtain ⟨b, hb, rfl⟩ := hb + simp only [EmbeddingLike.apply_eq_iff_eq] + rw [Finset.mapEmbedding_apply, Finset.mapEmbedding_apply] + rw [Finset.disjoint_map] + exact φsucΛ.2.2 a ha b hb⟩ + +lemma join_congr {φs : List 𝓕.States} {φsΛ : WickContraction φs.length} + {φsucΛ : WickContraction [φsΛ]ᵘᶜ.length} {φsΛ' : WickContraction φs.length} + (h1 : φsΛ = φsΛ') : + join φsΛ φsucΛ = join φsΛ' (congr (by simp [h1]) φsucΛ) := by + subst h1 + rfl + +/-- Given a contracting pair within `φsΛ` the corresponding contracting pair within + `(join φsΛ φsucΛ)`. -/ +def joinLiftLeft {φs : List 𝓕.States} {φsΛ : WickContraction φs.length} + {φsucΛ : WickContraction [φsΛ]ᵘᶜ.length} : φsΛ.1 → (join φsΛ φsucΛ).1 := + fun a => ⟨a, by simp [join]⟩ + +lemma jointLiftLeft_injective {φs : List 𝓕.States} {φsΛ : WickContraction φs.length} + {φsucΛ : WickContraction [φsΛ]ᵘᶜ.length} : + Function.Injective (@joinLiftLeft _ _ φsΛ φsucΛ) := by + intro a b h + simp only [joinLiftLeft] at h + rw [Subtype.mk_eq_mk] at h + refine Subtype.eq h + +/-- Given a contracting pair within `φsucΛ` the corresponding contracting pair within + `(join φsΛ φsucΛ)`. -/ +def joinLiftRight {φs : List 𝓕.States} {φsΛ : WickContraction φs.length} + {φsucΛ : WickContraction [φsΛ]ᵘᶜ.length} : φsucΛ.1 → (join φsΛ φsucΛ).1 := + fun a => ⟨a.1.map uncontractedListEmd, by + simp only [join, Finset.le_eq_subset, Finset.mem_union, Finset.mem_map, + RelEmbedding.coe_toEmbedding] + right + use a.1 + simp only [Finset.coe_mem, true_and] + rfl⟩ + +lemma joinLiftRight_injective {φs : List 𝓕.States} {φsΛ : WickContraction φs.length} + {φsucΛ : WickContraction [φsΛ]ᵘᶜ.length} : + Function.Injective (@joinLiftRight _ _ φsΛ φsucΛ) := by + intro a b h + simp only [joinLiftRight] at h + rw [Subtype.mk_eq_mk] at h + simp only [Finset.map_inj] at h + refine Subtype.eq h + +lemma jointLiftLeft_disjoint_joinLiftRight {φs : List 𝓕.States} {φsΛ : WickContraction φs.length} + {φsucΛ : WickContraction [φsΛ]ᵘᶜ.length} (a : φsΛ.1) (b : φsucΛ.1) : + Disjoint (@joinLiftLeft _ _ _ φsucΛ a).1 (joinLiftRight b).1 := by + simp only [joinLiftLeft, joinLiftRight] + symm + apply uncontractedListEmd_finset_disjoint_left + exact a.2 + +lemma jointLiftLeft_neq_joinLiftRight {φs : List 𝓕.States} {φsΛ : WickContraction φs.length} + {φsucΛ : WickContraction [φsΛ]ᵘᶜ.length} (a : φsΛ.1) (b : φsucΛ.1) : + joinLiftLeft a ≠ joinLiftRight b := by + by_contra hn + have h1 := jointLiftLeft_disjoint_joinLiftRight a b + rw [hn] at h1 + simp only [disjoint_self, Finset.bot_eq_empty] at h1 + have hj := (join φsΛ φsucΛ).2.1 (joinLiftRight b).1 (joinLiftRight b).2 + rw [h1] at hj + simp at hj + +/-- The map from contracted pairs of `φsΛ` and `φsucΛ` to contracted pairs in + `(join φsΛ φsucΛ)`. -/ +def joinLift {φs : List 𝓕.States} {φsΛ : WickContraction φs.length} + {φsucΛ : WickContraction [φsΛ]ᵘᶜ.length} : φsΛ.1 ⊕ φsucΛ.1 → (join φsΛ φsucΛ).1 := fun a => + match a with + | Sum.inl a => joinLiftLeft a + | Sum.inr a => joinLiftRight a + +lemma joinLift_injective {φs : List 𝓕.States} {φsΛ : WickContraction φs.length} + {φsucΛ : WickContraction [φsΛ]ᵘᶜ.length} : Function.Injective (@joinLift _ _ φsΛ φsucΛ) := by + intro a b h + match a, b with + | Sum.inl a, Sum.inl b => + simp only [Sum.inl.injEq] + exact jointLiftLeft_injective h + | Sum.inr a, Sum.inr b => + simp only [Sum.inr.injEq] + exact joinLiftRight_injective h + | Sum.inl a, Sum.inr b => + simp only [joinLift] at h + have h1 := jointLiftLeft_neq_joinLiftRight a b + simp_all + | Sum.inr a, Sum.inl b => + simp only [joinLift] at h + have h1 := jointLiftLeft_neq_joinLiftRight b a + simp_all + +lemma joinLift_surjective {φs : List 𝓕.States} {φsΛ : WickContraction φs.length} + {φsucΛ : WickContraction [φsΛ]ᵘᶜ.length} : Function.Surjective (@joinLift _ _ φsΛ φsucΛ) := by + intro a + have ha2 := a.2 + simp only [join, Finset.le_eq_subset, Finset.mem_union, Finset.mem_map, + RelEmbedding.coe_toEmbedding] at ha2 + rcases ha2 with ha2 | ⟨a2, ha3⟩ + · use Sum.inl ⟨a, ha2⟩ + simp [joinLift, joinLiftLeft] + · rw [Finset.mapEmbedding_apply] at ha3 + use Sum.inr ⟨a2, ha3.1⟩ + simp only [joinLift, joinLiftRight] + refine Subtype.eq ?_ + exact ha3.2 + +lemma joinLift_bijective {φs : List 𝓕.States} {φsΛ : WickContraction φs.length} + {φsucΛ : WickContraction [φsΛ]ᵘᶜ.length} : Function.Bijective (@joinLift _ _ φsΛ φsucΛ) := by + apply And.intro + · exact joinLift_injective + · exact joinLift_surjective + +lemma prod_join {φs : List 𝓕.States} (φsΛ : WickContraction φs.length) + (φsucΛ : WickContraction [φsΛ]ᵘᶜ.length) (f : (join φsΛ φsucΛ).1 → M) [CommMonoid M]: + ∏ (a : (join φsΛ φsucΛ).1), f a = (∏ (a : φsΛ.1), f (joinLiftLeft a)) * + ∏ (a : φsucΛ.1), f (joinLiftRight a) := by + let e1 := Equiv.ofBijective (@joinLift _ _ φsΛ φsucΛ) joinLift_bijective + rw [← e1.prod_comp] + simp only [Fintype.prod_sum_type, Finset.univ_eq_attach] + rfl + +lemma joinLiftLeft_or_joinLiftRight_of_mem_join {φs : List 𝓕.States} + (φsΛ : WickContraction φs.length) + (φsucΛ : WickContraction [φsΛ]ᵘᶜ.length) {a : Finset (Fin φs.length)} + (ha : a ∈ (join φsΛ φsucΛ).1) : + (∃ b, a = (joinLiftLeft (φsucΛ := φsucΛ) b).1) ∨ + (∃ b, a = (joinLiftRight (φsucΛ := φsucΛ) b).1) := by + simp only [join, Finset.le_eq_subset, Finset.mem_union, Finset.mem_map, + RelEmbedding.coe_toEmbedding] at ha + rcases ha with ha | ⟨a, ha, rfl⟩ + · left + use ⟨a, ha⟩ + rfl + · right + use ⟨a, ha⟩ + rfl + +@[simp] +lemma join_fstFieldOfContract_joinLiftRight {φs : List 𝓕.States} (φsΛ : WickContraction φs.length) + (φsucΛ : WickContraction [φsΛ]ᵘᶜ.length) (a : φsucΛ.1) : + (join φsΛ φsucΛ).fstFieldOfContract (joinLiftRight a) = + uncontractedListEmd (φsucΛ.fstFieldOfContract a) := by + apply eq_fstFieldOfContract_of_mem _ _ _ (uncontractedListEmd (φsucΛ.sndFieldOfContract a)) + · simp [joinLiftRight] + · simp [joinLiftRight] + · apply uncontractedListEmd_strictMono + exact fstFieldOfContract_lt_sndFieldOfContract φsucΛ a + +@[simp] +lemma join_sndFieldOfContract_joinLiftRight {φs : List 𝓕.States} (φsΛ : WickContraction φs.length) + (φsucΛ : WickContraction [φsΛ]ᵘᶜ.length) (a : φsucΛ.1) : + (join φsΛ φsucΛ).sndFieldOfContract (joinLiftRight a) = + uncontractedListEmd (φsucΛ.sndFieldOfContract a) := by + apply eq_sndFieldOfContract_of_mem _ _ (uncontractedListEmd (φsucΛ.fstFieldOfContract a)) + · simp [joinLiftRight] + · simp [joinLiftRight] + · apply uncontractedListEmd_strictMono + exact fstFieldOfContract_lt_sndFieldOfContract φsucΛ a + +@[simp] +lemma join_fstFieldOfContract_joinLiftLeft {φs : List 𝓕.States} (φsΛ : WickContraction φs.length) + (φsucΛ : WickContraction [φsΛ]ᵘᶜ.length) (a : φsΛ.1) : + (join φsΛ φsucΛ).fstFieldOfContract (joinLiftLeft a) = + (φsΛ.fstFieldOfContract a) := by + apply eq_fstFieldOfContract_of_mem _ _ _ (φsΛ.sndFieldOfContract a) + · simp [joinLiftLeft] + · simp [joinLiftLeft] + · exact fstFieldOfContract_lt_sndFieldOfContract φsΛ a + +@[simp] +lemma join_sndFieldOfContract_joinLift {φs : List 𝓕.States} (φsΛ : WickContraction φs.length) + (φsucΛ : WickContraction [φsΛ]ᵘᶜ.length) (a : φsΛ.1) : + (join φsΛ φsucΛ).sndFieldOfContract (joinLiftLeft a) = + (φsΛ.sndFieldOfContract a) := by + apply eq_sndFieldOfContract_of_mem _ _ (φsΛ.fstFieldOfContract a) (φsΛ.sndFieldOfContract a) + · simp [joinLiftLeft] + · simp [joinLiftLeft] + · exact fstFieldOfContract_lt_sndFieldOfContract φsΛ a + +lemma mem_join_right_iff {φs : List 𝓕.States} (φsΛ : WickContraction φs.length) + (φsucΛ : WickContraction [φsΛ]ᵘᶜ.length) (a : Finset (Fin [φsΛ]ᵘᶜ.length)) : + a ∈ φsucΛ.1 ↔ a.map uncontractedListEmd ∈ (join φsΛ φsucΛ).1 := by + simp only [join, Finset.le_eq_subset, Finset.mem_union, Finset.mem_map, + RelEmbedding.coe_toEmbedding] + have h1' : ¬ Finset.map uncontractedListEmd a ∈ φsΛ.1 := + uncontractedListEmd_finset_not_mem a + simp only [h1', false_or] + apply Iff.intro + · intro h + use a + simp only [h, true_and] + rw [Finset.mapEmbedding_apply] + · intro h + obtain ⟨a, ha, h2⟩ := h + rw [Finset.mapEmbedding_apply] at h2 + simp only [Finset.map_inj] at h2 + subst h2 + exact ha + +lemma join_card {φs : List 𝓕.States} {φsΛ : WickContraction φs.length} + {φsucΛ : WickContraction [φsΛ]ᵘᶜ.length} : + (join φsΛ φsucΛ).1.card = φsΛ.1.card + φsucΛ.1.card := by + simp only [join, Finset.le_eq_subset] + rw [Finset.card_union_of_disjoint] + simp only [Finset.card_map] + rw [@Finset.disjoint_left] + intro a ha + simp only [Finset.mem_map, RelEmbedding.coe_toEmbedding, not_exists, not_and] + intro x hx + by_contra hn + have hdis : Disjoint (Finset.map uncontractedListEmd x) a := by + exact uncontractedListEmd_finset_disjoint_left x a ha + rw [Finset.mapEmbedding_apply] at hn + rw [hn] at hdis + simp only [disjoint_self, Finset.bot_eq_empty] at hdis + have hcard := φsΛ.2.1 a ha + simp_all + +@[simp] +lemma empty_join {φs : List 𝓕.States} (φsΛ : WickContraction [empty (n := φs.length)]ᵘᶜ.length) : + join empty φsΛ = congr (by simp) φsΛ := by + apply Subtype.ext + simp only [join, Finset.le_eq_subset, uncontractedListEmd_empty] + ext a + conv_lhs => + left + left + rw [empty] + simp only [Finset.empty_union, Finset.mem_map, RelEmbedding.coe_toEmbedding] + rw [mem_congr_iff] + apply Iff.intro + · intro h + obtain ⟨a, ha, rfl⟩ := h + rw [Finset.mapEmbedding_apply] + rw [Finset.map_map] + apply Set.mem_of_eq_of_mem _ ha + trans Finset.map (Equiv.refl _).toEmbedding a + rfl + simp + · intro h + use Finset.map (finCongr (by simp)).toEmbedding a + simp only [h, true_and] + trans Finset.map (Equiv.refl _).toEmbedding a + rw [Finset.mapEmbedding_apply, Finset.map_map] + rfl + simp + +@[simp] +lemma join_empty {φs : List 𝓕.States} (φsΛ : WickContraction φs.length) : + join φsΛ empty = φsΛ := by + apply Subtype.ext + ext a + simp [join, empty] + +lemma join_timeContract {φs : List 𝓕.States} (φsΛ : WickContraction φs.length) + (φsucΛ : WickContraction [φsΛ]ᵘᶜ.length) : + (join φsΛ φsucΛ).timeContract = φsΛ.timeContract * φsucΛ.timeContract := by + simp only [timeContract, List.get_eq_getElem] + rw [prod_join] + congr 1 + congr + funext a + simp + +lemma join_staticContract {φs : List 𝓕.States} (φsΛ : WickContraction φs.length) + (φsucΛ : WickContraction [φsΛ]ᵘᶜ.length) : + (join φsΛ φsucΛ).staticContract = φsΛ.staticContract * φsucΛ.staticContract := by + simp only [staticContract, List.get_eq_getElem] + rw [prod_join] + congr 1 + congr + funext a + simp + +lemma mem_join_uncontracted_of_mem_right_uncontracted {φs : List 𝓕.States} + (φsΛ : WickContraction φs.length) + (φsucΛ : WickContraction [φsΛ]ᵘᶜ.length) (i : Fin [φsΛ]ᵘᶜ.length) + (ha : i ∈ φsucΛ.uncontracted) : + uncontractedListEmd i ∈ (join φsΛ φsucΛ).uncontracted := by + rw [mem_uncontracted_iff_not_contracted] + intro p hp + simp only [join, Finset.le_eq_subset, Finset.mem_union, Finset.mem_map, + RelEmbedding.coe_toEmbedding] at hp + rcases hp with hp | hp + · have hi : uncontractedListEmd i ∈ φsΛ.uncontracted := by + exact uncontractedListEmd_mem_uncontracted i + rw [mem_uncontracted_iff_not_contracted] at hi + exact hi p hp + · obtain ⟨p, hp, rfl⟩ := hp + rw [Finset.mapEmbedding_apply] + simp only [Finset.mem_map'] + rw [mem_uncontracted_iff_not_contracted] at ha + exact ha p hp + +lemma exists_mem_left_uncontracted_of_mem_join_uncontracted {φs : List 𝓕.States} + (φsΛ : WickContraction φs.length) + (φsucΛ : WickContraction [φsΛ]ᵘᶜ.length) (i : Fin φs.length) + (ha : i ∈ (join φsΛ φsucΛ).uncontracted) : + i ∈ φsΛ.uncontracted := by + rw [@mem_uncontracted_iff_not_contracted] + rw [@mem_uncontracted_iff_not_contracted] at ha + simp only [join, Finset.le_eq_subset, Finset.mem_union, Finset.mem_map, + RelEmbedding.coe_toEmbedding] at ha + intro p hp + simp_all + +lemma exists_mem_right_uncontracted_of_mem_join_uncontracted {φs : List 𝓕.States} + (φsΛ : WickContraction φs.length) + (φsucΛ : WickContraction [φsΛ]ᵘᶜ.length) (i : Fin φs.length) + (hi : i ∈ (join φsΛ φsucΛ).uncontracted) : + ∃ a, uncontractedListEmd a = i ∧ a ∈ φsucΛ.uncontracted := by + have hi' := exists_mem_left_uncontracted_of_mem_join_uncontracted _ _ i hi + obtain ⟨j, rfl⟩ := uncontractedListEmd_surjective_mem_uncontracted i hi' + use j + simp only [true_and] + rw [mem_uncontracted_iff_not_contracted] at hi + rw [mem_uncontracted_iff_not_contracted] + intro p hp + have hip := hi (p.map uncontractedListEmd) (by + simp only [join, Finset.le_eq_subset, Finset.mem_union, Finset.mem_map, + RelEmbedding.coe_toEmbedding] + right + use p + simp only [hp, true_and] + rw [Finset.mapEmbedding_apply]) + simpa using hip + +lemma join_uncontractedList {φs : List 𝓕.States} (φsΛ : WickContraction φs.length) + (φsucΛ : WickContraction [φsΛ]ᵘᶜ.length) : + (join φsΛ φsucΛ).uncontractedList = List.map uncontractedListEmd φsucΛ.uncontractedList := by + rw [uncontractedList_eq_sort] + rw [uncontractedList_eq_sort] + rw [fin_finset_sort_map_monotone] + congr + ext a + simp only [Finset.mem_map] + apply Iff.intro + · intro h + obtain ⟨a, rfl, ha⟩ := exists_mem_right_uncontracted_of_mem_join_uncontracted _ _ a h + use a, ha + · intro h + obtain ⟨a, ha, rfl⟩ := h + exact mem_join_uncontracted_of_mem_right_uncontracted φsΛ φsucΛ a ha + · intro a b h + exact uncontractedListEmd_strictMono h + +lemma join_uncontractedList_get {φs : List 𝓕.States} (φsΛ : WickContraction φs.length) + (φsucΛ : WickContraction [φsΛ]ᵘᶜ.length) : + ((join φsΛ φsucΛ).uncontractedList).get = + φsΛ.uncontractedListEmd ∘ (φsucΛ.uncontractedList).get ∘ + (Fin.cast (by rw [join_uncontractedList]; simp)) := by + have h1 {n : ℕ} (l1 l2 : List (Fin n)) (h : l1 = l2) : + l1.get = l2.get ∘ Fin.cast (by rw [h]) := by + subst h + rfl + conv_lhs => rw [h1 _ _ (join_uncontractedList φsΛ φsucΛ)] + ext i + simp + +lemma join_uncontractedListGet {φs : List 𝓕.States} (φsΛ : WickContraction φs.length) + (φsucΛ : WickContraction [φsΛ]ᵘᶜ.length) : + (join φsΛ φsucΛ).uncontractedListGet = φsucΛ.uncontractedListGet := by + simp only [uncontractedListGet, join_uncontractedList, List.map_map, List.map_inj_left, + Function.comp_apply, List.get_eq_getElem, List.getElem_map] + intro a ha + simp only [uncontractedListEmd, uncontractedIndexEquiv, List.get_eq_getElem, + Equiv.trans_toEmbedding, Function.Embedding.trans_apply, Equiv.coe_toEmbedding, Equiv.coe_fn_mk, + Function.Embedding.coe_subtype] + rfl + +lemma join_uncontractedListEmb {φs : List 𝓕.States} (φsΛ : WickContraction φs.length) + (φsucΛ : WickContraction [φsΛ]ᵘᶜ.length) : + (join φsΛ φsucΛ).uncontractedListEmd = + ((finCongr (congrArg List.length (join_uncontractedListGet _ _))).toEmbedding.trans + φsucΛ.uncontractedListEmd).trans φsΛ.uncontractedListEmd := by + refine Function.Embedding.ext_iff.mpr (congrFun ?_) + change uncontractedListEmd.toFun = _ + rw [uncontractedListEmd_toFun_eq_get] + rw [join_uncontractedList_get] + rfl + +lemma join_assoc {φs : List 𝓕.States} (φsΛ : WickContraction φs.length) + (φsucΛ : WickContraction [φsΛ]ᵘᶜ.length) (φsucΛ' : WickContraction [φsΛ.join φsucΛ]ᵘᶜ.length) : + join (join φsΛ φsucΛ) (φsucΛ') = join φsΛ (join φsucΛ (congr + (congrArg List.length (join_uncontractedListGet _ _)) φsucΛ')) := by + apply Subtype.ext + ext a + by_cases ha : a ∈ φsΛ.1 + · simp [ha, join] + simp only [join, Finset.le_eq_subset, Finset.union_assoc, Finset.mem_union, ha, Finset.mem_map, + RelEmbedding.coe_toEmbedding, false_or] + apply Iff.intro + · intro h + rcases h with h | h + · obtain ⟨a, ha', rfl⟩ := h + use a + simp [ha'] + · obtain ⟨a, ha', rfl⟩ := h + let a' := congrLift (congrArg List.length (join_uncontractedListGet _ _)) ⟨a, ha'⟩ + let a'' := joinLiftRight a' + use a'' + apply And.intro + · right + use a' + apply And.intro + · exact a'.2 + · simp only [joinLiftRight, a''] + rfl + · simp only [a''] + rw [Finset.mapEmbedding_apply, Finset.mapEmbedding_apply] + simp only [a', joinLiftRight, congrLift] + rw [join_uncontractedListEmb] + simp [Finset.map_map] + · intro h + obtain ⟨a, ha', rfl⟩ := h + rcases ha' with ha' | ha' + · left + use a + · obtain ⟨a, ha', rfl⟩ := ha' + right + let a' := congrLiftInv _ ⟨a, ha'⟩ + use a' + simp only [Finset.coe_mem, true_and] + simp only [a'] + rw [Finset.mapEmbedding_apply] + rw [join_uncontractedListEmb] + simp only [congrLiftInv, ← Finset.map_map] + congr + rw [Finset.map_map] + change Finset.map (Equiv.refl _).toEmbedding a = _ + simp only [Equiv.refl_toEmbedding, Finset.map_refl] + +lemma join_getDual?_apply_uncontractedListEmb_eq_none_iff {φs : List 𝓕.States} + (φsΛ : WickContraction φs.length) + (φsucΛ : WickContraction [φsΛ]ᵘᶜ.length) (i : Fin [φsΛ]ᵘᶜ.length) : + (join φsΛ φsucΛ).getDual? (uncontractedListEmd i) = none + ↔ φsucΛ.getDual? i = none := by + rw [getDual?_eq_none_iff_mem_uncontracted, getDual?_eq_none_iff_mem_uncontracted] + apply Iff.intro + · intro h + obtain ⟨a, ha', ha⟩ := exists_mem_right_uncontracted_of_mem_join_uncontracted _ _ + (uncontractedListEmd i) h + simp only [EmbeddingLike.apply_eq_iff_eq] at ha' + subst ha' + exact ha + · intro h + exact mem_join_uncontracted_of_mem_right_uncontracted φsΛ φsucΛ i h + +lemma join_getDual?_apply_uncontractedListEmb_isSome_iff {φs : List 𝓕.States} + (φsΛ : WickContraction φs.length) + (φsucΛ : WickContraction [φsΛ]ᵘᶜ.length) (i : Fin [φsΛ]ᵘᶜ.length) : + ((join φsΛ φsucΛ).getDual? (uncontractedListEmd i)).isSome + ↔ (φsucΛ.getDual? i).isSome := by + rw [← Decidable.not_iff_not] + simp [join_getDual?_apply_uncontractedListEmb_eq_none_iff] + +lemma join_getDual?_apply_uncontractedListEmb_some {φs : List 𝓕.States} + (φsΛ : WickContraction φs.length) + (φsucΛ : WickContraction [φsΛ]ᵘᶜ.length) (i : Fin [φsΛ]ᵘᶜ.length) + (hi :((join φsΛ φsucΛ).getDual? (uncontractedListEmd i)).isSome) : + ((join φsΛ φsucΛ).getDual? (uncontractedListEmd i)) = + some (uncontractedListEmd ((φsucΛ.getDual? i).get (by + simpa [join_getDual?_apply_uncontractedListEmb_isSome_iff]using hi))) := by + rw [getDual?_eq_some_iff_mem] + simp only [join, Finset.le_eq_subset, Finset.mem_union, Finset.mem_map, + RelEmbedding.coe_toEmbedding] + right + use {i, (φsucΛ.getDual? i).get (by + simpa [join_getDual?_apply_uncontractedListEmb_isSome_iff] using hi)} + simp only [self_getDual?_get_mem, true_and] + rw [Finset.mapEmbedding_apply] + simp + +@[simp] +lemma join_getDual?_apply_uncontractedListEmb {φs : List 𝓕.States} (φsΛ : WickContraction φs.length) + (φsucΛ : WickContraction [φsΛ]ᵘᶜ.length) (i : Fin [φsΛ]ᵘᶜ.length) : + ((join φsΛ φsucΛ).getDual? (uncontractedListEmd i)) = + Option.map uncontractedListEmd (φsucΛ.getDual? i) := by + by_cases h : (φsucΛ.getDual? i).isSome + · rw [join_getDual?_apply_uncontractedListEmb_some] + have h1 : (φsucΛ.getDual? i) = (φsucΛ.getDual? i).get (by simpa using h) := + Eq.symm (Option.some_get h) + conv_rhs => rw [h1] + simp only [Option.map_some'] + exact (join_getDual?_apply_uncontractedListEmb_isSome_iff φsΛ φsucΛ i).mpr h + · simp only [Bool.not_eq_true, Option.not_isSome, Option.isNone_iff_eq_none] at h + rw [h] + simp only [Option.map_none', join_getDual?_apply_uncontractedListEmb_eq_none_iff] + exact h + +/-! + +## Subcontractions and quotient contractions + +-/ + +section + +variable {φs : List 𝓕.States} (φsΛ : WickContraction φs.length) + +lemma join_sub_quot (S : Finset (Finset (Fin φs.length))) (ha : S ⊆ φsΛ.1) : + join (subContraction S ha) (quotContraction S ha) = φsΛ := by + apply Subtype.ext + ext a + simp only [join, Finset.le_eq_subset, Finset.mem_union, Finset.mem_map, + RelEmbedding.coe_toEmbedding] + apply Iff.intro + · intro h + rcases h with h | h + · exact mem_of_mem_subContraction h + · obtain ⟨a, ha, rfl⟩ := h + apply mem_of_mem_quotContraction ha + · intro h + have h1 := mem_subContraction_or_quotContraction (S := S) (a := a) (hs := ha) h + rcases h1 with h1 | h1 + · simp [h1] + · right + obtain ⟨a, rfl, ha⟩ := h1 + use a + simp only [ha, true_and] + rw [Finset.mapEmbedding_apply] + +lemma subContraction_card_plus_quotContraction_card_eq (S : Finset (Finset (Fin φs.length))) + (ha : S ⊆ φsΛ.1) : + (subContraction S ha).1.card + (quotContraction S ha).1.card = φsΛ.1.card := by + rw [← join_card] + simp [join_sub_quot] + +end +open FieldStatistic + +lemma stat_signFinset_right {φs : List 𝓕.States} (φsΛ : WickContraction φs.length) + (φsucΛ : WickContraction [φsΛ]ᵘᶜ.length) (i j : Fin [φsΛ]ᵘᶜ.length) : + (𝓕 |>ₛ ⟨[φsΛ]ᵘᶜ.get, φsucΛ.signFinset i j⟩) = + (𝓕 |>ₛ ⟨φs.get, (φsucΛ.signFinset i j).map uncontractedListEmd⟩) := by + simp only [ofFinset] + congr 1 + rw [← fin_finset_sort_map_monotone] + simp only [List.map_map, List.map_inj_left, Finset.mem_sort, List.get_eq_getElem, + Function.comp_apply, getElem_uncontractedListEmd, implies_true] + intro i j h + exact uncontractedListEmd_strictMono h + +lemma signFinset_right_map_uncontractedListEmd_eq_filter {φs : List 𝓕.States} + (φsΛ : WickContraction φs.length) (φsucΛ : WickContraction [φsΛ]ᵘᶜ.length) + (i j : Fin [φsΛ]ᵘᶜ.length) : (φsucΛ.signFinset i j).map uncontractedListEmd = + ((join φsΛ φsucΛ).signFinset (uncontractedListEmd i) (uncontractedListEmd j)).filter + (fun c => c ∈ φsΛ.uncontracted) := by + ext a + simp only [Finset.mem_map, Finset.mem_filter] + apply Iff.intro + · intro h + obtain ⟨a, ha, rfl⟩ := h + apply And.intro + · simp_all only [signFinset, Finset.mem_filter, Finset.mem_univ, true_and, + join_getDual?_apply_uncontractedListEmb, Option.map_eq_none', Option.isSome_map'] + apply And.intro + · exact uncontractedListEmd_strictMono ha.1 + · apply And.intro + · exact uncontractedListEmd_strictMono ha.2.1 + · have ha2 := ha.2.2 + simp_all only [and_true] + rcases ha2 with ha2 | ha2 + · simp [ha2] + · right + intro h + apply lt_of_lt_of_eq (uncontractedListEmd_strictMono (ha2 h)) + rw [Option.get_map] + · exact uncontractedListEmd_mem_uncontracted a + · intro h + have h2 := h.2 + have h2' := uncontractedListEmd_surjective_mem_uncontracted a h.2 + obtain ⟨a, rfl⟩ := h2' + use a + simp_all only [signFinset, Finset.mem_filter, Finset.mem_univ, + join_getDual?_apply_uncontractedListEmb, Option.map_eq_none', Option.isSome_map', true_and, + and_true, and_self] + apply And.intro + · have h1 := h.1 + rw [StrictMono.lt_iff_lt] at h1 + exact h1 + exact fun _ _ h => uncontractedListEmd_strictMono h + · apply And.intro + · have h1 := h.2.1 + rw [StrictMono.lt_iff_lt] at h1 + exact h1 + exact fun _ _ h => uncontractedListEmd_strictMono h + · have h1 := h.2.2 + simp_all only [and_true] + rcases h1 with h1 | h1 + · simp [h1] + · right + intro h + have h1' := h1 h + have hl : uncontractedListEmd i < uncontractedListEmd ((φsucΛ.getDual? a).get h) := by + apply lt_of_lt_of_eq h1' + simp [Option.get_map] + rw [StrictMono.lt_iff_lt] at hl + exact hl + exact fun _ _ h => uncontractedListEmd_strictMono h + +lemma sign_right_eq_prod_mul_prod {φs : List 𝓕.States} (φsΛ : WickContraction φs.length) + (φsucΛ : WickContraction [φsΛ]ᵘᶜ.length) : + φsucΛ.sign = (∏ a, 𝓢(𝓕|>ₛ [φsΛ]ᵘᶜ[φsucΛ.sndFieldOfContract a], 𝓕|>ₛ ⟨φs.get, + ((join φsΛ φsucΛ).signFinset (uncontractedListEmd (φsucΛ.fstFieldOfContract a)) + (uncontractedListEmd (φsucΛ.sndFieldOfContract a))).filter + (fun c => ¬ c ∈ φsΛ.uncontracted)⟩)) * + (∏ a, 𝓢(𝓕|>ₛ [φsΛ]ᵘᶜ[φsucΛ.sndFieldOfContract a], 𝓕|>ₛ ⟨φs.get, + ((join φsΛ φsucΛ).signFinset (uncontractedListEmd (φsucΛ.fstFieldOfContract a)) + (uncontractedListEmd (φsucΛ.sndFieldOfContract a)))⟩)) := by + rw [← Finset.prod_mul_distrib, sign] + congr + funext a + rw [← map_mul] + congr + rw [stat_signFinset_right, signFinset_right_map_uncontractedListEmd_eq_filter] + rw [ofFinset_filter] + +lemma join_singleton_signFinset_eq_filter {φs : List 𝓕.States} + {i j : Fin φs.length} (h : i < j) + (φsucΛ : WickContraction [singleton h]ᵘᶜ.length) : + (join (singleton h) φsucΛ).signFinset i j = + ((singleton h).signFinset i j).filter (fun c => ¬ + (((join (singleton h) φsucΛ).getDual? c).isSome ∧ + ((h1 : ((join (singleton h) φsucΛ).getDual? c).isSome) → + (((join (singleton h) φsucΛ).getDual? c).get h1) < i))) := by + ext a + simp only [signFinset, Finset.mem_filter, Finset.mem_univ, true_and, not_and, not_forall, not_lt, + and_assoc, and_congr_right_iff] + intro h1 h2 + have h1 : (singleton h).getDual? a = none := by + rw [singleton_getDual?_eq_none_iff_neq] + omega + simp only [h1, Option.isSome_none, Bool.false_eq_true, IsEmpty.forall_iff, or_self, true_and] + apply Iff.intro + · intro h1 h2 + rcases h1 with h1 | h1 + · simp only [h1, Option.isSome_none, Bool.false_eq_true, IsEmpty.exists_iff] + have h2' : ¬ (((singleton h).join φsucΛ).getDual? a).isSome := by + exact Option.not_isSome_iff_eq_none.mpr h1 + exact h2' h2 + use h2 + have h1 := h1 h2 + omega + · intro h2 + by_cases h2' : (((singleton h).join φsucΛ).getDual? a).isSome = true + · have h2 := h2 h2' + obtain ⟨hb, h2⟩ := h2 + right + intro hl + apply lt_of_le_of_ne h2 + by_contra hn + have hij : ((singleton h).join φsucΛ).getDual? i = j := by + rw [@getDual?_eq_some_iff_mem] + simp [join, singleton] + simp only [hn, getDual?_getDual?_get_get, Option.some.injEq] at hij + omega + · simp only [Bool.not_eq_true, Option.not_isSome, Option.isNone_iff_eq_none] at h2' + simp [h2'] + +lemma join_singleton_left_signFinset_eq_filter {φs : List 𝓕.States} + {i j : Fin φs.length} (h : i < j) + (φsucΛ : WickContraction [singleton h]ᵘᶜ.length) : + (𝓕 |>ₛ ⟨φs.get, (singleton h).signFinset i j⟩) + = (𝓕 |>ₛ ⟨φs.get, (join (singleton h) φsucΛ).signFinset i j⟩) * + (𝓕 |>ₛ ⟨φs.get, ((singleton h).signFinset i j).filter (fun c => + (((join (singleton h) φsucΛ).getDual? c).isSome ∧ + ((h1 : ((join (singleton h) φsucΛ).getDual? c).isSome) → + (((join (singleton h) φsucΛ).getDual? c).get h1) < i)))⟩) := by + conv_rhs => + left + rw [join_singleton_signFinset_eq_filter] + rw [mul_comm] + exact (ofFinset_filter_mul_neg 𝓕.statesStatistic _ _ _).symm + +/-- The difference in sign between `φsucΛ.sign` and the direct contribution of `φsucΛ` to + `(join (singleton h) φsucΛ)`. -/ +def joinSignRightExtra {φs : List 𝓕.States} + {i j : Fin φs.length} (h : i < j) + (φsucΛ : WickContraction [singleton h]ᵘᶜ.length) : ℂ := + ∏ a, 𝓢(𝓕|>ₛ [singleton h]ᵘᶜ[φsucΛ.sndFieldOfContract a], 𝓕|>ₛ ⟨φs.get, + ((join (singleton h) φsucΛ).signFinset (uncontractedListEmd (φsucΛ.fstFieldOfContract a)) + (uncontractedListEmd (φsucΛ.sndFieldOfContract a))).filter + (fun c => ¬ c ∈ (singleton h).uncontracted)⟩) + +/-- The difference in sign between `(singleton h).sign` and the direct contribution of + `(singleton h)` to `(join (singleton h) φsucΛ)`. -/ +def joinSignLeftExtra {φs : List 𝓕.States} + {i j : Fin φs.length} (h : i < j) + (φsucΛ : WickContraction [singleton h]ᵘᶜ.length) : ℂ := + 𝓢(𝓕 |>ₛ φs[j], (𝓕 |>ₛ ⟨φs.get, ((singleton h).signFinset i j).filter (fun c => + (((join (singleton h) φsucΛ).getDual? c).isSome ∧ + ((h1 : ((join (singleton h) φsucΛ).getDual? c).isSome) → + (((join (singleton h) φsucΛ).getDual? c).get h1) < i)))⟩)) + +lemma join_singleton_sign_left {φs : List 𝓕.States} + {i j : Fin φs.length} (h : i < j) + (φsucΛ : WickContraction [singleton h]ᵘᶜ.length) : + (singleton h).sign = 𝓢(𝓕 |>ₛ φs[j], + (𝓕 |>ₛ ⟨φs.get, (join (singleton h) φsucΛ).signFinset i j⟩)) * (joinSignLeftExtra h φsucΛ) := by + rw [singleton_sign_expand] + rw [join_singleton_left_signFinset_eq_filter h φsucΛ] + rw [map_mul] + rfl + +lemma join_singleton_sign_right {φs : List 𝓕.States} + {i j : Fin φs.length} (h : i < j) + (φsucΛ : WickContraction [singleton h]ᵘᶜ.length) : + φsucΛ.sign = + (joinSignRightExtra h φsucΛ) * + (∏ a, 𝓢(𝓕|>ₛ [singleton h]ᵘᶜ[φsucΛ.sndFieldOfContract a], 𝓕|>ₛ ⟨φs.get, + ((join (singleton h) φsucΛ).signFinset (uncontractedListEmd (φsucΛ.fstFieldOfContract a)) + (uncontractedListEmd (φsucΛ.sndFieldOfContract a)))⟩)) := by + rw [sign_right_eq_prod_mul_prod] + rfl + +@[simp] +lemma join_singleton_getDual?_left {φs : List 𝓕.States} + {i j : Fin φs.length} (h : i < j) + (φsucΛ : WickContraction [singleton h]ᵘᶜ.length) : + (join (singleton h) φsucΛ).getDual? i = some j := by + rw [@getDual?_eq_some_iff_mem] + simp [singleton, join] + +@[simp] +lemma join_singleton_getDual?_right {φs : List 𝓕.States} + {i j : Fin φs.length} (h : i < j) + (φsucΛ : WickContraction [singleton h]ᵘᶜ.length) : + (join (singleton h) φsucΛ).getDual? j = some i := by + rw [@getDual?_eq_some_iff_mem] + simp only [join, singleton, Finset.le_eq_subset, Finset.mem_union, Finset.mem_singleton, + Finset.mem_map, RelEmbedding.coe_toEmbedding] + left + exact Finset.pair_comm j i + +lemma joinSignRightExtra_eq_i_j_finset_eq_if {φs : List 𝓕.States} + {i j : Fin φs.length} (h : i < j) + (φsucΛ : WickContraction [singleton h]ᵘᶜ.length) : + joinSignRightExtra h φsucΛ = ∏ a, + 𝓢((𝓕|>ₛ [singleton h]ᵘᶜ[φsucΛ.sndFieldOfContract a]), + 𝓕 |>ₛ ⟨φs.get, (if uncontractedListEmd (φsucΛ.fstFieldOfContract a) < j ∧ + j < uncontractedListEmd (φsucΛ.sndFieldOfContract a) ∧ + uncontractedListEmd (φsucΛ.fstFieldOfContract a) < i then {j} else ∅) + ∪ (if uncontractedListEmd (φsucΛ.fstFieldOfContract a) < i ∧ + i < uncontractedListEmd (φsucΛ.sndFieldOfContract a) then {i} else ∅)⟩) := by + rw [joinSignRightExtra] + congr + funext a + congr + rw [signFinset] + rw [Finset.filter_comm] + have h11 : (Finset.filter (fun c => c ∉ (singleton h).uncontracted) Finset.univ) = {i, j} := by + ext x + simp only [Finset.mem_filter, Finset.mem_univ, true_and, Finset.mem_insert, + Finset.mem_singleton] + rw [@mem_uncontracted_iff_not_contracted] + simp only [singleton, Finset.mem_singleton, forall_eq, Finset.mem_insert, not_or, not_and, + Decidable.not_not] + omega + rw [h11] + ext x + simp only [Finset.mem_filter, Finset.mem_insert, Finset.mem_singleton, Finset.mem_union] + have hjneqfst := singleton_uncontractedEmd_neq_right h (φsucΛ.fstFieldOfContract a) + have hjneqsnd := singleton_uncontractedEmd_neq_right h (φsucΛ.sndFieldOfContract a) + have hineqfst := singleton_uncontractedEmd_neq_left h (φsucΛ.fstFieldOfContract a) + have hineqsnd := singleton_uncontractedEmd_neq_left h (φsucΛ.sndFieldOfContract a) + by_cases hj1 : ¬ uncontractedListEmd (φsucΛ.fstFieldOfContract a) < j + · simp only [hj1, false_and, ↓reduceIte, Finset.not_mem_empty, false_or] + have hi1 : ¬ uncontractedListEmd (φsucΛ.fstFieldOfContract a) < i := by omega + simp only [hi1, false_and, ↓reduceIte, Finset.not_mem_empty, iff_false, not_and, not_or, + not_forall, not_lt] + intro hxij h1 h2 + omega + · have hj1 : uncontractedListEmd (φsucΛ.fstFieldOfContract a) < j := by + omega + by_cases hi1 : ¬ i < uncontractedListEmd (φsucΛ.sndFieldOfContract a) + · simp only [hi1, and_false, ↓reduceIte, Finset.not_mem_empty, or_false] + have hj2 : ¬ j < uncontractedListEmd (φsucΛ.sndFieldOfContract a) := by omega + simp only [hj2, false_and, and_false, ↓reduceIte, Finset.not_mem_empty, iff_false, not_and, + not_or, not_forall, not_lt] + intro hxij h1 h2 + omega + · have hi1 : i < uncontractedListEmd (φsucΛ.sndFieldOfContract a) := by + omega + simp only [hj1, true_and, hi1, and_true] + by_cases hi2 : ¬ uncontractedListEmd (φsucΛ.fstFieldOfContract a) < i + · simp only [hi2, and_false, ↓reduceIte, Finset.not_mem_empty, or_self, iff_false, not_and, + not_or, not_forall, not_lt] + by_cases hj3 : ¬ j < uncontractedListEmd (φsucΛ.sndFieldOfContract a) + · omega + · have hj4 : j < uncontractedListEmd (φsucΛ.sndFieldOfContract a) := by omega + intro h + rcases h with h | h + · subst h + omega + · subst h + simp only [join_singleton_getDual?_right, reduceCtorEq, not_false_eq_true, + Option.get_some, Option.isSome_some, exists_const, true_and] + omega + · have hi2 : uncontractedListEmd (φsucΛ.fstFieldOfContract a) < i := by omega + simp only [hi2, and_true, ↓reduceIte, Finset.mem_singleton] + by_cases hj3 : ¬ j < uncontractedListEmd (φsucΛ.sndFieldOfContract a) + · simp only [hj3, ↓reduceIte, Finset.not_mem_empty, false_or] + apply Iff.intro + · intro h + omega + · intro h + subst h + simp only [true_or, join_singleton_getDual?_left, reduceCtorEq, Option.isSome_some, + Option.get_some, forall_const, false_or, true_and] + omega + · have hj3 : j < uncontractedListEmd (φsucΛ.sndFieldOfContract a) := by omega + simp only [hj3, ↓reduceIte, Finset.mem_singleton] + apply Iff.intro + · intro h + omega + · intro h + rcases h with h1 | h1 + · subst h1 + simp only [or_true, join_singleton_getDual?_right, reduceCtorEq, Option.isSome_some, + Option.get_some, forall_const, false_or, true_and] + omega + · subst h1 + simp only [true_or, join_singleton_getDual?_left, reduceCtorEq, Option.isSome_some, + Option.get_some, forall_const, false_or, true_and] + omega + +lemma joinSignLeftExtra_eq_joinSignRightExtra {φs : List 𝓕.States} + {i j : Fin φs.length} (h : i < j) (hs : (𝓕 |>ₛ φs[i]) = (𝓕 |>ₛ φs[j])) + (φsucΛ : WickContraction [singleton h]ᵘᶜ.length) : + joinSignLeftExtra h φsucΛ = joinSignRightExtra h φsucΛ := by + /- Simplifying joinSignLeftExtra. -/ + rw [joinSignLeftExtra] + rw [ofFinset_eq_prod] + rw [map_prod] + let e2 : Fin φs.length ≃ {x // (((singleton h).join φsucΛ).getDual? x).isSome} ⊕ + {x // ¬ (((singleton h).join φsucΛ).getDual? x).isSome} := by + exact (Equiv.sumCompl fun a => (((singleton h).join φsucΛ).getDual? a).isSome = true).symm + rw [← e2.symm.prod_comp] + simp only [Fin.getElem_fin, Fintype.prod_sum_type, instCommGroup] + conv_lhs => + enter [2, 2, x] + simp only [Equiv.symm_symm, Equiv.sumCompl_apply_inl, Equiv.sumCompl_apply_inr, e2] + rw [if_neg (by + simp only [Finset.mem_filter, mem_signFinset, not_and, not_forall, not_lt, and_imp] + intro h1 h2 + have hx := x.2 + simp_all)] + simp only [Finset.mem_filter, mem_signFinset, map_one, Finset.prod_const_one, mul_one] + rw [← ((singleton h).join φsucΛ).sigmaContractedEquiv.prod_comp] + erw [Finset.prod_sigma] + conv_lhs => + enter [2, a] + rw [prod_finset_eq_mul_fst_snd] + simp [e2, sigmaContractedEquiv] + rw [prod_join] + rw [singleton_prod] + simp only [join_fstFieldOfContract_joinLiftLeft, singleton_fstFieldOfContract, + join_sndFieldOfContract_joinLift, singleton_sndFieldOfContract, lt_self_iff_false, and_false, + ↓reduceIte, map_one, mul_one, join_fstFieldOfContract_joinLiftRight, + join_sndFieldOfContract_joinLiftRight, getElem_uncontractedListEmd] + rw [if_neg (by omega)] + simp only [map_one, one_mul] + /- Introducing joinSignRightExtra. -/ + rw [joinSignRightExtra_eq_i_j_finset_eq_if] + congr + funext a + have hjneqsnd := singleton_uncontractedEmd_neq_right h (φsucΛ.sndFieldOfContract a) + have hl : uncontractedListEmd (φsucΛ.fstFieldOfContract a) < + uncontractedListEmd (φsucΛ.sndFieldOfContract a) := by + apply uncontractedListEmd_strictMono + exact fstFieldOfContract_lt_sndFieldOfContract φsucΛ a + by_cases hj1 : ¬ uncontractedListEmd (φsucΛ.fstFieldOfContract a) < j + · have hi1 : ¬ uncontractedListEmd (φsucΛ.fstFieldOfContract a) < i := by omega + simp [hj1, hi1] + · have hj1 : uncontractedListEmd (φsucΛ.fstFieldOfContract a) < j := by omega + simp only [hj1, and_true, instCommGroup, Fin.getElem_fin, true_and] + by_cases hi2 : ¬ i < uncontractedListEmd (φsucΛ.sndFieldOfContract a) + · have hi1 : ¬ i < uncontractedListEmd (φsucΛ.fstFieldOfContract a) := by omega + have hj2 : ¬ j < uncontractedListEmd (φsucΛ.sndFieldOfContract a) := by omega + simp [hi2, hj2, hi1] + · have hi2 : i < uncontractedListEmd (φsucΛ.sndFieldOfContract a) := by omega + have hi2n : ¬ uncontractedListEmd (φsucΛ.sndFieldOfContract a) < i := by omega + simp only [hi2n, and_false, ↓reduceIte, map_one, hi2, true_and, one_mul, and_true] + by_cases hj2 : ¬ j < uncontractedListEmd (φsucΛ.sndFieldOfContract a) + · simp only [hj2, false_and, ↓reduceIte, Finset.empty_union] + have hj2 : uncontractedListEmd (φsucΛ.sndFieldOfContract a) < j:= by omega + simp only [hj2, true_and] + by_cases hi1 : ¬ uncontractedListEmd (φsucΛ.fstFieldOfContract a) < i + · simp [hi1] + · have hi1 : uncontractedListEmd (φsucΛ.fstFieldOfContract a) < i := by omega + simp only [hi1, ↓reduceIte, ofFinset_singleton, List.get_eq_getElem] + erw [hs] + exact exchangeSign_symm (𝓕|>ₛφs[↑j]) (𝓕|>ₛ[singleton h]ᵘᶜ[↑(φsucΛ.sndFieldOfContract a)]) + · simp only [not_lt, not_le] at hj2 + simp only [hj2, true_and] + by_cases hi1 : ¬ uncontractedListEmd (φsucΛ.fstFieldOfContract a) < i + · simp [hi1] + · have hi1 : uncontractedListEmd (φsucΛ.fstFieldOfContract a) < i := by omega + simp only [hi1, and_true, ↓reduceIte] + have hj2 : ¬ uncontractedListEmd (φsucΛ.sndFieldOfContract a) < j := by omega + simp only [hj2, ↓reduceIte, map_one] + rw [← ofFinset_union_disjoint] + simp only [instCommGroup, ofFinset_singleton, List.get_eq_getElem, hs] + erw [hs] + simp only [Fin.getElem_fin, mul_self, map_one] + simp only [Finset.disjoint_singleton_right, Finset.mem_singleton] + exact Fin.ne_of_lt h + +lemma join_sign_singleton {φs : List 𝓕.States} + {i j : Fin φs.length} (h : i < j) (hs : (𝓕 |>ₛ φs[i]) = (𝓕 |>ₛ φs[j])) + (φsucΛ : WickContraction [singleton h]ᵘᶜ.length) : + (join (singleton h) φsucΛ).sign = (singleton h).sign * φsucΛ.sign := by + rw [join_singleton_sign_right] + rw [join_singleton_sign_left h φsucΛ] + rw [joinSignLeftExtra_eq_joinSignRightExtra h hs φsucΛ] + rw [← mul_assoc] + rw [mul_assoc _ _ (joinSignRightExtra h φsucΛ)] + have h1 : (joinSignRightExtra h φsucΛ * joinSignRightExtra h φsucΛ) = 1 := by + rw [← joinSignLeftExtra_eq_joinSignRightExtra h hs φsucΛ] + simp [joinSignLeftExtra] + simp only [instCommGroup, Fin.getElem_fin, h1, mul_one] + rw [sign] + rw [prod_join] + congr + · rw [singleton_prod] + simp + · funext a + simp + +lemma exists_contraction_pair_of_card_ge_zero {φs : List 𝓕.States} (φsΛ : WickContraction φs.length) + (h : 0 < φsΛ.1.card) : + ∃ a, a ∈ φsΛ.1 := by + simpa using h + +lemma exists_join_singleton_of_card_ge_zero {φs : List 𝓕.States} (φsΛ : WickContraction φs.length) + (h : 0 < φsΛ.1.card) (hc : φsΛ.GradingCompliant) : + ∃ (i j : Fin φs.length) (h : i < j) (φsucΛ : WickContraction [singleton h]ᵘᶜ.length), + φsΛ = join (singleton h) φsucΛ ∧ (𝓕 |>ₛ φs[i]) = (𝓕 |>ₛ φs[j]) + ∧ φsucΛ.GradingCompliant ∧ φsucΛ.1.card + 1 = φsΛ.1.card := by + obtain ⟨a, ha⟩ := exists_contraction_pair_of_card_ge_zero φsΛ h + use φsΛ.fstFieldOfContract ⟨a, ha⟩ + use φsΛ.sndFieldOfContract ⟨a, ha⟩ + use φsΛ.fstFieldOfContract_lt_sndFieldOfContract ⟨a, ha⟩ + let φsucΛ : + WickContraction [singleton (φsΛ.fstFieldOfContract_lt_sndFieldOfContract ⟨a, ha⟩)]ᵘᶜ.length := + congr (by simp [← subContraction_singleton_eq_singleton]) + (φsΛ.quotContraction {a} (by simpa using ha)) + use φsucΛ + simp only [Fin.getElem_fin] + apply And.intro + · have h1 := join_congr (subContraction_singleton_eq_singleton _ ⟨a, ha⟩).symm (φsucΛ := φsucΛ) + simp only [id_eq, eq_mpr_eq_cast, h1, congr_trans_apply, congr_refl, φsucΛ] + rw [join_sub_quot] + · apply And.intro (hc ⟨a, ha⟩) + apply And.intro + · simp only [id_eq, eq_mpr_eq_cast, φsucΛ] + rw [gradingCompliant_congr (φs' := [(φsΛ.subContraction {a} (by simpa using ha))]ᵘᶜ)] + simp only [id_eq, eq_mpr_eq_cast, congr_trans_apply, congr_refl] + exact quotContraction_gradingCompliant hc + rw [← subContraction_singleton_eq_singleton] + · simp only [id_eq, eq_mpr_eq_cast, card_congr, φsucΛ] + have h1 := subContraction_card_plus_quotContraction_card_eq _ {a} (by simpa using ha) + simp only [subContraction, Finset.card_singleton, id_eq, eq_mpr_eq_cast] at h1 + omega + +lemma join_sign_induction {φs : List 𝓕.States} (φsΛ : WickContraction φs.length) + (φsucΛ : WickContraction [φsΛ]ᵘᶜ.length) (hc : φsΛ.GradingCompliant) : + (n : ℕ) → (hn : φsΛ.1.card = n) → + (join φsΛ φsucΛ).sign = φsΛ.sign * φsucΛ.sign + | 0, hn => by + rw [@card_zero_iff_empty] at hn + subst hn + simp only [empty_join, sign_empty, one_mul] + apply sign_congr + simp + | Nat.succ n, hn => by + obtain ⟨i, j, hij, φsucΛ', rfl, h1, h2, h3⟩ := + exists_join_singleton_of_card_ge_zero φsΛ (by simp [hn]) hc + rw [join_assoc] + rw [join_sign_singleton hij h1] + rw [join_sign_singleton hij h1] + have hn : φsucΛ'.1.card = n := by + omega + rw [join_sign_induction φsucΛ' (congr (by simp [join_uncontractedListGet]) φsucΛ) h2 + n hn] + rw [mul_assoc] + simp only [mul_eq_mul_left_iff] + left + left + apply sign_congr + exact join_uncontractedListGet (singleton hij) φsucΛ' + +lemma join_sign {φs : List 𝓕.States} (φsΛ : WickContraction φs.length) + (φsucΛ : WickContraction [φsΛ]ᵘᶜ.length) (hc : φsΛ.GradingCompliant) : + (join φsΛ φsucΛ).sign = φsΛ.sign * φsucΛ.sign := by + exact join_sign_induction φsΛ φsucΛ hc (φsΛ).1.card rfl + +lemma join_not_gradingCompliant_of_left_not_gradingCompliant {φs : List 𝓕.States} + (φsΛ : WickContraction φs.length) (φsucΛ : WickContraction [φsΛ]ᵘᶜ.length) + (hc : ¬ φsΛ.GradingCompliant) : ¬ (join φsΛ φsucΛ).GradingCompliant := by + simp_all only [GradingCompliant, Fin.getElem_fin, Subtype.forall, not_forall] + obtain ⟨a, ha, ha2⟩ := hc + use (joinLiftLeft (φsucΛ := φsucΛ) ⟨a, ha⟩).1 + use (joinLiftLeft (φsucΛ := φsucΛ) ⟨a, ha⟩).2 + simp only [Subtype.coe_eta, join_fstFieldOfContract_joinLiftLeft, + join_sndFieldOfContract_joinLift] + exact ha2 + +lemma join_sign_timeContract {φs : List 𝓕.States} (φsΛ : WickContraction φs.length) + (φsucΛ : WickContraction [φsΛ]ᵘᶜ.length) : + (join φsΛ φsucΛ).sign • (join φsΛ φsucΛ).timeContract.1 = + (φsΛ.sign • φsΛ.timeContract.1) * (φsucΛ.sign • φsucΛ.timeContract.1) := by + rw [join_timeContract] + by_cases h : φsΛ.GradingCompliant + · rw [join_sign _ _ h] + simp [smul_smul, mul_comm] + · rw [timeContract_of_not_gradingCompliant _ _ h] + simp + +end WickContraction diff --git a/HepLean/PerturbationTheory/WickContraction/Sign.lean b/HepLean/PerturbationTheory/WickContraction/Sign.lean index 6c8e937d..76bd293d 100644 --- a/HepLean/PerturbationTheory/WickContraction/Sign.lean +++ b/HepLean/PerturbationTheory/WickContraction/Sign.lean @@ -324,6 +324,16 @@ def sign (φs : List 𝓕.States) (φsΛ : WickContraction φs.length) : ℂ := ∏ (a : φsΛ.1), 𝓢(𝓕 |>ₛ φs[φsΛ.sndFieldOfContract a], 𝓕 |>ₛ ⟨φs.get, φsΛ.signFinset (φsΛ.fstFieldOfContract a) (φsΛ.sndFieldOfContract a)⟩) +lemma sign_empty (φs : List 𝓕.States) : + sign φs empty = 1 := by + rw [sign] + simp [empty] + +lemma sign_congr {φs φs' : List 𝓕.States} (h : φs = φs') (φsΛ : WickContraction φs.length) : + sign φs' (congr (by simp [h]) φsΛ) = sign φs φsΛ := by + subst h + rfl + /-! ## Sign insert diff --git a/HepLean/PerturbationTheory/WickContraction/Singleton.lean b/HepLean/PerturbationTheory/WickContraction/Singleton.lean new file mode 100644 index 00000000..e64af3db --- /dev/null +++ b/HepLean/PerturbationTheory/WickContraction/Singleton.lean @@ -0,0 +1,137 @@ +/- +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.TimeContract +import HepLean.PerturbationTheory.WickContraction.StaticContract +import HepLean.PerturbationTheory.Algebras.FieldOpAlgebra.TimeContraction +import HepLean.PerturbationTheory.WickContraction.SubContraction +/-! + +# Singleton of contractions + +-/ + +open FieldSpecification +variable {𝓕 : FieldSpecification} + +namespace WickContraction +variable {n : ℕ} (c : WickContraction n) +open HepLean.List +open FieldOpAlgebra +open FieldStatistic + +/-- The Wick contraction formed from a single ordered pair. -/ +def singleton {i j : Fin n} (hij : i < j) : WickContraction n := + ⟨{{i, j}}, by + intro i hi + simp only [Finset.mem_singleton] at hi + subst hi + rw [@Finset.card_eq_two] + use i, j + simp only [ne_eq, and_true] + omega, by + intro i hi j hj + simp_all⟩ + +lemma mem_singleton {i j : Fin n} (hij : i < j) : + {i, j} ∈ (singleton hij).1 := by + simp [singleton] + +lemma mem_singleton_iff {i j : Fin n} (hij : i < j) {a : Finset (Fin n)} : + a ∈ (singleton hij).1 ↔ a = {i, j} := by + simp [singleton] + +lemma of_singleton_eq {i j : Fin n} (hij : i < j) (a : (singleton hij).1) : + a = ⟨{i, j}, mem_singleton hij⟩ := by + have ha2 := a.2 + rw [@mem_singleton_iff] at ha2 + exact Subtype.coe_eq_of_eq_mk ha2 + +lemma singleton_prod {φs : List 𝓕.States} {i j : Fin φs.length} (hij : i < j) + (f : (singleton hij).1 → M) [CommMonoid M] : + ∏ a, f a = f ⟨{i,j}, mem_singleton hij⟩:= by + simp [singleton, of_singleton_eq] + +@[simp] +lemma singleton_fstFieldOfContract {i j : Fin n} (hij : i < j) : + (singleton hij).fstFieldOfContract ⟨{i, j}, mem_singleton hij⟩ = i := by + refine eq_fstFieldOfContract_of_mem (singleton hij) ⟨{i, j}, mem_singleton hij⟩ i j ?_ ?_ ?_ + · simp + · simp + · exact hij + +@[simp] +lemma singleton_sndFieldOfContract {i j : Fin n} (hij : i < j) : + (singleton hij).sndFieldOfContract ⟨{i, j}, mem_singleton hij⟩ = j := by + refine eq_sndFieldOfContract_of_mem (singleton hij) ⟨{i, j}, mem_singleton hij⟩ i j ?_ ?_ ?_ + · simp + · simp + · exact hij + +lemma singleton_sign_expand {φs : List 𝓕.States} {i j : Fin φs.length} (hij : i < j) : + (singleton hij).sign = 𝓢(𝓕 |>ₛ φs[j], 𝓕 |>ₛ ⟨φs.get, (singleton hij).signFinset i j⟩) := by + rw [sign, singleton_prod] + simp + +lemma singleton_getDual?_eq_none_iff_neq {i j : Fin n} (hij : i < j) (a : Fin n) : + (singleton hij).getDual? a = none ↔ (i ≠ a ∧ j ≠ a) := by + rw [getDual?_eq_none_iff_mem_uncontracted] + rw [mem_uncontracted_iff_not_contracted] + simp only [singleton, Finset.mem_singleton, forall_eq, Finset.mem_insert, not_or, ne_eq] + omega + +lemma singleton_uncontractedEmd_neq_left {φs : List 𝓕.States} {i j : Fin φs.length} (hij : i < j) + (a : Fin [singleton hij]ᵘᶜ.length) : + (singleton hij).uncontractedListEmd a ≠ i := by + by_contra hn + have h1 : (singleton hij).uncontractedListEmd a ∈ (singleton hij).uncontracted := by + simp [uncontractedListEmd] + have h2 : i ∉ (singleton hij).uncontracted := by + rw [mem_uncontracted_iff_not_contracted] + simp [singleton] + simp_all + +lemma singleton_uncontractedEmd_neq_right {φs : List 𝓕.States} {i j : Fin φs.length} (hij : i < j) + (a : Fin [singleton hij]ᵘᶜ.length) : + (singleton hij).uncontractedListEmd a ≠ j := by + by_contra hn + have h1 : (singleton hij).uncontractedListEmd a ∈ (singleton hij).uncontracted := by + simp [uncontractedListEmd] + have h2 : j ∉ (singleton hij).uncontracted := by + rw [mem_uncontracted_iff_not_contracted] + simp [singleton] + simp_all + +@[simp] +lemma mem_signFinset {i j : Fin n} (hij : i < j) (a : Fin n) : + a ∈ (singleton hij).signFinset i j ↔ i < a ∧ a < j := by + simp only [signFinset, Finset.mem_filter, Finset.mem_univ, true_and, and_congr_right_iff, + and_iff_left_iff_imp] + intro h1 h2 + rw [@singleton_getDual?_eq_none_iff_neq] + apply Or.inl + omega + +lemma subContraction_singleton_eq_singleton {φs : List 𝓕.States} + (φsΛ : WickContraction φs.length) + (a : φsΛ.1) : φsΛ.subContraction {a.1} (by simp) = + singleton (φsΛ.fstFieldOfContract_lt_sndFieldOfContract a) := by + apply Subtype.ext + simp only [subContraction, singleton, Finset.singleton_inj] + exact finset_eq_fstFieldOfContract_sndFieldOfContract φsΛ a + +lemma singleton_timeContract {φs : List 𝓕.States} {i j : Fin φs.length} (hij : i < j) : + (singleton hij).timeContract = + ⟨FieldOpAlgebra.timeContract φs[i] φs[j], timeContract_mem_center _ _⟩ := by + rw [timeContract, singleton_prod] + simp + +lemma singleton_staticContract {φs : List 𝓕.States} {i j : Fin φs.length} (hij : i < j) : + (singleton hij).staticContract.1 = + [anPart φs[i], ofFieldOp φs[j]]ₛ := by + rw [staticContract, singleton_prod] + simp + +end WickContraction diff --git a/HepLean/PerturbationTheory/WickContraction/StaticContract.lean b/HepLean/PerturbationTheory/WickContraction/StaticContract.lean index 369ebc5f..c4e2a980 100644 --- a/HepLean/PerturbationTheory/WickContraction/StaticContract.lean +++ b/HepLean/PerturbationTheory/WickContraction/StaticContract.lean @@ -51,7 +51,7 @@ lemma staticContract_insertAndContract_some (φsΛ ↩Λ φ i (some j)).staticContract = (if i < i.succAbove j then ⟨[anPart φ, ofFieldOp φs[j.1]]ₛ, superCommute_anPart_ofFieldOp_mem_center _ _⟩ - else ⟨[anPart φs[j.1], ofFieldOp φ]ₛ, superCommute_anPart_ofFieldOp_mem_center _ _⟩) * + else ⟨[anPart φs[j.1], ofFieldOp φ]ₛ, superCommute_anPart_ofFieldOp_mem_center _ _⟩) * φsΛ.staticContract := by rw [staticContract, insertAndContract_some_prod_contractions] congr 1 diff --git a/HepLean/PerturbationTheory/WickContraction/SubContraction.lean b/HepLean/PerturbationTheory/WickContraction/SubContraction.lean new file mode 100644 index 00000000..319d29ba --- /dev/null +++ b/HepLean/PerturbationTheory/WickContraction/SubContraction.lean @@ -0,0 +1,201 @@ +/- +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.TimeContract +import HepLean.PerturbationTheory.WickContraction.StaticContract +import HepLean.PerturbationTheory.Algebras.FieldOpAlgebra.TimeContraction +/-! + +# Sub contractions + +-/ + +open FieldSpecification +variable {𝓕 : FieldSpecification} + +namespace WickContraction +variable {n : ℕ} {φs : List 𝓕.States} {φsΛ : WickContraction φs.length} +open HepLean.List +open FieldOpAlgebra + +/-- Given a Wick contraction `φsΛ`, and a subset of `φsΛ.1`, the Wick contraction + conisting of contracted pairs within that subset. -/ +def subContraction (S : Finset (Finset (Fin φs.length))) (ha : S ⊆ φsΛ.1) : + WickContraction φs.length := + ⟨S, by + intro i hi + exact φsΛ.2.1 i (ha hi), + by + intro i hi j hj + exact φsΛ.2.2 i (ha hi) j (ha hj)⟩ + +lemma mem_of_mem_subContraction {S : Finset (Finset (Fin φs.length))} {hs : S ⊆ φsΛ.1} + {a : Finset (Fin φs.length)} (ha : a ∈ (φsΛ.subContraction S hs).1) : a ∈ φsΛ.1 := by + exact hs ha + +/-- Given a Wick contraction `φsΛ`, and a subset `S` of `φsΛ.1`, the Wick contraction + on the uncontracted list `[φsΛ.subContraction S ha]ᵘᶜ` + consisting of the remaining contracted pairs of `φsΛ` not in `S`. -/ +def quotContraction (S : Finset (Finset (Fin φs.length))) (ha : S ⊆ φsΛ.1) : + WickContraction [φsΛ.subContraction S ha]ᵘᶜ.length := + ⟨Finset.filter (fun a => Finset.map uncontractedListEmd a ∈ φsΛ.1) Finset.univ, + by + intro a ha' + simp only [Finset.mem_filter, Finset.mem_univ, true_and] at ha' + simpa using φsΛ.2.1 (Finset.map uncontractedListEmd a) ha', by + intro a ha b hb + simp only [Finset.mem_filter, Finset.mem_univ, true_and] at ha hb + by_cases hab : a = b + · simp [hab] + · simp only [hab, false_or] + have hx := φsΛ.2.2 (Finset.map uncontractedListEmd a) ha (Finset.map uncontractedListEmd b) hb + simp_all⟩ + +lemma mem_of_mem_quotContraction {S : Finset (Finset (Fin φs.length))} {hs : S ⊆ φsΛ.1} + {a : Finset (Fin [φsΛ.subContraction S hs]ᵘᶜ.length)} + (ha : a ∈ (quotContraction S hs).1) : Finset.map uncontractedListEmd a ∈ φsΛ.1 := by + simp only [quotContraction, Finset.mem_filter, Finset.mem_univ, true_and] at ha + exact ha + +lemma mem_subContraction_or_quotContraction {S : Finset (Finset (Fin φs.length))} {hs : S ⊆ φsΛ.1} + {a : Finset (Fin φs.length)} (ha : a ∈ φsΛ.1) : + a ∈ (φsΛ.subContraction S hs).1 ∨ + ∃ a', Finset.map uncontractedListEmd a' = a ∧ a' ∈ (quotContraction S hs).1 := by + by_cases h1 : a ∈ (φsΛ.subContraction S hs).1 + · simp [h1] + simp only [h1, false_or] + simp only [subContraction] at h1 + have h2 := φsΛ.2.1 a ha + rw [@Finset.card_eq_two] at h2 + obtain ⟨i, j, hij, rfl⟩ := h2 + have hi : i ∈ (φsΛ.subContraction S hs).uncontracted := by + rw [mem_uncontracted_iff_not_contracted] + intro p hp + have hp' : p ∈ φsΛ.1 := hs hp + have hp2 := φsΛ.2.2 p hp' {i, j} ha + simp only [subContraction] at hp + rcases hp2 with hp2 | hp2 + · simp_all + simp only [Finset.disjoint_insert_right, Finset.disjoint_singleton_right] at hp2 + exact hp2.1 + have hj : j ∈ (φsΛ.subContraction S hs).uncontracted := by + rw [mem_uncontracted_iff_not_contracted] + intro p hp + have hp' : p ∈ φsΛ.1 := hs hp + have hp2 := φsΛ.2.2 p hp' {i, j} ha + simp only [subContraction] at hp + rcases hp2 with hp2 | hp2 + · simp_all + simp only [Finset.disjoint_insert_right, Finset.disjoint_singleton_right] at hp2 + exact hp2.2 + obtain ⟨i, rfl⟩ := uncontractedListEmd_surjective_mem_uncontracted i hi + obtain ⟨j, rfl⟩ := uncontractedListEmd_surjective_mem_uncontracted j hj + use {i, j} + simp only [Finset.map_insert, Finset.map_singleton, quotContraction, Finset.mem_filter, + Finset.mem_univ, true_and] + exact ha + +@[simp] +lemma subContraction_uncontractedList_get {S : Finset (Finset (Fin φs.length))} {hs : S ⊆ φsΛ.1} + {a : Fin [subContraction S hs]ᵘᶜ.length} : + [subContraction S hs]ᵘᶜ[a] = φs[uncontractedListEmd a] := by + erw [← getElem_uncontractedListEmd] + rfl + +@[simp] +lemma subContraction_fstFieldOfContract {S : Finset (Finset (Fin φs.length))} {hs : S ⊆ φsΛ.1} + (a : (subContraction S hs).1) : + (subContraction S hs).fstFieldOfContract a = + φsΛ.fstFieldOfContract ⟨a.1, mem_of_mem_subContraction a.2⟩:= by + apply eq_fstFieldOfContract_of_mem _ _ _ + (φsΛ.sndFieldOfContract ⟨a.1, mem_of_mem_subContraction a.2⟩) + · have ha := finset_eq_fstFieldOfContract_sndFieldOfContract _ + ⟨a.1, mem_of_mem_subContraction a.2⟩ + simp only at ha + conv_lhs => + rw [ha] + simp + · have ha := finset_eq_fstFieldOfContract_sndFieldOfContract _ + ⟨a.1, mem_of_mem_subContraction a.2⟩ + simp only at ha + conv_lhs => + rw [ha] + simp + · exact fstFieldOfContract_lt_sndFieldOfContract φsΛ ⟨↑a, mem_of_mem_subContraction a.property⟩ + +@[simp] +lemma subContraction_sndFieldOfContract {S : Finset (Finset (Fin φs.length))} {hs : S ⊆ φsΛ.1} + (a : (subContraction S hs).1) : + (subContraction S hs).sndFieldOfContract a = + φsΛ.sndFieldOfContract ⟨a.1, mem_of_mem_subContraction a.2⟩:= by + apply eq_sndFieldOfContract_of_mem _ _ + (φsΛ.fstFieldOfContract ⟨a.1, mem_of_mem_subContraction a.2⟩) + · have ha := finset_eq_fstFieldOfContract_sndFieldOfContract _ + ⟨a.1, mem_of_mem_subContraction a.2⟩ + simp only at ha + conv_lhs => + rw [ha] + simp + · have ha := finset_eq_fstFieldOfContract_sndFieldOfContract _ + ⟨a.1, mem_of_mem_subContraction a.2⟩ + simp only at ha + conv_lhs => + rw [ha] + simp + · exact fstFieldOfContract_lt_sndFieldOfContract φsΛ ⟨↑a, mem_of_mem_subContraction a.property⟩ + +@[simp] +lemma quotContraction_fstFieldOfContract_uncontractedListEmd {S : Finset (Finset (Fin φs.length))} + {hs : S ⊆ φsΛ.1} (a : (quotContraction S hs).1) : + uncontractedListEmd ((quotContraction S hs).fstFieldOfContract a) = + (φsΛ.fstFieldOfContract + ⟨Finset.map uncontractedListEmd a.1, mem_of_mem_quotContraction a.2⟩) := by + symm + apply eq_fstFieldOfContract_of_mem _ _ _ + (uncontractedListEmd ((quotContraction S hs).sndFieldOfContract a)) + · simp only [Finset.mem_map', fstFieldOfContract_mem] + · simp + · apply uncontractedListEmd_strictMono + exact fstFieldOfContract_lt_sndFieldOfContract (quotContraction S hs) a + +@[simp] +lemma quotContraction_sndFieldOfContract_uncontractedListEmd {S : Finset (Finset (Fin φs.length))} + {hs : S ⊆ φsΛ.1} (a : (quotContraction S hs).1) : + uncontractedListEmd ((quotContraction S hs).sndFieldOfContract a) = + (φsΛ.sndFieldOfContract + ⟨Finset.map uncontractedListEmd a.1, mem_of_mem_quotContraction a.2⟩) := by + symm + apply eq_sndFieldOfContract_of_mem _ _ + (uncontractedListEmd ((quotContraction S hs).fstFieldOfContract a)) + · simp only [Finset.mem_map', fstFieldOfContract_mem] + · simp + · apply uncontractedListEmd_strictMono + exact fstFieldOfContract_lt_sndFieldOfContract (quotContraction S hs) a + +lemma quotContraction_gradingCompliant {S : Finset (Finset (Fin φs.length))} {hs : S ⊆ φsΛ.1} + (hsΛ : φsΛ.GradingCompliant) : + GradingCompliant [φsΛ.subContraction S hs]ᵘᶜ (quotContraction S hs) := by + simp only [GradingCompliant, Fin.getElem_fin, Subtype.forall] + intro a ha + erw [subContraction_uncontractedList_get] + erw [subContraction_uncontractedList_get] + simp only [quotContraction_fstFieldOfContract_uncontractedListEmd, Fin.getElem_fin, + quotContraction_sndFieldOfContract_uncontractedListEmd] + apply hsΛ + +lemma mem_quotContraction_iff {S : Finset (Finset (Fin φs.length))} {hs : S ⊆ φsΛ.1} + {a : Finset (Fin [φsΛ.subContraction S hs]ᵘᶜ.length)} : + a ∈ (quotContraction S hs).1 ↔ a.map uncontractedListEmd ∈ φsΛ.1 + ∧ a.map uncontractedListEmd ∉ (subContraction S hs).1 := by + apply Iff.intro + · intro h + apply And.intro + · exact mem_of_mem_quotContraction h + · exact uncontractedListEmd_finset_not_mem _ + · intro h + have h2 := mem_subContraction_or_quotContraction (S := S) (hs := hs) h.1 + simp_all + +end WickContraction diff --git a/HepLean/PerturbationTheory/WickContraction/TimeCond.lean b/HepLean/PerturbationTheory/WickContraction/TimeCond.lean new file mode 100644 index 00000000..3aa95a5f --- /dev/null +++ b/HepLean/PerturbationTheory/WickContraction/TimeCond.lean @@ -0,0 +1,554 @@ +/- +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.TimeContract +import HepLean.PerturbationTheory.WickContraction.Join +import HepLean.PerturbationTheory.Algebras.FieldOpAlgebra.TimeContraction +/-! + +# Time contractions + +-/ + +open FieldSpecification +variable {𝓕 : FieldSpecification} + +namespace WickContraction +variable {n : ℕ} (c : WickContraction n) +open HepLean.List +open FieldOpAlgebra + +/-- The condition on a Wick contraction which is true iff and only if every contraction + is between two fields of equal time. -/ +def EqTimeOnly {φs : List 𝓕.States} (φsΛ : WickContraction φs.length) : Prop := + ∀ (i j), {i, j} ∈ φsΛ.1 → timeOrderRel φs[i] φs[j] +noncomputable section + +instance {φs : List 𝓕.States} (φsΛ : WickContraction φs.length) : + Decidable (EqTimeOnly φsΛ) := + inferInstanceAs (Decidable (∀ (i j), {i, j} ∈ φsΛ.1 → timeOrderRel φs[i] φs[j])) + +namespace EqTimeOnly +variable {φs : List 𝓕.States} (φsΛ : WickContraction φs.length) + +lemma timeOrderRel_of_eqTimeOnly_pair {i j : Fin φs.length} (h : {i, j} ∈ φsΛ.1) + (hc : EqTimeOnly φsΛ) : + timeOrderRel φs[i] φs[j] := by + have h' := hc + simp only [EqTimeOnly, ne_eq, Fin.getElem_fin, Finset.mem_filter, Finset.mem_univ, + true_and] at h' + exact h' i j h + +lemma timeOrderRel_both_of_eqTimeOnly {i j : Fin φs.length} (h : {i, j} ∈ φsΛ.1) + (hc : EqTimeOnly φsΛ) : + timeOrderRel φs[i] φs[j] ∧ timeOrderRel φs[j] φs[i] := by + apply And.intro + · exact timeOrderRel_of_eqTimeOnly_pair φsΛ h hc + · apply timeOrderRel_of_eqTimeOnly_pair φsΛ _ hc + rw [@Finset.pair_comm] + exact h + +lemma eqTimeOnly_iff_forall_finset {φs : List 𝓕.States} (φsΛ : WickContraction φs.length) : + φsΛ.EqTimeOnly ↔ ∀ (a : φsΛ.1), + timeOrderRel (φs[φsΛ.fstFieldOfContract a]) (φs[φsΛ.sndFieldOfContract a]) + ∧ timeOrderRel (φs[φsΛ.sndFieldOfContract a]) (φs[φsΛ.fstFieldOfContract a]) := by + apply Iff.intro + · intro h a + apply timeOrderRel_both_of_eqTimeOnly φsΛ _ h + rw [← finset_eq_fstFieldOfContract_sndFieldOfContract] + simp + · intro h + simp only [EqTimeOnly, Fin.getElem_fin, Finset.mem_filter, Finset.mem_univ, + true_and] + intro i j h1 + have h' := h ⟨{i, j}, h1⟩ + by_cases hij: i < j + · have hi : φsΛ.fstFieldOfContract ⟨{i, j}, h1⟩ = i := by + apply eq_fstFieldOfContract_of_mem _ _ i j + · simp + · simp + · exact hij + have hj : φsΛ.sndFieldOfContract ⟨{i, j}, h1⟩ = j := by + apply eq_sndFieldOfContract_of_mem _ _ i j + · simp + · simp + · exact hij + simp_all + · have hij : i ≠ j := by + by_contra hij + subst hij + have h2 := φsΛ.2.1 {i, i} h1 + simp at h2 + have hj : φsΛ.fstFieldOfContract ⟨{i, j}, h1⟩ = j := by + apply eq_fstFieldOfContract_of_mem _ _ j i + · simp + · simp + · omega + have hi : φsΛ.sndFieldOfContract ⟨{i, j}, h1⟩ = i := by + apply eq_sndFieldOfContract_of_mem _ _ j i + · simp + · simp + · omega + simp_all + +@[simp] +lemma empty_mem {φs : List 𝓕.States} : empty (n := φs.length).EqTimeOnly := by + rw [eqTimeOnly_iff_forall_finset] + simp [empty] + +lemma staticContract_eq_timeContract_of_eqTimeOnly (h : φsΛ.EqTimeOnly) : + φsΛ.staticContract = φsΛ.timeContract := by + simp only [staticContract, timeContract] + apply congrArg + funext a + ext + simp only [List.get_eq_getElem] + rw [timeContract_of_timeOrderRel] + apply timeOrderRel_of_eqTimeOnly_pair φsΛ + rw [← finset_eq_fstFieldOfContract_sndFieldOfContract] + exact a.2 + exact h + +lemma eqTimeOnly_congr {φs φs' : List 𝓕.States} (h : φs = φs') (φsΛ : WickContraction φs.length) : + (congr (by simp [h]) φsΛ).EqTimeOnly (φs := φs') ↔ φsΛ.EqTimeOnly := by + subst h + simp + +lemma quotContraction_eqTimeOnly {φs : List 𝓕.States} {φsΛ : WickContraction φs.length} + (h : φsΛ.EqTimeOnly) (S : Finset (Finset (Fin φs.length))) (ha : S ⊆ φsΛ.1) : + (φsΛ.quotContraction S ha).EqTimeOnly := by + rw [eqTimeOnly_iff_forall_finset] + intro a + simp only [Fin.getElem_fin] + erw [subContraction_uncontractedList_get] + erw [subContraction_uncontractedList_get] + simp only [quotContraction_fstFieldOfContract_uncontractedListEmd, Fin.getElem_fin, + quotContraction_sndFieldOfContract_uncontractedListEmd] + rw [eqTimeOnly_iff_forall_finset] at h + apply h + +lemma exists_join_singleton_of_card_ge_zero {φs : List 𝓕.States} (φsΛ : WickContraction φs.length) + (h : 0 < φsΛ.1.card) (h1 : φsΛ.EqTimeOnly) : + ∃ (i j : Fin φs.length) (h : i < j) (φsucΛ : WickContraction [singleton h]ᵘᶜ.length), + φsΛ = join (singleton h) φsucΛ ∧ (timeOrderRel φs[i] φs[j] ∧ timeOrderRel φs[j] φs[i]) + ∧ φsucΛ.EqTimeOnly ∧ φsucΛ.1.card + 1 = φsΛ.1.card := by + obtain ⟨a, ha⟩ := exists_contraction_pair_of_card_ge_zero φsΛ h + use φsΛ.fstFieldOfContract ⟨a, ha⟩ + use φsΛ.sndFieldOfContract ⟨a, ha⟩ + use φsΛ.fstFieldOfContract_lt_sndFieldOfContract ⟨a, ha⟩ + let φsucΛ : + WickContraction [singleton (φsΛ.fstFieldOfContract_lt_sndFieldOfContract ⟨a, ha⟩)]ᵘᶜ.length := + congr (by simp [← subContraction_singleton_eq_singleton]) + (φsΛ.quotContraction {a} (by simpa using ha)) + use φsucΛ + simp only [Fin.getElem_fin] + apply And.intro + · have h1 := join_congr (subContraction_singleton_eq_singleton _ ⟨a, ha⟩).symm (φsucΛ := φsucΛ) + simp only [id_eq, eq_mpr_eq_cast, h1, congr_trans_apply, congr_refl, φsucΛ] + rw [join_sub_quot] + · apply And.intro + · apply timeOrderRel_both_of_eqTimeOnly φsΛ _ h1 + rw [← finset_eq_fstFieldOfContract_sndFieldOfContract] + simp [ha] + apply And.intro + · simp only [id_eq, eq_mpr_eq_cast, φsucΛ] + rw [eqTimeOnly_congr (φs := [(φsΛ.subContraction {a} (by simpa using ha))]ᵘᶜ)] + simp only [id_eq, eq_mpr_eq_cast] + exact quotContraction_eqTimeOnly h1 _ _ + rw [← subContraction_singleton_eq_singleton] + · simp only [id_eq, eq_mpr_eq_cast, card_congr, φsucΛ] + have h1 := subContraction_card_plus_quotContraction_card_eq _ {a} (by simpa using ha) + simp only [subContraction, Finset.card_singleton, id_eq, eq_mpr_eq_cast] at h1 + omega + +lemma timeOrder_timeContract_mul_of_eqTimeOnly_mid_induction {φs : List 𝓕.States} + (φsΛ : WickContraction φs.length) + (hl : φsΛ.EqTimeOnly) (a b: 𝓕.FieldOpAlgebra) : (n : ℕ) → (hn : φsΛ.1.card = n) → + 𝓣(a * φsΛ.timeContract.1 * b) = φsΛ.timeContract.1 * 𝓣(a * b) + | 0, hn => by + rw [@card_zero_iff_empty] at hn + subst hn + simp + | Nat.succ n, hn => by + obtain ⟨i, j, hij, φsucΛ, rfl, h2, h3, h4⟩ := + exists_join_singleton_of_card_ge_zero φsΛ (by simp [hn]) hl + rw [join_timeContract] + rw [singleton_timeContract] + simp only [Fin.getElem_fin, MulMemClass.coe_mul] + trans timeOrder (a * FieldOpAlgebra.timeContract φs[↑i] φs[↑j] * (φsucΛ.timeContract.1 * b)) + simp only [mul_assoc, Fin.getElem_fin] + rw [timeOrder_timeContract_eq_time_mid] + have ih := timeOrder_timeContract_mul_of_eqTimeOnly_mid_induction φsucΛ h3 a b n (by omega) + rw [← mul_assoc, ih] + simp only [Fin.getElem_fin, mul_assoc] + simp_all only [Nat.succ_eq_add_one, Fin.getElem_fin, add_left_inj] + simp_all + +lemma timeOrder_timeContract_mul_of_eqTimeOnly_mid {φs : List 𝓕.States} + (φsΛ : WickContraction φs.length) + (hl : φsΛ.EqTimeOnly) (a b : 𝓕.FieldOpAlgebra) : + 𝓣(a * φsΛ.timeContract.1 * b) = φsΛ.timeContract.1 * 𝓣(a * b) := by + exact timeOrder_timeContract_mul_of_eqTimeOnly_mid_induction φsΛ hl a b φsΛ.1.card rfl + +lemma timeOrder_timeContract_mul_of_eqTimeOnly_left {φs : List 𝓕.States} + (φsΛ : WickContraction φs.length) + (hl : φsΛ.EqTimeOnly) (b : 𝓕.FieldOpAlgebra) : + 𝓣(φsΛ.timeContract.1 * b) = φsΛ.timeContract.1 * 𝓣(b) := by + trans 𝓣(1 * φsΛ.timeContract.1 * b) + simp only [one_mul] + rw [timeOrder_timeContract_mul_of_eqTimeOnly_mid φsΛ hl] + simp + +lemma exists_join_singleton_of_not_eqTimeOnly {φs : List 𝓕.States} (φsΛ : WickContraction φs.length) + (h1 : ¬ φsΛ.EqTimeOnly) : + ∃ (i j : Fin φs.length) (h : i < j) (φsucΛ : WickContraction [singleton h]ᵘᶜ.length), + φsΛ = join (singleton h) φsucΛ ∧ (¬ timeOrderRel φs[i] φs[j] ∨ ¬ timeOrderRel φs[j] φs[i]) := by + rw [eqTimeOnly_iff_forall_finset] at h1 + simp only [Fin.getElem_fin, Subtype.forall, not_forall, not_and] at h1 + obtain ⟨a, ha, hr⟩ := h1 + use φsΛ.fstFieldOfContract ⟨a, ha⟩ + use φsΛ.sndFieldOfContract ⟨a, ha⟩ + use φsΛ.fstFieldOfContract_lt_sndFieldOfContract ⟨a, ha⟩ + let φsucΛ : + WickContraction [singleton (φsΛ.fstFieldOfContract_lt_sndFieldOfContract ⟨a, ha⟩)]ᵘᶜ.length := + congr (by simp [← subContraction_singleton_eq_singleton]) + (φsΛ.quotContraction {a} (by simpa using ha)) + use φsucΛ + simp only [Fin.getElem_fin] + apply And.intro + · have h1 := join_congr (subContraction_singleton_eq_singleton _ ⟨a, ha⟩).symm (φsucΛ := φsucΛ) + simp only [id_eq, eq_mpr_eq_cast, h1, congr_trans_apply, congr_refl, φsucΛ] + rw [join_sub_quot] + · by_cases h1 : timeOrderRel φs[↑(φsΛ.fstFieldOfContract ⟨a, ha⟩)] + φs[↑(φsΛ.sndFieldOfContract ⟨a, ha⟩)] + · simp_all [h1] + · simp_all [h1] + +lemma timeOrder_timeContract_of_not_eqTimeOnly {φs : List 𝓕.States} + (φsΛ : WickContraction φs.length) + (hl : ¬ φsΛ.EqTimeOnly) : 𝓣(φsΛ.timeContract.1) = 0 := by + obtain ⟨i, j, hij, φsucΛ, rfl, hr⟩ := exists_join_singleton_of_not_eqTimeOnly φsΛ hl + rw [join_timeContract] + rw [singleton_timeContract] + simp only [Fin.getElem_fin, MulMemClass.coe_mul] + rw [timeOrder_timeOrder_left] + rw [timeOrder_timeContract_neq_time] + simp only [zero_mul, map_zero] + simp_all only [Fin.getElem_fin, not_and] + intro h + simp_all + +lemma timeOrder_staticContract_of_not_mem {φs : List 𝓕.States} (φsΛ : WickContraction φs.length) + (hl : ¬ φsΛ.EqTimeOnly) : 𝓣(φsΛ.staticContract.1) = 0 := by + obtain ⟨i, j, hij, φsucΛ, rfl, hr⟩ := exists_join_singleton_of_not_eqTimeOnly φsΛ hl + rw [join_staticContract] + simp only [MulMemClass.coe_mul] + rw [singleton_staticContract] + rw [timeOrder_timeOrder_left] + rw [timeOrder_superCommute_anPart_ofFieldOp_neq_time] + simp only [zero_mul, map_zero] + intro h + simp_all + +end EqTimeOnly + +/-- The condition on a Wick contraction which is true if it has at least one contraction + which is between two equal time fields. -/ +def HaveEqTime {φs : List 𝓕.States} (φsΛ : WickContraction φs.length) : Prop := + ∃ (i j : Fin φs.length) (h : {i, j} ∈ φsΛ.1), + timeOrderRel φs[i] φs[j] ∧ timeOrderRel φs[j] φs[i] + +noncomputable instance {φs : List 𝓕.States} (φsΛ : WickContraction φs.length) : + Decidable (HaveEqTime φsΛ) := + inferInstanceAs (Decidable (∃ (i j : Fin φs.length) + (h : ({i, j} : Finset (Fin φs.length)) ∈ φsΛ.1), + timeOrderRel φs[i] φs[j] ∧ timeOrderRel φs[j] φs[i])) + +lemma haveEqTime_iff_finset {φs : List 𝓕.States} (φsΛ : WickContraction φs.length) : + HaveEqTime φsΛ ↔ ∃ (a : Finset (Fin φs.length)) (h : a ∈ φsΛ.1), + timeOrderRel φs[φsΛ.fstFieldOfContract ⟨a, h⟩] φs[φsΛ.sndFieldOfContract ⟨a, h⟩] + ∧ timeOrderRel φs[φsΛ.sndFieldOfContract ⟨a, h⟩] φs[φsΛ.fstFieldOfContract ⟨a, h⟩] := by + simp only [HaveEqTime, Fin.getElem_fin, exists_and_left, exists_prop] + apply Iff.intro + · intro h + obtain ⟨i, j, hij, h1, h2⟩ := h + use {i, j}, h1 + by_cases hij : i < j + · have h1n := eq_fstFieldOfContract_of_mem φsΛ ⟨{i,j}, h1⟩ i j (by simp) (by simp) hij + have h2n := eq_sndFieldOfContract_of_mem φsΛ ⟨{i,j}, h1⟩ i j (by simp) (by simp) hij + simp only [h1n, h2n] + simp_all only [forall_true_left, true_and] + · have hineqj : i ≠ j := by + by_contra hineqj + subst hineqj + have h2 := φsΛ.2.1 {i, i} h1 + simp_all + have hji : j < i := by omega + have h1n := eq_fstFieldOfContract_of_mem φsΛ ⟨{i,j}, h1⟩ j i (by simp) (by simp) hji + have h2n := eq_sndFieldOfContract_of_mem φsΛ ⟨{i,j}, h1⟩ j i (by simp) (by simp) hji + simp only [h1n, h2n] + simp_all + · intro h + obtain ⟨a, h1, h2, h3⟩ := h + use φsΛ.fstFieldOfContract ⟨a, h1⟩ + use φsΛ.sndFieldOfContract ⟨a, h1⟩ + simp_all only [and_true, true_and] + rw [← finset_eq_fstFieldOfContract_sndFieldOfContract] + exact h1 + +@[simp] +lemma empty_not_haveEqTime {φs : List 𝓕.States} : + ¬ HaveEqTime (empty : WickContraction φs.length) := by + rw [haveEqTime_iff_finset] + simp [empty] + +/-- Given a Wick contraction the subset of contracted pairs between eqaul time fields. -/ +def eqTimeContractSet {φs : List 𝓕.States} (φsΛ : WickContraction φs.length) : + Finset (Finset (Fin φs.length)) := + Finset.univ.filter (fun a => + a ∈ φsΛ.1 ∧ ∀ (h : a ∈ φsΛ.1), + timeOrderRel φs[φsΛ.fstFieldOfContract ⟨a, h⟩] φs[φsΛ.sndFieldOfContract ⟨a, h⟩] + ∧ timeOrderRel φs[φsΛ.sndFieldOfContract ⟨a, h⟩] φs[φsΛ.fstFieldOfContract ⟨a, h⟩]) + +lemma eqTimeContractSet_subset {φs : List 𝓕.States} (φsΛ : WickContraction φs.length) : + eqTimeContractSet φsΛ ⊆ φsΛ.1 := by + simp only [eqTimeContractSet, Fin.getElem_fin] + intro a + simp only [Finset.mem_filter, Finset.mem_univ, true_and, and_imp] + intro h _ + exact h + +lemma mem_of_mem_eqTimeContractSet{φs : List 𝓕.States} {φsΛ : WickContraction φs.length} + {a : Finset (Fin φs.length)} (h : a ∈ eqTimeContractSet φsΛ) : a ∈ φsΛ.1 := by + simp only [eqTimeContractSet, Fin.getElem_fin, Finset.mem_filter, Finset.mem_univ, true_and] at h + exact h.1 + +lemma join_eqTimeContractSet {φs : List 𝓕.States} (φsΛ : WickContraction φs.length) + (φsucΛ : WickContraction [φsΛ]ᵘᶜ.length) : + eqTimeContractSet (join φsΛ φsucΛ) = φsΛ.eqTimeContractSet ∪ + φsucΛ.eqTimeContractSet.map (Finset.mapEmbedding uncontractedListEmd).toEmbedding := by + ext a + apply Iff.intro + · intro h + have hmem := mem_of_mem_eqTimeContractSet h + have ht := joinLiftLeft_or_joinLiftRight_of_mem_join (φsucΛ := φsucΛ) _ hmem + rcases ht with ht | ht + · obtain ⟨b, rfl⟩ := ht + simp only [Finset.le_eq_subset, Finset.mem_union, Finset.mem_map, + RelEmbedding.coe_toEmbedding] + left + simp only [eqTimeContractSet, Fin.getElem_fin, Finset.mem_filter, Finset.mem_univ, true_and] + apply And.intro (by simp [joinLiftLeft]) + intro h' + simp only [eqTimeContractSet, Fin.getElem_fin, Finset.mem_filter, Finset.mem_univ, + Finset.coe_mem, Subtype.coe_eta, join_fstFieldOfContract_joinLiftLeft, + join_sndFieldOfContract_joinLift, forall_true_left, true_and] at h + exact h + · obtain ⟨b, rfl⟩ := ht + simp only [Finset.le_eq_subset, Finset.mem_union, Finset.mem_map, + RelEmbedding.coe_toEmbedding] + right + use b + rw [Finset.mapEmbedding_apply] + simp only [joinLiftRight, and_true] + simpa [eqTimeContractSet] using h + · intro h + simp only [Finset.le_eq_subset, Finset.mem_union, Finset.mem_map, + RelEmbedding.coe_toEmbedding] at h + rcases h with h | h + · simp only [eqTimeContractSet, Fin.getElem_fin, Finset.mem_filter, Finset.mem_univ, true_and] + simp only [eqTimeContractSet, Fin.getElem_fin, Finset.mem_filter, Finset.mem_univ, + true_and] at h + apply And.intro + · simp [join, h.1] + · intro h' + have h2 := h.2 h.1 + exact h2 + · simp only [eqTimeContractSet, Fin.getElem_fin, Finset.mem_filter, Finset.mem_univ, true_and] + simp only [eqTimeContractSet, Fin.getElem_fin, Finset.mem_filter, Finset.mem_univ, + true_and] at h + obtain ⟨b, h1, h2, rfl⟩ := h + apply And.intro + · simp [join, h1] + · intro h' + have h2 := h1.2 h1.1 + have hj : ⟨(Finset.mapEmbedding uncontractedListEmd) b, h'⟩ + = joinLiftRight ⟨b, h1.1⟩ := by rfl + simp only [hj, join_fstFieldOfContract_joinLiftRight, getElem_uncontractedListEmd, + join_sndFieldOfContract_joinLiftRight] + simpa using h2 + +lemma eqTimeContractSet_of_not_haveEqTime {φs : List 𝓕.States} {φsΛ : WickContraction φs.length} + (h : ¬ HaveEqTime φsΛ) : eqTimeContractSet φsΛ = ∅ := by + ext a + simp only [Finset.not_mem_empty, iff_false] + by_contra hn + rw [haveEqTime_iff_finset] at h + simp only [Fin.getElem_fin, not_exists, not_and] at h + simp only [eqTimeContractSet, Fin.getElem_fin, Finset.mem_filter, Finset.mem_univ, true_and] at hn + have h2 := hn.2 hn.1 + simp_all + +lemma eqTimeContractSet_of_mem_eqTimeOnly {φs : List 𝓕.States} {φsΛ : WickContraction φs.length} + (h : φsΛ.EqTimeOnly) : eqTimeContractSet φsΛ = φsΛ.1 := by + ext a + simp only [eqTimeContractSet, Fin.getElem_fin, Finset.mem_filter, Finset.mem_univ, true_and, + and_iff_left_iff_imp, imp_forall_iff_forall] + rw [EqTimeOnly.eqTimeOnly_iff_forall_finset] at h + exact fun h_1 => h ⟨a, h_1⟩ + +lemma subContraction_eqTimeContractSet_eqTimeOnly {φs : List 𝓕.States} + (φsΛ : WickContraction φs.length) : + (φsΛ.subContraction (eqTimeContractSet φsΛ) (eqTimeContractSet_subset φsΛ)).EqTimeOnly := by + rw [EqTimeOnly.eqTimeOnly_iff_forall_finset] + intro a + have ha2 := a.2 + simp only [subContraction, eqTimeContractSet, Fin.getElem_fin, Finset.mem_filter, Finset.mem_univ, + true_and] at ha2 + simp only [subContraction_fstFieldOfContract, Fin.getElem_fin, subContraction_sndFieldOfContract] + exact ha2.2 ha2.1 + +lemma pair_mem_eqTimeContractSet_iff {φs : List 𝓕.States} {i j : Fin φs.length} + (φsΛ : WickContraction φs.length) (h : {i, j} ∈ φsΛ.1) : + {i, j} ∈ φsΛ.eqTimeContractSet ↔ timeOrderRel φs[i] φs[j] ∧ timeOrderRel φs[j] φs[i] := by + simp only [eqTimeContractSet, Fin.getElem_fin, Finset.mem_filter, Finset.mem_univ, true_and] + by_cases hij : i < j + · have h1 := eq_fstFieldOfContract_of_mem φsΛ ⟨{i,j}, h⟩ i j (by simp) (by simp) hij + have h2 := eq_sndFieldOfContract_of_mem φsΛ ⟨{i,j}, h⟩ i j (by simp) (by simp) hij + simp only [h1, h2] + simp_all only [forall_true_left, true_and] + · have hineqj : i ≠ j := by + by_contra hineqj + subst hineqj + have h2 := φsΛ.2.1 {i, i} h + simp_all + have hji : j < i := by omega + have h1 := eq_fstFieldOfContract_of_mem φsΛ ⟨{i,j}, h⟩ j i (by simp) (by simp) hji + have h2 := eq_sndFieldOfContract_of_mem φsΛ ⟨{i,j}, h⟩ j i (by simp) (by simp) hji + simp only [h1, h2] + simp_all only [not_lt, ne_eq, forall_true_left, true_and] + apply Iff.intro + · intro a + simp_all only [and_self] + · intro a + simp_all only [and_self] + +lemma subContraction_eqTimeContractSet_not_empty_of_haveEqTime + {φs : List 𝓕.States} (φsΛ : WickContraction φs.length) (h : HaveEqTime φsΛ) : + φsΛ.subContraction (eqTimeContractSet φsΛ) (eqTimeContractSet_subset φsΛ) ≠ empty := by + simp only [ne_eq] + erw [Subtype.eq_iff] + simp only [subContraction, empty] + rw [Finset.eq_empty_iff_forall_not_mem] + simp only [HaveEqTime, Fin.getElem_fin, exists_and_left, exists_prop] at h + obtain ⟨i, j, hij, h1, h2⟩ := h + simp only [not_forall, Decidable.not_not] + use {i, j} + rw [pair_mem_eqTimeContractSet_iff] + simp_all only [Fin.getElem_fin, and_self] + exact h1 + +lemma quotContraction_eqTimeContractSet_not_haveEqTime {φs : List 𝓕.States} + (φsΛ : WickContraction φs.length) : + ¬ HaveEqTime (φsΛ.quotContraction (eqTimeContractSet φsΛ) (eqTimeContractSet_subset φsΛ)) := by + rw [haveEqTime_iff_finset] + simp only [Fin.getElem_fin, not_exists, not_and] + intro a ha + erw [subContraction_uncontractedList_get] + erw [subContraction_uncontractedList_get] + simp only [quotContraction_fstFieldOfContract_uncontractedListEmd, Fin.getElem_fin, + quotContraction_sndFieldOfContract_uncontractedListEmd] + simp only [quotContraction, Finset.mem_filter, Finset.mem_univ, true_and] at ha + have hn' : Finset.map uncontractedListEmd a ∉ + (φsΛ.subContraction (eqTimeContractSet φsΛ) (eqTimeContractSet_subset φsΛ)).1 := by + exact uncontractedListEmd_finset_not_mem a + simp only [subContraction, eqTimeContractSet, Fin.getElem_fin, Finset.mem_filter, Finset.mem_univ, + true_and, not_and, not_forall] at hn' + have hn'' := hn' ha + obtain ⟨h, h1⟩ := hn'' + simp_all + +lemma join_haveEqTime_of_eqTimeOnly_nonEmpty {φs : List 𝓕.States} (φsΛ : WickContraction φs.length) + (h1 : φsΛ.EqTimeOnly) (h2 : φsΛ ≠ empty) + (φsucΛ : WickContraction [φsΛ]ᵘᶜ.length) : + HaveEqTime (join φsΛ φsucΛ) := by + simp only [HaveEqTime, Fin.getElem_fin, join, Finset.le_eq_subset, Finset.mem_union, + Finset.mem_map, RelEmbedding.coe_toEmbedding, exists_and_left, exists_prop] + simp only [EqTimeOnly, Fin.getElem_fin, Finset.mem_filter, Finset.mem_univ, + true_and] at h1 + obtain ⟨i, j, h⟩ := exists_pair_of_not_eq_empty _ h2 + use i, j + simp_all only [ne_eq, true_or, true_and] + apply h1 j i + rw [Finset.pair_comm] + exact h + +lemma hasEqTimeEquiv_ext_sigma {φs : List 𝓕.States} {x1 x2 : + Σ (φsΛ : {φsΛ : WickContraction φs.length // φsΛ.EqTimeOnly ∧ φsΛ ≠ empty}), + {φssucΛ : WickContraction [φsΛ.1]ᵘᶜ.length // ¬ HaveEqTime φssucΛ}} + (h1 : x1.1.1 = x2.1.1) (h2 : x1.2.1 = congr (by simp [h1]) x2.2.1) : x1 = x2 := by + match x1, x2 with + | ⟨⟨a1, b1⟩, ⟨c1, d1⟩⟩, ⟨⟨a2, b2⟩, ⟨c2, d2⟩⟩ => + simp only at h1 + subst h1 + simp only [ne_eq, congr_refl] at h2 + simp [h2] + +/-- The equivalence which seperates a Wick contraction which has an equal time contraction +into a non-empty contraction only between equal-time fields and a Wick contraction which +does not have equal time contractions. -/ +def hasEqTimeEquiv (φs : List 𝓕.States) : + {φsΛ : WickContraction φs.length // HaveEqTime φsΛ} ≃ + Σ (φsΛ : {φsΛ : WickContraction φs.length // φsΛ.EqTimeOnly ∧ φsΛ ≠ empty}), + {φssucΛ : WickContraction [φsΛ.1]ᵘᶜ.length // ¬ HaveEqTime φssucΛ} where + toFun φsΛ := ⟨⟨φsΛ.1.subContraction (eqTimeContractSet φsΛ.1) (eqTimeContractSet_subset φsΛ.1), + subContraction_eqTimeContractSet_eqTimeOnly φsΛ.1, + subContraction_eqTimeContractSet_not_empty_of_haveEqTime φsΛ.1 φsΛ.2⟩, + ⟨φsΛ.1.quotContraction (eqTimeContractSet φsΛ.1) (eqTimeContractSet_subset φsΛ.1), + quotContraction_eqTimeContractSet_not_haveEqTime φsΛ.1⟩⟩ + invFun φsΛ := ⟨join φsΛ.1.1 φsΛ.2.1, + join_haveEqTime_of_eqTimeOnly_nonEmpty φsΛ.1.1 φsΛ.1.2.1 φsΛ.1.2.2 φsΛ.2⟩ + left_inv φsΛ := by + match φsΛ with + | ⟨φsΛ, h1, h2⟩ => + simp only [ne_eq, Fin.getElem_fin, Subtype.mk.injEq] + exact join_sub_quot φsΛ φsΛ.eqTimeContractSet (eqTimeContractSet_subset φsΛ) + right_inv φsΛ' := by + match φsΛ' with + | ⟨⟨φsΛ, h1⟩, ⟨φsucΛ, h2⟩⟩ => + have hs : subContraction (φsΛ.join φsucΛ).eqTimeContractSet + (eqTimeContractSet_subset (φsΛ.join φsucΛ)) = φsΛ := by + apply Subtype.ext + ext a + simp only [subContraction] + rw [join_eqTimeContractSet] + rw [eqTimeContractSet_of_not_haveEqTime h2] + simp only [Finset.le_eq_subset, ne_eq, Finset.map_empty, Finset.union_empty] + rw [eqTimeContractSet_of_mem_eqTimeOnly h1.1] + refine hasEqTimeEquiv_ext_sigma ?_ ?_ + · simp only [ne_eq] + exact hs + · simp only [ne_eq] + apply Subtype.ext + ext a + simp only [quotContraction, Finset.mem_filter, Finset.mem_univ, true_and] + rw [mem_congr_iff] + rw [mem_join_right_iff] + simp only [ne_eq] + rw [uncontractedListEmd_congr hs] + rw [Finset.map_map] + +lemma sum_haveEqTime (φs : List 𝓕.States) + (f : WickContraction φs.length → M) [AddCommMonoid M]: + ∑ (φsΛ : {φsΛ : WickContraction φs.length // HaveEqTime φsΛ}), f φsΛ = + ∑ (φsΛ : {φsΛ : WickContraction φs.length // φsΛ.EqTimeOnly ∧ φsΛ ≠ empty}), + ∑ (φssucΛ : {φssucΛ : WickContraction [φsΛ.1]ᵘᶜ.length // ¬ HaveEqTime φssucΛ}), + f (join φsΛ.1 φssucΛ.1) := by + rw [← (hasEqTimeEquiv φs).symm.sum_comp] + erw [Finset.sum_sigma] + rfl + +end +end WickContraction diff --git a/HepLean/PerturbationTheory/WickContraction/TimeContract.lean b/HepLean/PerturbationTheory/WickContraction/TimeContract.lean index 05a5e674..96d166ea 100644 --- a/HepLean/PerturbationTheory/WickContraction/TimeContract.lean +++ b/HepLean/PerturbationTheory/WickContraction/TimeContract.lean @@ -70,6 +70,12 @@ lemma timeConract_insertAndContract_some ext a simp +@[simp] +lemma timeContract_empty (φs : List 𝓕.States) : + (@empty φs.length).timeContract = 1 := by + rw [timeContract, empty] + simp + open FieldStatistic lemma timeConract_insertAndContract_some_eq_mul_contractStateAtIndex_lt diff --git a/HepLean/PerturbationTheory/WickContraction/Uncontracted.lean b/HepLean/PerturbationTheory/WickContraction/Uncontracted.lean index 6920957d..ec894108 100644 --- a/HepLean/PerturbationTheory/WickContraction/Uncontracted.lean +++ b/HepLean/PerturbationTheory/WickContraction/Uncontracted.lean @@ -24,6 +24,10 @@ lemma congr_uncontracted {n m : ℕ} (c : WickContraction n) (h : n = m) : subst h simp +lemma getDual?_eq_none_iff_mem_uncontracted (i : Fin n) : + c.getDual? i = none ↔ i ∈ c.uncontracted := by + simp [uncontracted] + /-- The equivalence of `Option c.uncontracted` for two propositionally equal Wick contractions. -/ def uncontractedCongr {c c': WickContraction n} (h : c = c') : Option c.uncontracted ≃ Option c'.uncontracted := @@ -64,4 +68,40 @@ lemma mem_uncontracted_iff_not_contracted (i : Fin n) : apply h {i, j} hj simp +lemma mem_uncontracted_empty (i : Fin n) : i ∈ empty.uncontracted := by + rw [@mem_uncontracted_iff_not_contracted] + intro p hp + simp [empty] at hp + +@[simp] +lemma getDual?_empty_eq_none (i : Fin n) : empty.getDual? i = none := by + simpa [uncontracted] using mem_uncontracted_empty i + +@[simp] +lemma uncontracted_empty {n : ℕ} : (@empty n).uncontracted = Finset.univ := by + simp [uncontracted] + +lemma uncontracted_card_le (c : WickContraction n) : c.uncontracted.card ≤ n := by + simp only [uncontracted] + apply le_of_le_of_eq (Finset.card_filter_le _ _) + simp + +lemma uncontracted_card_eq_iff (c : WickContraction n) : + c.uncontracted.card = n ↔ c = empty := by + apply Iff.intro + · intro h + have hc : c.uncontracted.card = (Finset.univ (α := Fin n)).card := by simpa using h + simp only [uncontracted] at hc + rw [Finset.card_filter_eq_iff] at hc + by_contra hn + have hc' := exists_pair_of_not_eq_empty c hn + obtain ⟨i, j, hij⟩ := hc' + have hci : c.getDual? i = some j := by + rw [@getDual?_eq_some_iff_mem] + exact hij + simp_all + · intro h + subst h + simp + end WickContraction diff --git a/HepLean/PerturbationTheory/WickContraction/UncontractedList.lean b/HepLean/PerturbationTheory/WickContraction/UncontractedList.lean index 38fff2d6..fc05cf57 100644 --- a/HepLean/PerturbationTheory/WickContraction/UncontractedList.lean +++ b/HepLean/PerturbationTheory/WickContraction/UncontractedList.lean @@ -46,6 +46,24 @@ lemma fin_list_sorted_succAboveEmb_sorted (l: List (Fin n)) (hl : l.Sorted (· simp only [Fin.coe_succAboveEmb] exact Fin.strictMono_succAbove i +lemma fin_finset_sort_map_monotone {n m : ℕ} (a : Finset (Fin n)) (f : Fin n ↪ Fin m) + (hf : StrictMono f) : (Finset.sort (· ≤ ·) a).map f = + (Finset.sort (· ≤ ·) (a.map f)) := by + have h1 : ((Finset.sort (· ≤ ·) a).map f).Sorted (· ≤ ·) := by + apply fin_list_sorted_monotone_sorted + exact Finset.sort_sorted (fun x1 x2 => x1 ≤ x2) a + exact hf + have h2 : ((Finset.sort (· ≤ ·) a).map f).Nodup := by + refine (List.nodup_map_iff_inj_on ?_).mpr ?_ + exact Finset.sort_nodup (fun x1 x2 => x1 ≤ x2) a + intro a ha b hb hf + exact f.2 hf + have h3 : ((Finset.sort (· ≤ ·) a).map f).toFinset = (a.map f) := by + ext a + simp + rw [← h3] + exact ((List.toFinset_sort (· ≤ ·) h2).mpr h1).symm + lemma fin_list_sorted_split : (l : List (Fin n)) → (hl : l.Sorted (· ≤ ·)) → (i : ℕ) → l = l.filter (fun x => x.1 < i) ++ l.filter (fun x => i ≤ x.1) @@ -178,6 +196,9 @@ lemma uncontractedList_mem_iff (i : Fin n) : simp [uncontractedList] @[simp] +lemma uncontractedList_empty : (empty (n := n)).uncontractedList = List.finRange n := by + simp [uncontractedList] + lemma nil_zero_uncontractedList : (empty (n := 0)).uncontractedList = [] := by simp [empty, uncontractedList] @@ -197,6 +218,12 @@ lemma uncontractedList_sorted : List.Sorted (· ≤ ·) c.uncontractedList := by rw [← List.ofFn_id] exact Monotone.ofFn_sorted fun ⦃a b⦄ a => a +lemma uncontractedList_sorted_lt : List.Sorted (· < ·) c.uncontractedList := by + rw [uncontractedList] + apply List.Sorted.filter + rw [← List.ofFn_id] + exact List.sorted_lt_ofFn_iff.mpr fun ⦃a b⦄ a => a + lemma uncontractedList_nodup : c.uncontractedList.Nodup := by rw [uncontractedList] refine List.Nodup.filter (fun x => decide (x ∈ c.uncontracted)) ?_ @@ -294,6 +321,12 @@ def uncontractedListGet {φs : List 𝓕.States} (φsΛ : WickContraction φs.le @[inherit_doc uncontractedListGet] scoped[WickContraction] notation "[" φsΛ "]ᵘᶜ" => uncontractedListGet φsΛ + +@[simp] +lemma uncontractedListGet_empty {φs : List 𝓕.States} : + (empty (n := φs.length)).uncontractedListGet = φs := by + simp [uncontractedListGet] + /-! ## uncontractedStatesEquiv @@ -321,6 +354,89 @@ lemma uncontractedStatesEquiv_list_sum [AddCommMonoid α] (φs : List 𝓕.State /-! +## uncontractedListEmd + +-/ + +/-- The embedding of `Fin [φsΛ]ᵘᶜ.length` into `Fin φs.length`. -/ +def uncontractedListEmd {φs : List 𝓕.States} {φsΛ : WickContraction φs.length} : + Fin [φsΛ]ᵘᶜ.length ↪ Fin φs.length := ((finCongr (by simp [uncontractedListGet])).trans + φsΛ.uncontractedIndexEquiv).toEmbedding.trans + (Function.Embedding.subtype fun x => x ∈ φsΛ.uncontracted) + +lemma uncontractedListEmd_congr {φs : List 𝓕.States} {φsΛ φsΛ' : WickContraction φs.length} + (h : φsΛ = φsΛ') : φsΛ.uncontractedListEmd = + (finCongr (by simp [h])).toEmbedding.trans φsΛ'.uncontractedListEmd := by + subst h + rfl + +lemma uncontractedListEmd_toFun_eq_get (φs : List 𝓕.States) (φsΛ : WickContraction φs.length) : + (uncontractedListEmd (φsΛ := φsΛ)).toFun = + φsΛ.uncontractedList.get ∘ (finCongr (by simp [uncontractedListGet])) := by + rfl + +lemma uncontractedListEmd_strictMono {φs : List 𝓕.States} {φsΛ : WickContraction φs.length} + {i j : Fin [φsΛ]ᵘᶜ.length} (h : i < j) : uncontractedListEmd i < uncontractedListEmd j := by + simp only [uncontractedListEmd, uncontractedIndexEquiv, List.get_eq_getElem, + Equiv.trans_toEmbedding, Function.Embedding.trans_apply, Equiv.coe_toEmbedding, finCongr_apply, + Equiv.coe_fn_mk, Fin.coe_cast, Function.Embedding.coe_subtype] + exact List.Sorted.get_strictMono φsΛ.uncontractedList_sorted_lt h + +lemma uncontractedListEmd_mem_uncontracted {φs : List 𝓕.States} {φsΛ : WickContraction φs.length} + (i : Fin [φsΛ]ᵘᶜ.length) : uncontractedListEmd i ∈ φsΛ.uncontracted := by + simp [uncontractedListEmd] + +lemma uncontractedListEmd_surjective_mem_uncontracted {φs : List 𝓕.States} + {φsΛ : WickContraction φs.length} (i : Fin φs.length) (hi : i ∈ φsΛ.uncontracted) : + ∃ j, φsΛ.uncontractedListEmd j = i := by + simp only [uncontractedListEmd, Equiv.trans_toEmbedding, Function.Embedding.trans_apply, + Equiv.coe_toEmbedding, finCongr_apply, Function.Embedding.coe_subtype] + have hj : ∃ j, φsΛ.uncontractedIndexEquiv j = ⟨i, hi⟩ := by + exact φsΛ.uncontractedIndexEquiv.surjective ⟨i, hi⟩ + obtain ⟨j, hj⟩ := hj + have hj' : ∃ j', Fin.cast uncontractedListEmd.proof_1 j' = j := by + exact (finCongr uncontractedListEmd.proof_1).surjective j + obtain ⟨j', rfl⟩ := hj' + use j' + rw [hj] + +@[simp] +lemma uncontractedListEmd_finset_disjoint_left {φs : List 𝓕.States} + {φsΛ : WickContraction φs.length} (a : Finset (Fin [φsΛ]ᵘᶜ.length)) + (b : Finset (Fin φs.length)) (hb : b ∈ φsΛ.1) : Disjoint (a.map uncontractedListEmd) b := by + rw [Finset.disjoint_left] + intro x hx + simp only [Finset.mem_map] at hx + obtain ⟨x, hx, rfl⟩ := hx + have h1 : uncontractedListEmd x ∈ φsΛ.uncontracted := + uncontractedListEmd_mem_uncontracted x + rw [mem_uncontracted_iff_not_contracted] at h1 + exact h1 b hb + +lemma uncontractedListEmd_finset_not_mem {φs : List 𝓕.States} {φsΛ : WickContraction φs.length} + (a : Finset (Fin [φsΛ]ᵘᶜ.length)) : + a.map uncontractedListEmd ∉ φsΛ.1 := by + by_contra hn + have h1 := uncontractedListEmd_finset_disjoint_left a (a.map uncontractedListEmd) hn + simp only [disjoint_self, Finset.bot_eq_empty, Finset.map_eq_empty] at h1 + have h2 := φsΛ.2.1 (a.map uncontractedListEmd) hn + rw [h1] at h2 + simp at h2 + +@[simp] +lemma getElem_uncontractedListEmd {φs : List 𝓕.States} {φsΛ : WickContraction φs.length} + (k : Fin [φsΛ]ᵘᶜ.length) : φs[(uncontractedListEmd k).1] = [φsΛ]ᵘᶜ[k.1] := by + simp only [uncontractedListGet, List.getElem_map, List.get_eq_getElem] + rfl + +@[simp] +lemma uncontractedListEmd_empty {φs : List 𝓕.States} : + (empty (n := φs.length)).uncontractedListEmd = (finCongr (by simp)).toEmbedding := by + ext x + simp [uncontractedListEmd, uncontractedIndexEquiv] + +/-! + ## Uncontracted List for extractEquiv symm none -/