OAI/Combinatorics/LowSpaceSubsetSum/Representation/RepresentationLeafDomains.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Actual cardinalities of the representation leaf domains

  1. def OAI.LowSpaceSubsetSum.RepresentationSetup.rawBlockFiberEquiv line 21

    Source documentation

    The set-level filter is exactly the corresponding fiber of the sampled balanced coloring.

    def rawBlockFiberEquiv (z : Layout n) (f : R.Partitions z) (j : Fin 3)
    (a : Fin (blockCount j)) :
    ↥(R.rawPartitionBlock z f j a.val) ≃
      {x : ↥(R.orderedMixers z j) // (f j).val x = a} where
…

    Mentions: OAI.LowSpaceSubsetSum.RepresentationSetup.Layout, OAI.LowSpaceSubsetSum.RepresentationSetup.blockCount

  2. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.rawPartitionBlock_card line 34
  3. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.rawPartitionBlock_biUnion line 41
  4. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.rawLeaf_top_card line 54
  5. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.rawLeaf_local_card line 59
  6. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.rawLeaf_topDomain line 69
  7. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.rawLeaf_mixerDomain line 79
  8. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.rawLeaf_topCount_bound line 99
  9. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.rawLeaf_localCount_bound line 113
  10. theorem OAI.LowSpaceSubsetSum.balancedBlockCounts_error line 133

    Source documentation

    Balanced block counts differ from their rational ideal by at most one.

    theorem balancedBlockCounts_error (l k : ℕ) (hl : 0 < l) (j : Fin l) :
    |(balancedBlockCounts l k j : ℝ) - (k : ℝ) / l| ≤ 1 := by
…

    Mentions: OAI.LowSpaceSubsetSum.balancedBlockCounts