OAI/Combinatorics/ContingencyTables/Dense/DenseMatrixTable.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Constructing the actual dense transition matrix from its finite states

  1. abbrev OAI.ContingencyTables.DensePrograms.CountRowData line 14

    Source documentation

    Shared unary allowance and binary denominator, current exponent data, and the enumeration of all states.

    abbrev CountRowData := ((List Bool×ℕ)×FlatExponentData)×List (List ℕ)

    Mentions: OAI.ContingencyTables.DensePrograms.FlatExponentData

  2. def OAI.ContingencyTables.DensePrograms.rowOffEntry line 16
  3. def OAI.ContingencyTables.DensePrograms.rowOffEntryRealizer line 19
  4. lemma OAI.ContingencyTables.DensePrograms.polynomial_rowOffEntry line 24
  5. def OAI.ContingencyTables.DensePrograms.rowOffCounts line 32
  6. def OAI.ContingencyTables.DensePrograms.rowOffCountsRealizer line 34
  7. lemma OAI.ContingencyTables.DensePrograms.polynomial_rowOffCounts line 37
  8. def OAI.ContingencyTables.DensePrograms.rowEntry line 41
  9. def OAI.ContingencyTables.DensePrograms.rowEntryRealizer line 45
  10. lemma OAI.ContingencyTables.DensePrograms.polynomial_rowEntry line 55
  11. lemma OAI.ContingencyTables.DensePrograms.rowEntry_actual line 72