Physlib.QFT.PerturbationTheory.WickContraction.Uncontracted

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.Basic

Uncontracted elements

@[expose] public section

For a Wick contraction c, c.uncontracted is defined as the finset of elements of Fin n which are not in any contracted pair.

def uncontracted : Finset (Fin n) := Finset.filter (fun i => c.getDual? i = none) (Finset.univ)

lemma congr_uncontracted {n m : ℕ} (c : WickContraction n) (h : n = m) :
    (c.congr h).uncontracted = Finset.map (finCongr h).toEmbedding c.uncontracted := byn:ℕm:ℕc:WickContraction nh:n = m⊢ ((congr h) c).uncontracted = Finset.map (finCongr h).toEmbedding c.uncontracted
  subst hn:ℕc:WickContraction n⊢ ((congr ⋯) c).uncontracted = Finset.map (finCongr ⋯).toEmbedding c.uncontracted
  simpAll goals completed! 🐙

lemma getDual?_eq_none_iff_mem_uncontracted (i : Fin n) :
    c.getDual? i = none ↔ i ∈ c.uncontracted := byn:ℕc:WickContraction ni:Fin n⊢ c.getDual? i = none ↔ i ∈ c.uncontracted
  simp [uncontracted]All goals completed! 🐙

The equivalence of Option c.uncontracted for two propositionally equal Wick contractions.


