OAI/Combinatorics/ContingencyTables/Counting/CountingPositiveWordBound.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Public polynomial bounds for the executed positive counting words

  1. def OAI.ContingencyTables.CountingPositiveWordBound.measurePolynomial line 14
  2. def OAI.ContingencyTables.CountingPositiveWordBound.widthPolynomial line 15
  3. def OAI.ContingencyTables.CountingPositiveWordBound.singlePolynomial line 17
  4. def OAI.ContingencyTables.CountingPositiveWordBound.amplifiedPolynomial line 19
  5. lemma OAI.ContingencyTables.CountingPositiveWordBound.control_parts line 21
  6. lemma OAI.ContingencyTables.CountingPositiveWordBound.phaseCount_public line 32
  7. lemma OAI.ContingencyTables.CountingPositiveWordBound.measure_public line 43
  8. lemma OAI.ContingencyTables.CountingPositiveWordBound.width_value line 91
  9. theorem OAI.ContingencyTables.CountingPositiveWordBound.single_public line 97
  10. theorem OAI.ContingencyTables.CountingPositiveWordBound.amplified_public line 110
  11. theorem OAI.ContingencyTables.CountingPositiveWordBound.branch_public line 120