OAI/Combinatorics/LowSpaceSubsetSum/Streams/MeasuredMixerCount.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Mixer counts from generated and sorted half-sum arrays

All subset weights, comparisons, array copies and streamed sum keys are charged. The returned natural number is the exact distinct-sum count.

  1. def OAI.LowSpaceSubsetSum.MeasuredMixerCount.sortedWeights line 17
  2. theorem OAI.LowSpaceSubsetSum.MeasuredMixerCount.sortedWeights_value line 22
  3. theorem OAI.LowSpaceSubsetSum.MeasuredMixerCount.sortedWeights_size line 27
  4. theorem OAI.LowSpaceSubsetSum.MeasuredMixerCount.sortedWeights_sorted line 32
  5. def OAI.LowSpaceSubsetSum.MeasuredMixerCount.coefficient line 41
  6. theorem OAI.LowSpaceSubsetSum.MeasuredMixerCount.sortedWeights_work line 43
  7. def OAI.LowSpaceSubsetSum.MeasuredMixerCount.run line 57
  8. theorem OAI.LowSpaceSubsetSum.MeasuredMixerCount.run_source line 63
  9. theorem OAI.LowSpaceSubsetSum.MeasuredMixerCount.run_work line 68
  10. def OAI.LowSpaceSubsetSum.MeasuredMixerCount.mixerCount line 82
  11. theorem OAI.LowSpaceSubsetSum.MeasuredMixerCount.mixerCount_value line 86