The pair-colouring count with margins

Summed over all permutations, the number of fixed pair colourings with prescribed row and column margins is n! times the number of pair contents with those margins: Fubini, the pair stabilizer count, content grouping, and orbit–stabilizer.

def RS.pairContentSym {n k : ℕ} (p : Fin n → Fin k × Fin k) : Sym (Fin k × Fin k) n

The pair content as a symmetric power.

Equations

• RS.pairContentSym p = ⟨RS.pairContent p, ⋯⟩

theorem RS.pair_exists_content {n k : ℕ} (s : Sym (Fin k × Fin k) n) : ∃ (p : Fin n → Fin k × Fin k), pairContentSym p = s

Every pair content is realized.

theorem RS.margin_fst_of_content {n k : ℕ} (p : Fin n → Fin k × Fin k) (a : Fin k) : fibreCard (fun (i : Fin n) => (p i).1) a = ∑ b : Fin k, Multiset.count (a, b) ↑(pairContentSym p)

Margins are determined by the content.

theorem RS.margin_snd_of_content {n k : ℕ} (p : Fin n → Fin k × Fin k) (b : Fin k) : fibreCard (fun (i : Fin n) => (p i).2) b = ∑ a : Fin k, Multiset.count (a, b) ↑(pairContentSym p)

The second-coordinate analogue.

theorem RS.pair_count_sum {n k : ℕ} (α β : Fin k → ℕ) : ∑ π : Equiv.Perm (Fin n), {p : Fin n → Fin k × Fin k | (∀ (a : Fin k), fibreCard (fun (i : Fin n) => (p i).1) a = α a) ∧ (∀ (b : Fin k), fibreCard (fun (i : Fin n) => (p i).2) b = β b) ∧ p ∘ ⇑π = p}.card = n.factorial * Fintype.card { s : Sym (Fin k × Fin k) n // (∀ (a : Fin k), ∑ b : Fin k, Multiset.count (a, b) ↑s = α a) ∧ ∀ (b : Fin k), ∑ a : Fin k, Multiset.count (a, b) ↑s = β b }

The pair-colouring count with margins.