OAI/Combinatorics/LowSpaceSubsetSum/Counting/BalancedLeafEntropy.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Entropy of the actual balanced leaf counts

Both the selected count and its complementary half count are treated with the same unit rounding error. This is applied to the four top blocks and the two local blocks sampled by the representation experiment.

  1. def OAI.LowSpaceSubsetSum.orientedBlockCount line 16
  2. def OAI.LowSpaceSubsetSum.orientedDensity line 19
  3. theorem OAI.LowSpaceSubsetSum.orientedDensity_mem line 22
  4. theorem OAI.LowSpaceSubsetSum.orientedBlockCount_error line 28
  5. theorem OAI.LowSpaceSubsetSum.orientedBlockCount_entropy line 52
  6. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.guess_density line 66
  7. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.rawLeaf_top_entropy line 86
  8. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.rawLeaf_local_entropy line 120