Even tables in random determinant moments

DefinitionColumn weight#✓fully proved

Let \(n\) be a natural number, \(M\) a commutative monoid and \(f \colon \mathbb{N} \to M\) a function. A column is a finite list of entries from \(\{0, 1, \dots, n - 1\}\); for each \(j\) in this range let \(c_j\) be the number of times \(j\) occurs in the column. The weight of the column is the product \(\prod_{j=0}^{n-1} f(c_j)\) in \(M\).

def columnWeight (n : ℕ) {M : Type*} [CommMonoid M]
    (factor : ℕ → M) (column : List (Fin n)) : M :=
  ∏ j, factor ((column.filter (· = j)).length)
Sources
Used by 1
Used byWeight of an even table

StructureEven table#✓fully proved

For natural numbers \(k\) and \(n\), an even \(k \times n\) table is a \(k \times n\) array of entries from \(\{0, 1, \dots, n-1\}\) such that \(k\) is even, every row is a permutation of \(\{0, 1, \dots, n-1\}\), and in every column each value that occurs there occurs an even number of times.

structure EvenTable (k n : ℕ) where
  entries : Fin k → Fin n → Fin n
  isEven : Even k
  rowBijective : ∀ i, Function.Bijective (entries i)
  colEven : ∀ (j : Fin n) (v : Fin n), (∃ i, entries i j = v) →
    Even ((List.ofFn fun i => entries i j).count v)
Used by 1
Used byWeight of an even table

DefinitionWeight of an even table#✓fully proved

Let \(M\) be a commutative monoid and \(f : \mathbb{N} \to M\). The weight of an even \(k \times n\) table \(t\) with respect to \(f\) is the product of the column weights of its \(n\) columns with respect to \(f\):

\[\prod_{j=0}^{n-1} \prod_{v=0}^{n-1} f(m_j(v)),\]

where \(m_j(v)\) is the number of times the value \(v\) occurs in column \(j\) of \(t\).

def evenTableWeight {M : Type*} [CommMonoid M] {k n : ℕ}
    (factor : ℕ → M) (t : EvenTable k n) : M :=
  ∏ j, columnWeight n factor (List.ofFn fun i => t.entries i j)
Uses 2
Statement usesEven table · Column weight
3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.