OAI/Combinatorics/ContingencyTables/Dense/DenseCountProgram.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Executable dense off-diagonal counts without acceptance-word enumeration

  1. abbrev OAI.ContingencyTables.DensePrograms.CountInput line 13
  2. def OAI.ContingencyTables.DensePrograms.countProposalInput line 15
  3. def OAI.ContingencyTables.DensePrograms.countProposalInputRealizer line 18
  4. lemma OAI.ContingencyTables.DensePrograms.polynomial_countProposalInput line 25
  5. def OAI.ContingencyTables.DensePrograms.countPowerInput line 36
  6. def OAI.ContingencyTables.DensePrograms.countPowerInputRealizer line 39
  7. lemma OAI.ContingencyTables.DensePrograms.polynomial_countPowerInput line 45
  8. def OAI.ContingencyTables.DensePrograms.offCountCode line 57
  9. def OAI.ContingencyTables.DensePrograms.offCountCodeRealizer line 60
  10. def OAI.ContingencyTables.DensePrograms.countMeasure line 64
  11. theorem OAI.ContingencyTables.DensePrograms.work_offCountCode line 68

    Source documentation

    Even a huge acceptance denominator only increases binary integer length. The exponent and the supplied state encodings bound the work.

    theorem work_offCountCode : WorkBound offCountCodeRealizer countMeasure := by
…

    Mentions: OAI.ContingencyTables.DensePrograms.offCountCodeRealizer, OAI.ContingencyTables.DensePrograms.countMeasure

  12. theorem OAI.ContingencyTables.DensePrograms.offCountCode_eq line 86