OAI/Combinatorics/LowSpaceSubsetSum/Representation/RepresentationAllocation.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LowSpaceSubsetSum.representationCount line 14
2. def OAI.LowSpaceSubsetSum.representationBits line 17
3. def OAI.LowSpaceSubsetSum.representationBackgroundSize line 20
4. def OAI.LowSpaceSubsetSum.representationParentSize line 22
5. def OAI.LowSpaceSubsetSum.representationChildSize line 26
6. def OAI.LowSpaceSubsetSum.representationLeafCounts line 30
7. def OAI.LowSpaceSubsetSum.representationEntropy line 36
8. theorem OAI.LowSpaceSubsetSum.representation_log_budget line 41

   Source documentation

   The main-branch input-scale test supplies the small allocation error.

   theorem representation_log_budget {n : ℕ} {u : ℝ} (hn : 10000 ≤ n)
       (hmu : (mixerSize n : ℝ) + 1 ≤ u) (hlog : Real.logb 2 u ≤ (n : ℝ) / 1000000000) :
       Real.logb 2 ((mixerSize n : ℝ) + 1) + 1 ≤ (n : ℝ) / 1000 := by
   …

   Mentions: OAI.LowSpaceSubsetSum.mixerSize

9. theorem OAI.LowSpaceSubsetSum.representationCount_le line 49
10. theorem OAI.LowSpaceSubsetSum.representationCount_fraction line 55
11. theorem OAI.LowSpaceSubsetSum.representationBits_entropy_error line 73
12. theorem OAI.LowSpaceSubsetSum.representationBits_difference line 82
13. theorem OAI.LowSpaceSubsetSum.allocation_guards_of_error line 94
14. theorem OAI.LowSpaceSubsetSum.weighted_parent_allocation_bound line 103
15. theorem OAI.LowSpaceSubsetSum.allocation_three_levels_feasible line 111
16. theorem OAI.LowSpaceSubsetSum.representationAllocation_feasible line 127
17. theorem OAI.LowSpaceSubsetSum.representationLeafCounts_sum line 156