def uncontractedCongr {c c': WickContraction n} (h : c = c') :
    Option c.uncontracted ≃ Option c'.uncontracted :=
    Equiv.optionCongr (Equiv.subtypeEquivRight (by𝓕:FieldSpecificationn:ℕc✝:WickContraction nc:WickContraction nc':WickContraction nh:c = c'⊢ ∀ (x : Fin n), x ∈ c.uncontracted ↔ x ∈ c'.uncontracted rw [h𝓕:FieldSpecificationn:ℕc✝:WickContraction nc:WickContraction nc':WickContraction nh:c = c'⊢ ∀ (x : Fin n), x ∈ c'.uncontracted ↔ x ∈ c'.uncontracted𝓕:FieldSpecificationn:ℕc✝:WickContraction nc:WickContraction nc':WickContraction nh:c = c'⊢ ∀ (x : Fin n), x ∈ c'.uncontracted ↔ x ∈ c'.uncontracted]𝓕:FieldSpecificationn:ℕc✝:WickContraction nc:WickContraction nc':WickContraction nh:c = c'⊢ ∀ (x : Fin n), x ∈ c'.uncontracted ↔ x ∈ c'.uncontracted; simpAll goals completed! 🐙))

              @[simp]
lemma uncontractedCongr_none {c c': WickContraction n} (h : c = c') :
    (uncontractedCongr h) none = none := byn:ℕc:WickContraction nc':WickContraction nh:c = c'⊢ (uncontractedCongr h) none = none
  simp [uncontractedCongr]All goals completed! 🐙

@[simp]
lemma uncontractedCongr_some {c c': WickContraction n} (h : c = c') (i : c.uncontracted) :
    (uncontractedCongr h) (some i) = some (Equiv.subtypeEquivRight (by𝓕:FieldSpecificationn:ℕc✝:WickContraction nc:WickContraction nc':WickContraction nh:c = c'i:↥c.uncontracted⊢ ∀ (x : Fin n), x ∈ c.uncontracted ↔ x ∈ c'.uncontracted rw [h𝓕:FieldSpecificationn:ℕc✝:WickContraction nc:WickContraction nc':WickContraction nh:c = c'i:↥c.uncontracted⊢ ∀ (x : Fin n), x ∈ c'.uncontracted ↔ x ∈ c'.uncontracted𝓕:FieldSpecificationn:ℕc✝:WickContraction nc:WickContraction nc':WickContraction nh:c = c'i:↥c.uncontracted⊢ ∀ (x : Fin n), x ∈ c'.uncontracted ↔ x ∈ c'.uncontracted]𝓕:FieldSpecificationn:ℕc✝:WickContraction nc:WickContraction nc':WickContraction nh:c = c'i:↥c.uncontracted⊢ ∀ (x : Fin n), x ∈ c'.uncontracted ↔ x ∈ c'.uncontracted; simpAll goals completed! 🐙) i) := byn:ℕc:WickContraction nc':WickContraction nh:c = c'i:↥c.uncontracted⊢ (uncontractedCongr h) (some i) = some ((Equiv.subtypeEquivRight ⋯) i)
  simp [uncontractedCongr]All goals completed! 🐙

lemma mem_uncontracted_iff_not_contracted (i : Fin n) :
    i ∈ c.uncontracted ↔ ∀ p ∈ c.1, i ∉ p := byn:ℕc:WickContraction ni:Fin n⊢ i ∈ c.uncontracted ↔ ∀ p ∈ ↑c, i ∉ p
  simp only [uncontracted, getDual?, Finset.mem_filter, Finset.mem_univ, true_and]n:ℕc:WickContraction ni:Fin n⊢ (Fin.find? fun j => decide ({i, j} ∈ ↑c)) = none ↔ ∀ p ∈ ↑c, i ∉ p
  apply Iff.intrompn:ℕc:WickContraction ni:Fin n⊢ (Fin.find? fun j => decide ({i, j} ∈ ↑c)) = none → ∀ p ∈ ↑c, i ∉ pmprn:ℕc:WickContraction ni:Fin n⊢ (∀ p ∈ ↑c, i ∉ p) → (Fin.find? fun j => decide ({i, j} ∈ ↑c)) = none
  ·mpn:ℕc:WickContraction ni:Fin n⊢ (Fin.find? fun j => decide ({i, j} ∈ ↑c)) = none → ∀ p ∈ ↑c, i ∉ p intro h p hpmpn:ℕc:WickContraction ni:Fin nh:(Fin.find? fun j => decide ({i, j} ∈ ↑c)) = nonep:Finset (Fin n)hp:p ∈ ↑c⊢ i ∉ p
    have hp := c.2.1 p hpmpn:ℕc:WickContraction ni:Fin nh:(Fin.find? fun j => decide ({i, j} ∈ ↑c)) = nonep:Finset (Fin n)hp✝:p ∈ ↑chp:p.card = 2⊢ i ∉ p
    rw [Finset.card_eq_twompn:ℕc:WickContraction ni:Fin nh:(Fin.find? fun j => decide ({i, j} ∈ ↑c)) = nonep:Finset (Fin n)hp✝:p ∈ ↑chp:∃ x y, x ≠ y ∧ p = {x, y}⊢ i ∉ pmpn:ℕc:WickContraction ni:Fin nh:(Fin.find? fun j => decide ({i, j} ∈ ↑c)) = nonep:Finset (Fin n)hp✝:p ∈ ↑chp:∃ x y, x ≠ y ∧ p = {x, y}⊢ i ∉ p] at hpmpn:ℕc:WickContraction ni:Fin nh:(Fin.find? fun j => decide ({i, j} ∈ ↑c)) = nonep:Finset (Fin n)hp✝:p ∈ ↑chp:∃ x y, x ≠ y ∧ p = {x, y}⊢ i ∉ p
    obtain ⟨a, b, ha, hb, hab⟩ := hpmpn:ℕc:WickContraction ni:Fin nh:(Fin.find? fun j => decide ({i, j} ∈ ↑c)) = nonea:Fin nb:Fin nha:a ≠ bhp:{a, b} ∈ ↑c⊢ i ∉ {a, b}
    rw [Fin.find?_eq_none_iffmpn:ℕc:WickContraction ni:Fin nh:∀ (i_1 : Fin n), decide ({i, i_1} ∈ ↑c) = falsea:Fin nb:Fin nha:a ≠ bhp:{a, b} ∈ ↑c⊢ i ∉ {a, b}mpn:ℕc:WickContraction ni:Fin nh:∀ (i_1 : Fin n), decide ({i, i_1} ∈ ↑c) = falsea:Fin nb:Fin nha:a ≠ bhp:{a, b} ∈ ↑c⊢ i ∉ {a, b}] at hmpn:ℕc:WickContraction ni:Fin nh:∀ (i_1 : Fin n), decide ({i, i_1} ∈ ↑c) = falsea:Fin nb:Fin nha:a ≠ bhp:{a, b} ∈ ↑c⊢ i ∉ {a, b}
    by_contra hnmpn:ℕc:WickContraction ni:Fin nh:∀ (i_1 : Fin n), decide ({i, i_1} ∈ ↑c) = falsea:Fin nb:Fin nha:a ≠ bhp:{a, b} ∈ ↑chn:i ∈ {a, b}⊢ False
    simp only [Finset.mem_insert, Finset.mem_singleton] at hnmpn:ℕc:WickContraction ni:Fin nh:∀ (i_1 : Fin n), decide ({i, i_1} ∈ ↑c) = falsea:Fin nb:Fin nha:a ≠ bhp:{a, b} ∈ ↑chn:i = a ∨ i = b⊢ False
    rcases hn with hn | hnmp.inln:ℕc:WickContraction ni:Fin nh:∀ (i_1 : Fin n), decide ({i, i_1} ∈ ↑c) = falsea:Fin nb:Fin nha:a ≠ bhp:{a, b} ∈ ↑chn:i = a⊢ Falsemp.inrn:ℕc:WickContraction ni:Fin nh:∀ (i_1 : Fin n), decide ({i, i_1} ∈ ↑c) = falsea:Fin nb:Fin nha:a ≠ bhp:{a, b} ∈ ↑chn:i = b⊢ False
    ·mp.inln:ℕc:WickContraction ni:Fin nh:∀ (i_1 : Fin n), decide ({i, i_1} ∈ ↑c) = falsea:Fin nb:Fin nha:a ≠ bhp:{a, b} ∈ ↑chn:i = a⊢ False subst hnmp.inln:ℕc:WickContraction ni:Fin nh:∀ (i_1 : Fin n), decide ({i, i_1} ∈ ↑c) = falseb:Fin nha:i ≠ bhp:{i, b} ∈ ↑c⊢ False
      simp at hmp.inln:ℕc:WickContraction ni:Fin nb:Fin nha:i ≠ bhp:{i, b} ∈ ↑ch:∀ (i_1 : Fin n), {i, i_1} ∉ ↑c⊢ False
      exact h b hpAll goals completed! 🐙
    ·mp.inrn:ℕc:WickContraction ni:Fin nh:∀ (i_1 : Fin n), decide ({i, i_1} ∈ ↑c) = falsea:Fin nb:Fin nha:a ≠ bhp:{a, b} ∈ ↑chn:i = b⊢ False subst hnmp.inrn:ℕc:WickContraction ni:Fin nh:∀ (i_1 : Fin n), decide ({i, i_1} ∈ ↑c) = falsea:Fin nha:a ≠ ihp:{a, i} ∈ ↑c⊢ False
      rw [Finset.pair_commmp.inrn:ℕc:WickContraction ni:Fin nh:∀ (i_1 : Fin n), decide ({i, i_1} ∈ ↑c) = falsea:Fin nha:a ≠ ihp:{i, a} ∈ ↑c⊢ Falsemp.inrn:ℕc:WickContraction ni:Fin nh:∀ (i_1 : Fin n), decide ({i, i_1} ∈ ↑c) = falsea:Fin nha:a ≠ ihp:{i, a} ∈ ↑c⊢ False] at hpmp.inrn:ℕc:WickContraction ni:Fin nh:∀ (i_1 : Fin n), decide ({i, i_1} ∈ ↑c) = falsea:Fin nha:a ≠ ihp:{i, a} ∈ ↑c⊢ False
      simp at hmp.inrn:ℕc:WickContraction ni:Fin na:Fin nha:a ≠ ihp:{i, a} ∈ ↑ch:∀ (i_1 : Fin n), {i, i_1} ∉ ↑c⊢ False
      exact h a hpAll goals completed! 🐙
  ·mprn:ℕc:WickContraction ni:Fin n⊢ (∀ p ∈ ↑c, i ∉ p) → (Fin.find? fun j => decide ({i, j} ∈ ↑c)) = none intro hmprn:ℕc:WickContraction ni:Fin nh:∀ p ∈ ↑c, i ∉ p⊢ (Fin.find? fun j => decide ({i, j} ∈ ↑c)) = none
    rw [Fin.find?_eq_none_iffmprn:ℕc:WickContraction ni:Fin nh:∀ p ∈ ↑c, i ∉ p⊢ ∀ (i_1 : Fin n), decide ({i, i_1} ∈ ↑c) = falsemprn:ℕc:WickContraction ni:Fin nh:∀ p ∈ ↑c, i ∉ p⊢ ∀ (i_1 : Fin n), decide ({i, i_1} ∈ ↑c) = false]mprn:ℕc:WickContraction ni:Fin nh:∀ p ∈ ↑c, i ∉ p⊢ ∀ (i_1 : Fin n), decide ({i, i_1} ∈ ↑c) = false
    by_contra hnmprn:ℕc:WickContraction ni:Fin nh:∀ p ∈ ↑c, i ∉ phn:¬∀ (i_1 : Fin n), decide ({i, i_1} ∈ ↑c) = false⊢ False
    simp only [decide_eq_false_iff_not, not_forall, Decidable.not_not] at hnmprn:ℕc:WickContraction ni:Fin nh:∀ p ∈ ↑c, i ∉ phn:∃ x, {i, x} ∈ ↑c⊢ False
    obtain ⟨j, hj⟩ := hnmprn:ℕc:WickContraction ni:Fin nh:∀ p ∈ ↑c, i ∉ pj:Fin nhj:{i, j} ∈ ↑c⊢ False
    apply h {i, j} hjmprn:ℕc:WickContraction ni:Fin nh:∀ p ∈ ↑c, i ∉ pj:Fin nhj:{i, j} ∈ ↑c⊢ i ∈ {i, j}
    simpAll goals completed! 🐙

lemma mem_uncontracted_empty (i : Fin n) : i ∈ empty.uncontracted := byn:ℕi:Fin n⊢ i ∈ empty.uncontracted
  rw [@mem_uncontracted_iff_not_contractedn:ℕi:Fin n⊢ ∀ p ∈ ↑empty, i ∉ pn:ℕi:Fin n⊢ ∀ p ∈ ↑empty, i ∉ p]n:ℕi:Fin n⊢ ∀ p ∈ ↑empty, i ∉ p
  intro p hpn:ℕi:Fin np:Finset (Fin n)hp:p ∈ ↑empty⊢ i ∉ p
  simp [empty] at hpAll goals completed! 🐙@[simp]
lemma getDual?_empty_eq_none (i : Fin n) : empty.getDual? i = none := byn:ℕi:Fin n⊢ empty.getDual? i = none
  simpa [uncontracted] using mem_uncontracted_empty iAll goals completed! 🐙@[simp]
lemma uncontracted_empty {n : ℕ} : (@empty n).uncontracted = Finset.univ := byn:ℕ⊢ empty.uncontracted = Finset.univ
  simp [uncontracted]All goals completed! 🐙lemma uncontracted_card_le (c : WickContraction n) : c.uncontracted.card ≤ n := byn:ℕc:WickContraction n⊢ c.uncontracted.card ≤ n
  simp only [uncontracted]n:ℕc:WickContraction n⊢ {i | c.getDual? i = none}.card ≤ n
  apply le_of_le_of_eq (Finset.card_filter_le _ _)n:ℕc:WickContraction n⊢ Finset.univ.card = n
  simpAll goals completed! 🐙

lemma uncontracted_card_eq_iff (c : WickContraction n) :
    c.uncontracted.card = n ↔ c = empty := byn:ℕc:WickContraction n⊢ c.uncontracted.card = n ↔ c = empty
  apply Iff.intrompn:ℕc:WickContraction n⊢ c.uncontracted.card = n → c = emptymprn:ℕc:WickContraction n⊢ c = empty → c.uncontracted.card = n
  ·mpn:ℕc:WickContraction n⊢ c.uncontracted.card = n → c = empty intro hmpn:ℕc:WickContraction nh:c.uncontracted.card = n⊢ c = empty
    have hc : c.uncontracted.card = (Finset.univ (α := Fin n)).card := byn:ℕc:WickContraction n⊢ c.uncontracted.card = n ↔ c = emptympn:ℕc:WickContraction nh:c.uncontracted.card = nhc:c.uncontracted.card = Finset.univ.card⊢ c = empty simpa using hmpn:ℕc:WickContraction nh:c.uncontracted.card = nhc:c.uncontracted.card = Finset.univ.card⊢ c = emptympn:ℕc:WickContraction nh:c.uncontracted.card = nhc:c.uncontracted.card = Finset.univ.card⊢ c = empty
    simp only [uncontracted] at hcmpn:ℕc:WickContraction nh:c.uncontracted.card = nhc:{i | c.getDual? i = none}.card = Finset.univ.card⊢ c = empty
    rw [Finset.card_filter_eq_iffmpn:ℕc:WickContraction nh:c.uncontracted.card = nhc:∀ x ∈ Finset.univ, c.getDual? x = none⊢ c = emptympn:ℕc:WickContraction nh:c.uncontracted.card = nhc:∀ x ∈ Finset.univ, c.getDual? x = none⊢ c = empty] at hcmpn:ℕc:WickContraction nh:c.uncontracted.card = nhc:∀ x ∈ Finset.univ, c.getDual? x = none⊢ c = empty
    by_contra hnmpn:ℕc:WickContraction nh:c.uncontracted.card = nhc:∀ x ∈ Finset.univ, c.getDual? x = nonehn:¬c = empty⊢ False
    have hc' := exists_pair_of_not_eq_empty c hnmpn:ℕc:WickContraction nh:c.uncontracted.card = nhc:∀ x ∈ Finset.univ, c.getDual? x = nonehn:¬c = emptyhc':∃ i j, {i, j} ∈ ↑c⊢ False
    obtain ⟨i, j, hij⟩ := hc'mpn:ℕc:WickContraction nh:c.uncontracted.card = nhc:∀ x ∈ Finset.univ, c.getDual? x = nonehn:¬c = emptyi:Fin nj:Fin nhij:{i, j} ∈ ↑c⊢ False
    have hci : c.getDual? i = some j := byn:ℕc:WickContraction n⊢ c.uncontracted.card = n ↔ c = emptympn:ℕc:WickContraction nh:c.uncontracted.card = nhc:∀ x ∈ Finset.univ, c.getDual? x = nonehn:¬c = emptyi:Fin nj:Fin nhij:{i, j} ∈ ↑chci:c.getDual? i = some j⊢ False
      rw [@getDual?_eq_some_iff_memn:ℕc:WickContraction nh:c.uncontracted.card = nhc:∀ x ∈ Finset.univ, c.getDual? x = nonehn:¬c = emptyi:Fin nj:Fin nhij:{i, j} ∈ ↑c⊢ {i, j} ∈ ↑cn:ℕc:WickContraction nh:c.uncontracted.card = nhc:∀ x ∈ Finset.univ, c.getDual? x = nonehn:¬c = emptyi:Fin nj:Fin nhij:{i, j} ∈ ↑c⊢ {i, j} ∈ ↑cmpn:ℕc:WickContraction nh:c.uncontracted.card = nhc:∀ x ∈ Finset.univ, c.getDual? x = nonehn:¬c = emptyi:Fin nj:Fin nhij:{i, j} ∈ ↑chci:c.getDual? i = some j⊢ False]n:ℕc:WickContraction nh:c.uncontracted.card = nhc:∀ x ∈ Finset.univ, c.getDual? x = nonehn:¬c = emptyi:Fin nj:Fin nhij:{i, j} ∈ ↑c⊢ {i, j} ∈ ↑cmpn:ℕc:WickContraction nh:c.uncontracted.card = nhc:∀ x ∈ Finset.univ, c.getDual? x = nonehn:¬c = emptyi:Fin nj:Fin nhij:{i, j} ∈ ↑chci:c.getDual? i = some j⊢ False
      exact hijmpn:ℕc:WickContraction nh:c.uncontracted.card = nhc:∀ x ∈ Finset.univ, c.getDual? x = nonehn:¬c = emptyi:Fin nj:Fin nhij:{i, j} ∈ ↑chci:c.getDual? i = some j⊢ Falsempn:ℕc:WickContraction nh:c.uncontracted.card = nhc:∀ x ∈ Finset.univ, c.getDual? x = nonehn:¬c = emptyi:Fin nj:Fin nhij:{i, j} ∈ ↑chci:c.getDual? i = some j⊢ False
    simp_allAll goals completed! 🐙
  ·mprn:ℕc:WickContraction n⊢ c = empty → c.uncontracted.card = n intro hmprn:ℕc:WickContraction nh:c = empty⊢ c.uncontracted.card = n
    subst hmprn:ℕ⊢ empty.uncontracted.card = n
    simpAll goals completed! 🐙