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
meta import Physlib.QFT.PerturbationTheory.WickContraction.InsertAndContractNat
public import Physlib.QFT.PerturbationTheory.WickContraction.InsertAndContractNat
import all Init.Data.Fin.FoldEquivalence extracting element from contraction
@[expose] public sectionAll goals completed! 🐙) c2.2) : c1 = c2 := n:ℕc1:(c : WickContraction n) × Option ↥c.uncontractedc2:(c : WickContraction n) × Option ↥c.uncontractedh:c1.fst = c2.fstho:c1.snd = (uncontractedCongr ⋯) c2.snd⊢ c1 = c2
n:ℕc2:(c : WickContraction n) × Option ↥c.uncontractedfst✝:WickContraction nsnd✝:Option ↥fst✝.uncontractedh:⟨fst✝, snd✝⟩.fst = c2.fstho:⟨fst✝, snd✝⟩.snd = (uncontractedCongr ⋯) c2.snd⊢ ⟨fst✝, snd✝⟩ = c2
n:ℕfst✝¹:WickContraction nsnd✝¹:Option ↥fst✝.uncontractedfst✝:WickContraction nsnd✝:Option ↥fst✝.uncontractedh:⟨fst✝¹, snd✝¹⟩.fst = ⟨fst✝, snd✝⟩.fstho:⟨fst✝¹, snd✝¹⟩.snd = (uncontractedCongr ⋯) ⟨fst✝, snd✝⟩.snd⊢ ⟨fst✝¹, snd✝¹⟩ = ⟨fst✝, snd✝⟩
n:ℕfst✝¹:WickContraction nsnd✝¹:Option ↥fst✝.uncontractedfst✝:WickContraction nsnd✝:Option ↥fst✝.uncontractedh:⟨fst✝¹, snd✝¹⟩.fst = ⟨fst✝, snd✝⟩.fstho:snd✝¹ = (uncontractedCongr ⋯) snd✝⊢ fst✝¹ = fst✝ ∧ (uncontractedCongr ⋯) snd✝ ≍ snd✝
n:ℕfst✝¹:WickContraction nsnd✝¹:Option ↥fst✝.uncontractedfst✝:WickContraction nsnd✝:Option ↥fst✝.uncontractedh:fst✝¹ = fst✝ho:snd✝¹ = (uncontractedCongr ⋯) snd✝⊢ fst✝¹ = fst✝ ∧ (uncontractedCongr ⋯) snd✝ ≍ snd✝
n:ℕfst✝:WickContraction nsnd✝¹:Option ↥fst✝.uncontractedsnd✝:Option ↥fst✝.uncontractedho:snd✝¹ = (uncontractedCongr ⋯) snd✝⊢ fst✝ = fst✝ ∧ (uncontractedCongr ⋯) snd✝ ≍ snd✝
n:ℕfst✝:WickContraction nsnd✝¹:Option ↥fst✝.uncontractedsnd✝:Option ↥fst✝.uncontractedho:snd✝¹ = (uncontractedCongr ⋯) snd✝⊢ Option.map (⇑(Equiv.subtypeEquivRight ⋯)) snd✝ = snd✝
n:ℕfst✝:WickContraction nsnd✝:Option ↥fst✝.uncontracteda:Option ↥fst✝.uncontractedho:snd✝¹ = (uncontractedCongr ⋯) snd✝⊢ Option.map (⇑(Equiv.subtypeEquivRight ⋯)) snd✝ = snd✝
match a with
n:ℕfst✝:WickContraction nsnd✝:Option ↥fst✝.uncontracteda:Option ↥fst✝.uncontractedho:snd✝ = (uncontractedCongr ⋯) none⊢ Option.map (⇑(Equiv.subtypeEquivRight ⋯)) none = none All goals completed! 🐙
n:ℕfst✝:WickContraction nsnd✝:Option ↥fst✝.uncontracteda✝:Option ↥fst✝.uncontracteda:↥fst✝.uncontractedho:snd✝ = (uncontractedCongr ⋯) (some a)⊢ Option.map (⇑(Equiv.subtypeEquivRight ⋯)) (some a) = some a
n:ℕfst✝:WickContraction nsnd✝:Option ↥fst✝.uncontracteda✝:Option ↥fst✝.uncontracteda:↥fst✝.uncontractedho:snd✝ = (uncontractedCongr ⋯) (some a)⊢ (Equiv.subtypeEquivRight ⋯) a = a
n:ℕfst✝:WickContraction nsnd✝:Option ↥fst✝.uncontracteda✝:Option ↥fst✝.uncontracteda:↥fst✝.uncontractedho:snd✝ = (uncontractedCongr ⋯) (some a)⊢ ↑↑((Equiv.subtypeEquivRight ⋯) a) = ↑↑a
All goals completed! 🐙
The equivalence between WickContraction n.succ and the sigma type
(c : WickContraction n) × Option c.uncontracted formed by inserting
and erasing elements from a contraction.
def extractEquiv (i : Fin n.succ) : WickContraction n.succ ≃
(c : WickContraction n) × Option c.uncontracted where
toFun := fun c => ⟨erase c i, getDualErase c i⟩
invFun := fun ⟨c, j⟩ => insertAndContractNat c i j
left_inv f := 𝓕:FieldSpecificationn:ℕc:WickContraction ni:Fin n.succf:WickContraction n.succ⊢ (fun x =>
match x with
| ⟨c, j⟩ => c.insertAndContractNat i j)
((fun c => ⟨c.erase i, c.getDualErase i⟩) f) =
f
All goals completed! 🐙
right_inv f := 𝓕:FieldSpecificationn:ℕc:WickContraction ni:Fin n.succf:(c : WickContraction n) × Option ↥c.uncontracted⊢ (fun c => ⟨c.erase i, c.getDualErase i⟩)
((fun x =>
match x with
| ⟨c, j⟩ => c.insertAndContractNat i j)
f) =
f
𝓕:FieldSpecificationn:ℕc:WickContraction ni:Fin n.succf:(c : WickContraction n) × Option ↥c.uncontracted⊢ ((fun c => ⟨c.erase i, c.getDualErase i⟩)
((fun x =>
match x with
| ⟨c, j⟩ => c.insertAndContractNat i j)
f)).fst =
f.fst𝓕:FieldSpecificationn:ℕc:WickContraction ni:Fin n.succf:(c : WickContraction n) × Option ↥c.uncontracted⊢ ((fun c => ⟨c.erase i, c.getDualErase i⟩)
((fun x =>
match x with
| ⟨c, j⟩ => c.insertAndContractNat i j)
f)).snd =
(uncontractedCongr ⋯) f.snd
𝓕:FieldSpecificationn:ℕc:WickContraction ni:Fin n.succf:(c : WickContraction n) × Option ↥c.uncontracted⊢ ((fun c => ⟨c.erase i, c.getDualErase i⟩)
((fun x =>
match x with
| ⟨c, j⟩ => c.insertAndContractNat i j)
f)).snd =
(uncontractedCongr ⋯) f.snd
𝓕:FieldSpecificationn:ℕc:WickContraction ni:Fin n.succf:(c : WickContraction n) × Option ↥c.uncontracted⊢ (f.fst.insertAndContractNat i f.snd).getDualErase i = (uncontractedCongr ⋯) f.snd
𝓕:FieldSpecificationn:ℕc:WickContraction ni:Fin n.succf:(c : WickContraction n) × Option ↥c.uncontractedh1:(f.fst.insertAndContractNat i f.snd).getDualErase i = (uncontractedCongr ⋯) f.snd⊢ (f.fst.insertAndContractNat i f.snd).getDualErase i = (uncontractedCongr ⋯) f.snd
All goals completed! 🐙lemma extractEquiv_symm_none_uncontracted (i : Fin n.succ) (c : WickContraction n) :
((extractEquiv i).symm ⟨c, none⟩).uncontracted =
(Insert.insert i (c.uncontracted.map i.succAboveEmb)) := n:ℕi:Fin n.succc:WickContraction n⊢ ((extractEquiv i).symm ⟨c, none⟩).uncontracted = insert i (Finset.map i.succAboveEmb c.uncontracted)
All goals completed! 🐙All goals completed! 🐙) ((extractEquiv ⟨k, hnk⟩).symm ⟨c, i⟩)))).1 = c := n:ℕm:ℕk:ℕhnk:k < n.succhkm:k < m.succhnm:n = mc:WickContraction ni:↥c.uncontracted⊢ (congr ⋯) ((extractEquiv ⟨k, hkm⟩) ((congr ⋯) ((extractEquiv ⟨k, hnk⟩).symm ⟨c, some i⟩))).fst = c
n:ℕk:ℕhnk:k < n.succc:WickContraction ni:↥c.uncontractedhkm:k < n.succ⊢ (congr ⋯) ((extractEquiv ⟨k, hkm⟩) ((congr ⋯) ((extractEquiv ⟨k, hnk⟩).symm ⟨c, some i⟩))).fst = c
All goals completed! 🐙
The fintype instance of WickContraction 0 defined through its single
element empty.
𝓕:FieldSpecificationn:ℕc✝:WickContraction nc:WickContraction 0a:Finset (Fin 0)h:a ∈ ↑chc:∃ x y, x ≠ y ∧ a = {x, y}⊢ a ∈ ∅
𝓕:FieldSpecificationn:ℕc✝:WickContraction nc:WickContraction 0a:Finset (Fin 0)h:a ∈ ↑cx:Fin 0y:Fin 0hxy:x ≠ yha:a = {x, y}⊢ a ∈ ∅
All goals completed! 🐙
𝓕:FieldSpecificationn:ℕc✝:WickContraction nc:WickContraction 0a:Finset (Fin 0)⊢ a ∈ ∅ → a ∈ ↑c All goals completed! 🐙M:Type u_1f:WickContraction 0 → Minst✝:AddCommMonoid M⊢ empty ∈ Finset.univM:Type u_1f:WickContraction 0 → Minst✝:AddCommMonoid M⊢ ∀ b ∈ Finset.univ, b ≠ empty → f b = 0
M:Type u_1f:WickContraction 0 → Minst✝:AddCommMonoid M⊢ ∀ b ∈ Finset.univ, b ≠ empty → f b = 0
M:Type u_1f:WickContraction 0 → Minst✝:AddCommMonoid Mb:WickContraction 0hb:b ∈ Finset.univ⊢ b ≠ empty → f b = 0
M:Type u_1f:WickContraction 0 → Minst✝:AddCommMonoid Mhb:empty ∈ Finset.univ⊢ empty ≠ empty → f empty = 0
All goals completed! 🐙
The fintype instance of WickContraction n, for n.succ this is defined
through the equivalence extractEquiv.
instance fintypeSucc : (n : ℕ) → Fintype (WickContraction n)
| 0 => fintypeZero
𝓕:FieldSpecificationn✝:ℕc:WickContraction n✝n:ℕ⊢ Fintype (WickContraction n.succ) 𝓕:FieldSpecificationn✝:ℕc:WickContraction n✝n:ℕ⊢ Fintype (WickContraction n.succ)
𝓕:FieldSpecificationn✝:ℕc:WickContraction n✝n:ℕthis:Fintype (WickContraction n) := fintypeSucc n⊢ Fintype (WickContraction n.succ)
All goals completed! 🐙M:Type u_1inst✝:AddCommMonoid Mm:ℕi:Fin m.succf:WickContraction m.succ → M⊢ ∑ i_1, f ((extractEquiv i).symm i_1) =
∑ x ∈ Finset.univ.sigma fun x => Finset.univ, f ((extractEquiv i).symm ⟨x.fst, x.snd⟩)
All goals completed! 🐙
For n = 3 there are 4 possible Wick contractions:
∅, corresponding to the case where no fields are contracted.
{{0, 1}}, corresponding to the case where the field at position 0 and 1 are contracted.
{{0, 2}}, corresponding to the case where the field at position 0 and 2 are contracted.
{{1, 2}}, corresponding to the case where the field at position 1 and 2 are contracted.
The proof of this result uses the fact that Lean is an executable programming language
and can calculate all Wick contractions for a given n.
lemma mem_three (c : WickContraction 3) : c.1 ∈ ({∅, {{0, 1}}, {{0, 2}}, {{1, 2}}} :
Finset (Finset (Finset (Fin 3)))) := c:WickContraction 3⊢ ↑c ∈ {∅, {{0, 1}}, {{0, 2}}, {{1, 2}}}
⊢ ∀ (c : WickContraction 3), ↑c ∈ {∅, {{0, 1}}, {{0, 2}}, {{1, 2}}}
All goals completed! 🐙
For n = 4 there are 10 possible Wick contractions including e.g.
∅, corresponding to the case where no fields are contracted.
{{0, 1}, {2, 3}}, corresponding to the case where the fields at position 0 and 1 are
contracted, and the fields at position 2 and 3 are contracted.
{{0, 2}, {1, 3}}, corresponding to the case where the fields at position 0 and 2 are
contracted, and the fields at position 1 and 3 are contracted.
The proof of this result uses the fact that Lean is an executable programming language
and can calculate all Wick contractions for a given n.
lemma mem_four (c : WickContraction 4) : c.1 ∈ ({∅,
{{0, 1}}, {{0, 2}}, {{0, 3}}, {{1, 2}}, {{1, 3}}, {{2,3}},
{{0, 1}, {2, 3}}, {{0, 2}, {1, 3}}, {{0, 3}, {1, 2}}} :
Finset (Finset (Finset (Fin 4)))) := c:WickContraction 4⊢ ↑c ∈
{∅, {{0, 1}}, {{0, 2}}, {{0, 3}}, {{1, 2}}, {{1, 3}}, {{2, 3}}, {{0, 1}, {2, 3}}, {{0, 2}, {1, 3}}, {{0, 3}, {1, 2}}}
⊢ ∀ (c : WickContraction 4),
↑c ∈
{∅, {{0, 1}}, {{0, 2}}, {{0, 3}}, {{1, 2}}, {{1, 3}}, {{2, 3}}, {{0, 1}, {2, 3}}, {{0, 2}, {1, 3}},
{{0, 3}, {1, 2}}}
All goals completed! 🐙