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

refactor: Lint

Browse source
This commit is contained in:
jstoobysmith 2025-02-03 05:39:48 +00:00
parent 006e29fd08
commit fca3f02eca
16 changed files with 416 additions and 352 deletions
Download patch file Download diff file Expand all files Collapse all files

6
HepLean/PerturbationTheory/WickContraction/Basic.lean
View file

@ -52,10 +52,10 @@ lemma card_zero_iff_empty (c : WickContraction n) : c.1.card = 0 ↔ c = empty :
lemma exists_pair_of_not_eq_empty (c : WickContraction n) (h : c ≠ empty) :
∃ i j, {i, j} ∈ c.1 := by
by_contra hn
simp at hn
simp only [not_exists] at hn
have hc : c.1 = ∅ := by
ext a
simp
simp only [Finset.not_mem_empty, iff_false]
by_contra hn'
have hc := c.2.1 a hn'
rw [@Finset.card_eq_two] at hc
@ -148,7 +148,7 @@ lemma congrLift_bijective {n m : ℕ} {c : WickContraction n} (h : n = m) :
/-- Given a contracted pair in `c : WickContraction n` the contracted pair
in `congr h c`. -/
def congrLiftInv {n m : ℕ} (h : n = m) {c : WickContraction n} (a : (congr h c).1 ) : c.1 :=
def congrLiftInv {n m : ℕ} (h : n = m) {c : WickContraction n} (a : (congr h c).1) : c.1 :=
⟨a.1.map (finCongr h.symm).toEmbedding, by
subst h
simp⟩

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

