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

refactor: Split sign files

Browse source
This commit is contained in:
jstoobysmith 2025-02-03 10:47:18 +00:00
parent da030df5ce
commit ff4a56226c
14 changed files with 829 additions and 739 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -311,4 +311,61 @@ lemma insertAndContract_uncontractedList_none_zero (φ : 𝓕.States) {φs : Lis
rw [insertAndContract_uncontractedList_none_map]
simp [uncontractedListOrderPos]
open FieldStatistic in
lemma stat_ofFinset_of_insertAndContractLiftFinset (φ : 𝓕.States) (φs : List 𝓕.States)
(i : Fin φs.length.succ) (a : Finset (Fin φs.length)) :
(𝓕 |>ₛ ⟨(φs.insertIdx i φ).get, insertAndContractLiftFinset φ i a⟩) = 𝓕 |>ₛ ⟨φs.get, a⟩ := by
simp only [ofFinset, Nat.succ_eq_add_one]
congr 1
rw [get_eq_insertIdx_succAbove φ _ i, ← List.map_map, ← List.map_map]
congr
have h1 : (List.map (⇑(finCongr (insertIdx_length_fin φ φs i).symm))
(List.map i.succAbove (Finset.sort (fun x1 x2 => x1 ≤ x2) a))).Sorted (· ≤ ·) := by
simp only [Nat.succ_eq_add_one, List.map_map]
refine
fin_list_sorted_monotone_sorted (Finset.sort (fun x1 x2 => x1 ≤ x2) a) ?hl
(⇑(finCongr (Eq.symm (insertIdx_length_fin φ φs i))) ∘ i.succAbove) ?hf
exact Finset.sort_sorted (fun x1 x2 => x1 ≤ x2) a
refine StrictMono.comp (fun ⦃a b⦄ a => a) ?hf.hf
exact Fin.strictMono_succAbove i
have h2 : (List.map (⇑(finCongr (insertIdx_length_fin φ φs i).symm))
(List.map i.succAbove (Finset.sort (fun x1 x2 => x1 ≤ x2) a))).Nodup := by
simp only [Nat.succ_eq_add_one, List.map_map]
refine List.Nodup.map ?_ ?_
apply (Equiv.comp_injective _ (finCongr _)).mpr
exact Fin.succAbove_right_injective
exact Finset.sort_nodup (fun x1 x2 => x1 ≤ x2) a
have h3 : (List.map (⇑(finCongr (insertIdx_length_fin φ φs i).symm))
(List.map i.succAbove (Finset.sort (fun x1 x2 => x1 ≤ x2) a))).toFinset
= (insertAndContractLiftFinset φ i a) := by
ext b
simp only [Nat.succ_eq_add_one, List.map_map, List.mem_toFinset, List.mem_map, Finset.mem_sort,
Function.comp_apply, finCongr_apply]
rcases insert_fin_eq_self φ i b with hk | hk
· subst hk
simp only [Nat.succ_eq_add_one, self_not_mem_insertAndContractLiftFinset, iff_false,
not_exists, not_and]
intro x hx
refine Fin.ne_of_val_ne ?h.inl.h
simp only [Fin.coe_cast, ne_eq]
rw [Fin.val_eq_val]
exact Fin.succAbove_ne i x
· obtain ⟨k, hk⟩ := hk
subst hk
simp only [Nat.succ_eq_add_one]
rw [succAbove_mem_insertAndContractLiftFinset]
apply Iff.intro
· intro h
obtain ⟨x, hx⟩ := h
simp only [Fin.ext_iff, Fin.coe_cast] at hx
rw [Fin.val_eq_val] at hx
rw [Function.Injective.eq_iff] at hx
rw [← hx.2]
exact hx.1
exact Fin.succAbove_right_injective
· intro h
use k
rw [← h3]
rw [(List.toFinset_sort (· ≤ ·) h2).mpr h1]
end WickContraction

421
HepLean/PerturbationTheory/WickContraction/Join.lean
View file

@ -589,191 +589,6 @@ lemma subContraction_card_plus_quotContraction_card_eq (S : Finset (Finset (Fin
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)
@ -793,200 +608,6 @@ lemma join_singleton_getDual?_right {φs : List 𝓕.States}
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) :
@ -1024,38 +645,6 @@ lemma exists_join_singleton_of_card_ge_zero {φs : List 𝓕.States} (φsΛ : Wi
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
@ -1067,15 +656,5 @@ lemma join_not_gradingCompliant_of_left_not_gradingCompliant {φs : List 𝓕.St
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

49
HepLean/PerturbationTheory/WickContraction/Sign/Basic.lean Normal file
View file

@ -0,0 +1,49 @@
/-
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.InsertAndContract
/-!
# Sign associated with a contraction
-/
open FieldSpecification
variable {𝓕 : FieldSpecification}
namespace WickContraction
variable {n : ℕ} (c : WickContraction n)
open HepLean.List
open FieldStatistic
/-- Given a Wick contraction `c : WickContraction n` and `i1 i2 : Fin n` the finite set
of elements of `Fin n` between `i1` and `i2` which are either uncontracted
or are contracted but are contracted with an element occuring after `i1`.
I.e. the elements of `Fin n` between `i1` and `i2` which are not contracted with before `i1`.
One should assume `i1 < i2` otherwise this finite set is empty. -/
def signFinset (c : WickContraction n) (i1 i2 : Fin n) : Finset (Fin n) :=
Finset.univ.filter (fun i => i1 < i ∧ i < i2 ∧
(c.getDual? i = none ∨ ∀ (h : (c.getDual? i).isSome), i1 < (c.getDual? i).get h))
/-- Given a Wick contraction `φsΛ` associated with a list of states `φs`
the sign associated with `φsΛ` is sign corresponding to the number
of fermionic-fermionic exchanges one must do to put elements in contracted pairs
of `φsΛ` next to each other. -/
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
end WickContraction

237
HepLean/PerturbationTheory/WickContraction/Sign/InsertNone.lean Normal file
View file

@ -0,0 +1,237 @@
/-
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.Sign.Basic
/-!
# Sign on inserting and not contracting
-/
open FieldSpecification
variable {𝓕 : FieldSpecification}
namespace WickContraction
variable {n : ℕ} (c : WickContraction n)
open HepLean.List
open FieldStatistic
lemma signFinset_insertAndContract_none (φ : 𝓕.States) (φs : List 𝓕.States)
(φsΛ : WickContraction φs.length)
(i : Fin φs.length.succ) (i1 i2 : Fin φs.length) :
(φsΛ ↩Λ φ i none).signFinset (finCongr (insertIdx_length_fin φ φs i).symm
(i.succAbove i1)) (finCongr (insertIdx_length_fin φ φs i).symm (i.succAbove i2)) =
if i.succAbove i1 < i ∧ i < i.succAbove i2 then
Insert.insert (finCongr (insertIdx_length_fin φ φs i).symm i)
(insertAndContractLiftFinset φ i (φsΛ.signFinset i1 i2))
else
(insertAndContractLiftFinset φ i (φsΛ.signFinset i1 i2)) := by
ext k
rcases insert_fin_eq_self φ i k with hk | hk
· subst hk
conv_lhs => simp only [Nat.succ_eq_add_one, signFinset, finCongr_apply, Finset.mem_filter,
Finset.mem_univ, insertAndContract_none_getDual?_self, Option.isSome_none, Bool.false_eq_true,
IsEmpty.forall_iff, or_self, and_true, true_and]
by_cases h : i.succAbove i1 < i ∧ i < i.succAbove i2
· simp [h, Fin.lt_def]
· simp only [Nat.succ_eq_add_one, h, ↓reduceIte, self_not_mem_insertAndContractLiftFinset,
iff_false]
rw [Fin.lt_def, Fin.lt_def] at h ⊢
simp_all
· obtain ⟨k, hk⟩ := hk
subst hk
have h1 : Fin.cast (insertIdx_length_fin φ φs i).symm (i.succAbove k) ∈
(if i.succAbove i1 < i ∧ i < i.succAbove i2 then
Insert.insert ((finCongr (insertIdx_length_fin φ φs i).symm) i)
(insertAndContractLiftFinset φ i (φsΛ.signFinset i1 i2))
else insertAndContractLiftFinset φ i (φsΛ.signFinset i1 i2)) ↔
Fin.cast (insertIdx_length_fin φ φs i).symm (i.succAbove k) ∈
insertAndContractLiftFinset φ i (φsΛ.signFinset i1 i2) := by
split
· simp only [Nat.succ_eq_add_one, finCongr_apply, Finset.mem_insert, Fin.ext_iff,
Fin.coe_cast, or_iff_right_iff_imp]
intro h
have h1 : i.succAbove k ≠ i := by
exact Fin.succAbove_ne i k
omega
· simp
rw [h1]
rw [succAbove_mem_insertAndContractLiftFinset]
simp only [Nat.succ_eq_add_one, signFinset, finCongr_apply, Finset.mem_filter, Finset.mem_univ,
insertAndContract_none_succAbove_getDual?_eq_none_iff, true_and,
insertAndContract_none_succAbove_getDual?_isSome_iff, insertAndContract_none_getDual?_get_eq]
rw [Fin.lt_def, Fin.lt_def, Fin.lt_def, Fin.lt_def]
simp only [Fin.coe_cast, Fin.val_fin_lt]
rw [Fin.succAbove_lt_succAbove_iff, Fin.succAbove_lt_succAbove_iff]
simp only [and_congr_right_iff]
intro h1 h2
conv_lhs =>
rhs
enter [h]
rw [Fin.lt_def]
simp only [Fin.coe_cast, Fin.val_fin_lt]
rw [Fin.succAbove_lt_succAbove_iff]
/-- Given a Wick contraction `φsΛ` associated with a list of states `φs`
and an `i : Fin φs.length.succ`, the change in sign of the contraction associated with
inserting `φ` into `φs` at position `i` without contracting it.
For each contracted pair `{a1, a2}` in `φsΛ` if `a1 < a2` such that `i` is within the range
`a1 < i < a2` we pick up a sign equal to `𝓢(φ, φs[a2])`. -/
def signInsertNone (φ : 𝓕.States) (φs : List 𝓕.States) (φsΛ : WickContraction φs.length)
(i : Fin φs.length.succ) : ℂ :=
∏ (a : φsΛ.1),
if i.succAbove (φsΛ.fstFieldOfContract a) < i ∧ i < i.succAbove (φsΛ.sndFieldOfContract a) then
𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φs[φsΛ.sndFieldOfContract a])
else 1
lemma sign_insert_none (φ : 𝓕.States) (φs : List 𝓕.States) (φsΛ : WickContraction φs.length)
(i : Fin φs.length.succ) :
(φsΛ ↩Λ φ i none).sign = (φsΛ.signInsertNone φ φs i) * φsΛ.sign := by
rw [sign]
rw [signInsertNone, sign, ← Finset.prod_mul_distrib]
rw [insertAndContract_none_prod_contractions]
congr
funext a
simp only [instCommGroup, Nat.succ_eq_add_one, insertAndContract_sndFieldOfContract,
finCongr_apply, Fin.getElem_fin, Fin.coe_cast, insertIdx_getElem_fin,
insertAndContract_fstFieldOfContract, ite_mul, one_mul]
erw [signFinset_insertAndContract_none]
split
· rw [ofFinset_insert]
simp only [instCommGroup, Nat.succ_eq_add_one, finCongr_apply, Fin.getElem_fin, Fin.coe_cast,
List.getElem_insertIdx_self, map_mul]
rw [stat_ofFinset_of_insertAndContractLiftFinset]
simp only [exchangeSign_symm, instCommGroup.eq_1]
simp
· rw [stat_ofFinset_of_insertAndContractLiftFinset]
lemma signInsertNone_eq_mul_fst_snd (φ : 𝓕.States) (φs : List 𝓕.States)
(φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) :
φsΛ.signInsertNone φ φs i = ∏ (a : φsΛ.1),
(if i.succAbove (φsΛ.fstFieldOfContract a) < i then
𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φs[φsΛ.sndFieldOfContract a])
else 1) *
(if i.succAbove (φsΛ.sndFieldOfContract a) < i then
𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φs[φsΛ.sndFieldOfContract a])
else 1) := by
rw [signInsertNone]
congr
funext a
split
· rename_i h
simp only [instCommGroup.eq_1, Fin.getElem_fin, h.1, ↓reduceIte, mul_ite, exchangeSign_mul_self,
mul_one]
rw [if_neg]
omega
· rename_i h
simp only [Nat.succ_eq_add_one, not_and, not_lt] at h
split <;> rename_i h1
· simp_all only [forall_const, instCommGroup.eq_1, Fin.getElem_fin, mul_ite,
exchangeSign_mul_self, mul_one]
rw [if_pos]
have h1 :i.succAbove (φsΛ.sndFieldOfContract a) ≠ i :=
Fin.succAbove_ne i (φsΛ.sndFieldOfContract a)
omega
· simp only [not_lt] at h1
rw [if_neg]
simp only [mul_one]
have hn := fstFieldOfContract_lt_sndFieldOfContract φsΛ a
have hx := (Fin.succAbove_lt_succAbove_iff (p := i)).mpr hn
omega
lemma signInsertNone_eq_prod_prod (φ : 𝓕.States) (φs : List 𝓕.States)
(φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (hG : GradingCompliant φs φsΛ) :
φsΛ.signInsertNone φ φs i = ∏ (a : φsΛ.1), ∏ (x : a),
(if i.succAbove x < i then 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φs[x.1]) else 1) := by
rw [signInsertNone_eq_mul_fst_snd]
congr
funext a
rw [prod_finset_eq_mul_fst_snd]
congr 1
congr 1
congr 1
simp only [Fin.getElem_fin]
erw [hG a]
rfl
lemma sign_insert_none_zero (φ : 𝓕.States) (φs : List 𝓕.States) (φsΛ : WickContraction φs.length) :
(φsΛ ↩Λ φ 0 none).sign = φsΛ.sign := by
rw [sign_insert_none]
simp [signInsertNone]
lemma signInsertNone_eq_prod_getDual?_Some (φ : 𝓕.States) (φs : List 𝓕.States)
(φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (hG : GradingCompliant φs φsΛ) :
φsΛ.signInsertNone φ φs i = ∏ (x : Fin φs.length),
if (φsΛ.getDual? x).isSome then
(if i.succAbove x < i then 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φs[x.1]) else 1)
else 1 := by
rw [signInsertNone_eq_prod_prod]
trans ∏ (x : (a : φsΛ.1) × a), (if i.succAbove x.2 < i then 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φs[x.2.1]) else 1)
· rw [Finset.prod_sigma']
rfl
rw [← φsΛ.sigmaContractedEquiv.symm.prod_comp]
let e2 : Fin φs.length ≃ {x // (φsΛ.getDual? x).isSome} ⊕ {x // ¬ (φsΛ.getDual? x).isSome} := by
exact (Equiv.sumCompl fun a => (φsΛ.getDual? a).isSome = true).symm
rw [← e2.symm.prod_comp]
simp only [instCommGroup.eq_1, Fin.getElem_fin, Fintype.prod_sum_type]
conv_rhs =>
rhs
enter [2, a]
rw [if_neg (by simpa [e2] using a.2)]
conv_rhs =>
lhs
enter [2, a]
rw [if_pos (by simpa [e2] using a.2)]
simp only [Equiv.symm_symm, Equiv.sumCompl_apply_inl, Finset.prod_const_one, mul_one, e2]
rfl
exact hG
lemma signInsertNone_eq_filter_map (φ : 𝓕.States) (φs : List 𝓕.States)
(φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (hG : GradingCompliant φs φsΛ) :
φsΛ.signInsertNone φ φs i =
𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ ((List.filter (fun x => (φsΛ.getDual? x).isSome ∧ i.succAbove x < i)
(List.finRange φs.length)).map φs.get)) := by
rw [signInsertNone_eq_prod_getDual?_Some]
rw [FieldStatistic.ofList_map_eq_finset_prod]
rw [map_prod]
congr
funext a
simp only [instCommGroup.eq_1, Bool.decide_and, Bool.decide_eq_true, List.mem_filter,
List.mem_finRange, Bool.and_eq_true, decide_eq_true_eq, true_and, Fin.getElem_fin]
split
· rename_i h
simp only [h, true_and]
split
· rfl
· simp only [map_one]
· rename_i h
simp [h]
· refine List.Nodup.filter _ ?_
exact List.nodup_finRange φs.length
· exact hG
/-- The change in sign when inserting a field `φ` at `i` into `φsΛ` is equal
to the sign got by moving `φ` through each field `φ₀…φᵢ₋₁` which has a dual. -/
lemma signInsertNone_eq_filterset (φ : 𝓕.States) (φs : List 𝓕.States)
(φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (hG : GradingCompliant φs φsΛ) :
φsΛ.signInsertNone φ φs i = 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ ⟨φs.get, Finset.univ.filter
(fun x => (φsΛ.getDual? x).isSome ∧ i.succAbove x < i)⟩) := by
rw [ofFinset_eq_prod, signInsertNone_eq_prod_getDual?_Some, map_prod]
congr
funext a
simp only [instCommGroup.eq_1, Finset.mem_filter, Finset.mem_univ, true_and, Fin.getElem_fin]
split
· rename_i h
simp only [h, true_and]
split
· rfl
· simp only [map_one]
· rename_i h
simp [h]
· exact hG
end WickContraction

325
HepLean/PerturbationTheory/WickContraction/Sign.lean → HepLean/PerturbationTheory/WickContraction/Sign/InsertSome.lean
View file

@ -3,11 +3,11 @@ 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.InsertAndContract
import HepLean.PerturbationTheory.WickContraction.Sign.Basic
/-!
# Sign associated with a contraction
# Sign on inserting and contracting
-/
@ -19,127 +19,13 @@ variable {n : ℕ} (c : WickContraction n)
open HepLean.List
open FieldStatistic
/-- Given a Wick contraction `c : WickContraction n` and `i1 i2 : Fin n` the finite set
of elements of `Fin n` between `i1` and `i2` which are either uncontracted
or are contracted but are contracted with an element occuring after `i1`.
One should assume `i1 < i2` otherwise this finite set is empty. -/
def signFinset (c : WickContraction n) (i1 i2 : Fin n) : Finset (Fin n) :=
Finset.univ.filter (fun i => i1 < i ∧ i < i2 ∧
(c.getDual? i = none ∨ ∀ (h : (c.getDual? i).isSome), i1 < (c.getDual? i).get h))
lemma signFinset_insertAndContract_none (φ : 𝓕.States) (φs : List 𝓕.States)
(φsΛ : WickContraction φs.length)
(i : Fin φs.length.succ) (i1 i2 : Fin φs.length) :
(φsΛ ↩Λ φ i none).signFinset (finCongr (insertIdx_length_fin φ φs i).symm
(i.succAbove i1)) (finCongr (insertIdx_length_fin φ φs i).symm (i.succAbove i2)) =
if i.succAbove i1 < i ∧ i < i.succAbove i2 then
Insert.insert (finCongr (insertIdx_length_fin φ φs i).symm i)
(insertAndContractLiftFinset φ i (φsΛ.signFinset i1 i2))
else
(insertAndContractLiftFinset φ i (φsΛ.signFinset i1 i2)) := by
ext k
rcases insert_fin_eq_self φ i k with hk | hk
· subst hk
conv_lhs => simp only [Nat.succ_eq_add_one, signFinset, finCongr_apply, Finset.mem_filter,
Finset.mem_univ, insertAndContract_none_getDual?_self, Option.isSome_none, Bool.false_eq_true,
IsEmpty.forall_iff, or_self, and_true, true_and]
by_cases h : i.succAbove i1 < i ∧ i < i.succAbove i2
· simp [h, Fin.lt_def]
· simp only [Nat.succ_eq_add_one, h, ↓reduceIte, self_not_mem_insertAndContractLiftFinset,
iff_false]
rw [Fin.lt_def, Fin.lt_def] at h ⊢
simp_all
· obtain ⟨k, hk⟩ := hk
subst hk
have h1 : Fin.cast (insertIdx_length_fin φ φs i).symm (i.succAbove k) ∈
(if i.succAbove i1 < i ∧ i < i.succAbove i2 then
Insert.insert ((finCongr (insertIdx_length_fin φ φs i).symm) i)
(insertAndContractLiftFinset φ i (φsΛ.signFinset i1 i2))
else insertAndContractLiftFinset φ i (φsΛ.signFinset i1 i2)) ↔
Fin.cast (insertIdx_length_fin φ φs i).symm (i.succAbove k) ∈
insertAndContractLiftFinset φ i (φsΛ.signFinset i1 i2) := by
split
· simp only [Nat.succ_eq_add_one, finCongr_apply, Finset.mem_insert, Fin.ext_iff,
Fin.coe_cast, or_iff_right_iff_imp]
intro h
have h1 : i.succAbove k ≠ i := by
exact Fin.succAbove_ne i k
omega
· simp
rw [h1]
rw [succAbove_mem_insertAndContractLiftFinset]
simp only [Nat.succ_eq_add_one, signFinset, finCongr_apply, Finset.mem_filter, Finset.mem_univ,
insertAndContract_none_succAbove_getDual?_eq_none_iff, true_and,
insertAndContract_none_succAbove_getDual?_isSome_iff, insertAndContract_none_getDual?_get_eq]
rw [Fin.lt_def, Fin.lt_def, Fin.lt_def, Fin.lt_def]
simp only [Fin.coe_cast, Fin.val_fin_lt]
rw [Fin.succAbove_lt_succAbove_iff, Fin.succAbove_lt_succAbove_iff]
simp only [and_congr_right_iff]
intro h1 h2
conv_lhs =>
rhs
enter [h]
rw [Fin.lt_def]
simp only [Fin.coe_cast, Fin.val_fin_lt]
rw [Fin.succAbove_lt_succAbove_iff]
/-!
## Sign insert some
-/
lemma stat_ofFinset_of_insertAndContractLiftFinset (φ : 𝓕.States) (φs : List 𝓕.States)
(i : Fin φs.length.succ) (a : Finset (Fin φs.length)) :
(𝓕 |>ₛ ⟨(φs.insertIdx i φ).get, insertAndContractLiftFinset φ i a⟩) = 𝓕 |>ₛ ⟨φs.get, a⟩ := by
simp only [ofFinset, Nat.succ_eq_add_one]
congr 1
rw [get_eq_insertIdx_succAbove φ _ i]
rw [← List.map_map, ← List.map_map]
congr
have h1 : (List.map (⇑(finCongr (insertIdx_length_fin φ φs i).symm))
(List.map i.succAbove (Finset.sort (fun x1 x2 => x1 ≤ x2) a))).Sorted (· ≤ ·) := by
simp only [Nat.succ_eq_add_one, List.map_map]
refine
fin_list_sorted_monotone_sorted (Finset.sort (fun x1 x2 => x1 ≤ x2) a) ?hl
(⇑(finCongr (Eq.symm (insertIdx_length_fin φ φs i))) ∘ i.succAbove) ?hf
exact Finset.sort_sorted (fun x1 x2 => x1 ≤ x2) a
refine StrictMono.comp (fun ⦃a b⦄ a => a) ?hf.hf
exact Fin.strictMono_succAbove i
have h2 : (List.map (⇑(finCongr (insertIdx_length_fin φ φs i).symm))
(List.map i.succAbove (Finset.sort (fun x1 x2 => x1 ≤ x2) a))).Nodup := by
simp only [Nat.succ_eq_add_one, List.map_map]
refine List.Nodup.map ?_ ?_
apply (Equiv.comp_injective _ (finCongr _)).mpr
exact Fin.succAbove_right_injective
exact Finset.sort_nodup (fun x1 x2 => x1 ≤ x2) a
have h3 : (List.map (⇑(finCongr (insertIdx_length_fin φ φs i).symm))
(List.map i.succAbove (Finset.sort (fun x1 x2 => x1 ≤ x2) a))).toFinset
= (insertAndContractLiftFinset φ i a) := by
ext b
simp only [Nat.succ_eq_add_one, List.map_map, List.mem_toFinset, List.mem_map, Finset.mem_sort,
Function.comp_apply, finCongr_apply]
rcases insert_fin_eq_self φ i b with hk | hk
· subst hk
simp only [Nat.succ_eq_add_one, self_not_mem_insertAndContractLiftFinset, iff_false,
not_exists, not_and]
intro x hx
refine Fin.ne_of_val_ne ?h.inl.h
simp only [Fin.coe_cast, ne_eq]
rw [@Fin.val_eq_val]
exact Fin.succAbove_ne i x
· obtain ⟨k, hk⟩ := hk
subst hk
simp only [Nat.succ_eq_add_one]
rw [succAbove_mem_insertAndContractLiftFinset]
apply Iff.intro
· intro h
obtain ⟨x, hx⟩ := h
simp only [Fin.ext_iff, Fin.coe_cast] at hx
rw [@Fin.val_eq_val] at hx
rw [Function.Injective.eq_iff] at hx
rw [← hx.2]
exact hx.1
exact Fin.succAbove_right_injective
· intro h
use k
rw [← h3]
symm
rw [(List.toFinset_sort (· ≤ ·) h2).mpr h1]
lemma stat_ofFinset_eq_one_of_gradingCompliant (φs : List 𝓕.States)
(a : Finset (Fin φs.length)) (φsΛ : WickContraction φs.length) (hg : GradingCompliant φs φsΛ)
@ -177,6 +63,7 @@ lemma stat_ofFinset_eq_one_of_gradingCompliant (φs : List 𝓕.States)
exact False.elim (h1 hsom')
rfl
lemma signFinset_insertAndContract_some (φ : 𝓕.States) (φs : List 𝓕.States)
(φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (i1 i2 : Fin φs.length)
(j : φsΛ.uncontracted) :
@ -314,192 +201,6 @@ lemma signFinset_insertAndContract_some (φ : 𝓕.States) (φs : List 𝓕.Stat
simp only [Fin.coe_cast, Option.get_map, Function.comp_apply, Fin.val_fin_lt]
rw [Fin.succAbove_lt_succAbove_iff]
/-- Given a Wick contraction `c` associated with a list of states `φs`
the sign associated with `c` is sign corresponding to the number
of fermionic-fermionic exchanges one must do to put elements in contracted pairs
of `c` next to each other.
It is important to note that this sign does not depend on any ordering
placed on `φs` other then the order of the list itself. -/
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
-/
/-- Given a Wick contraction `c` associated with a list of states `φs`
and an `i : Fin φs.length.succ`, the change in sign of the contraction associated with
inserting `φ` into `φs` at position `i` without contracting it. -/
def signInsertNone (φ : 𝓕.States) (φs : List 𝓕.States) (φsΛ : WickContraction φs.length)
(i : Fin φs.length.succ) : ℂ :=
∏ (a : φsΛ.1),
if i.succAbove (φsΛ.fstFieldOfContract a) < i ∧ i < i.succAbove (φsΛ.sndFieldOfContract a) then
𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φs[φsΛ.sndFieldOfContract a])
else 1
lemma sign_insert_none (φ : 𝓕.States) (φs : List 𝓕.States) (φsΛ : WickContraction φs.length)
(i : Fin φs.length.succ) :
(φsΛ ↩Λ φ i none).sign = (φsΛ.signInsertNone φ φs i) * φsΛ.sign := by
rw [sign]
rw [signInsertNone, sign, ← Finset.prod_mul_distrib]
rw [insertAndContract_none_prod_contractions]
congr
funext a
simp only [instCommGroup, Nat.succ_eq_add_one, insertAndContract_sndFieldOfContract,
finCongr_apply, Fin.getElem_fin, Fin.coe_cast, insertIdx_getElem_fin,
insertAndContract_fstFieldOfContract, ite_mul, one_mul]
erw [signFinset_insertAndContract_none]
split
· rw [ofFinset_insert]
simp only [instCommGroup, Nat.succ_eq_add_one, finCongr_apply, Fin.getElem_fin, Fin.coe_cast,
List.getElem_insertIdx_self, map_mul]
rw [stat_ofFinset_of_insertAndContractLiftFinset]
simp only [exchangeSign_symm, instCommGroup.eq_1]
simp
· rw [stat_ofFinset_of_insertAndContractLiftFinset]
lemma signInsertNone_eq_mul_fst_snd (φ : 𝓕.States) (φs : List 𝓕.States)
(φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) :
φsΛ.signInsertNone φ φs i = ∏ (a : φsΛ.1),
(if i.succAbove (φsΛ.fstFieldOfContract a) < i then
𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φs[φsΛ.sndFieldOfContract a])
else 1) *
(if i.succAbove (φsΛ.sndFieldOfContract a) < i then
𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φs[φsΛ.sndFieldOfContract a])
else 1) := by
rw [signInsertNone]
congr
funext a
split
· rename_i h
simp only [instCommGroup.eq_1, Fin.getElem_fin, h.1, ↓reduceIte, mul_ite, exchangeSign_mul_self,
mul_one]
rw [if_neg]
omega
· rename_i h
simp only [Nat.succ_eq_add_one, not_and, not_lt] at h
split <;> rename_i h1
· simp_all only [forall_const, instCommGroup.eq_1, Fin.getElem_fin, mul_ite,
exchangeSign_mul_self, mul_one]
rw [if_pos]
have h1 :i.succAbove (φsΛ.sndFieldOfContract a) ≠ i :=
Fin.succAbove_ne i (φsΛ.sndFieldOfContract a)
omega
· simp only [not_lt] at h1
rw [if_neg]
simp only [mul_one]
have hn := fstFieldOfContract_lt_sndFieldOfContract φsΛ a
have hx := (Fin.succAbove_lt_succAbove_iff (p := i)).mpr hn
omega
lemma signInsertNone_eq_prod_prod (φ : 𝓕.States) (φs : List 𝓕.States)
(φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (hG : GradingCompliant φs φsΛ) :
φsΛ.signInsertNone φ φs i = ∏ (a : φsΛ.1), ∏ (x : a),
(if i.succAbove x < i then 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φs[x.1]) else 1) := by
rw [signInsertNone_eq_mul_fst_snd]
congr
funext a
rw [prod_finset_eq_mul_fst_snd]
congr 1
congr 1
congr 1
simp only [Fin.getElem_fin]
erw [hG a]
rfl
lemma sign_insert_none_zero (φ : 𝓕.States) (φs : List 𝓕.States) (φsΛ : WickContraction φs.length) :
(φsΛ ↩Λ φ 0 none).sign = φsΛ.sign := by
rw [sign_insert_none]
simp [signInsertNone]
lemma signInsertNone_eq_prod_getDual?_Some (φ : 𝓕.States) (φs : List 𝓕.States)
(φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (hG : GradingCompliant φs φsΛ) :
φsΛ.signInsertNone φ φs i = ∏ (x : Fin φs.length),
if (φsΛ.getDual? x).isSome then
(if i.succAbove x < i then 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φs[x.1]) else 1)
else 1 := by
rw [signInsertNone_eq_prod_prod]
trans ∏ (x : (a : φsΛ.1) × a), (if i.succAbove x.2 < i then 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φs[x.2.1]) else 1)
· rw [Finset.prod_sigma']
rfl
rw [← φsΛ.sigmaContractedEquiv.symm.prod_comp]
let e2 : Fin φs.length ≃ {x // (φsΛ.getDual? x).isSome} ⊕ {x // ¬ (φsΛ.getDual? x).isSome} := by
exact (Equiv.sumCompl fun a => (φsΛ.getDual? a).isSome = true).symm
rw [← e2.symm.prod_comp]
simp only [instCommGroup.eq_1, Fin.getElem_fin, Fintype.prod_sum_type]
conv_rhs =>
rhs
enter [2, a]
rw [if_neg (by simpa [e2] using a.2)]
conv_rhs =>
lhs
enter [2, a]
rw [if_pos (by simpa [e2] using a.2)]
simp only [Equiv.symm_symm, Equiv.sumCompl_apply_inl, Finset.prod_const_one, mul_one, e2]
rfl
exact hG
lemma signInsertNone_eq_filter_map (φ : 𝓕.States) (φs : List 𝓕.States)
(φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (hG : GradingCompliant φs φsΛ) :
φsΛ.signInsertNone φ φs i =
𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ ((List.filter (fun x => (φsΛ.getDual? x).isSome ∧ i.succAbove x < i)
(List.finRange φs.length)).map φs.get)) := by
rw [signInsertNone_eq_prod_getDual?_Some]
rw [FieldStatistic.ofList_map_eq_finset_prod]
rw [map_prod]
congr
funext a
simp only [instCommGroup.eq_1, Bool.decide_and, Bool.decide_eq_true, List.mem_filter,
List.mem_finRange, Bool.and_eq_true, decide_eq_true_eq, true_and, Fin.getElem_fin]
split
· rename_i h
simp only [h, true_and]
split
· rfl
· simp only [map_one]
· rename_i h
simp [h]
· refine List.Nodup.filter _ ?_
exact List.nodup_finRange φs.length
· exact hG
lemma signInsertNone_eq_filterset (φ : 𝓕.States) (φs : List 𝓕.States)
(φsΛ : WickContraction φs.length)
(i : Fin φs.length.succ) (hG : GradingCompliant φs φsΛ) :
φsΛ.signInsertNone φ φs i = 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ ⟨φs.get, Finset.univ.filter
(fun x => (φsΛ.getDual? x).isSome ∧ i.succAbove x < i)⟩) := by
rw [ofFinset_eq_prod, signInsertNone_eq_prod_getDual?_Some, map_prod]
congr
funext a
simp only [instCommGroup.eq_1, Finset.mem_filter, Finset.mem_univ, true_and, Fin.getElem_fin]
split
· rename_i h
simp only [h, true_and]
split
· rfl
· simp only [map_one]
· rename_i h
simp [h]
· exact hG
/-!
## Sign insert some
-/
/-- Given a Wick contraction `c` associated with a list of states `φs`
and an `i : Fin φs.length.succ`, the change in sign of the contraction associated with
inserting `φ` into `φs` at position `i` and contracting it with `j : c.uncontracted`
@ -531,7 +232,7 @@ def signInsertSomeCoef (φ : 𝓕.States) (φs : List 𝓕.States) (φsΛ : Wick
(φsΛ ↩Λ φ i (some j)) ((φsΛ ↩Λ φ i (some j)).fstFieldOfContract a)
((φsΛ ↩Λ φ i (some j)).sndFieldOfContract a)⟩)
/-- Given a Wick contraction `c` associated with a list of states `φs`
/-- Given a Wick contraction `φsΛ` associated with a list of states `φs`
and an `i : Fin φs.length.succ`, the change in sign of the contraction associated with
inserting `φ` into `φs` at position `i` and contracting it with `j : c.uncontracted`. -/
def signInsertSome (φ : 𝓕.States) (φs : List 𝓕.States) (φsΛ : WickContraction φs.length)
@ -932,6 +633,10 @@ lemma signInsertSomeCoef_eq_finset (φ : 𝓕.States) (φs : List 𝓕.States)
stat_signFinset_insert_some_self_fst]
simp [hφj]
/-- The change in sign when inserting a field `φ` at `i` into `φsΛ` and
contracting it with `k` (`k < i`) is equal
to the sign got by moving `φ` through each field `φ₀…φᵢ₋₁`
multiplied by the sign got moving `φ` through each uncontracted field `φ₀…φₖ`. -/
lemma signInsertSome_mul_filter_contracted_of_lt (φ : 𝓕.States) (φs : List 𝓕.States)
(φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (k : φsΛ.uncontracted)
(hk : i.succAbove k < i) (hg : GradingCompliant φs φsΛ ∧ (𝓕 |>ₛ φ) = 𝓕 |>ₛ φs[k.1]) :
@ -1035,6 +740,10 @@ lemma signInsertSome_mul_filter_contracted_of_lt (φ : 𝓕.States) (φs : List
or_true, imp_self]
omega
/-- The change in sign when inserting a field `φ` at `i` into `φsΛ` and
contracting it with `k` (`i < k`) is equal
to the sign got by moving `φ` through each field `φ₀…φᵢ₋₁`
multiplied by the sign got moving `φ` through each uncontracted field `φ₀…φₖ₋₁`. -/
lemma signInsertSome_mul_filter_contracted_of_not_lt (φ : 𝓕.States) (φs : List 𝓕.States)
(φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (k : φsΛ.uncontracted)
(hk : ¬ i.succAbove k < i) (hg : GradingCompliant φs φsΛ ∧ (𝓕 |>ₛ φ) = 𝓕 |>ₛ φs[k.1]) :

447
HepLean/PerturbationTheory/WickContraction/Sign/Join.lean Normal file
View file

@ -0,0 +1,447 @@
/-
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.Join
/-!
# Sign associated with joining two Wick contractions
-/
open FieldSpecification
variable {𝓕 : FieldSpecification}
namespace WickContraction
variable {n : ℕ} (c : WickContraction n)
open HepLean.List
open FieldOpAlgebra
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
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 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_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

3
HepLean/PerturbationTheory/WickContraction/Singleton.lean
View file

@ -3,9 +3,6 @@ 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
/-!

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

@ -3,7 +3,7 @@ Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import HepLean.PerturbationTheory.WickContraction.Sign
import HepLean.PerturbationTheory.WickContraction.Sign.Basic
import HepLean.PerturbationTheory.Algebras.FieldOpAlgebra.TimeContraction
/-!

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

@ -3,9 +3,7 @@ Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import HepLean.PerturbationTheory.WickContraction.TimeContract
import HepLean.PerturbationTheory.WickContraction.Join
import HepLean.PerturbationTheory.Algebras.FieldOpAlgebra.TimeContraction
/-!
# Time contractions

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

@ -3,7 +3,7 @@ Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import HepLean.PerturbationTheory.WickContraction.Sign
import HepLean.PerturbationTheory.WickContraction.Sign.Basic
import HepLean.PerturbationTheory.Algebras.FieldOpAlgebra.TimeContraction
/-!