OAI/Combinatorics/MatchingCount/Algorithm/OnlineMedian.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatchingFPRAS.OnlineMedian.relation line 10
  2. instance OAI.MatchingFPRAS.OnlineMedian.(instance at line 11) line 11
  3. def OAI.MatchingFPRAS.OnlineMedian.compareRealizer line 12
  4. lemma OAI.MatchingFPRAS.OnlineMedian.polynomial_compare line 17
  5. lemma OAI.MatchingFPRAS.OnlineMedian.relation_repr line 21
  6. def OAI.MatchingFPRAS.OnlineMedian.sorted line 32
  7. def OAI.MatchingFPRAS.OnlineMedian.sortedRealizer line 33
  8. lemma OAI.MatchingFPRAS.OnlineMedian.polynomial_sorted line 34
  9. def OAI.MatchingFPRAS.OnlineMedian.median line 36
  10. def OAI.MatchingFPRAS.OnlineMedian.medianRealizer line 37
  11. lemma OAI.MatchingFPRAS.OnlineMedian.polynomial_median line 39
  12. lemma OAI.MatchingFPRAS.OnlineMedian.sorted_repr line 43
  13. lemma OAI.MatchingFPRAS.OnlineMedian.median_repr line 51