OAI/Combinatorics/ContingencyTables/Counting/CountingOracleWordBounds.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Polynomial word sizes for the executed density oracle

  1. lemma OAI.ContingencyTables.CountingOracleWordBounds.binWordBits_bound line 16
  2. lemma OAI.ContingencyTables.CountingOracleWordBounds.oracle_time_bound line 41
  3. lemma OAI.ContingencyTables.CountingOracleWordBounds.samples_bound line 56
  4. lemma OAI.ContingencyTables.CountingOracleWordBounds.offset_bound line 65
  5. def OAI.ContingencyTables.CountingOracleWordBounds.timeBound line 72
  6. def OAI.ContingencyTables.CountingOracleWordBounds.sampleBound line 74
  7. def OAI.ContingencyTables.CountingOracleWordBounds.binBound line 75
  8. def OAI.ContingencyTables.CountingOracleWordBounds.estimatorBound line 76
  9. lemma OAI.ContingencyTables.CountingOracleWordBounds.oracle_time_uniform line 80
  10. lemma OAI.ContingencyTables.CountingOracleWordBounds.estimator_bound line 92
  11. def OAI.ContingencyTables.CountingOracleWordBounds.innerPolynomial line 124
  12. def OAI.ContingencyTables.CountingOracleWordBounds.timePolynomial line 125
  13. def OAI.ContingencyTables.CountingOracleWordBounds.samplePolynomial line 127
  14. def OAI.ContingencyTables.CountingOracleWordBounds.binPolynomial line 128
  15. def OAI.ContingencyTables.CountingOracleWordBounds.estimatorPolynomial line 129
  16. def OAI.ContingencyTables.CountingOracleWordBounds.medianPolynomial line 132
  17. lemma OAI.ContingencyTables.CountingOracleWordBounds.estimatorPolynomial_eval line 134
  18. lemma OAI.ContingencyTables.CountingOracleWordBounds.median_bound_separate line 140
  19. lemma OAI.ContingencyTables.CountingOracleWordBounds.median_bound line 164