1. Physlib
  2. QFT
  3. PerturbationTheory
  4. WickContraction
  5. Erase
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.Uncontracted public import Physlib.Mathematics.Fin

Erasing an element from a contraction

@[expose] public section

Given a Wick contraction WickContraction n.succ and a i : Fin n.succ the Wick contraction associated with n obtained by removing i. If i is contracted with j in the new Wick contraction j will be uncontracted.

𝓕:FieldSpecificationn:ℕc✝:WickContraction nc:WickContraction n.succi:Fin n.succa:Finset (Fin n)b:Finset (Fin n)ha:Finset.map i.succAboveEmb a ∈ ↑chb:Finset.map i.succAboveEmb b ∈ ↑c⊢ Finset.map i.succAboveEmb a = Finset.map i.succAboveEmb b ∨ Disjoint (Finset.map i.succAboveEmb a) (Finset.map i.succAboveEmb b) All goals completed! 🐙
n:ℕc:WickContraction n.succi:Fin n.succj:Fin nk:Fin nh:{i.succAbove j, i} ∈ ↑chn:¬decide ({i.succAbove j, i.succAbove k} ∈ ↑c) = falsehc:{i.succAbove j, i} = {i.succAbove j, i.succAbove k}hi:i ∈ {i.succAbove j, i.succAbove k}⊢ False n:ℕc:WickContraction n.succi:Fin n.succj:Fin nk:Fin nh:{i.succAbove j, i} ∈ ↑chn:¬decide ({i.succAbove j, i.succAbove k} ∈ ↑c) = falsehc:{i.succAbove j, i} = {i.succAbove j, i.succAbove k}hi:i = i.succAbove j ∨ i = i.succAbove k⊢ False n:ℕc:WickContraction n.succi:Fin n.succj:Fin nk:Fin nh:{i.succAbove j, i} ∈ ↑chn:¬decide ({i.succAbove j, i.succAbove k} ∈ ↑c) = falsehc:{i.succAbove j, i} = {i.succAbove j, i.succAbove k}hi:i = i.succAbove j⊢ Falsen:ℕc:WickContraction n.succi:Fin n.succj:Fin nk:Fin nh:{i.succAbove j, i} ∈ ↑chn:¬decide ({i.succAbove j, i.succAbove k} ∈ ↑c) = falsehc:{i.succAbove j, i} = {i.succAbove j, i.succAbove k}hi:i = i.succAbove k⊢ False n:ℕc:WickContraction n.succi:Fin n.succj:Fin nk:Fin nh:{i.succAbove j, i} ∈ ↑chn:¬decide ({i.succAbove j, i.succAbove k} ∈ ↑c) = falsehc:{i.succAbove j, i} = {i.succAbove j, i.succAbove k}hi:i = i.succAbove j⊢ False All goals completed! 🐙 n:ℕc:WickContraction n.succi:Fin n.succj:Fin nk:Fin nh:{i.succAbove j, i} ∈ ↑chn:¬decide ({i.succAbove j, i.succAbove k} ∈ ↑c) = falsehc:{i.succAbove j, i} = {i.succAbove j, i.succAbove k}hi:i = i.succAbove k⊢ False All goals completed! 🐙n:ℕc:WickContraction n.succi:Fin n.succh:(c.getDual? i).isSome = truex:Fin n.succy:Fin n.succhx:x ≠ yha:{x, y} ∈ ↑cha2:{x, y} ≠ {i, (c.getDual? i).get h}hxn:¬x = ihyn:¬y = i⊢ ∃ a' ∈ ↑(c.erase i), {x, y} = Finset.map i.succAboveEmb a' n:ℕc:WickContraction n.succi:Fin n.succh:(c.getDual? i).isSome = truex:Fin n.succy:Fin n.succhx:x ≠ yha:{x, y} ∈ ↑cha2:{x, y} ≠ {i, (c.getDual? i).get h}hxn:∃ z, i.succAbove z = xhyn:∃ z, i.succAbove z = y⊢ ∃ a' ∈ ↑(c.erase i), {x, y} = Finset.map i.succAboveEmb a' n:ℕc:WickContraction n.succi:Fin n.succh:(c.getDual? i).isSome = truex:Fin n.succy:Fin n.succhx:x ≠ yha:{x, y} ∈ ↑cha2:{x, y} ≠ {i, (c.getDual? i).get h}hyn:∃ z, i.succAbove z = yx':Fin nhx':i.succAbove x' = x⊢ ∃ a' ∈ ↑(c.erase i), {x, y} = Finset.map i.succAboveEmb a' n:ℕc:WickContraction n.succi:Fin n.succh:(c.getDual? i).isSome = truex:Fin n.succy:Fin n.succhx:x ≠ yha:{x, y} ∈ ↑cha2:{x, y} ≠ {i, (c.getDual? i).get h}x':Fin nhx':i.succAbove x' = xy':Fin nhy':i.succAbove y' = y⊢ ∃ a' ∈ ↑(c.erase i), {x, y} = Finset.map i.succAboveEmb a' n:ℕc:WickContraction n.succi:Fin n.succh:(c.getDual? i).isSome = truex:Fin n.succy:Fin n.succhx:x ≠ yha:{x, y} ∈ ↑cha2:{x, y} ≠ {i, (c.getDual? i).get h}x':Fin nhx':i.succAbove x' = xy':Fin nhy':i.succAbove y' = y⊢ {x', y'} ∈ ↑(c.erase i) ∧ {x, y} = Finset.map i.succAboveEmb {x', y'} n:ℕc:WickContraction n.succi:Fin n.succh:(c.getDual? i).isSome = truex':Fin ny':Fin nhx:i.succAbove x' ≠ i.succAbove y'ha:{i.succAbove x', i.succAbove y'} ∈ ↑cha2:{i.succAbove x', i.succAbove y'} ≠ {i, (c.getDual? i).get h}⊢ {x', y'} ∈ ↑(c.erase i) ∧ {i.succAbove x', i.succAbove y'} = Finset.map i.succAboveEmb {x', y'} n:ℕc:WickContraction n.succi:Fin n.succh:(c.getDual? i).isSome = truex':Fin ny':Fin nhx:i.succAbove x' ≠ i.succAbove y'ha:{i.succAbove x', i.succAbove y'} ∈ ↑cha2:{i.succAbove x', i.succAbove y'} ≠ {i, (c.getDual? i).get h}⊢ {i.succAbove x', i.succAbove y'} ∈ ↑c All goals completed! 🐙n:ℕc:WickContraction n.succi:Fin n.succh:(c.getDual? i).isNone = truex:Fin n.succy:Fin n.succhx:x ≠ yha:{x, y} ∈ ↑chi:∀ p ∈ ↑c, i ∉ phxn:¬x = ihyn:¬y = i⊢ ∃ a' ∈ ↑(c.erase i), {x, y} = Finset.map i.succAboveEmb a' n:ℕc:WickContraction n.succi:Fin n.succh:(c.getDual? i).isNone = truex:Fin n.succy:Fin n.succhx:x ≠ yha:{x, y} ∈ ↑chi:∀ p ∈ ↑c, i ∉ phxn:∃ z, i.succAbove z = xhyn:∃ z, i.succAbove z = y⊢ ∃ a' ∈ ↑(c.erase i), {x, y} = Finset.map i.succAboveEmb a' n:ℕc:WickContraction n.succi:Fin n.succh:(c.getDual? i).isNone = truex:Fin n.succy:Fin n.succhx:x ≠ yha:{x, y} ∈ ↑chi:∀ p ∈ ↑c, i ∉ phyn:∃ z, i.succAbove z = yx':Fin nhx':i.succAbove x' = x⊢ ∃ a' ∈ ↑(c.erase i), {x, y} = Finset.map i.succAboveEmb a' n:ℕc:WickContraction n.succi:Fin n.succh:(c.getDual? i).isNone = truex:Fin n.succy:Fin n.succhx:x ≠ yha:{x, y} ∈ ↑chi:∀ p ∈ ↑c, i ∉ px':Fin nhx':i.succAbove x' = xy':Fin nhy':i.succAbove y' = y⊢ ∃ a' ∈ ↑(c.erase i), {x, y} = Finset.map i.succAboveEmb a' n:ℕc:WickContraction n.succi:Fin n.succh:(c.getDual? i).isNone = truex:Fin n.succy:Fin n.succhx:x ≠ yha:{x, y} ∈ ↑chi:∀ p ∈ ↑c, i ∉ px':Fin nhx':i.succAbove x' = xy':Fin nhy':i.succAbove y' = y⊢ {x', y'} ∈ ↑(c.erase i) ∧ {x, y} = Finset.map i.succAboveEmb {x', y'} n:ℕc:WickContraction n.succi:Fin n.succh:(c.getDual? i).isNone = truehi:∀ p ∈ ↑c, i ∉ px':Fin ny':Fin nhx:i.succAbove x' ≠ i.succAbove y'ha:{i.succAbove x', i.succAbove y'} ∈ ↑c⊢ {x', y'} ∈ ↑(c.erase i) ∧ {i.succAbove x', i.succAbove y'} = Finset.map i.succAboveEmb {x', y'} n:ℕc:WickContraction n.succi:Fin n.succh:(c.getDual? i).isNone = truehi:∀ p ∈ ↑c, i ∉ px':Fin ny':Fin nhx:i.succAbove x' ≠ i.succAbove y'ha:{i.succAbove x', i.succAbove y'} ∈ ↑c⊢ {i.succAbove x', i.succAbove y'} ∈ ↑c All goals completed! 🐙

