Pair partitions

A finite partition of a finite set s is a pairing (or pair partition) if each of its parts has exactly two elements. Pairings index the Wick formula for the moments of Gaussian variables, and the noncrossing pairings index the moments of semicircular variables in free probability.

Main definitions

• Finpartition.IsPairing P — every part of the finite partition P has two elements.

Main results

• Finpartition.isPairing_iff_part — P is a pairing iff the part through each position has two elements.
• Finpartition.IsPairing.card_eq_two_mul — a pairing of s has #s / 2 parts.
• Finpartition.IsPairing.even_card — only a set of even size has a pairing.

def Finpartition.IsPairing {α : Type u_1} [DecidableEq α] {s : Finset α} (P : Finpartition s) : Prop

A finite partition of a finite set is a pairing (a pair partition) if each of its parts has exactly two elements.

theorem Finpartition.isPairing_iff {α : Type u_1} [DecidableEq α] {s : Finset α} {P : Finpartition s} : P.IsPairing ↔ ∀ B ∈ P.parts, B.card = 2

Unfolding of IsPairing: every part has two elements.

@[instance_reducible]

instance Finpartition.instDecidablePredFinsetIsPairing {α : Type u_1} [DecidableEq α] {s : Finset α} : DecidablePred IsPairing

theorem Finpartition.isPairing_iff_part {α : Type u_1} [DecidableEq α] {s : Finset α} {P : Finpartition s} : P.IsPairing ↔ ∀ a ∈ s, (P.part a).card = 2

A finite partition is a pairing iff the part through each position has two elements.

theorem Finpartition.IsPairing.existsUnique_mem_part_ne {α : Type u_1} [DecidableEq α] {s : Finset α} {P : Finpartition s} (hP : P.IsPairing) {a : α} (ha : a ∈ s) : ∃! b : α, b ∈ P.part a ∧ b ≠ a

In a pair partition, each point has a unique distinct partner in its block.

theorem Finpartition.IsPairing.card_eq_two_mul {α : Type u_1} [DecidableEq α] {s : Finset α} {P : Finpartition s} (hP : P.IsPairing) : s.card = 2 * P.parts.card

A pairing of s has half as many parts as s has elements.

theorem Finpartition.IsPairing.even_card {α : Type u_1} [DecidableEq α] {s : Finset α} {P : Finpartition s} (hP : P.IsPairing) : Even s.card

A finite set with a pairing has an even number of elements.