OAI/Combinatorics/ParityLifts/ColorSpan.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ParityWL.pairAtomic line 16
  2. def OAI.ParityWL.pairJoint line 19
  3. def OAI.ParityWL.pairSeparate line 22
  4. def OAI.ParityWL.boolIndicator line 25
  5. lemma OAI.ParityWL.boolIndicator_injective line 27
  6. lemma OAI.ParityWL.testEval_equality line 31
  7. lemma OAI.ParityWL.testEval_edge line 35
  8. lemma OAI.ParityWL.atomic_indicator_mem line 39
  9. lemma OAI.ParityWL.joint_indicator_sum line 58
  10. lemma OAI.ParityWL.separate_indicator_sum line 85
  11. lemma OAI.ParityWL.pairJoint_zero line 93
  12. lemma OAI.ParityWL.pairSeparate_zero line 97
  13. lemma OAI.ParityWL.pairJoint_fst line 101
  14. lemma OAI.ParityWL.pairSeparate_fst line 105
  15. lemma OAI.ParityWL.joint_indicator_mem line 109
  16. lemma OAI.ParityWL.separate_indicator_mem line 142
  17. lemma OAI.ParityWL.sum_eq_of_mem_testSpan line 186
  18. lemma OAI.ParityWL.histograms_eq_of_tests line 200
  19. theorem OAI.ParityWL.no_choice_equivalent line 213