OAI/Combinatorics/ContingencyTables/Machines/ScheduledScalarBounds.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Charging scalar tabulation loops to the ordinary sampler's word

  1. lemma OAI.ContingencyTables.ProfilePrograms.parameterDimension_pos line 11
  2. lemma OAI.ContingencyTables.ProfilePrograms.parameterBinaryLength_pos line 15
  3. lemma OAI.ContingencyTables.ProfilePrograms.parameterSteps_pos line 20
  4. lemma OAI.ContingencyTables.ProfilePrograms.parameterTrials_pos line 25
  5. lemma OAI.ContingencyTables.ProfilePrograms.parameterCompletionWidth_pos line 29
  6. lemma OAI.ContingencyTables.ProfilePrograms.parameterDimension_le_steps line 33
  7. lemma OAI.ContingencyTables.ProfilePrograms.parameterBinaryLength_le_steps line 42
  8. lemma OAI.ContingencyTables.ProfilePrograms.parameterAccuracy_le_steps line 51
  9. theorem OAI.ContingencyTables.ProfilePrograms.schedule_numeric_polynomial line 56
  10. lemma OAI.ContingencyTables.ProfilePrograms.scheduledCountInputMeasure_le line 73
  11. theorem OAI.ContingencyTables.SmallGraphProfiles.exact_count_input_measure_polynomial line 114