OAI/Combinatorics/ParityLifts/BalancedBags.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ParityWL.regionSet line 16
  2. lemma OAI.ParityWL.sum_regions line 19
  3. structure OAI.ParityWL.BalancedStar line 27

    Source documentation

    The star about a sink bag, with its vertex partition obtained from a tree decomposition.

    structure BalancedStar (w : WeightedWitness (template t) F a b) where
…

    Mentions: OAI.ParityWL.WeightedWitness, OAI.ParityWL.template

  4. lemma OAI.ParityWL.main_card_le line 43
  5. lemma OAI.ParityWL.missing_main line 59
  6. lemma OAI.ParityWL.BalancedStar.partition_mass line 66
  7. lemma OAI.ParityWL.BalancedStar.main_present line 74
  8. lemma OAI.ParityWL.BalancedStar.representatives line 88
  9. def OAI.ParityWL.leftTest line 116
  10. def OAI.ParityWL.rightTest line 119
  11. def OAI.ParityWL.helperTest line 122
  12. lemma OAI.ParityWL.test_main_compatible line 125
  13. lemma OAI.ParityWL.test_helper_left_compatible line 134
  14. lemma OAI.ParityWL.test_helper_right_compatible line 142
  15. lemma OAI.ParityWL.bit_complement_left line 151
  16. lemma OAI.ParityWL.bit_complement_right line 155