OAI/Combinatorics/ContingencyTables/Machines/PreparedDenseCount.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Polynomial transition entries with a shared acceptance allowance

  1. abbrev OAI.ContingencyTables.DensePrograms.PreparedCountInput line 13
  2. def OAI.ContingencyTables.DensePrograms.preparedGap line 15
  3. def OAI.ContingencyTables.DensePrograms.preparedGapRealizer line 18
  4. lemma OAI.ContingencyTables.DensePrograms.polynomial_preparedGap line 23
  5. def OAI.ContingencyTables.DensePrograms.preparedOffCount line 30
  6. def OAI.ContingencyTables.DensePrograms.preparedOffCountRealizer line 34
  7. theorem OAI.ContingencyTables.DensePrograms.polynomial_preparedOffCount line 43

    Source documentation

    The allowance is supplied once. Enumerating a row or the whole matrix then uses only polynomial-time operations on binary entries.

    theorem polynomial_preparedOffCount : PolynomialTime preparedOffCountRealizer := by
…

    Mentions: OAI.ContingencyTables.DensePrograms.preparedOffCountRealizer

  8. lemma OAI.ContingencyTables.DensePrograms.preparedOffCount_eq line 51
  9. lemma OAI.ContingencyTables.DensePrograms.offCountCode_actual line 57