OAI/Combinatorics/LowSpaceSubsetSum/Representation/RepresentationAllocatedEntries.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.rawBackground_disjoint line 15
2. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.rawLeaf_background_card_sum line 23
3. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.rawLeaf_allocated_backgroundDomain_card line 38
4. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.rawLeaf_topCount_sum line 58
5. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.rawLeaf_allocated_entry_card line 90
6. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.rawLeaf_allocated_entry_card_bound line 112

   Source documentation

   The entire deterministic entry-allocation loss is at most two plus one binary logarithm. The local distinct-sum factor is retained exactly.

   theorem rawLeaf_allocated_entry_card_bound (z : Layout n) (g : Guesses n)
       (f : R.Partitions z) (hn : 10000 ≤ n)
       (hlog : Real.logb 2 ((mixerSize n : ℝ) + 1) + 1 ≤ (n : ℝ) / 1000) (j : Fin 2) :
       ((RepresentationUniverse.validEntries (R.signedWeights z)
         (R.rawLeaf z g f (R.allocatedBackground z g hn hlog) j)).card : ℝ) ≤
         (2 : ℝ) ^ ((representationBackgroundSize n : ℝ) / 2 +
           (representationEntropy n g false 0 + representationEntropy n g true 0) / 2 +
           (mixerSize n : ℝ) - deficiency (R.signedWeights z) (R.orderedMixers z j.succ) +
           Real.logb 2 ((mixerSize n : ℝ) + 1) + 2) := by
   …

   Mentions: OAI.LowSpaceSubsetSum.RepresentationSetup.Layout, OAI.LowSpaceSubsetSum.RepresentationSetup.Guesses, OAI.LowSpaceSubsetSum.mixerSize, OAI.LowSpaceSubsetSum.RepresentationUniverse.validEntries, OAI.LowSpaceSubsetSum.representationBackgroundSize, OAI.LowSpaceSubsetSum.representationEntropy, OAI.LowSpaceSubsetSum.deficiency