PhysLean Documentation

PhysLean.QFT.PerturbationTheory.WickContraction.Card

Cardinality of Wick contractions #

source
theorem WickContraction.wickContraction_card_eq_sum_zero_none_isSome {n : ℕ} :
Fintype.card (WickContraction n.succ) = Fintype.card { c : WickContraction n.succ // ¬(c.getDual? 0).isSome = true } + Fintype.card { c : WickContraction n.succ // (c.getDual? 0).isSome = true }
source
theorem WickContraction.wickContraction_zero_none_card {n : ℕ} :
Fintype.card { c : WickContraction n.succ // ¬(c.getDual? 0).isSome = true } = Fintype.card (WickContraction n)
source
theorem WickContraction.wickContraction_zero_some_eq_sum {n : ℕ} :
Fintype.card { c : WickContraction n.succ // (c.getDual? 0).isSome = true } = ∑ i : Fin n, Fintype.card { c : WickContraction n.succ // (c.getDual? 0).isSome = true ∧ ∀ (h : (c.getDual? 0).isSome = true), (c.getDual? 0).get h = i.succ }
source
theorem WickContraction.finset_succAbove_succ_disjoint {n : ℕ} (a : Finset (Fin n)) (i : Fin n.succ) :
Disjoint (Finset.map (Fin.succEmb (n + 1)) (Finset.map i.succAboveEmb a)) {0, i.succ}
source
def WickContraction.consAddContract {n : ℕ} (i : Fin n.succ) (c : WickContraction n) :
WickContraction n.succ.succ

The Wick contraction in WickContraction n.succ.succ formed by a Wick contraction WickContraction n by inserting at the 0 and i.succ and contracting these two.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem WickContraction.consAddContract_getDual?_zero {n : ℕ} (i : Fin n.succ) (c : WickContraction n) :
    (consAddContract i c).getDual? 0 = some i.succ
    source
    @[simp]
    theorem WickContraction.consAddContract_getDual?_self_succ {n : ℕ} (i : Fin n.succ) (c : WickContraction n) :
    (consAddContract i c).getDual? i.succ = some 0
    source
    theorem WickContraction.mem_consAddContract_of_mem_iff {n : ℕ} (i : Fin n.succ) (c : WickContraction n) (a : Finset (Fin n)) :
    a ∈ ↑c ↔ Finset.map (Fin.succEmb n.succ) (Finset.map i.succAboveEmb a) ∈ ↑(consAddContract i c)
    source
    theorem WickContraction.consAddContract_injective {n : ℕ} (i : Fin n.succ) :
    Function.Injective (consAddContract i)
    source
    theorem WickContraction.consAddContract_surjective_on_zero_contract {n : ℕ} (i : Fin n.succ) (c : WickContraction n.succ.succ) (h : (c.getDual? 0).isSome = true) (h2 : (c.getDual? 0).get h = i.succ) :
    ∃ (c' : WickContraction n), consAddContract i c' = c
    source
    theorem WickContraction.consAddContract_bijection {n : ℕ} (i : Fin n.succ) :
    Function.Bijective fun (c : WickContraction n) => ⟨consAddContract i c, ⋯⟩
    source
    theorem WickContraction.wickContraction_zero_some_eq_mul {n : ℕ} :
    Fintype.card { c : WickContraction n.succ.succ // (c.getDual? 0).isSome = true } = (n + 1) * Fintype.card (WickContraction n)
    source
    def WickContraction.cardFun :
    ℕ → ℕ

    The cardinality of Wick's contractions as a recursive formula. This corresponds to OEIS:A000085.

    Equations
    Instances For
      source
      theorem WickContraction.card_eq_cardFun (n : ℕ) :
      Fintype.card (WickContraction n) = cardFun n

      The number of Wick contractions in WickContraction n is equal to the terms in Online Encyclopedia of Integer Sequences (OEIS) A000085. That is: 1, 1, 2, 4, 10, 26, 76, 232, 764, 2620, 9496, ...