OAI/Combinatorics/HadwigerCounterexample/RandomBinaryMixing.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Random Binary Mixing

  1. instance OAI.HadwigerCounterexample.momFintype line 10
  2. instance OAI.HadwigerCounterexample.idxDec line 11
  3. instance OAI.HadwigerCounterexample.arrFintype line 12
  4. instance OAI.HadwigerCounterexample.drawFintype line 13
  5. theorem OAI.HadwigerCounterexample.rank_fifth_bound line 20
  6. theorem OAI.HadwigerCounterexample.pr_surj_rank line 36
  7. theorem OAI.HadwigerCounterexample.ztest_prob line 45
  8. theorem OAI.HadwigerCounterexample.stest_prob line 58
  9. theorem OAI.HadwigerCounterexample.binary_likely line 80