Given a Wick contraction c : WickContraction n.succ and a i : Fin n.succ the (optional) element of (erase c i).uncontracted which comes from the element in c contracted with i.

𝓕:FieldSpecificationn✝¹:ℕc✝:WickContraction n✝n✝:ℕn:ℕc:WickContraction n.succ.succi:Fin n.succ.succhj:(c.getDual? i).isSome = true⊢ {(c.getDual? i).get hj, i} ∈ ↑c𝓕:FieldSpecificationn✝¹:ℕc✝:WickContraction n✝n✝:ℕn:ℕc:WickContraction n.succ.succi:Fin n.succ.succhj:(c.getDual? i).isSome = true⊢ i ≠ (c.getDual? i).get hj 𝓕:FieldSpecificationn✝¹:ℕc✝:WickContraction n✝n✝:ℕn:ℕc:WickContraction n.succ.succi:Fin n.succ.succhj:(c.getDual? i).isSome = true⊢ {(c.getDual? i).get hj, i} ∈ ↑c All goals completed! 🐙 𝓕:FieldSpecificationn✝¹:ℕc✝:WickContraction n✝n✝:ℕn:ℕc:WickContraction n.succ.succi:Fin n.succ.succhj:(c.getDual? i).isSome = true⊢ i ≠ (c.getDual? i).get hj 𝓕:FieldSpecificationn✝¹:ℕc✝:WickContraction n✝n✝:ℕn:ℕc:WickContraction n.succ.succi:Fin n.succ.succhj:(c.getDual? i).isSome = true⊢ c.getDual? i = some ((c.getDual? i).get hj) All goals completed! 🐙
@[simp] lemma getDualErase_isSome_iff_getDual?_isSome (c : WickContraction n.succ) (i : Fin n.succ) : (c.getDualErase i).isSome ↔ (c.getDual? i).isSome := n:ℕc:WickContraction n.succi:Fin n.succ⊢ (c.getDualErase i).isSome = true ↔ (c.getDual? i).isSome = true match n with n:ℕc:WickContraction (Nat.succ 0)i:Fin (Nat.succ 0)⊢ (c.getDualErase i).isSome = true ↔ (c.getDual? i).isSome = true n:ℕc:WickContraction (Nat.succ 0)⊢ (c.getDualErase ((fun i => i) ⟨0, ⋯⟩)).isSome = true ↔ (c.getDual? ((fun i => i) ⟨0, ⋯⟩)).isSome = true All goals completed! 🐙 n✝:ℕn:ℕc:WickContraction n.succ.succi:Fin n.succ.succ⊢ (c.getDualErase i).isSome = true ↔ (c.getDual? i).isSome = true All goals completed! 🐙@[simp] lemma getDualErase_one (c : WickContraction 1) (i : Fin 1) : c.getDualErase i = none := c:WickContraction 1i:Fin 1⊢ c.getDualErase i = none c:WickContraction 1⊢ c.getDualErase ((fun i => i) ⟨0, ⋯⟩) = none All goals completed! 🐙