OAI/Combinatorics/ContingencyTables/Sampling/ProfileMatrixEntryRuntime.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Finite-box work bound for the executable transition entries

  1. def OAI.ContingencyTables.ProfilePrograms.matrixEntryMeasure line 14
  2. lemma OAI.ContingencyTables.ProfilePrograms.input_le_measure line 17
  3. lemma OAI.ContingencyTables.ProfilePrograms.polynomial_work line 21
  4. lemma OAI.ContingencyTables.ProfilePrograms.work_entryCache line 25
  5. lemma OAI.ContingencyTables.ProfilePrograms.work_entryQuery line 33
  6. lemma OAI.ContingencyTables.ProfilePrograms.work_validMatrixEntry line 46
  7. lemma OAI.ContingencyTables.ProfilePrograms.work_matrixDenominator line 59
  8. lemma OAI.ContingencyTables.ProfilePrograms.work_entryDenominator line 78
  9. lemma OAI.ContingencyTables.ProfilePrograms.work_diagonalMatrixEntry line 91
  10. lemma OAI.ContingencyTables.ProfilePrograms.work_matrixEntry line 99