OAI/Combinatorics/ContingencyTables/Counting/CountingPublicInputBounds.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Bounding counting parameters by the public binary input

  1. def OAI.ContingencyTables.CountingPublicInputBounds.size line 14
  2. lemma OAI.ContingencyTables.CountingPublicInputBounds.nat_length line 18
  3. lemma OAI.ContingencyTables.CountingPublicInputBounds.successor_size line 21
  4. lemma OAI.ContingencyTables.CountingPublicInputBounds.matrix_length line 28
  5. lemma OAI.ContingencyTables.CountingPublicInputBounds.cells_le_matrix_length line 33
  6. lemma OAI.ContingencyTables.CountingPublicInputBounds.matrix_le_input line 40
  7. lemma OAI.ContingencyTables.CountingPublicInputBounds.dimension_le line 46
  8. lemma OAI.ContingencyTables.CountingPublicInputBounds.capacityBits_le line 53
  9. lemma OAI.ContingencyTables.CountingPublicInputBounds.inverse_le line 69
  10. lemma OAI.ContingencyTables.CountingPublicInputBounds.repeats_le line 77