Full contraction

We say that a contraction is full if it has no uncontracted fields.

def WickContraction.IsFull {n : ℕ} (c : WickContraction n) : Prop

A contraction is full if there are no uncontracted fields, i.e. the finite set of uncontracted fields is empty.

Equations

• c.IsFull = (c.uncontracted = ∅)

instance WickContraction.instDecidableIsFull {n : ℕ} (c : WickContraction n) : Decidable c.IsFull

The condition on whether or not a contraction is full is decidable.

Equations

• c.instDecidableIsFull = decEq c.uncontracted ∅

theorem WickContraction.isFull_iff_equivInvolution_no_fixed_point {n : ℕ} (c : WickContraction n) : c.IsFull ↔ ∀ (i : Fin n), ↑(equivInvolution c) i ≠ i

def WickContraction.isFullInvolutionEquiv {n : ℕ} : { c : WickContraction n // c.IsFull } ≃ { f : Fin n → Fin n // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i }

The equivalence between full contractions and fixed-point free involutions.

Equations

• One or more equations did not get rendered due to their size.

theorem WickContraction.card_of_isfull_even {n : ℕ} (he : Even n) : Fintype.card { c : WickContraction n // c.IsFull } = (n - 1).doubleFactorial

If n is even then the number of full contractions is (n-1)!!.

theorem WickContraction.card_of_isfull_odd {n : ℕ} (ho : Odd n) : Fintype.card { c : WickContraction n // c.IsFull } = 0

If n is odd then there are no full contractions. This is because there will always be at least one element unpaired.