1081 lines
46 KiB
Text
1081 lines
46 KiB
Text
/-
|
||
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
|