OAI/Combinatorics/LowSpaceSubsetSum/Separators/SeparatorParameters.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Exact integer construction of the separator sample size

The logarithm floor is the binary bit count of 3^(4g). The subsequent floor is a natural-number division. Neither operation uses real arithmetic.

  1. def OAI.LowSpaceSubsetSum.SeparatorParameters.logBits line 15
  2. def OAI.LowSpaceSubsetSum.SeparatorParameters.sampleSize line 17
  3. def OAI.LowSpaceSubsetSum.SeparatorParameters.familyCount line 20
  4. def OAI.LowSpaceSubsetSum.SeparatorParameters.rationalBias line 24
  5. theorem OAI.LowSpaceSubsetSum.SeparatorParameters.logBits_bounds line 27
  6. theorem OAI.LowSpaceSubsetSum.SeparatorParameters.logBits_le line 45
  7. theorem OAI.LowSpaceSubsetSum.SeparatorParameters.numerator_nonnegative line 54
  8. theorem OAI.LowSpaceSubsetSum.SeparatorParameters.sampleSize_eq_floor line 58
  9. theorem OAI.LowSpaceSubsetSum.SeparatorParameters.rationalBias_bounds line 71
  10. theorem OAI.LowSpaceSubsetSum.SeparatorParameters.sampleSize_error line 89
  11. theorem OAI.LowSpaceSubsetSum.SeparatorParameters.rationalBias_error line 98
  12. theorem OAI.LowSpaceSubsetSum.SeparatorParameters.sampleSize_ideal_error line 119
  13. theorem OAI.LowSpaceSubsetSum.SeparatorParameters.sampleSize_upper line 130
  14. theorem OAI.LowSpaceSubsetSum.SeparatorParameters.count_le_sampleSize line 143
  15. def OAI.LowSpaceSubsetSum.SeparatorParameters.rounded line 154
  16. theorem OAI.LowSpaceSubsetSum.SeparatorParameters.ceil_ratio line 182
  17. theorem OAI.LowSpaceSubsetSum.SeparatorParameters.familyCount_eq line 196