OAI/Combinatorics/LowSpaceSubsetSum/Representation/RepresentationSamplerExecution.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

Executed counters for the complete representation sampler

  1. def OAI.LowSpaceSubsetSum.SamplerExecution.subset line 17
  2. theorem OAI.LowSpaceSubsetSum.SamplerExecution.subset_bounded line 20
  3. def OAI.LowSpaceSubsetSum.SamplerExecution.fixedSize line 23
  4. theorem OAI.LowSpaceSubsetSum.SamplerExecution.fixedSize_bounded line 26
  5. def OAI.LowSpaceSubsetSum.SamplerExecution.bitArray line 29
  6. def OAI.LowSpaceSubsetSum.SamplerExecution.sign line 33
  7. theorem OAI.LowSpaceSubsetSum.SamplerExecution.sign_bounded line 35
  8. def OAI.LowSpaceSubsetSum.SamplerExecution.factor line 37
  9. def OAI.LowSpaceSubsetSum.SamplerExecution.primeTestBudget line 43
  10. theorem OAI.LowSpaceSubsetSum.SamplerExecution.factor_bounded line 45
  11. def OAI.LowSpaceSubsetSum.SamplerExecution.triplePrime line 56
  12. theorem OAI.LowSpaceSubsetSum.SamplerExecution.triplePrime_bounded line 59
  13. def OAI.LowSpaceSubsetSum.SeparatorExpectation.RoundedParameters.samplerExecution line 72
  14. theorem OAI.LowSpaceSubsetSum.SeparatorExpectation.RoundedParameters.samplerExecution_bounded line 77
  15. instance OAI.LowSpaceSubsetSum.RepresentationSetup.guessNonempty line 102

    Also declared: OAI/Combinatorics/LowSpaceSubsetSum/Representation/RepresentationSamplerCoupling.lean:93 (same declaration text).

  16. def OAI.LowSpaceSubsetSum.RepresentationSetup.layoutExecution line 105
  17. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.layoutExecution_bounded line 108
  18. def OAI.LowSpaceSubsetSum.RepresentationSetup.guessesExecution line 113
  19. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.guessesExecution_bounded line 116
  20. def OAI.LowSpaceSubsetSum.RepresentationSetup.partitionsExecution line 119
  21. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.partitionsExecution_bounded line 123
  22. def OAI.LowSpaceSubsetSum.RepresentationSetup.nestedExecution line 131
  23. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.nestedExecution_bounded line 135
  24. def OAI.LowSpaceSubsetSum.RepresentationSetup.residuesExecution line 140
  25. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.residuesExecution_bounded line 149
  26. def OAI.LowSpaceSubsetSum.RepresentationSetup.guessHistoryExecution line 160
  27. def OAI.LowSpaceSubsetSum.RepresentationSetup.partitionHistoryExecution line 163
  28. def OAI.LowSpaceSubsetSum.RepresentationSetup.primeHistoryExecution line 166
  29. def OAI.LowSpaceSubsetSum.RepresentationSetup.trialHistoryExecution line 169
  30. def OAI.LowSpaceSubsetSum.RepresentationSetup.extraPrimeExecution line 172
  31. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.extraPrimeExecution_bounded line 176
  32. def OAI.LowSpaceSubsetSum.RepresentationSetup.extraHistoryExecution line 182
  33. def OAI.LowSpaceSubsetSum.RepresentationSetup.bucketHistoryExecution line 187
  34. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.bucketHistoryExecution_bounded line 192
  35. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.primeTestBudget_half line 215
  36. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.bucketHistoryExecution_operations line 231

    Source documentation

    Every executed sampler history, including an exhausted one, has this candidate-read plus divisor-test bound. No success event is assumed.

    theorem bucketHistoryExecution_operations (hn : 10000 ≤ n)
    (s : (R.bucketHistoryCoupling hn).Seed) :
    ((R.bucketHistoryExecution hn).run s).reads +
        ((R.bucketHistoryExecution hn).run s).tests ≤
      128 * (inputScale R.input : ℝ) ^ 4 * (2 : ℝ) ^ ((n : ℝ) / 2) := by
…

    Mentions: OAI.LowSpaceSubsetSum.inputScale