OAI/Combinatorics/LowSpaceSubsetSum/Representation/RepresentationAllocatedLeaves.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Leaf bounds for the actual computed background partition

  1. def OAI.LowSpaceSubsetSum.representationBeta line 14
  2. theorem OAI.LowSpaceSubsetSum.representationLeafCounts_eq line 19
  3. theorem OAI.LowSpaceSubsetSum.representationBackgroundSize_cast line 25
  4. theorem OAI.LowSpaceSubsetSum.representationEntropy_pair_le line 32
  5. theorem OAI.LowSpaceSubsetSum.representationBeta_upper line 43
  6. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.orderedMixers_card_mixerSize line 57
  7. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.mixerUnion_card line 63
  8. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.backgroundDomain_card line 72
  9. def OAI.LowSpaceSubsetSum.RepresentationSetup.allocatedBackground line 79

    Source documentation

    The background coloring used by the finite program, in its fixed sorted order.

    def allocatedBackground (z : Layout n) (g : Guesses n) (hn : 10000 ≤ n)
    (hlog : Real.logb 2 ((mixerSize n : ℝ) + 1) + 1 ≤ (n : ℝ) / 1000) :
    Fin n → Fin 2 × Fin 4 :=
…

    Mentions: OAI.LowSpaceSubsetSum.RepresentationSetup.Layout, OAI.LowSpaceSubsetSum.RepresentationSetup.Guesses, OAI.LowSpaceSubsetSum.mixerSize

  10. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.rawLeaf_allocated_background_card line 85
  11. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.rawLeaf_allocated_entropy line 96
  12. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.rawLeaf_allocated_card line 141