@ -27,7 +27,8 @@ 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 at 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
@ -35,7 +36,8 @@ def join {φs : List 𝓕.States} (φsΛ : WickContraction φs.length)
simp only [Finset.card_map]
exact φsucΛ.2.1 a ha, by
intro a ha b hb
simp at ha 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
@ -109,7 +111,7 @@ lemma jointLiftLeft_neq_joinLiftRight {φs : List 𝓕.States} {φsΛ : WickCont
by_contra hn
have h1 := jointLiftLeft_disjoint_joinLiftRight a b
rw [hn] at h1
simp 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
@ -125,17 +127,17 @@ lemma joinLift_injective {φs : List 𝓕.States} {φsΛ : WickContraction φs.l
intro a b h
match a, b with
| Sum.inl a, Sum.inl b =>
simp
simp only [Sum.inl.injEq]
exact jointLiftLeft_injective h
| Sum.inr a, Sum.inr b =>
simp
simp only [Sum.inr.injEq]
exact joinLiftRight_injective h
| Sum.inl a, Sum.inr b =>
simp [joinLift] at h
simp only [joinLift] at h
have h1 := jointLiftLeft_neq_joinLiftRight a b
simp_all
| Sum.inr a, Sum.inl b =>
simp [joinLift] at h
simp only [joinLift] at h
have h1 := jointLiftLeft_neq_joinLiftRight b a
simp_all
@ -143,13 +145,14 @@ lemma joinLift_surjective {φs : List 𝓕.States} {φsΛ : WickContraction φs.
{φsucΛ : WickContraction [φsΛ]ᵘᶜ.length} : Function.Surjective (@joinLift _ _ φsΛ φsucΛ) := by
intro a
have ha2 := a.2
simp [- Finset.coe_mem, join] at ha2
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 [joinLift, joinLiftRight]
simp only [joinLift, joinLiftRight]
refine Subtype.eq ?_
exact ha3.2
@ -171,7 +174,8 @@ lemma prod_join {φs : List 𝓕.States} (φsΛ : WickContraction φs.length)
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 [join] at ha
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⟩
@ -227,38 +231,39 @@ lemma join_sndFieldOfContract_joinLift {φs : List 𝓕.States} (φsΛ : WickCon
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 [join]
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 [h1']
simp only [h1', false_or]
apply Iff.intro
· intro h
use a
simp [h]
simp only [h, true_and]
rw [Finset.mapEmbedding_apply]
· intro h
obtain ⟨a, ha, h2⟩ := h
rw [Finset.mapEmbedding_apply] at h2
simp 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 [join]
simp only [join, Finset.le_eq_subset]
rw [Finset.card_union_of_disjoint]
simp
simp only [Finset.card_map]
rw [@Finset.disjoint_left]
intro a ha
simp
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 at hdis
simp only [disjoint_self, Finset.bot_eq_empty] at hdis
have hcard := φsΛ.2.1 a ha
simp_all
@ -266,13 +271,13 @@ lemma join_card {φs : List 𝓕.States} {φsΛ : WickContraction φs.length}
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 [join]
simp only [join, Finset.le_eq_subset, uncontractedListEmd_empty]
ext a
conv_lhs =>
left
left
rw [empty]
simp
simp only [Finset.empty_union, Finset.mem_map, RelEmbedding.coe_toEmbedding]
rw [mem_congr_iff]
apply Iff.intro
· intro h
@ -285,7 +290,7 @@ lemma empty_join {φs : List 𝓕.States} (φsΛ : WickContraction [empty (n :=
simp
· intro h
use Finset.map (finCongr (by simp)).toEmbedding a
simp [h]
simp only [h, true_and]
trans Finset.map (Equiv.refl _).toEmbedding a
rw [Finset.mapEmbedding_apply, Finset.map_map]
rfl
@ -325,7 +330,8 @@ lemma mem_join_uncontracted_of_mem_right_uncontracted {φs : List 𝓕.States}
uncontractedListEmd i ∈ (join φsΛ φsucΛ).uncontracted := by
rw [mem_uncontracted_iff_not_contracted]
intro p hp
simp [join] at 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
@ -333,7 +339,7 @@ lemma mem_join_uncontracted_of_mem_right_uncontracted {φs : List 𝓕.States}
exact hi p hp
· obtain ⟨p, hp, rfl⟩ := hp
rw [Finset.mapEmbedding_apply]
simp
simp only [Finset.mem_map']
rw [mem_uncontracted_iff_not_contracted] at ha
exact ha p hp
@ -344,7 +350,8 @@ lemma exists_mem_left_uncontracted_of_mem_join_uncontracted {φs : List 𝓕.Sta
i ∈ φsΛ.uncontracted := by
rw [@mem_uncontracted_iff_not_contracted]
rw [@mem_uncontracted_iff_not_contracted] at ha
simp [join] at ha
simp only [join, Finset.le_eq_subset, Finset.mem_union, Finset.mem_map,
RelEmbedding.coe_toEmbedding] at ha
intro p hp
have hp' := ha p
simp_all
@ -357,15 +364,16 @@ lemma exists_mem_right_uncontracted_of_mem_join_uncontracted {φs : List 𝓕.St
have hi' := exists_mem_left_uncontracted_of_mem_join_uncontracted _ _ i hi
obtain ⟨j, rfl⟩ := uncontractedListEmd_surjective_mem_uncontracted i hi'
use j
simp
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 [join]
simp only [join, Finset.le_eq_subset, Finset.mem_union, Finset.mem_map,
RelEmbedding.coe_toEmbedding]
right
use p
simp [hp]
simp only [hp, true_and]
rw [Finset.mapEmbedding_apply])
simpa using hip
@ -377,7 +385,7 @@ lemma join_uncontractedList {φs : List 𝓕.States} (φsΛ : WickContraction φ
rw [fin_finset_sort_map_monotone]
congr
ext a
simp
simp only [Finset.mem_map]
apply Iff.intro
· intro h
obtain ⟨a, rfl, ha⟩ := exists_mem_right_uncontracted_of_mem_join_uncontracted _ _ a h
@ -404,9 +412,12 @@ lemma join_uncontractedList_get {φs : List 𝓕.States} (φsΛ : WickContractio
lemma join_uncontractedListGet {φs : List 𝓕.States} (φsΛ : WickContraction φs.length)
(φsucΛ : WickContraction [φsΛ]ᵘᶜ.length) :
(join φsΛ φsucΛ).uncontractedListGet = φsucΛ.uncontractedListGet := by
simp [uncontractedListGet, join_uncontractedList]
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 [uncontractedListEmd, uncontractedIndexEquiv]
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)
@ -427,7 +438,8 @@ lemma join_assoc {φs : List 𝓕.States} (φsΛ : WickContraction φs.length)
ext a
by_cases ha : a ∈ φsΛ.1
· simp [ha, join]
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
@ -459,7 +471,7 @@ lemma join_assoc {φs : List 𝓕.States} (φsΛ : WickContraction φs.length)
right
let a' := congrLiftInv _ ⟨a, ha'⟩
use a'
simp
simp only [Finset.coe_mem, true_and]
simp only [a']
rw [Finset.mapEmbedding_apply]
rw [join_uncontractedListEmb]
@ -478,7 +490,7 @@ lemma join_getDual?_apply_uncontractedListEmb_eq_none_iff {φs : List 𝓕.Stat
apply Iff.intro
· intro h
obtain ⟨a, ha', ha⟩ := exists_mem_right_uncontracted_of_mem_join_uncontracted _ _ (uncontractedListEmd i) h
simp at ha'
simp only [EmbeddingLike.apply_eq_iff_eq] at ha'
subst ha'
exact ha
· intro h
@ -498,10 +510,11 @@ lemma join_getDual?_apply_uncontractedListEmb_some {φs : List 𝓕.States} (φs
((join φsΛ φsucΛ).getDual? (uncontractedListEmd i)) =
some (uncontractedListEmd ((φsucΛ.getDual? i).get (by simpa using hi))) := by
rw [getDual?_eq_some_iff_mem]
simp [join]
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 using hi)}
simp
simp only [self_getDual?_get_mem, true_and]
rw [Finset.mapEmbedding_apply]
simp
@ -514,11 +527,11 @@ lemma join_getDual?_apply_uncontractedListEmb {φs : List 𝓕.States} (φsΛ :
have h1 : (φsucΛ.getDual? i) =(φsucΛ.getDual? i).get (by simpa using h) :=
Eq.symm (Option.some_get h)
conv_rhs => rw [h1]
simp [- Option.some_get]
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
simp only [Option.map_none', join_getDual?_apply_uncontractedListEmb_eq_none_iff]
exact h
/-!
@ -535,7 +548,8 @@ 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 [join]
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
@ -549,7 +563,7 @@ lemma join_sub_quot (S : Finset (Finset (Fin φs.length))) (ha : S ⊆ φsΛ.1)
· right
obtain ⟨a, rfl, ha⟩ := h1
use a
simp [ha]
simp only [ha, true_and]
rw [Finset.mapEmbedding_apply]
lemma subContraction_card_plus_quotContraction_card_eq (S : Finset (Finset (Fin φs.length)))
@ -565,10 +579,11 @@ lemma stat_signFinset_right {φs : List 𝓕.States} (φsΛ : WickContraction φ
(φ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 [ofFinset]
simp only [ofFinset]
congr 1
rw [← fin_finset_sort_map_monotone]
simp
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
@ -578,18 +593,19 @@ lemma signFinset_right_map_uncontractedListEmd_eq_filter {φs : List 𝓕.States
((join φsΛ φsucΛ).signFinset (uncontractedListEmd i) (uncontractedListEmd j)).filter
(fun c => c ∈ φsΛ.uncontracted) := by
ext a
simp
simp only [Finset.mem_map, Finset.mem_filter]
apply Iff.intro
· intro h
obtain ⟨a, ha, rfl⟩ := h
apply And.intro
· simp_all [signFinset]
· 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
simp_all only [and_true]
rcases ha2 with ha2 | ha2
· simp [ha2]
· right
@ -605,7 +621,9 @@ lemma signFinset_right_map_uncontractedListEmd_eq_filter {φs : List 𝓕.States
obtain ⟨a, rfl⟩ := h2'
use a
have h1 := h.1
simp_all [signFinset]
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
@ -617,7 +635,7 @@ lemma signFinset_right_map_uncontractedListEmd_eq_filter {φs : List 𝓕.States
exact h1
exact fun _ _ h => uncontractedListEmd_strictMono h
· have h1 := h.2.2
simp_all
simp_all only [and_true]
rcases h1 with h1 | h1
· simp [h1]
· right
@ -655,16 +673,17 @@ lemma join_singleton_signFinset_eq_filter {φs : List 𝓕.States}
((h1 : ((join (singleton h) φsucΛ).getDual? c).isSome) →
(((join (singleton h) φsucΛ).getDual? c).get h1) < i))) := by
ext a
simp [signFinset, and_assoc]
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 [h1]
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 [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
@ -682,9 +701,9 @@ lemma join_singleton_signFinset_eq_filter {φs : List 𝓕.States}
have hij : ((singleton h).join φsucΛ).getDual? i = j := by
rw [@getDual?_eq_some_iff_mem]
simp [join, singleton]
simp [hn] at hij
simp only [hn, getDual?_getDual?_get_get, Option.some.injEq] at hij
omega
· simp at h2'
· simp only [Bool.not_eq_true, Option.not_isSome, Option.isNone_iff_eq_none] at h2'
simp [h2']
@ -756,7 +775,8 @@ lemma join_singleton_getDual?_right {φs : List 𝓕.States}
(φsucΛ : WickContraction [singleton h]ᵘᶜ.length) :
(join (singleton h) φsucΛ).getDual? j = some i := by
rw [@getDual?_eq_some_iff_mem]
simp [singleton, join]
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
@ -779,36 +799,41 @@ lemma joinSignRightExtra_eq_i_j_finset_eq_if {φs : List 𝓕.States}
rw [Finset.filter_comm]
have h11 : (Finset.filter (fun c => c ∉ (singleton h).uncontracted) Finset.univ) = {i, j} := by
ext x
simp
simp only [Finset.mem_filter, Finset.mem_univ, true_and, Finset.mem_insert,
Finset.mem_singleton]
rw [@mem_uncontracted_iff_not_contracted]
simp [singleton]
simp only [singleton, Finset.mem_singleton, forall_eq, Finset.mem_insert, not_or, not_and,
Decidable.not_not]
omega
rw [h11]
ext x
simp
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 [hj1]
· simp only [hj1, false_and, ↓reduceIte, Finset.not_mem_empty, false_or]
have hi1 : ¬ uncontractedListEmd (φsucΛ.fstFieldOfContract a) < i := by omega
simp [hi1]
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 [hi1]
· simp only [hi1, and_false, ↓reduceIte, Finset.not_mem_empty, or_false]
have hj2 : ¬ j < uncontractedListEmd (φsucΛ.sndFieldOfContract a) := by omega
simp [hj2]
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 [hi1, hj1]
simp only [hj1, true_and, hi1, and_true]
by_cases hi2 : ¬ uncontractedListEmd (φsucΛ.fstFieldOfContract a) < i
· simp [hi2]
· 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
@ -817,31 +842,35 @@ lemma joinSignRightExtra_eq_i_j_finset_eq_if {φs : List 𝓕.States}
· subst h
omega
· subst h
simp
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 [hi2]
simp only [hi2, and_true, ↓reduceIte, Finset.mem_singleton]
by_cases hj3 : ¬ j < uncontractedListEmd (φsucΛ.sndFieldOfContract a)
· simp [hj3]
· simp only [hj3, ↓reduceIte, Finset.not_mem_empty, false_or]
apply Iff.intro
· intro h
omega
· intro h
subst h
simp
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 [hj3]
simp only [hj3, ↓reduceIte, Finset.mem_singleton]
apply Iff.intro
· intro h
omega
· intro h
rcases h with h1 | h1
· subst h1
simp
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
simp only [true_or, join_singleton_getDual?_left, reduceCtorEq, Option.isSome_some,
Option.get_some, forall_const, false_or, true_and]
omega
@ -860,13 +889,12 @@ lemma joinSignLeftExtra_eq_joinSignRightExtra {φs : List 𝓕.States}
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
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
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 =>
@ -896,38 +924,38 @@ lemma joinSignLeftExtra_eq_joinSignRightExtra {φs : List 𝓕.States}
· have hi1 : ¬ uncontractedListEmd (φsucΛ.fstFieldOfContract a) < i := by omega
simp [hj1, hi1]
· have hj1 : uncontractedListEmd (φsucΛ.fstFieldOfContract a) < j := by omega
simp [hj1]
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 [hi2, hi2n]
simp only [hi2n, and_false, ↓reduceIte, map_one, hi2, true_and, one_mul, and_true]
by_cases hj2 : ¬ j < uncontractedListEmd (φsucΛ.sndFieldOfContract a)
· simp [hj2]
· simp only [hj2, false_and, ↓reduceIte, Finset.empty_union]
have hj2 : uncontractedListEmd (φsucΛ.sndFieldOfContract a) < j:= by omega
simp [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 [hi1, ofFinset_singleton]
simp only [hi1, ↓reduceIte, ofFinset_singleton, List.get_eq_getElem]
erw [hs]
exact exchangeSign_symm (𝓕|>ₛφs[↑j]) (𝓕|>ₛ[singleton h]ᵘᶜ[↑(φsucΛ.sndFieldOfContract a)])
· simp at hj2
simp [hj2]
· 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 [hi1]
simp only [hi1, and_true, ↓reduceIte]
have hj2 : ¬ uncontractedListEmd (φsucΛ.sndFieldOfContract a) < j := by omega
simp [hj2]
simp only [hj2, ↓reduceIte, map_one]
rw [← ofFinset_union_disjoint]
simp only [instCommGroup, ofFinset_singleton, List.get_eq_getElem, hs]
erw [hs]
simp
simp
omega
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]))
@ -968,21 +996,21 @@ lemma exists_join_singleton_of_card_ge_zero {φs : List 𝓕.States} (φsΛ : Wi
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 [← subContraction_singleton_eq_singleton]
simp only [Fin.getElem_fin]
apply And.intro
· have h1 := join_congr (subContraction_singleton_eq_singleton _ ⟨a, ha⟩).symm (φsucΛ := φsucΛ)
simp [h1, φ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 [φsucΛ]
· simp only [id_eq, eq_mpr_eq_cast, φsucΛ]
rw [gradingCompliant_congr (φs' := [(φsΛ.subContraction {a} (by simpa using ha))]ᵘᶜ)]
simp
simp only [id_eq, eq_mpr_eq_cast, congr_trans_apply, congr_refl]
exact quotContraction_gradingCompliant hc
rw [← subContraction_singleton_eq_singleton]
· simp [φsucΛ]
· 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 [subContraction] at h1
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)
@ -992,7 +1020,7 @@ lemma join_sign_induction {φs : List 𝓕.States} (φsΛ : WickContraction φs.
| 0, hn => by
rw [@card_zero_iff_empty] at hn
subst hn
simp [sign_empty]
simp only [empty_join, sign_empty, one_mul]
apply sign_congr
simp
| Nat.succ n, hn => by
@ -1005,7 +1033,7 @@ lemma join_sign_induction {φs : List 𝓕.States} (φsΛ : WickContraction φs.
rw [join_sign_induction φsucΛ' (congr (by simp [join_uncontractedListGet]) φsucΛ) h2
n hn]
rw [mul_assoc]
simp [sign_congr]
simp only [mul_eq_mul_left_iff]
left
left
apply sign_congr
@ -1019,11 +1047,12 @@ lemma join_sign {φs : List 𝓕.States} (φsΛ : WickContraction φs.length)
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 [GradingCompliant]
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
simp only [Subtype.coe_eta, join_fstFieldOfContract_joinLiftLeft,
join_sndFieldOfContract_joinLift]
exact ha2
lemma join_sign_timeContract {φs : List 𝓕.States} (φsΛ : WickContraction φs.length)

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

@ -25,11 +25,11 @@ open FieldStatistic
def singleton {i j : Fin n} (hij : i < j) : WickContraction n :=
⟨{{i, j}}, by
intro i hi
simp at hi
simp only [Finset.mem_singleton] at hi
subst hi
rw [@Finset.card_eq_two]
use i, j
simp
simp only [ne_eq, and_true]
omega
, by
intro i hi j hj
@ -80,7 +80,7 @@ lemma singleton_getDual?_eq_none_iff_neq {i j : Fin n} (hij : i < j) (a : Fin n)
(singleton hij).getDual? a = none ↔ (i ≠ a ∧ j ≠ a) := by
rw [getDual?_eq_none_iff_mem_uncontracted]
rw [mem_uncontracted_iff_not_contracted]
simp [singleton]
simp only [singleton, Finset.mem_singleton, forall_eq, Finset.mem_insert, not_or, ne_eq]
omega
lemma singleton_uncontractedEmd_neq_left {φs : List 𝓕.States} {i j : Fin φs.length} (hij : i < j)
@ -108,7 +108,8 @@ lemma singleton_uncontractedEmd_neq_right {φs : List 𝓕.States} {i j : Fin φ
@[simp]
lemma mem_signFinset {i j : Fin n} (hij : i < j) (a : Fin n) :
a ∈ (singleton hij).signFinset i j ↔ i < a ∧ a < j := by
simp [signFinset]
simp only [signFinset, Finset.mem_filter, Finset.mem_univ, true_and, and_congr_right_iff,
and_iff_left_iff_imp]
intro h1 h2
rw [@singleton_getDual?_eq_none_iff_neq]
apply Or.inl
@ -119,7 +120,7 @@ lemma subContraction_singleton_eq_singleton {φs : List 𝓕.States}
(a : φsΛ.1) : φsΛ.subContraction {a.1} (by simp) =
singleton (φsΛ.fstFieldOfContract_lt_sndFieldOfContract a) := by
apply Subtype.ext
simp [subContraction, singleton]
simp only [subContraction, singleton, Finset.singleton_inj]
exact finset_eq_fstFieldOfContract_sndFieldOfContract φsΛ a
lemma singleton_timeContract {φs : List 𝓕.States} {i j : Fin φs.length} (hij : i < j) :

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

@ -51,7 +51,7 @@ lemma staticContract_insertAndContract_some
(φsΛ ↩Λ φ i (some j)).staticContract =
(if i < i.succAbove j then
⟨[anPart φ, ofFieldOp φs[j.1]]ₛ, superCommute_anPart_ofFieldOp_mem_center _ _⟩
else ⟨[anPart φs[j.1], ofFieldOp φ]ₛ, superCommute_anPart_ofFieldOp_mem_center _ _⟩) *
else ⟨[anPart φs[j.1], ofFieldOp φ]ₛ, superCommute_anPart_ofFieldOp_mem_center _ _⟩) *
φsΛ.staticContract := by
rw [staticContract, insertAndContract_some_prod_contractions]
congr 1

39
HepLean/PerturbationTheory/WickContraction/SubContraction.lean
View file

@ -37,21 +37,20 @@ def quotContraction (S : Finset (Finset (Fin φs.length))) (ha : S ⊆ φsΛ.1)
⟨Finset.filter (fun a => Finset.map uncontractedListEmd a ∈ φsΛ.1) Finset.univ,
by
intro a ha'
simp at ha'
simpa using φsΛ.2.1 (Finset.map uncontractedListEmd a) ha'
, by
simp only [Finset.mem_filter, Finset.mem_univ, true_and] at ha'
simpa using φsΛ.2.1 (Finset.map uncontractedListEmd a) ha' , by
intro a ha b hb
simp at ha hb
simp only [Finset.mem_filter, Finset.mem_univ, true_and] at ha hb
by_cases hab : a = b
· simp [hab]
· simp [hab]
· simp only [hab, false_or]
have hx := φsΛ.2.2 (Finset.map uncontractedListEmd a) ha (Finset.map uncontractedListEmd b) hb
simp_all⟩
lemma mem_of_mem_quotContraction {S : Finset (Finset (Fin φs.length))} {hs : S ⊆ φsΛ.1}
{a : Finset (Fin [φsΛ.subContraction S hs]ᵘᶜ.length)}
(ha : a ∈ (quotContraction S hs).1) : Finset.map uncontractedListEmd a ∈ φsΛ.1 := by
simp [quotContraction] at ha
simp only [quotContraction, Finset.mem_filter, Finset.mem_univ, true_and] at ha
exact ha
lemma mem_subContraction_or_quotContraction {S : Finset (Finset (Fin φs.length))} {hs : S ⊆ φsΛ.1}
@ -60,8 +59,8 @@ lemma mem_subContraction_or_quotContraction {S : Finset (Finset (Fin φs.length)
∃ a', Finset.map uncontractedListEmd a' = a ∧ a' ∈ (quotContraction S hs).1 := by
by_cases h1 : a ∈ (φsΛ.subContraction S hs).1
· simp [h1]
simp [h1]
simp [subContraction] at h1
simp only [h1, false_or]
simp only [subContraction] at h1
have h2 := φsΛ.2.1 a ha
rw [@Finset.card_eq_two] at h2
obtain ⟨i, j, hij, rfl⟩ := h2
@ -70,25 +69,26 @@ lemma mem_subContraction_or_quotContraction {S : Finset (Finset (Fin φs.length)
intro p hp
have hp' : p ∈ φsΛ.1 := hs hp
have hp2 := φsΛ.2.2 p hp' {i, j} ha
simp [subContraction] at hp
simp only [subContraction] at hp
rcases hp2 with hp2 | hp2
· simp_all
simp at hp2
simp only [Finset.disjoint_insert_right, Finset.disjoint_singleton_right] at hp2
exact hp2.1
have hj : j ∈ (φsΛ.subContraction S hs).uncontracted := by
rw [mem_uncontracted_iff_not_contracted]
intro p hp
have hp' : p ∈ φsΛ.1 := hs hp
have hp2 := φsΛ.2.2 p hp' {i, j} ha
simp [subContraction] at hp
simp only [subContraction] at hp
rcases hp2 with hp2 | hp2
· simp_all
simp at hp2
simp only [Finset.disjoint_insert_right, Finset.disjoint_singleton_right] at hp2
exact hp2.2
obtain ⟨i, rfl⟩ := uncontractedListEmd_surjective_mem_uncontracted i hi
obtain ⟨j, rfl⟩ := uncontractedListEmd_surjective_mem_uncontracted j hj
use {i, j}
simp [quotContraction]
simp only [Finset.map_insert, Finset.map_singleton, quotContraction, Finset.mem_filter,
Finset.mem_univ, true_and]
exact ha
@[simp]
@ -105,12 +105,12 @@ lemma subContraction_fstFieldOfContract {S : Finset (Finset (Fin φs.length))} {
φsΛ.fstFieldOfContract ⟨a.1, mem_of_mem_subContraction a.2⟩:= by
apply eq_fstFieldOfContract_of_mem _ _ _ (φsΛ.sndFieldOfContract ⟨a.1, mem_of_mem_subContraction a.2⟩)
· have ha := finset_eq_fstFieldOfContract_sndFieldOfContract _ ⟨a.1, mem_of_mem_subContraction a.2⟩
simp at ha
simp only at ha
conv_lhs =>
rw [ha]
simp
· have ha := finset_eq_fstFieldOfContract_sndFieldOfContract _ ⟨a.1, mem_of_mem_subContraction a.2⟩
simp at ha
simp only at ha
conv_lhs =>
rw [ha]
simp
@ -123,12 +123,12 @@ lemma subContraction_sndFieldOfContract {S : Finset (Finset (Fin φs.length))} {
φsΛ.sndFieldOfContract ⟨a.1, mem_of_mem_subContraction a.2⟩:= by
apply eq_sndFieldOfContract_of_mem _ _ (φsΛ.fstFieldOfContract ⟨a.1, mem_of_mem_subContraction a.2⟩)
· have ha := finset_eq_fstFieldOfContract_sndFieldOfContract _ ⟨a.1, mem_of_mem_subContraction a.2⟩
simp at ha
simp only at ha
conv_lhs =>
rw [ha]
simp
· have ha := finset_eq_fstFieldOfContract_sndFieldOfContract _ ⟨a.1, mem_of_mem_subContraction a.2⟩
simp at ha
simp only at ha
conv_lhs =>
rw [ha]
simp
@ -162,12 +162,13 @@ lemma quotContraction_sndFieldOfContract_uncontractedListEmd {S : Finset (Finset
lemma quotContraction_gradingCompliant {S : Finset (Finset (Fin φs.length))} {hs : S ⊆ φsΛ.1}
(hsΛ : φsΛ.GradingCompliant) :
GradingCompliant [φsΛ.subContraction S hs]ᵘᶜ (quotContraction S hs) := by
simp [GradingCompliant]
simp only [GradingCompliant, Fin.getElem_fin, Subtype.forall]
intro a ha
have h1' := mem_of_mem_quotContraction ha
erw [subContraction_uncontractedList_get]
erw [subContraction_uncontractedList_get]
simp
simp only [quotContraction_fstFieldOfContract_uncontractedListEmd, Fin.getElem_fin,
quotContraction_sndFieldOfContract_uncontractedListEmd]
apply hsΛ
lemma mem_quotContraction_iff {S : Finset (Finset (Fin φs.length))} {hs : S ⊆ φsΛ.1}

280
HepLean/PerturbationTheory/WickContraction/TimeSet.lean
View file

@ -20,48 +20,49 @@ variable {n : ℕ} (c : WickContraction n)
open HepLean.List
open FieldOpAlgebra
def EqTimeOnlyCond {φs : List 𝓕.States} (φsΛ : WickContraction φs.length) : Prop :=
/-- The condition on a Wick contraction which is true iff and only if every contraction
is between two fields of equal time. -/
def EqTimeOnly {φs : List 𝓕.States} (φsΛ : WickContraction φs.length) : Prop :=
∀ (i j), {i, j} ∈ φsΛ.1 → timeOrderRel φs[i] φs[j]
noncomputable section
noncomputable instance {φs : List 𝓕.States} (φsΛ : WickContraction φs.length) :
Decidable (EqTimeOnlyCond φsΛ) :=
instance {φs : List 𝓕.States} (φsΛ : WickContraction φs.length) :
Decidable (EqTimeOnly φsΛ) :=
inferInstanceAs (Decidable (∀ (i j), {i, j} ∈ φsΛ.1 → timeOrderRel φs[i] φs[j]))
noncomputable def EqTimeOnly (φs : List 𝓕.States) :
Finset (WickContraction φs.length) := {φsΛ | EqTimeOnlyCond φsΛ}
namespace EqTimeOnly
variable {φs : List 𝓕.States} (φsΛ : EqTimeOnly φs)
variable {φs : List 𝓕.States} (φsΛ : WickContraction φs.length)
lemma timeOrderRel_of_mem {i j : Fin φs.length} (h : {i, j} ∈ φsΛ.1.1) :
lemma timeOrderRel_of_eqTimeOnly_pair {i j : Fin φs.length} (h : {i, j} ∈ φsΛ.1)
(hc : EqTimeOnly φsΛ) :
timeOrderRel φs[i] φs[j] := by
have h' := φsΛ.2
simp only [EqTimeOnly, EqTimeOnlyCond, ne_eq, Fin.getElem_fin, Finset.mem_filter, Finset.mem_univ,
have h' := hc
simp only [EqTimeOnly, ne_eq, Fin.getElem_fin, Finset.mem_filter, Finset.mem_univ,
true_and] at h'
exact h' i j h
lemma timeOrderRel_both_of_mem {i j : Fin φs.length} (h : {i, j} ∈ φsΛ.1.1) :
lemma timeOrderRel_both_of_eqTimeOnly {i j : Fin φs.length} (h : {i, j} ∈ φsΛ.1)
(hc : EqTimeOnly φsΛ) :
timeOrderRel φs[i] φs[j] ∧ timeOrderRel φs[j] φs[i] := by
apply And.intro
· exact timeOrderRel_of_mem φsΛ h
· apply timeOrderRel_of_mem φsΛ
· exact timeOrderRel_of_eqTimeOnly_pair φsΛ h hc
· apply timeOrderRel_of_eqTimeOnly_pair φsΛ _ hc
rw [@Finset.pair_comm]
exact h
lemma mem_iff_forall_finset {φs : List 𝓕.States} (φsΛ : WickContraction φs.length) :
φsΛ ∈ EqTimeOnly φs ↔ ∀ (a : φsΛ.1),
lemma eqTimeOnly_iff_forall_finset {φs : List 𝓕.States} (φsΛ : WickContraction φs.length) :
φsΛ.EqTimeOnly ↔ ∀ (a : φsΛ.1),
timeOrderRel (φs[φsΛ.fstFieldOfContract a]) (φs[φsΛ.sndFieldOfContract a])
∧ timeOrderRel (φs[φsΛ.sndFieldOfContract a]) (φs[φsΛ.fstFieldOfContract a]) := by
apply Iff.intro
· intro h a
apply timeOrderRel_both_of_mem ⟨φsΛ, h⟩
simp
apply timeOrderRel_both_of_eqTimeOnly φsΛ _ h
rw [← finset_eq_fstFieldOfContract_sndFieldOfContract]
simp
· intro h
simp [EqTimeOnly, EqTimeOnlyCond]
simp only [EqTimeOnly, Fin.getElem_fin, Finset.mem_filter, Finset.mem_univ,
true_and]
intro i j h1
have h' := h ⟨{i, j}, h1⟩
by_cases hij: i < j
@ -94,43 +95,46 @@ lemma mem_iff_forall_finset {φs : List 𝓕.States} (φsΛ : WickContraction φ
simp_all
@[simp]
lemma empty_mem {φs : List 𝓕.States} : empty ∈ EqTimeOnly φs := by
rw [mem_iff_forall_finset]
lemma empty_mem {φs : List 𝓕.States} : empty (n := φs.length).EqTimeOnly := by
rw [eqTimeOnly_iff_forall_finset]
simp [empty]
lemma staticContract_eq_timeContract : φsΛ.1.staticContract = φsΛ.1.timeContract := by
lemma staticContract_eq_timeContract_of_eqTimeOnly (h : φsΛ.EqTimeOnly) :
φsΛ.staticContract = φsΛ.timeContract := by
simp only [staticContract, timeContract]
apply congrArg
funext a
ext
simp only [List.get_eq_getElem]
rw [timeContract_of_timeOrderRel]
apply timeOrderRel_of_mem φsΛ
apply timeOrderRel_of_eqTimeOnly_pair φsΛ
rw [← finset_eq_fstFieldOfContract_sndFieldOfContract]
exact a.2
exact h
lemma mem_congr {φs φs' : List 𝓕.States} (h : φs = φs') (φsΛ : WickContraction φs.length):
congr (by simp [h]) φsΛ ∈ EqTimeOnly φs' ↔ φsΛ ∈ EqTimeOnly φs := by
lemma eqTimeOnly_congr {φs φs' : List 𝓕.States} (h : φs = φs') (φsΛ : WickContraction φs.length):
(congr (by simp [h]) φsΛ).EqTimeOnly (φs := φs') ↔ φsΛ.EqTimeOnly := by
subst h
simp
lemma quotContraction_mem {φs : List 𝓕.States} {φsΛ : WickContraction φs.length}
(h : φsΛ ∈ EqTimeOnly φs) (S : Finset (Finset (Fin φs.length))) (ha : S ⊆ φsΛ.1) :
φsΛ.quotContraction S ha ∈ EqTimeOnly [φsΛ.subContraction S ha]ᵘᶜ := by
rw [mem_iff_forall_finset]
lemma quotContraction_eqTimeOnly {φs : List 𝓕.States} {φsΛ : WickContraction φs.length}
(h : φsΛ.EqTimeOnly) (S : Finset (Finset (Fin φs.length))) (ha : S ⊆ φsΛ.1) :
(φsΛ.quotContraction S ha).EqTimeOnly := by
rw [eqTimeOnly_iff_forall_finset]
intro a
simp
simp only [Fin.getElem_fin]
erw [subContraction_uncontractedList_get]
erw [subContraction_uncontractedList_get]
simp
rw [mem_iff_forall_finset] at h
simp only [quotContraction_fstFieldOfContract_uncontractedListEmd, Fin.getElem_fin,
quotContraction_sndFieldOfContract_uncontractedListEmd]
rw [eqTimeOnly_iff_forall_finset] at h
apply h
lemma exists_join_singleton_of_card_ge_zero {φs : List 𝓕.States} (φsΛ : WickContraction φs.length)
(h : 0 < φsΛ.1.card) (h1 : φsΛ ∈ EqTimeOnly φs) :
(h : 0 < φsΛ.1.card) (h1 : φsΛ.EqTimeOnly) :
∃ (i j : Fin φs.length) (h : i < j) (φsucΛ : WickContraction [singleton h]ᵘᶜ.length),
φsΛ = join (singleton h) φsucΛ ∧ (timeOrderRel φs[i] φs[j] ∧ timeOrderRel φs[j] φs[i])
∧ φsucΛ ∈ EqTimeOnly [singleton h]ᵘᶜ ∧ φsucΛ.1.card + 1 = φsΛ.1.card := by
∧ φsucΛ.EqTimeOnly ∧ φsucΛ.1.card + 1 = φsΛ.1.card := by
obtain ⟨a, ha⟩ := exists_contraction_pair_of_card_ge_zero φsΛ h
use φsΛ.fstFieldOfContract ⟨a, ha⟩
use φsΛ.sndFieldOfContract ⟨a, ha⟩
@ -139,29 +143,28 @@ lemma exists_join_singleton_of_card_ge_zero {φs : List 𝓕.States} (φsΛ : Wi
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 [← subContraction_singleton_eq_singleton]
simp only [Fin.getElem_fin]
apply And.intro
· have h1 := join_congr (subContraction_singleton_eq_singleton _ ⟨a, ha⟩).symm (φsucΛ := φsucΛ)
simp [h1, φsucΛ]
simp only [id_eq, eq_mpr_eq_cast, h1, congr_trans_apply, congr_refl, φsucΛ]
rw [join_sub_quot]
· apply And.intro
· apply timeOrderRel_both_of_mem ⟨φsΛ, h1⟩
simp
· apply timeOrderRel_both_of_eqTimeOnly φsΛ _ h1
rw [← finset_eq_fstFieldOfContract_sndFieldOfContract]
simp [ha]
apply And.intro
· simp [φsucΛ]
rw [mem_congr (φs := [(φsΛ.subContraction {a} (by simpa using ha))]ᵘᶜ)]
simp
exact quotContraction_mem h1 _ _
· simp only [id_eq, eq_mpr_eq_cast, φsucΛ]
rw [eqTimeOnly_congr (φs := [(φsΛ.subContraction {a} (by simpa using ha))]ᵘᶜ)]
simp only [id_eq, eq_mpr_eq_cast]
exact quotContraction_eqTimeOnly h1 _ _
rw [← subContraction_singleton_eq_singleton]
· simp [φsucΛ]
· 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 [subContraction] at h1
simp only [subContraction, Finset.card_singleton, id_eq, eq_mpr_eq_cast] at h1
omega
lemma timeOrder_timeContract_mul_of_mem_mid_induction {φs : List 𝓕.States} (φsΛ : WickContraction φs.length)
(hl : φsΛ ∈ EqTimeOnly φs) (a b: 𝓕.FieldOpAlgebra) : (n : ℕ) → (hn : φsΛ.1.card = n) →
lemma timeOrder_timeContract_mul_of_eqTimeOnly_mid_induction {φs : List 𝓕.States} (φsΛ : WickContraction φs.length)
(hl : φsΛ.EqTimeOnly) (a b: 𝓕.FieldOpAlgebra) : (n : ℕ) → (hn : φsΛ.1.card = n) →
𝓣(a * φsΛ.timeContract.1 * b) = φsΛ.timeContract.1 * 𝓣(a * b)
| 0, hn => by
rw [@card_zero_iff_empty] at hn
@ -171,35 +174,37 @@ lemma timeOrder_timeContract_mul_of_mem_mid_induction {φs : List 𝓕.States}
obtain ⟨i, j, hij, φsucΛ, rfl, h2, h3, h4⟩ := exists_join_singleton_of_card_ge_zero φsΛ (by simp [hn]) hl
rw [join_timeContract]
rw [singleton_timeContract]
simp
simp only [Fin.getElem_fin, MulMemClass.coe_mul]
trans timeOrder (a * FieldOpAlgebra.timeContract φs[↑i] φs[↑j] * (φsucΛ.timeContract.1 * b))
simp [mul_assoc]
simp only [mul_assoc, Fin.getElem_fin]
rw [timeOrder_timeContract_eq_time_mid]
have ih := timeOrder_timeContract_mul_of_mem_mid_induction φsucΛ h3 a b n (by omega)
have ih := timeOrder_timeContract_mul_of_eqTimeOnly_mid_induction φsucΛ h3 a b n (by omega)
rw [← mul_assoc, ih]
simp [mul_assoc]
simp_all
simp only [Fin.getElem_fin, mul_assoc]
simp_all only [Nat.succ_eq_add_one, Fin.getElem_fin, add_left_inj]
simp_all
lemma timeOrder_timeContract_mul_of_mem_mid {φs : List 𝓕.States} (φsΛ : WickContraction φs.length)
(hl : φsΛ ∈ EqTimeOnly φs) (a b : 𝓕.FieldOpAlgebra) :
lemma timeOrder_timeContract_mul_of_eqTimeOnly_mid {φs : List 𝓕.States}
(φsΛ : WickContraction φs.length)
(hl : φsΛ.EqTimeOnly) (a b : 𝓕.FieldOpAlgebra) :
𝓣(a * φsΛ.timeContract.1 * b) = φsΛ.timeContract.1 * 𝓣(a * b) := by
exact timeOrder_timeContract_mul_of_mem_mid_induction φsΛ hl a b φsΛ.1.card rfl
exact timeOrder_timeContract_mul_of_eqTimeOnly_mid_induction φsΛ hl a b φsΛ.1.card rfl
lemma timeOrder_timeContract_mul_of_mem_left {φs : List 𝓕.States} (φsΛ : WickContraction φs.length)
(hl : φsΛ ∈ EqTimeOnly φs) ( b : 𝓕.FieldOpAlgebra) :
lemma timeOrder_timeContract_mul_of_eqTimeOnly_left {φs : List 𝓕.States}
(φsΛ : WickContraction φs.length)
(hl : φsΛ.EqTimeOnly) ( b : 𝓕.FieldOpAlgebra) :
𝓣( φsΛ.timeContract.1 * b) = φsΛ.timeContract.1 * 𝓣( b) := by
trans 𝓣(1 * φsΛ.timeContract.1 * b)
simp
rw [timeOrder_timeContract_mul_of_mem_mid φsΛ hl]
simp only [one_mul]
rw [timeOrder_timeContract_mul_of_eqTimeOnly_mid φsΛ hl]
simp
lemma exists_join_singleton_of_ne_mem {φs : List 𝓕.States} (φsΛ : WickContraction φs.length)
(h1 : ¬ φsΛ ∈ EqTimeOnly φs) :
lemma exists_join_singleton_of_not_eqTimeOnly {φs : List 𝓕.States} (φsΛ : WickContraction φs.length)
(h1 : ¬ φsΛ.EqTimeOnly) :
∃ (i j : Fin φs.length) (h : i < j) (φsucΛ : WickContraction [singleton h]ᵘᶜ.length),
φsΛ = join (singleton h) φsucΛ ∧ (¬ timeOrderRel φs[i] φs[j] ∨ ¬ timeOrderRel φs[j] φs[i]) := by
rw [mem_iff_forall_finset] at h1
simp at h1
rw [eqTimeOnly_iff_forall_finset] at h1
simp only [Fin.getElem_fin, Subtype.forall, not_forall, not_and] at h1
obtain ⟨a, ha, hr⟩ := h1
use φsΛ.fstFieldOfContract ⟨a, ha⟩
use φsΛ.sndFieldOfContract ⟨a, ha⟩
@ -208,38 +213,38 @@ lemma exists_join_singleton_of_ne_mem {φs : List 𝓕.States} (φsΛ : WickCont
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 [← subContraction_singleton_eq_singleton]
simp only [Fin.getElem_fin]
apply And.intro
· have h1 := join_congr (subContraction_singleton_eq_singleton _ ⟨a, ha⟩).symm (φsucΛ := φsucΛ)
simp [h1, φsucΛ]
simp only [id_eq, eq_mpr_eq_cast, h1, congr_trans_apply, congr_refl, φsucΛ]
rw [join_sub_quot]
· by_cases h1 : timeOrderRel φs[↑(φsΛ.fstFieldOfContract ⟨a, ha⟩)]
φs[↑(φsΛ.sndFieldOfContract ⟨a, ha⟩)]
· simp_all [h1]
· simp_all [h1]
lemma timeOrder_timeContract_of_not_mem {φs : List 𝓕.States} (φsΛ : WickContraction φs.length)
(hl : ¬ φsΛ ∈ EqTimeOnly φs) : 𝓣(φsΛ.timeContract.1) = 0 := by
obtain ⟨i, j, hij, φsucΛ, rfl, hr⟩ := exists_join_singleton_of_ne_mem φsΛ hl
lemma timeOrder_timeContract_of_not_eqTimeOnly {φs : List 𝓕.States} (φsΛ : WickContraction φs.length)
(hl : ¬ φsΛ.EqTimeOnly) : 𝓣(φsΛ.timeContract.1) = 0 := by
obtain ⟨i, j, hij, φsucΛ, rfl, hr⟩ := exists_join_singleton_of_not_eqTimeOnly φsΛ hl
rw [join_timeContract]
rw [singleton_timeContract]
simp
simp only [Fin.getElem_fin, MulMemClass.coe_mul]
rw [timeOrder_timeOrder_left]
rw [timeOrder_timeContract_neq_time]
simp
simp_all
simp only [zero_mul, map_zero]
simp_all only [Fin.getElem_fin, not_and]
intro h
simp_all
lemma timeOrder_staticContract_of_not_mem {φs : List 𝓕.States} (φsΛ : WickContraction φs.length)
(hl : ¬ φsΛ ∈ EqTimeOnly φs) : 𝓣(φsΛ.staticContract.1) = 0 := by
obtain ⟨i, j, hij, φsucΛ, rfl, hr⟩ := exists_join_singleton_of_ne_mem φsΛ hl
(hl : ¬ φsΛ.EqTimeOnly) : 𝓣(φsΛ.staticContract.1) = 0 := by
obtain ⟨i, j, hij, φsucΛ, rfl, hr⟩ := exists_join_singleton_of_not_eqTimeOnly φsΛ hl
rw [join_staticContract]
simp
simp only [MulMemClass.coe_mul]
rw [singleton_staticContract]
rw [timeOrder_timeOrder_left]
rw [timeOrder_superCommute_anPart_ofFieldOp_neq_time]
simp
simp only [zero_mul, map_zero]
intro h
simp_all
@ -259,7 +264,7 @@ noncomputable instance {φs : List 𝓕.States} (φsΛ : WickContraction φs.le
lemma haveEqTime_iff_finset {φs : List 𝓕.States} (φsΛ : WickContraction φs.length) :
HaveEqTime φsΛ ↔ ∃ (a : Finset (Fin φs.length)) (h : a ∈ φsΛ.1), timeOrderRel φs[φsΛ.fstFieldOfContract ⟨a, h⟩] φs[φsΛ.sndFieldOfContract ⟨a, h⟩]
∧ timeOrderRel φs[φsΛ.sndFieldOfContract ⟨a, h⟩] φs[φsΛ.fstFieldOfContract ⟨a, h⟩] := by
simp [HaveEqTime]
simp only [HaveEqTime, Fin.getElem_fin, exists_and_left, exists_prop]
apply Iff.intro
· intro h
obtain ⟨i, j, hij, h1, h2⟩ := h
@ -267,7 +272,7 @@ lemma haveEqTime_iff_finset {φs : List 𝓕.States} (φsΛ : WickContraction φ
by_cases hij : i < j
· have h1n := eq_fstFieldOfContract_of_mem φsΛ ⟨{i,j}, h1⟩ i j (by simp) (by simp) hij
have h2n := eq_sndFieldOfContract_of_mem φsΛ ⟨{i,j}, h1⟩ i j (by simp) (by simp) hij
simp [h1n, h2n]
simp only [h1n, h2n]
simp_all only [forall_true_left, true_and]
· have hineqj : i ≠ j := by
by_contra hineqj
@ -277,13 +282,13 @@ lemma haveEqTime_iff_finset {φs : List 𝓕.States} (φsΛ : WickContraction φ
have hji : j < i := by omega
have h1n := eq_fstFieldOfContract_of_mem φsΛ ⟨{i,j}, h1⟩ j i (by simp) (by simp) hji
have h2n := eq_sndFieldOfContract_of_mem φsΛ ⟨{i,j}, h1⟩ j i (by simp) (by simp) hji
simp [h1n, h2n]
simp only [h1n, h2n]
simp_all
· intro h
obtain ⟨a, h1, h2, h3⟩ := h
use φsΛ.fstFieldOfContract ⟨a, h1⟩
use φsΛ.sndFieldOfContract ⟨a, h1⟩
simp_all
simp_all only [and_true, true_and]
rw [← finset_eq_fstFieldOfContract_sndFieldOfContract]
exact h1
@ -301,15 +306,15 @@ def eqTimeContractSet {φs : List 𝓕.States} (φsΛ : WickContraction φs.leng
lemma eqTimeContractSet_subset {φs : List 𝓕.States} (φsΛ : WickContraction φs.length) :
eqTimeContractSet φsΛ ⊆ φsΛ.1 := by
simp [eqTimeContractSet]
simp only [eqTimeContractSet, Fin.getElem_fin]
intro a
simp
simp only [Finset.mem_filter, Finset.mem_univ, true_and, and_imp]
intro h _
exact h
lemma mem_of_mem_eqTimeContractSet{φs : List 𝓕.States} {φsΛ : WickContraction φs.length}
{a : Finset (Fin φs.length)} (h : a ∈ eqTimeContractSet φsΛ) : a ∈ φsΛ.1 := by
simp [eqTimeContractSet] at h
simp only [eqTimeContractSet, Fin.getElem_fin, Finset.mem_filter, Finset.mem_univ, true_and] at h
exact h.1
lemma join_eqTimeContractSet {φs : List 𝓕.States} (φsΛ : WickContraction φs.length)
@ -323,78 +328,87 @@ lemma join_eqTimeContractSet {φs : List 𝓕.States} (φsΛ : WickContraction
have ht := joinLiftLeft_or_joinLiftRight_of_mem_join (φsucΛ := φsucΛ) _ hmem
rcases ht with ht | ht
· obtain ⟨b, rfl⟩ := ht
simp
simp only [Finset.le_eq_subset, Finset.mem_union, Finset.mem_map,
RelEmbedding.coe_toEmbedding]
left
simp [eqTimeContractSet]
simp only [eqTimeContractSet, Fin.getElem_fin, Finset.mem_filter, Finset.mem_univ, true_and]
apply And.intro (by simp [joinLiftLeft])
intro h'
simp [eqTimeContractSet] at h
simp only [eqTimeContractSet, Fin.getElem_fin, Finset.mem_filter, Finset.mem_univ,
Finset.coe_mem, Subtype.coe_eta, join_fstFieldOfContract_joinLiftLeft,
join_sndFieldOfContract_joinLift, forall_true_left, true_and] at h
exact h
· obtain ⟨b, rfl⟩ := ht
simp
simp only [Finset.le_eq_subset, Finset.mem_union, Finset.mem_map,
RelEmbedding.coe_toEmbedding]
right
use b
rw [Finset.mapEmbedding_apply]
simp [joinLiftRight]
simp only [joinLiftRight, and_true]
simpa [eqTimeContractSet] using h
· intro h
simp at h
simp only [Finset.le_eq_subset, Finset.mem_union, Finset.mem_map,
RelEmbedding.coe_toEmbedding] at h
rcases h with h | h
· simp [eqTimeContractSet]
simp [eqTimeContractSet] at h
· simp only [eqTimeContractSet, Fin.getElem_fin, Finset.mem_filter, Finset.mem_univ, true_and]
simp only [eqTimeContractSet, Fin.getElem_fin, Finset.mem_filter, Finset.mem_univ,
true_and] at h
apply And.intro
· simp [join, h.1]
· intro h'
have h2 := h.2 h.1
exact h2
· simp [eqTimeContractSet]
simp [eqTimeContractSet] at h
· simp only [eqTimeContractSet, Fin.getElem_fin, Finset.mem_filter, Finset.mem_univ, true_and]
simp only [eqTimeContractSet, Fin.getElem_fin, Finset.mem_filter, Finset.mem_univ,
true_and] at h
obtain ⟨b, h1, h2, rfl⟩ := h
apply And.intro
· simp [join, h1]
· intro h'
have h2 := h1.2 h1.1
have hj : ⟨(Finset.mapEmbedding uncontractedListEmd) b, h'⟩ = joinLiftRight ⟨b, h1.1⟩ := by rfl
simp [hj]
simp only [hj, join_fstFieldOfContract_joinLiftRight, getElem_uncontractedListEmd,
join_sndFieldOfContract_joinLiftRight]
simpa using h2
lemma eqTimeContractSet_of_not_haveEqTime {φs : List 𝓕.States} {φsΛ : WickContraction φs.length}
(h : ¬ HaveEqTime φsΛ) : eqTimeContractSet φsΛ = ∅ := by
ext a
simp
simp only [Finset.not_mem_empty, iff_false]
by_contra hn
rw [haveEqTime_iff_finset] at h
simp at h
simp [eqTimeContractSet] at hn
simp only [Fin.getElem_fin, not_exists, not_and] at h
simp only [eqTimeContractSet, Fin.getElem_fin, Finset.mem_filter, Finset.mem_univ, true_and] at hn
have h2 := hn.2 hn.1
have h3 := h a hn.1
simp_all
lemma eqTimeContractSet_of_mem_eqTimeOnly {φs : List 𝓕.States} {φsΛ : WickContraction φs.length}
(h : φsΛ ∈ EqTimeOnly φs) : eqTimeContractSet φsΛ = φsΛ.1 := by
(h : φsΛ.EqTimeOnly) : eqTimeContractSet φsΛ = φsΛ.1 := by
ext a
simp [eqTimeContractSet]
rw [@EqTimeOnly.mem_iff_forall_finset] at h
simp only [eqTimeContractSet, Fin.getElem_fin, Finset.mem_filter, Finset.mem_univ, true_and,
and_iff_left_iff_imp, imp_forall_iff_forall]
rw [EqTimeOnly.eqTimeOnly_iff_forall_finset] at h
exact fun h_1 => h ⟨a, h_1⟩
lemma subContraction_eqTimeContractSet_eqTimeOnly {φs : List 𝓕.States} (φsΛ : WickContraction φs.length) :
φsΛ.subContraction (eqTimeContractSet φsΛ) (eqTimeContractSet_subset φsΛ) ∈
EqTimeOnly φs := by
rw [EqTimeOnly.mem_iff_forall_finset]
(φsΛ.subContraction (eqTimeContractSet φsΛ) (eqTimeContractSet_subset φsΛ)).EqTimeOnly := by
rw [EqTimeOnly.eqTimeOnly_iff_forall_finset]
intro a
have ha2 := a.2
simp [subContraction, -Finset.coe_mem, eqTimeContractSet] at ha2
simp
simp only [subContraction, eqTimeContractSet, Fin.getElem_fin, Finset.mem_filter, Finset.mem_univ,
true_and] at ha2
simp only [subContraction_fstFieldOfContract, Fin.getElem_fin, subContraction_sndFieldOfContract]
exact ha2.2 ha2.1
lemma pair_mem_eqTimeContractSet_iff {φs : List 𝓕.States} {i j : Fin φs.length} (φsΛ : WickContraction φs.length) (h : {i, j} ∈ φsΛ.1) :
{i, j} ∈ φsΛ.eqTimeContractSet ↔ timeOrderRel φs[i] φs[j] ∧ timeOrderRel φs[j] φs[i] := by
simp [eqTimeContractSet]
simp only [eqTimeContractSet, Fin.getElem_fin, Finset.mem_filter, Finset.mem_univ, true_and]
by_cases hij : i < j
· have h1 := eq_fstFieldOfContract_of_mem φsΛ ⟨{i,j}, h⟩ i j (by simp) (by simp) hij
have h2 := eq_sndFieldOfContract_of_mem φsΛ ⟨{i,j}, h⟩ i j (by simp) (by simp) hij
simp [h1, h2]
simp only [h1, h2]
simp_all only [forall_true_left, true_and]
· have hineqj : i ≠ j := by
by_contra hineqj
@ -404,7 +418,7 @@ lemma pair_mem_eqTimeContractSet_iff {φs : List 𝓕.States} {i j : Fin φs.le
have hji : j < i := by omega
have h1 := eq_fstFieldOfContract_of_mem φsΛ ⟨{i,j}, h⟩ j i (by simp) (by simp) hji
have h2 := eq_sndFieldOfContract_of_mem φsΛ ⟨{i,j}, h⟩ j i (by simp) (by simp) hji
simp [h1, h2]
simp only [h1, h2]
simp_all only [not_lt, ne_eq, forall_true_left, true_and]
apply Iff.intro
· intro a
@ -415,62 +429,66 @@ lemma pair_mem_eqTimeContractSet_iff {φs : List 𝓕.States} {i j : Fin φs.le
lemma subContraction_eqTimeContractSet_not_empty_of_haveEqTime
{φs : List 𝓕.States} (φsΛ : WickContraction φs.length) (h : HaveEqTime φsΛ) :
φsΛ.subContraction (eqTimeContractSet φsΛ) (eqTimeContractSet_subset φsΛ) ≠ empty := by
simp
simp only [ne_eq]
erw [Subtype.eq_iff]
simp [empty, subContraction]
rw [@Finset.eq_empty_iff_forall_not_mem]
simp [HaveEqTime] at h
simp only [subContraction, empty]
rw [Finset.eq_empty_iff_forall_not_mem]
simp only [HaveEqTime, Fin.getElem_fin, exists_and_left, exists_prop] at h
obtain ⟨i, j, hij, h1, h2⟩ := h
simp
simp only [not_forall, Decidable.not_not]
use {i, j}
rw [pair_mem_eqTimeContractSet_iff]
simp_all
simp_all only [Fin.getElem_fin, and_self]
exact h1
lemma quotContraction_eqTimeContractSet_not_haveEqTime {φs : List 𝓕.States} (φsΛ : WickContraction φs.length) :
¬ HaveEqTime (φsΛ.quotContraction (eqTimeContractSet φsΛ) (eqTimeContractSet_subset φsΛ)) := by
rw [haveEqTime_iff_finset]
simp
simp only [Fin.getElem_fin, not_exists, not_and]
intro a ha
erw [subContraction_uncontractedList_get]
erw [subContraction_uncontractedList_get]
simp
simp [quotContraction] at ha
simp only [quotContraction_fstFieldOfContract_uncontractedListEmd, Fin.getElem_fin,
quotContraction_sndFieldOfContract_uncontractedListEmd]
simp only [quotContraction, Finset.mem_filter, Finset.mem_univ, true_and] at ha
have hn' : Finset.map uncontractedListEmd a ∉
(φsΛ.subContraction (eqTimeContractSet φsΛ) (eqTimeContractSet_subset φsΛ) ).1 := by
exact uncontractedListEmd_finset_not_mem a
simp [subContraction, eqTimeContractSet] at hn'
simp only [subContraction, eqTimeContractSet, Fin.getElem_fin, Finset.mem_filter, Finset.mem_univ,
true_and, not_and, not_forall] at hn'
have hn'' := hn' ha
obtain ⟨h, h1⟩ := hn''
simp_all
lemma join_haveEqTime_of_eqTimeOnly_nonEmpty {φs : List 𝓕.States} (φsΛ : WickContraction φs.length)
(h1 : φsΛ ∈ EqTimeOnly φs) (h2 : φsΛ ≠ empty)
(h1 : φsΛ.EqTimeOnly) (h2 : φsΛ ≠ empty)
(φsucΛ : WickContraction [φsΛ]ᵘᶜ.length) :
HaveEqTime (join φsΛ φsucΛ) := by
simp [join, HaveEqTime]
simp [EqTimeOnly, EqTimeOnlyCond] at h1
simp only [HaveEqTime, Fin.getElem_fin, join, Finset.le_eq_subset, Finset.mem_union,
Finset.mem_map, RelEmbedding.coe_toEmbedding, exists_and_left, exists_prop]
simp only [EqTimeOnly, Fin.getElem_fin, Finset.mem_filter, Finset.mem_univ,
true_and] at h1
obtain ⟨i, j, h⟩ := exists_pair_of_not_eq_empty _ h2
use i, j
have h1 := h1 i j h
simp_all
simp_all only [ne_eq, true_or, true_and]
apply h1 j i
rw [Finset.pair_comm]
exact h
lemma hasEqTimeEquiv_ext_sigma {φs : List 𝓕.States} {x1 x2 : Σ (φsΛ : {φsΛ : WickContraction φs.length // φsΛ ∈ EqTimeOnly φs ∧ φsΛ ≠ empty}),
lemma hasEqTimeEquiv_ext_sigma {φs : List 𝓕.States} {x1 x2 : Σ (φsΛ : {φsΛ : WickContraction φs.length // φsΛ.EqTimeOnly ∧ φsΛ ≠ empty}),
{φssucΛ : WickContraction [φsΛ.1]ᵘᶜ.length // ¬ HaveEqTime φssucΛ}}
(h1 : x1.1.1 = x2.1.1) (h2 : x1.2.1 = congr (by simp [h1]) x2.2.1) : x1 = x2 := by
match x1, x2 with
| ⟨⟨a1, b1⟩, ⟨c1, d1⟩⟩, ⟨⟨a2, b2⟩, ⟨c2, d2⟩⟩ =>
simp at h1
simp only at h1
subst h1
simp at h2
simp only [ne_eq, congr_refl] at h2
simp [h2]
def hasEqTimeEquiv (φs : List 𝓕.States) :
{φsΛ : WickContraction φs.length // HaveEqTime φsΛ} ≃
Σ (φsΛ : {φsΛ : WickContraction φs.length // φsΛ ∈ EqTimeOnly φs ∧ φsΛ ≠ empty}),
Σ (φsΛ : {φsΛ : WickContraction φs.length // φsΛ.EqTimeOnly ∧ φsΛ ≠ empty}),
{φssucΛ : WickContraction [φsΛ.1]ᵘᶜ.length // ¬ HaveEqTime φssucΛ} where
toFun φsΛ := ⟨⟨φsΛ.1.subContraction (eqTimeContractSet φsΛ.1) (eqTimeContractSet_subset φsΛ.1),
subContraction_eqTimeContractSet_eqTimeOnly φsΛ.1,
@ -481,7 +499,7 @@ def hasEqTimeEquiv (φs : List 𝓕.States) :
left_inv φsΛ := by
match φsΛ with
| ⟨φsΛ, h1, h2⟩ =>
simp
simp only [ne_eq, Fin.getElem_fin, Subtype.mk.injEq]
exact join_sub_quot φsΛ φsΛ.eqTimeContractSet (eqTimeContractSet_subset φsΛ)
right_inv φsΛ' := by
match φsΛ' with
@ -490,21 +508,21 @@ def hasEqTimeEquiv (φs : List 𝓕.States) :
eqTimeContractSet_subset (φsΛ.join φsucΛ)) = φsΛ := by
apply Subtype.ext
ext a
simp [subContraction]
simp only [subContraction]
rw [join_eqTimeContractSet]
rw [eqTimeContractSet_of_not_haveEqTime h2]
simp
simp only [Finset.le_eq_subset, ne_eq, Finset.map_empty, Finset.union_empty]
rw [eqTimeContractSet_of_mem_eqTimeOnly h1.1]
refine hasEqTimeEquiv_ext_sigma ?_ ?_
· simp
· simp only [ne_eq]
exact hs
· simp
· simp only [ne_eq]
apply Subtype.ext
ext a
simp [quotContraction]
simp only [quotContraction, Finset.mem_filter, Finset.mem_univ, true_and]
rw [mem_congr_iff]
rw [mem_join_right_iff]
simp
simp only [ne_eq]
rw [uncontractedListEmd_congr hs]
rw [Finset.map_map]
@ -512,7 +530,7 @@ def hasEqTimeEquiv (φs : List 𝓕.States) :
lemma sum_haveEqTime (φs : List 𝓕.States)
(f : WickContraction φs.length → M) [AddCommMonoid M]:
∑ (φsΛ : {φsΛ : WickContraction φs.length // HaveEqTime φsΛ}), f φsΛ =
∑ (φsΛ : {φsΛ : WickContraction φs.length // φsΛ ∈ EqTimeOnly φs ∧ φsΛ ≠ empty}),
∑ (φsΛ : {φsΛ : WickContraction φs.length // φsΛ.EqTimeOnly ∧ φsΛ ≠ empty}),
∑ (φssucΛ : {φssucΛ : WickContraction [φsΛ.1]ᵘᶜ.length // ¬ HaveEqTime φssucΛ}),
f (join φsΛ.1 φssucΛ.1) := by
rw [← (hasEqTimeEquiv φs).symm.sum_comp]

5
HepLean/PerturbationTheory/WickContraction/Uncontracted.lean
View file

@ -24,7 +24,6 @@ lemma congr_uncontracted {n m : ℕ} (c : WickContraction n) (h : n = m) :
subst h
simp
lemma getDual?_eq_none_iff_mem_uncontracted (i : Fin n) :
c.getDual? i = none ↔ i ∈ c.uncontracted := by
simp [uncontracted]
@ -81,10 +80,10 @@ lemma getDual?_empty_eq_none (i : Fin n) : empty.getDual? i = none := by
@[simp]
lemma uncontracted_empty {n : ℕ} : (@empty n).uncontracted = Finset.univ := by
simp [ uncontracted]
simp [uncontracted]
lemma uncontracted_card_le (c : WickContraction n) : c.uncontracted.card ≤ n := by
simp [uncontracted]
simp only [uncontracted]
apply le_of_le_of_eq (Finset.card_filter_le _ _)
simp

48
HepLean/PerturbationTheory/WickContraction/UncontractedList.lean
View file

@ -58,14 +58,12 @@ lemma fin_finset_sort_map_monotone {n m : ℕ} (a : Finset (Fin n)) (f : Fin n
exact Finset.sort_nodup (fun x1 x2 => x1 ≤ x2) a
intro a ha b hb hf
exact f.2 hf
have h3 : ((Finset.sort (· ≤ ·) a).map f).toFinset = (a.map f) := by
have h3 : ((Finset.sort (· ≤ ·) a).map f).toFinset = (a.map f) := by
ext a
simp
rw [← h3]
exact ((List.toFinset_sort (· ≤ ·) h2).mpr h1).symm
lemma fin_list_sorted_split :
(l : List (Fin n)) → (hl : l.Sorted (· ≤ ·)) → (i : ℕ) →
l = l.filter (fun x => x.1 < i) ++ l.filter (fun x => i ≤ x.1)
@ -363,34 +361,37 @@ lemma uncontractedStatesEquiv_list_sum [AddCommMonoid α] (φs : List 𝓕.State
/-- The embedding of `Fin [φsΛ]ᵘᶜ.length` into `Fin φs.length`. -/
def uncontractedListEmd {φs : List 𝓕.States} {φsΛ : WickContraction φs.length} :
Fin [φsΛ]ᵘᶜ.length ↪ Fin φs.length :=
((finCongr (by simp [uncontractedListGet])).trans φsΛ.uncontractedIndexEquiv).toEmbedding.trans
(Function.Embedding.subtype fun x => x ∈ φsΛ.uncontracted)
Fin [φsΛ]ᵘᶜ.length ↪ Fin φs.length := ((finCongr (by simp [uncontractedListGet])).trans
φsΛ.uncontractedIndexEquiv).toEmbedding.trans
(Function.Embedding.subtype fun x => x ∈ φsΛ.uncontracted)
lemma uncontractedListEmd_congr {φs : List 𝓕.States} {φsΛ φsΛ' : WickContraction φs.length}
(h : φsΛ = φsΛ') :
φsΛ.uncontractedListEmd = (finCongr (by simp [h])).toEmbedding.trans φsΛ'.uncontractedListEmd := by
(h : φsΛ = φsΛ') : φsΛ.uncontractedListEmd =
(finCongr (by simp [h])).toEmbedding.trans φsΛ'.uncontractedListEmd := by
subst h
rfl
lemma uncontractedListEmd_toFun_eq_get (φs : List 𝓕.States) (φsΛ : WickContraction φs.length) :
(uncontractedListEmd (φsΛ := φsΛ)).toFun =
φsΛ.uncontractedList.get ∘ (finCongr (by simp [uncontractedListGet])):= by
rfl
(uncontractedListEmd (φsΛ := φsΛ)).toFun =
φsΛ.uncontractedList.get ∘ (finCongr (by simp [uncontractedListGet])) := by
rfl
lemma uncontractedListEmd_strictMono {φs : List 𝓕.States} {φsΛ : WickContraction φs.length}
{i j : Fin [φsΛ]ᵘᶜ.length} (h : i < j) : uncontractedListEmd i < uncontractedListEmd j := by
simp [uncontractedListEmd, uncontractedIndexEquiv]
lemma uncontractedListEmd_strictMono {φs : List 𝓕.States} {φsΛ : WickContraction φs.length}
{i j : Fin [φsΛ]ᵘᶜ.length} (h : i < j) : uncontractedListEmd i < uncontractedListEmd j := by
simp only [uncontractedListEmd, uncontractedIndexEquiv, List.get_eq_getElem,
Equiv.trans_toEmbedding, Function.Embedding.trans_apply, Equiv.coe_toEmbedding, finCongr_apply,
Equiv.coe_fn_mk, Fin.coe_cast, Function.Embedding.coe_subtype]
exact List.Sorted.get_strictMono φsΛ.uncontractedList_sorted_lt h
lemma uncontractedListEmd_mem_uncontracted {φs : List 𝓕.States} {φsΛ : WickContraction φs.length}
(i : Fin [φsΛ]ᵘᶜ.length) : uncontractedListEmd i ∈ φsΛ.uncontracted := by
simp [uncontractedListEmd]
lemma uncontractedListEmd_surjective_mem_uncontracted {φs : List 𝓕.States} {φsΛ : WickContraction φs.length}
(i : Fin φs.length) (hi : i ∈ φsΛ.uncontracted) :
lemma uncontractedListEmd_surjective_mem_uncontracted {φs : List 𝓕.States}
{φsΛ : WickContraction φs.length} (i : Fin φs.length) (hi : i ∈ φsΛ.uncontracted) :
∃ j, φsΛ.uncontractedListEmd j = i := by
simp [uncontractedListEmd]
simp only [uncontractedListEmd, Equiv.trans_toEmbedding, Function.Embedding.trans_apply,
Equiv.coe_toEmbedding, finCongr_apply, Function.Embedding.coe_subtype]
have hj : ∃ j, φsΛ.uncontractedIndexEquiv j = ⟨i, hi⟩ := by
exact φsΛ.uncontractedIndexEquiv.surjective ⟨i, hi⟩
obtain ⟨j, hj⟩ := hj
@ -401,11 +402,12 @@ lemma uncontractedListEmd_surjective_mem_uncontracted {φs : List 𝓕.States} {
rw [hj]
@[simp]
lemma uncontractedListEmd_finset_disjoint_left {φs : List 𝓕.States} {φsΛ : WickContraction φs.length}
(a : Finset (Fin [φsΛ]ᵘᶜ.length)) (b : Finset (Fin φs.length)) (hb : b ∈ φsΛ.1) : Disjoint (a.map uncontractedListEmd) b := by
lemma uncontractedListEmd_finset_disjoint_left {φs : List 𝓕.States}
{φsΛ : WickContraction φs.length} (a : Finset (Fin [φsΛ]ᵘᶜ.length))
(b : Finset (Fin φs.length)) (hb : b ∈ φsΛ.1) : Disjoint (a.map uncontractedListEmd) b := by
rw [Finset.disjoint_left]
intro x hx
simp at hx
simp only [Finset.mem_map] at hx
obtain ⟨x, hx, rfl⟩ := hx
have h1 : uncontractedListEmd x ∈ φsΛ.uncontracted :=
uncontractedListEmd_mem_uncontracted x
@ -417,16 +419,15 @@ lemma uncontractedListEmd_finset_not_mem {φs : List 𝓕.States} {φsΛ : WickC
a.map uncontractedListEmd ∉ φsΛ.1 := by
by_contra hn
have h1 := uncontractedListEmd_finset_disjoint_left a (a.map uncontractedListEmd) hn
simp at h1
simp only [disjoint_self, Finset.bot_eq_empty, Finset.map_eq_empty] at h1
have h2 := φsΛ.2.1 (a.map uncontractedListEmd) hn
rw [h1] at h2
simp at h2
@[simp]
lemma getElem_uncontractedListEmd {φs : List 𝓕.States} {φsΛ : WickContraction φs.length}
(k : Fin [φsΛ]ᵘᶜ.length) : φs[(uncontractedListEmd k).1] = [φsΛ]ᵘᶜ[k.1] := by
simp [uncontractedListGet]
simp only [uncontractedListGet, List.getElem_map, List.get_eq_getElem]
rfl
@[simp]
@ -435,7 +436,6 @@ lemma uncontractedListEmd_empty {φs : List 𝓕.States} :
ext x
simp [uncontractedListEmd, uncontractedIndexEquiv]
/-!
## Uncontracted List for extractEquiv symm none