OAI/Combinatorics/LowSpaceSubsetSum/Representation/RepresentationChosenLeaves.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

The chosen solution masks are actual raw leaf occurrences

  1. def OAI.LowSpaceSubsetSum.orientedMask line 11
  2. def OAI.LowSpaceSubsetSum.RepresentationSetup.categoryBlockEquiv line 18
  3. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.prescription_block_card line 30
  4. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.prescribedMask_block_card line 44
  5. def OAI.LowSpaceSubsetSum.RepresentationSetup.maskLeafOccurrence line 58

    Source documentation

    The top and local mask components are chosen by the representation; the background component is the fixed solution restricted to its leaf.

    def maskLeafOccurrence (z : Layout n) (f : R.Partitions z) (B : Fin n → Fin 2 × Fin 4)
    (D : Fin 3 → Finset (Fin n)) (j : Fin 2) (i : Fin 4) : RepresentationLeaf.Occurrence (Fin n) :=
…

    Mentions: OAI.LowSpaceSubsetSum.RepresentationSetup.Layout, OAI.LowSpaceSubsetSum.RepresentationLeaf.Occurrence

  6. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.maskLeafOccurrence_mem line 65
  7. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.chosenLeafOccurrence_mem line 87
  8. def OAI.LowSpaceSubsetSum.RepresentationSetup.maskParentOccurrence line 100
  9. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.four_of_pairwise line 105
  10. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.two_mask_parts_disjoint line 112
  11. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.maskParentOccurrence_valid line 129
  12. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.chosenParentOccurrence_mem line 145
  13. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.chosenEntry_mem line 156