OAI/Combinatorics/ContingencyTables/Machines/MedianFractionProgram.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

Binary fraction median with polynomial running time

  1. abbrev OAI.ContingencyTables.MedianFractionProgram.State line 12
  2. def OAI.ContingencyTables.MedianFractionProgram.insertRaw line 14
  3. def OAI.ContingencyTables.MedianFractionProgram.step line 18
  4. def OAI.ContingencyTables.MedianFractionProgram.stepRealizer line 22
  5. lemma OAI.ContingencyTables.MedianFractionProgram.polynomial_step line 32
  6. def OAI.ContingencyTables.MedianFractionProgram.insert line 51
  7. lemma OAI.ContingencyTables.MedianFractionProgram.insert_fold line 54
  8. lemma OAI.ContingencyTables.MedianFractionProgram.insert_eq line 62
  9. lemma OAI.ContingencyTables.MedianFractionProgram.insert_weight line 66
  10. lemma OAI.ContingencyTables.MedianFractionProgram.fold_weight line 75
  11. lemma OAI.ContingencyTables.MedianFractionProgram.state_weight line 97
  12. lemma OAI.ContingencyTables.MedianFractionProgram.polynomial_stepFold line 102
  13. def OAI.ContingencyTables.MedianFractionProgram.insertRealizer line 112
  14. lemma OAI.ContingencyTables.MedianFractionProgram.polynomial_insert line 126
  15. def OAI.ContingencyTables.MedianFractionProgram.sort line 136
  16. def OAI.ContingencyTables.MedianFractionProgram.sortRealizer line 139
  17. lemma OAI.ContingencyTables.MedianFractionProgram.sortFold_weight line 144
  18. lemma OAI.ContingencyTables.MedianFractionProgram.polynomial_insertFold line 153
  19. lemma OAI.ContingencyTables.MedianFractionProgram.polynomial_sort line 161
  20. lemma OAI.ContingencyTables.MedianFractionProgram.insert_pos line 165
  21. lemma OAI.ContingencyTables.MedianFractionProgram.insert_map line 182
  22. lemma OAI.ContingencyTables.MedianFractionProgram.sort_cons line 195
  23. lemma OAI.ContingencyTables.MedianFractionProgram.sort_pos line 198
  24. lemma OAI.ContingencyTables.MedianFractionProgram.sort_map line 206
  25. def OAI.ContingencyTables.MedianFractionProgram.median line 216
  26. def OAI.ContingencyTables.MedianFractionProgram.medianRealizer line 219
  27. lemma OAI.ContingencyTables.MedianFractionProgram.polynomial_median line 225
  28. lemma OAI.ContingencyTables.MedianFractionProgram.median_val line 232