Imports
/-
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
-/
module
public import Physlib.QFT.PerturbationTheory.WickContraction.EraseInserting an element into a contraction
@[expose] public sectionInserting an element into a contraction
Given a Wick contraction c for n, a position i : Fin n.succ and
an optional uncontracted element j : Option (c.uncontracted) of c.
The Wick contraction for n.succ formed by 'inserting' i into Fin n
and contracting it optionally with j.
𝓕:FieldSpecificationn:ℕc✝:WickContraction nc:WickContraction ni:Fin n.succj✝:Option ↥c.uncontractedf:Finset (Finset (Fin (n + 1))) := Finset.map (Finset.mapEmbedding i.succAboveEmb).toEmbedding ↑cf':Finset (Finset (Fin (n + 1))) :=
match j with
| none => f
| some j => insert {i, i.succAbove ↑j} fj:↥c.uncontracteda':Finset (Fin n)ha':a' ∈ ↑cb':Finset (Fin n)hb':b' ∈ ↑c⊢ a' = b' ∨ Disjoint a' b'
All goals completed! 🐙lemma insertAndContractNat_of_isSome (c : WickContraction n) (i : Fin n.succ)
(j : Option c.uncontracted) (hj : j.isSome) :
(insertAndContractNat c i j).1 = Insert.insert {i, i.succAbove (j.get hj)}
(Finset.map (Finset.mapEmbedding i.succAboveEmb).toEmbedding c.1) := n:ℕc:WickContraction ni:Fin n.succj:Option ↥c.uncontractedhj:j.isSome = true⊢ ↑(c.insertAndContractNat i j) =
insert {i, i.succAbove ↑(j.get hj)} (Finset.map (Finset.mapEmbedding i.succAboveEmb).toEmbedding ↑c)
n:ℕc:WickContraction ni:Fin n.succj:↥c.uncontractedhj:(some j).isSome = true⊢ ↑(c.insertAndContractNat i (some j)) =
insert {i, i.succAbove ↑((some j).get hj)} (Finset.map (Finset.mapEmbedding i.succAboveEmb).toEmbedding ↑c)
All goals completed! 🐙n:ℕc:WickContraction ni:Fin n.succx:Fin ny:Fin nhxy:x ≠ yha:{x, y} ∈ ↑c⊢ i ∉ Finset.map i.succAboveEmb {x, y}
n:ℕc:WickContraction ni:Fin n.succx:Fin ny:Fin nhxy:x ≠ yha:{x, y} ∈ ↑c⊢ ¬i = i.succAbove x ∧ ¬i = i.succAbove y
n:ℕc:WickContraction ni:Fin n.succx:Fin ny:Fin nhxy:x ≠ yha:{x, y} ∈ ↑c⊢ ¬i = i.succAbove xn:ℕc:WickContraction ni:Fin n.succx:Fin ny:Fin nhxy:x ≠ yha:{x, y} ∈ ↑c⊢ ¬i = i.succAbove y
n:ℕc:WickContraction ni:Fin n.succx:Fin ny:Fin nhxy:x ≠ yha:{x, y} ∈ ↑c⊢ ¬i = i.succAbove x All goals completed! 🐙
n:ℕc:WickContraction ni:Fin n.succx:Fin ny:Fin nhxy:x ≠ yha:{x, y} ∈ ↑c⊢ ¬i = i.succAbove y All goals completed! 🐙n:ℕc:WickContraction ni:Fin n.succj:↥c.uncontracted⊢ ¬∀ p ∈ ↑(c.insertAndContractNat i (some j)), i ∉ p
All goals completed! 🐙lemma insertAndContractNat_succAbove_mem_uncontracted_iff (c : WickContraction n) (i : Fin n.succ)
(j : Fin n) :
(i.succAbove j) ∈ (insertAndContractNat c i none).uncontracted ↔ j ∈ c.uncontracted := n:ℕc:WickContraction ni:Fin n.succj:Fin n⊢ i.succAbove j ∈ (c.insertAndContractNat i none).uncontracted ↔ j ∈ c.uncontracted
All goals completed! 🐙@[simp]
lemma mem_uncontracted_insertAndContractNat_none_iff (c : WickContraction n) (i : Fin n.succ)
(k : Fin n.succ) : k ∈ (insertAndContractNat c i none).uncontracted ↔
k = i ∨ ∃ j, k = i.succAbove j ∧ j ∈ c.uncontracted := n:ℕc:WickContraction ni:Fin n.succk:Fin n.succ⊢ k ∈ (c.insertAndContractNat i none).uncontracted ↔ k = i ∨ ∃ j, k = i.succAbove j ∧ j ∈ c.uncontracted
n:ℕc:WickContraction nk:Fin n.succ⊢ k ∈ (c.insertAndContractNat k none).uncontracted ↔ k = k ∨ ∃ j, k = k.succAbove j ∧ j ∈ c.uncontractedn:ℕc:WickContraction ni:Fin n.succz:Fin n⊢ i.succAbove z ∈ (c.insertAndContractNat i none).uncontracted ↔
i.succAbove z = i ∨ ∃ j, i.succAbove z = i.succAbove j ∧ j ∈ c.uncontracted
n:ℕc:WickContraction nk:Fin n.succ⊢ k ∈ (c.insertAndContractNat k none).uncontracted ↔ k = k ∨ ∃ j, k = k.succAbove j ∧ j ∈ c.uncontracted All goals completed! 🐙
n:ℕc:WickContraction ni:Fin n.succz:Fin n⊢ i.succAbove z ∈ (c.insertAndContractNat i none).uncontracted ↔
i.succAbove z = i ∨ ∃ j, i.succAbove z = i.succAbove j ∧ j ∈ c.uncontracted All goals completed! 🐙lemma insertAndContractNat_none_uncontracted (c : WickContraction n) (i : Fin n.succ) :
(insertAndContractNat c i none).uncontracted =
Insert.insert i (c.uncontracted.map i.succAboveEmb) := n:ℕc:WickContraction ni:Fin n.succ⊢ (c.insertAndContractNat i none).uncontracted = insert i (Finset.map i.succAboveEmb c.uncontracted)
n:ℕc:WickContraction ni:Fin n.succa:Fin n.succ⊢ a ∈ (c.insertAndContractNat i none).uncontracted ↔ a ∈ insert i (Finset.map i.succAboveEmb c.uncontracted)
All goals completed! 🐙n:ℕc:WickContraction ni:Fin n.succj:↥c.uncontractedz:Fin nhjz:¬↑j = zhz':(∀ p ∈ ↑c, z ∉ p) ∧ z ≠ ↑j⊢ ∀ a ∈ ↑c, i.succAbove z ∉ (Finset.mapEmbedding i.succAboveEmb) a
All goals completed! 🐙lemma insertAndContractNat_some_uncontracted (c : WickContraction n) (i : Fin n.succ)
(j : c.uncontracted) :
(insertAndContractNat c i (some j)).uncontracted =
(c.uncontracted.erase j).map i.succAboveEmb := n:ℕc:WickContraction ni:Fin n.succj:↥c.uncontracted⊢ (c.insertAndContractNat i (some j)).uncontracted = Finset.map i.succAboveEmb (c.uncontracted.erase ↑j)
n:ℕc:WickContraction ni:Fin n.succj:↥c.uncontracteda:Fin n.succ⊢ a ∈ (c.insertAndContractNat i (some j)).uncontracted ↔ a ∈ Finset.map i.succAboveEmb (c.uncontracted.erase ↑j)
n:ℕc:WickContraction ni:Fin n.succj:↥c.uncontracteda:Fin n.succ⊢ (∃ z, a = i.succAbove z ∧ z ∈ c.uncontracted ∧ ¬z = ↑j) ↔
¬a = i.succAbove ↑j ∧ ∃ a_1 ∈ c.uncontracted, i.succAbove a_1 = a
All goals completed! 🐙Insert and getDual?
set_option backward.isDefEq.respectTransparency false in
lemma insertAndContractNat_none_getDual?_isNone (c : WickContraction n) (i : Fin n.succ) :
((insertAndContractNat c i none).getDual? i).isNone := n:ℕc:WickContraction ni:Fin n.succ⊢ ((c.insertAndContractNat i none).getDual? i).isNone = true
All goals completed! 🐙set_option backward.isDefEq.respectTransparency false in
@[simp]
lemma insertAndContractNat_none_getDual?_eq_none (c : WickContraction n) (i : Fin n.succ) :
(insertAndContractNat c i none).getDual? i = none := n:ℕc:WickContraction ni:Fin n.succ⊢ (c.insertAndContractNat i none).getDual? i = none
All goals completed! 🐙@[simp]
lemma insertAndContractNat_succAbove_getDual?_eq_none_iff (c : WickContraction n) (i : Fin n.succ)
(j : Fin n) :
(insertAndContractNat c i none).getDual? (i.succAbove j) = none ↔ c.getDual? j = none := n:ℕc:WickContraction ni:Fin n.succj:Fin n⊢ (c.insertAndContractNat i none).getDual? (i.succAbove j) = none ↔ c.getDual? j = none
All goals completed! 🐙@[simp]
lemma insertAndContractNat_succAbove_getDual?_isSome_iff (c : WickContraction n) (i : Fin n.succ)
(j : Fin n) :
((insertAndContractNat c i none).getDual? (i.succAbove j)).isSome ↔ (c.getDual? j).isSome := n:ℕc:WickContraction ni:Fin n.succj:Fin n⊢ ((c.insertAndContractNat i none).getDual? (i.succAbove j)).isSome = true ↔ (c.getDual? j).isSome = true
All goals completed! 🐙@[simp]
lemma insertAndContractNat_succAbove_getDual?_get (c : WickContraction n) (i : Fin n.succ)
(j : Fin n) (h : ((insertAndContractNat c i none).getDual? (i.succAbove j)).isSome) :
((insertAndContractNat c i none).getDual? (i.succAbove j)).get h =
i.succAbove ((c.getDual? j).get (𝓕:FieldSpecificationn:ℕc✝:WickContraction nc:WickContraction ni:Fin n.succj:Fin nh:((c.insertAndContractNat i none).getDual? (i.succAbove j)).isSome = true⊢ (c.getDual? j).isSome = true All goals completed! 🐙)) := n:ℕc:WickContraction ni:Fin n.succj:Fin nh:((c.insertAndContractNat i none).getDual? (i.succAbove j)).isSome = true⊢ ((c.insertAndContractNat i none).getDual? (i.succAbove j)).get h = i.succAbove ((c.getDual? j).get ⋯)
n:ℕc:WickContraction ni:Fin n.succj:Fin nh:((c.insertAndContractNat i none).getDual? (i.succAbove j)).isSome = true⊢ {i.succAbove j, i.succAbove ((c.getDual? j).get ⋯)} ∈ ↑(c.insertAndContractNat i none)
n:ℕc:WickContraction ni:Fin n.succj:Fin nh:((c.insertAndContractNat i none).getDual? (i.succAbove j)).isSome = true⊢ ∃ a ∈ ↑c, (Finset.mapEmbedding i.succAboveEmb) a = {i.succAbove j, i.succAbove ((c.getDual? j).get ⋯)}
exact ⟨_, self_getDual?_get_mem c j (n:ℕc:WickContraction ni:Fin n.succj:Fin nh:((c.insertAndContractNat i none).getDual? (i.succAbove j)).isSome = true⊢ (c.getDual? j).isSome = true All goals completed! 🐙),
n:ℕc:WickContraction ni:Fin n.succj:Fin nh:((c.insertAndContractNat i none).getDual? (i.succAbove j)).isSome = true⊢ (Finset.mapEmbedding i.succAboveEmb) {j, (c.getDual? j).get ⋯} = {i.succAbove j, i.succAbove ((c.getDual? j).get ⋯)} All goals completed! 🐙⟩n:ℕc:WickContraction ni:Fin n.succj:↥c.uncontracted⊢ {i, i.succAbove ↑j} ∈ ↑(c.insertAndContractNat i (some j))
All goals completed! 🐙lemma insertAndContractNat_some_getDual?_ne_none (c : WickContraction n) (i : Fin n.succ)
(j : c.uncontracted) (k : Fin n) (hkj : k ≠ j.1) :
(insertAndContractNat c i (some j)).getDual? (i.succAbove k) = none ↔ c.getDual? k = none := n:ℕc:WickContraction ni:Fin n.succj:↥c.uncontractedk:Fin nhkj:k ≠ ↑j⊢ (c.insertAndContractNat i (some j)).getDual? (i.succAbove k) = none ↔ c.getDual? k = none
All goals completed! 🐙lemma insertAndContractNat_some_getDual?_ne_isSome (c : WickContraction n) (i : Fin n.succ)
(j : c.uncontracted) (k : Fin n) (hkj : k ≠ j.1) :
((insertAndContractNat c i (some j)).getDual? (i.succAbove k)).isSome ↔
(c.getDual? k).isSome := n:ℕc:WickContraction ni:Fin n.succj:↥c.uncontractedk:Fin nhkj:k ≠ ↑j⊢ ((c.insertAndContractNat i (some j)).getDual? (i.succAbove k)).isSome = true ↔ (c.getDual? k).isSome = true
All goals completed! 🐙lemma insertAndContractNat_some_getDual?_ne_isSome_get (c : WickContraction n) (i : Fin n.succ)
(j : c.uncontracted) (k : Fin n) (hkj : k ≠ j.1)
(h : ((insertAndContractNat c i (some j)).getDual? (i.succAbove k)).isSome) :
((insertAndContractNat c i (some j)).getDual? (i.succAbove k)).get h =
i.succAbove ((c.getDual? k).get
(𝓕:FieldSpecificationn:ℕc✝:WickContraction nc:WickContraction ni:Fin n.succj:↥c.uncontractedk:Fin nhkj:k ≠ ↑jh:((c.insertAndContractNat i (some j)).getDual? (i.succAbove k)).isSome = true⊢ (c.getDual? k).isSome = true All goals completed! 🐙)) := n:ℕc:WickContraction ni:Fin n.succj:↥c.uncontractedk:Fin nhkj:k ≠ ↑jh:((c.insertAndContractNat i (some j)).getDual? (i.succAbove k)).isSome = true⊢ ((c.insertAndContractNat i (some j)).getDual? (i.succAbove k)).get h = i.succAbove ((c.getDual? k).get ⋯)
n:ℕc:WickContraction ni:Fin n.succj:↥c.uncontractedk:Fin nhkj:k ≠ ↑jh:((c.insertAndContractNat i (some j)).getDual? (i.succAbove k)).isSome = true⊢ {i.succAbove k, i.succAbove ((c.getDual? k).get ⋯)} ∈ ↑(c.insertAndContractNat i (some j))
n:ℕc:WickContraction ni:Fin n.succj:↥c.uncontractedk:Fin nhkj:k ≠ ↑jh:((c.insertAndContractNat i (some j)).getDual? (i.succAbove k)).isSome = true⊢ {i.succAbove k, i.succAbove ((c.getDual? k).get ⋯)} = {i, i.succAbove ↑j} ∨
∃ a ∈ ↑c, (Finset.mapEmbedding i.succAboveEmb) a = {i.succAbove k, i.succAbove ((c.getDual? k).get ⋯)}
exact Or.inr ⟨_, self_getDual?_get_mem c k
(n:ℕc:WickContraction ni:Fin n.succj:↥c.uncontractedk:Fin nhkj:k ≠ ↑jh:((c.insertAndContractNat i (some j)).getDual? (i.succAbove k)).isSome = true⊢ (c.getDual? k).isSome = true All goals completed! 🐙),
n:ℕc:WickContraction ni:Fin n.succj:↥c.uncontractedk:Fin nhkj:k ≠ ↑jh:((c.insertAndContractNat i (some j)).getDual? (i.succAbove k)).isSome = true⊢ (Finset.mapEmbedding i.succAboveEmb) {k, (c.getDual? k).get ⋯} = {i.succAbove k, i.succAbove ((c.getDual? k).get ⋯)} All goals completed! 🐙⟩n:ℕc:WickContraction ni:Fin n.succj:↥c.uncontractedk:Fin nhkj:k ≠ ↑jd:Fin nhc:c.getDual? k = some d⊢ {i.succAbove k, i.succAbove d} ∈ ↑(c.insertAndContractNat i (some j))
n:ℕc:WickContraction ni:Fin n.succj:↥c.uncontractedk:Fin nhkj:k ≠ ↑jd:Fin nhc:c.getDual? k = some d⊢ {i.succAbove k, i.succAbove d} = {i, i.succAbove ↑j} ∨
∃ a ∈ ↑c, (Finset.mapEmbedding i.succAboveEmb) a = {i.succAbove k, i.succAbove d}
exact Or.inr ⟨{k, d}, (c.getDual?_eq_some_iff_mem k d).mp hc,
n:ℕc:WickContraction ni:Fin n.succj:↥c.uncontractedk:Fin nhkj:k ≠ ↑jd:Fin nhc:c.getDual? k = some d⊢ (Finset.mapEmbedding i.succAboveEmb) {k, d} = {i.succAbove k, i.succAbove d} All goals completed! 🐙⟩Interaction with erase.
n:ℕc:WickContraction ni:Fin n.succj✝:Option ↥c.uncontracteda:Finset (Fin n)j:↥c.uncontractedhn:Finset.map i.succAboveEmb a ≠ {i, i.succAbove ↑j}⊢ (Finset.map i.succAboveEmb a ∈
match some j with
| none => Finset.map (Finset.mapEmbedding i.succAboveEmb).toEmbedding ↑c
| some j => insert {i, i.succAbove ↑j} (Finset.map (Finset.mapEmbedding i.succAboveEmb).toEmbedding ↑c)) ↔
a ∈ ↑c
All goals completed! 🐙set_option backward.isDefEq.respectTransparency false in
lemma insertAndContractNat_getDualErase (c : WickContraction n) (i : Fin n.succ)
(j : Option c.uncontracted) : (insertAndContractNat c i j).getDualErase i =
uncontractedCongr (c := c) (c' := (c.insertAndContractNat i j).erase i) (𝓕:FieldSpecificationn:ℕc✝:WickContraction nc:WickContraction ni:Fin n.succj:Option ↥c.uncontracted⊢ c = (c.insertAndContractNat i j).erase i All goals completed! 🐙) j := n:ℕc:WickContraction ni:Fin n.succj:Option ↥c.uncontracted⊢ (c.insertAndContractNat i j).getDualErase i = (uncontractedCongr ⋯) j
match n with
n:ℕc:WickContraction 0i:Fin (Nat.succ 0)j:Option ↥c.uncontracted⊢ (c.insertAndContractNat i j).getDualErase i = (uncontractedCongr ⋯) j
n:ℕc:WickContraction 0i:Fin (Nat.succ 0)⊢ (c.insertAndContractNat i none).getDualErase i = (uncontractedCongr ⋯) none
All goals completed! 🐙
n✝:ℕn:ℕc:WickContraction n.succi:Fin n.succ.succj:Option ↥c.uncontracted⊢ (c.insertAndContractNat i j).getDualErase i = (uncontractedCongr ⋯) j
match j with
n✝:ℕn:ℕc:WickContraction n.succi:Fin n.succ.succj:Option ↥c.uncontracted⊢ (c.insertAndContractNat i none).getDualErase i = (uncontractedCongr ⋯) none
All goals completed! 🐙
n✝:ℕn:ℕc:WickContraction n.succi:Fin n.succ.succj✝:Option ↥c.uncontractedj:↥c.uncontracted⊢ (c.insertAndContractNat i (some j)).getDualErase i = (uncontractedCongr ⋯) (some j)
n✝:ℕn:ℕc:WickContraction n.succi:Fin n.succ.succj✝:Option ↥c.uncontractedj:↥c.uncontracted⊢ ⟨↑j, ⋯⟩ = (Equiv.subtypeEquivRight ⋯) j
All goals completed! 🐙n✝:ℕn:ℕc:WickContraction n.succ.succi:Fin n.succ.succhi:¬(c.getDual? i).isSome = truea':Finset (Fin (n + 1))ha':a' ∈ ↑(c.erase i)ha:Finset.map i.succAboveEmb a' ∈ ↑c⊢ ∃ a ∈ ↑(c.erase i), (Finset.mapEmbedding i.succAboveEmb) a = Finset.map i.succAboveEmb a'
All goals completed! 🐙
Lifts a contraction in c to a contraction in (c.insert i j).
def insertLift {c : WickContraction n} (i : Fin n.succ) (j : Option (c.uncontracted))
(a : c.1) : (c.insertAndContractNat i j).1 := ⟨a.1.map (Fin.succAboveEmb i), 𝓕:FieldSpecificationn:ℕc✝:WickContraction nc:WickContraction ni:Fin n.succj:Option ↥c.uncontracteda:↥↑c⊢ Finset.map i.succAboveEmb ↑a ∈ ↑(c.insertAndContractNat i j)
𝓕:FieldSpecificationn:ℕc✝:WickContraction nc:WickContraction ni:Fin n.succj:Option ↥c.uncontracteda:↥↑c⊢ Finset.map i.succAboveEmb ↑a ∈
match j with
| none => Finset.map (Finset.mapEmbedding i.succAboveEmb).toEmbedding ↑c
| some j => insert {i, i.succAbove ↑j} (Finset.map (Finset.mapEmbedding i.succAboveEmb).toEmbedding ↑c)
match j with
𝓕:FieldSpecificationn:ℕc✝:WickContraction nc:WickContraction ni:Fin n.succj:Option ↥c.uncontracteda:↥↑c⊢ Finset.map i.succAboveEmb ↑a ∈
match none with
| none => Finset.map (Finset.mapEmbedding i.succAboveEmb).toEmbedding ↑c
| some j => insert {i, i.succAbove ↑j} (Finset.map (Finset.mapEmbedding i.succAboveEmb).toEmbedding ↑c)
𝓕:FieldSpecificationn:ℕc✝:WickContraction nc:WickContraction ni:Fin n.succj:Option ↥c.uncontracteda:↥↑c⊢ ∃ a_1 ∈ ↑c, (Finset.mapEmbedding i.succAboveEmb) a_1 = Finset.map i.succAboveEmb ↑a
𝓕:FieldSpecificationn:ℕc✝:WickContraction nc:WickContraction ni:Fin n.succj:Option ↥c.uncontracteda:↥↑c⊢ ↑a ∈ ↑c ∧ (Finset.mapEmbedding i.succAboveEmb) ↑a = Finset.map i.succAboveEmb ↑a
𝓕:FieldSpecificationn:ℕc✝:WickContraction nc:WickContraction ni:Fin n.succj:Option ↥c.uncontracteda:↥↑c⊢ (Finset.mapEmbedding i.succAboveEmb) ↑a = Finset.map i.succAboveEmb ↑a
All goals completed! 🐙
𝓕:FieldSpecificationn:ℕc✝:WickContraction nc:WickContraction ni:Fin n.succj✝:Option ↥c.uncontracteda:↥↑cj:↥c.uncontracted⊢ Finset.map i.succAboveEmb ↑a ∈
match some j with
| none => Finset.map (Finset.mapEmbedding i.succAboveEmb).toEmbedding ↑c
| some j => insert {i, i.succAbove ↑j} (Finset.map (Finset.mapEmbedding i.succAboveEmb).toEmbedding ↑c)
𝓕:FieldSpecificationn:ℕc✝:WickContraction nc:WickContraction ni:Fin n.succj✝:Option ↥c.uncontracteda:↥↑cj:↥c.uncontracted⊢ Finset.map i.succAboveEmb ↑a = {i, i.succAbove ↑j} ∨
∃ a_1 ∈ ↑c, (Finset.mapEmbedding i.succAboveEmb) a_1 = Finset.map i.succAboveEmb ↑a
𝓕:FieldSpecificationn:ℕc✝:WickContraction nc:WickContraction ni:Fin n.succj✝:Option ↥c.uncontracteda:↥↑cj:↥c.uncontracted⊢ ∃ a_1 ∈ ↑c, (Finset.mapEmbedding i.succAboveEmb) a_1 = Finset.map i.succAboveEmb ↑a
𝓕:FieldSpecificationn:ℕc✝:WickContraction nc:WickContraction ni:Fin n.succj✝:Option ↥c.uncontracteda:↥↑cj:↥c.uncontracted⊢ ↑a ∈ ↑c ∧ (Finset.mapEmbedding i.succAboveEmb) ↑a = Finset.map i.succAboveEmb ↑a
𝓕:FieldSpecificationn:ℕc✝:WickContraction nc:WickContraction ni:Fin n.succj✝:Option ↥c.uncontracteda:↥↑cj:↥c.uncontracted⊢ (Finset.mapEmbedding i.succAboveEmb) ↑a = Finset.map i.succAboveEmb ↑a
All goals completed! 🐙⟩lemma insertLift_injective {c : WickContraction n} (i : Fin n.succ) (j : Option (c.uncontracted)) :
Function.Injective (insertLift i j) := fun _ _ hab =>
Subtype.ext (Finset.map_injective _ (Subtype.ext_iff.mp hab))lemma insertLift_none_surjective {c : WickContraction n} (i : Fin n.succ) :
Function.Surjective (c.insertLift i none) := n:ℕc:WickContraction ni:Fin n.succ⊢ Function.Surjective (insertLift i none)
n:ℕc:WickContraction ni:Fin n.succa:↥↑(c.insertAndContractNat i none)⊢ ∃ a_1, insertLift i none a_1 = a
n:ℕc:WickContraction ni:Fin n.succa:↥↑(c.insertAndContractNat i none)a':Finset (Fin n)ha':a' ∈ ↑cha'':(Finset.mapEmbedding i.succAboveEmb).toEmbedding a' = ↑a⊢ ∃ a_1, insertLift i none a_1 = a
All goals completed! 🐙lemma insertLift_none_bijective {c : WickContraction n} (i : Fin n.succ) :
Function.Bijective (c.insertLift i none) :=
⟨insertLift_injective i none, insertLift_none_surjective i⟩@[simp]
lemma insertAndContractNat_fstFieldOfContract (c : WickContraction n) (i : Fin n.succ)
(j : Option (c.uncontracted)) (a : c.1) :
(c.insertAndContractNat i j).fstFieldOfContract (insertLift i j a) =
i.succAbove (c.fstFieldOfContract a) :=
(c.insertAndContractNat i j).eq_fstFieldOfContract_of_mem (insertLift i j a)
(i.succAbove (c.fstFieldOfContract a)) (i.succAbove (c.sndFieldOfContract a))
(Finset.mem_map_of_mem _ (fstFieldOfContract_mem c a))
(Finset.mem_map_of_mem _ (sndFieldOfContract_mem c a))
(Fin.succAbove_lt_succAbove_iff.mpr (fstFieldOfContract_lt_sndFieldOfContract c a))@[simp]
lemma insertAndContractNat_sndFieldOfContract (c : WickContraction n) (i : Fin n.succ)
(j : Option (c.uncontracted)) (a : c.1) :
(c.insertAndContractNat i j).sndFieldOfContract (insertLift i j a) =
i.succAbove (c.sndFieldOfContract a) :=
(c.insertAndContractNat i j).eq_sndFieldOfContract_of_mem (insertLift i j a)
(i.succAbove (c.fstFieldOfContract a)) (i.succAbove (c.sndFieldOfContract a))
(Finset.mem_map_of_mem _ (fstFieldOfContract_mem c a))
(Finset.mem_map_of_mem _ (sndFieldOfContract_mem c a))
(Fin.succAbove_lt_succAbove_iff.mpr (fstFieldOfContract_lt_sndFieldOfContract c a))
Given a contracted pair for a Wick contraction WickContraction n, the
corresponding contracted pair of a wick contraction (c.insert i (some j)) formed
by inserting an element i into the contraction.
def insertLiftSome {c : WickContraction n} (i : Fin n.succ) (j : c.uncontracted)
(a : Unit ⊕ c.1) : (c.insertAndContractNat i (some j)).1 :=
match a with
| Sum.inl () => ⟨{i, i.succAbove j}, 𝓕:FieldSpecificationn:ℕc✝:WickContraction nc:WickContraction ni:Fin n.succj:↥c.uncontracteda:Unit ⊕ ↥↑c⊢ {i, i.succAbove ↑j} ∈ ↑(c.insertAndContractNat i (some j))
All goals completed! 🐙⟩
| Sum.inr a => c.insertLift i j alemma insertLiftSome_injective {c : WickContraction n} (i : Fin n.succ) (j : c.uncontracted) :
Function.Injective (insertLiftSome i j) := n:ℕc:WickContraction ni:Fin n.succj:↥c.uncontracted⊢ Function.Injective (insertLiftSome i j)
n:ℕc:WickContraction ni:Fin n.succj:↥c.uncontracteda:Unit ⊕ ↥↑cb:Unit ⊕ ↥↑chab:insertLiftSome i j a = insertLiftSome i j b⊢ a = b
match a, b with
n:ℕc:WickContraction ni:Fin n.succj:↥c.uncontracteda:Unit ⊕ ↥↑cb:Unit ⊕ ↥↑chab:insertLiftSome i j (Sum.inl ()) = insertLiftSome i j (Sum.inl ())⊢ Sum.inl () = Sum.inl () All goals completed! 🐙
n:ℕc:WickContraction ni:Fin n.succj:↥c.uncontracteda✝:Unit ⊕ ↥↑cb:Unit ⊕ ↥↑ca:↥↑chab:insertLiftSome i j (Sum.inr a) = insertLiftSome i j (Sum.inl ())⊢ Sum.inr a = Sum.inl ()n:ℕc:WickContraction ni:Fin n.succj:↥c.uncontracteda✝:Unit ⊕ ↥↑cb:Unit ⊕ ↥↑ca:↥↑chab:insertLiftSome i j (Sum.inl ()) = insertLiftSome i j (Sum.inr a)⊢ Sum.inl () = Sum.inr a
n:ℕc:WickContraction ni:Fin n.succj:↥c.uncontracteda✝:Unit ⊕ ↥↑cb:Unit ⊕ ↥↑ca:↥↑chab:Finset.map i.succAboveEmb ↑a = {i, i.succAbove ↑j}⊢ Sum.inr a = Sum.inl ()
n:ℕc:WickContraction ni:Fin n.succj:↥c.uncontracteda✝:Unit ⊕ ↥↑cb:Unit ⊕ ↥↑ca:↥↑chab:Finset.map i.succAboveEmb ↑a = {i, i.succAbove ↑j}hi:i ∈ Finset.map i.succAboveEmb ↑a⊢ Sum.inr a = Sum.inl ()
All goals completed! 🐙
n:ℕc:WickContraction ni:Fin n.succj:↥c.uncontracteda✝:Unit ⊕ ↥↑cb✝:Unit ⊕ ↥↑ca:↥↑cb:↥↑chab:insertLiftSome i j (Sum.inr a) = insertLiftSome i j (Sum.inr b)⊢ Sum.inr a = Sum.inr b
All goals completed! 🐙lemma insertLiftSome_surjective {c : WickContraction n} (i : Fin n.succ) (j : c.uncontracted) :
Function.Surjective (insertLiftSome i j) := n:ℕc:WickContraction ni:Fin n.succj:↥c.uncontracted⊢ Function.Surjective (insertLiftSome i j)
n:ℕc:WickContraction ni:Fin n.succj:↥c.uncontracteda:↥↑(c.insertAndContractNat i (some j))⊢ ∃ a_1, insertLiftSome i j a_1 = a
n:ℕc:WickContraction ni:Fin n.succj:↥c.uncontracteda:↥↑(c.insertAndContractNat i (some j))ha:↑a = {i, i.succAbove ↑j}⊢ ∃ a_1, insertLiftSome i j a_1 = an:ℕc:WickContraction ni:Fin n.succj:↥c.uncontracteda:↥↑(c.insertAndContractNat i (some j))ha:↑a ∈ Finset.map (Finset.mapEmbedding i.succAboveEmb).toEmbedding ↑c⊢ ∃ a_1, insertLiftSome i j a_1 = a
n:ℕc:WickContraction ni:Fin n.succj:↥c.uncontracteda:↥↑(c.insertAndContractNat i (some j))ha:↑a = {i, i.succAbove ↑j}⊢ ∃ a_1, insertLiftSome i j a_1 = a All goals completed! 🐙
n:ℕc:WickContraction ni:Fin n.succj:↥c.uncontracteda:↥↑(c.insertAndContractNat i (some j))ha:↑a ∈ Finset.map (Finset.mapEmbedding i.succAboveEmb).toEmbedding ↑c⊢ ∃ a_1, insertLiftSome i j a_1 = a n:ℕc:WickContraction ni:Fin n.succj:↥c.uncontracteda:↥↑(c.insertAndContractNat i (some j))ha:↑a ∈ Finset.map (Finset.mapEmbedding i.succAboveEmb).toEmbedding ↑ca':Finset (Fin n)ha':a' ∈ ↑cha'':(Finset.mapEmbedding i.succAboveEmb).toEmbedding a' = ↑a⊢ ∃ a_1, insertLiftSome i j a_1 = a
All goals completed! 🐙lemma insertLiftSome_bijective {c : WickContraction n} (i : Fin n.succ) (j : c.uncontracted) :
Function.Bijective (insertLiftSome i j) :=
⟨insertLiftSome_injective i j, insertLiftSome_surjective i j⟩insertAndContractNat c i none and injection
set_option backward.isDefEq.respectTransparency false in
lemma insertAndContractNat_injective (i : Fin n.succ) :
Function.Injective (fun c => insertAndContractNat c i none) := fun _ _ hc =>
Subtype.ext (n:ℕi:Fin n.succx✝¹:WickContraction nx✝:WickContraction nhc:(fun c => c.insertAndContractNat i none) x✝¹ = (fun c => c.insertAndContractNat i none) x✝⊢ ↑x✝¹ = ↑x✝ All goals completed! 🐙)n:ℕi:Fin n.succc:WickContraction n.succhc:c.getDual? i = noneh0:c.getDualErase i = none⊢ ∃ c', c'.insertAndContractNat i none = c
All goals completed! 🐙lemma insertAndContractNat_bijective (i : Fin n.succ) :
Function.Bijective (fun c => (⟨insertAndContractNat c i none, 𝓕:FieldSpecificationn:ℕc✝:WickContraction ni:Fin n.succc:WickContraction n⊢ (c.insertAndContractNat i none).getDual? i = none All goals completed! 🐙⟩ :
{c : WickContraction n.succ // c.getDual? i = none})) := n:ℕi:Fin n.succ⊢ Function.Bijective fun c => ⟨c.insertAndContractNat i none, ⋯⟩
refine ⟨fun a b hab => insertAndContractNat_injective i (n:ℕi:Fin n.succa:WickContraction nb:WickContraction nhab:(fun c => ⟨c.insertAndContractNat i none, ⋯⟩) a = (fun c => ⟨c.insertAndContractNat i none, ⋯⟩) b⊢ (fun c => c.insertAndContractNat i none) a = (fun c => c.insertAndContractNat i none) b All goals completed! 🐙), fun c => ?_⟩
All goals completed! 🐙