OAI/Combinatorics/MatchingCount/Algorithm/SortedList.lean

GitHub source file

54 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatchingFPRAS.Amplification.sortedList line 11
  2. lemma OAI.MatchingFPRAS.Amplification.sortedList_length line 14
  3. def OAI.MatchingFPRAS.Amplification.sortedValue line 17
  4. def OAI.MatchingFPRAS.Amplification.median line 20
  5. lemma OAI.MatchingFPRAS.Amplification.sortedValue_monotone line 22
  6. lemma OAI.MatchingFPRAS.Amplification.ofFn_sortedValue line 26
  7. lemma OAI.MatchingFPRAS.Amplification.majority_sorted line 33
  8. lemma OAI.MatchingFPRAS.Amplification.good_count line 65
  9. lemma OAI.MatchingFPRAS.Amplification.sorted_good_count line 71
  10. theorem OAI.MatchingFPRAS.Amplification.median_majority line 77
  11. lemma OAI.MatchingFPRAS.Amplification.product_bad line 89
  12. lemma OAI.MatchingFPRAS.Amplification.product_moment line 95
  13. lemma OAI.MatchingFPRAS.Amplification.majority_tail line 110
  14. lemma OAI.MatchingFPRAS.Amplification.median_failure line 143
  15. lemma OAI.MatchingFPRAS.Amplification.median_nonneg line 162
  16. def OAI.MatchingFPRAS.Amplification.halfRepetitions line 174
  17. lemma OAI.MatchingFPRAS.Amplification.repetitions_source line 175
  18. lemma OAI.MatchingFPRAS.Amplification.amplification_precision line 178
  19. lemma OAI.MatchingFPRAS.Amplification.median_delta line 192
  20. def OAI.MatchingFPRAS.FiniteTrial.amplifiedOutput line 204
  21. lemma OAI.MatchingFPRAS.FiniteTrial.amplifiedOutput_nonneg line 207
  22. theorem OAI.MatchingFPRAS.FiniteTrial.actual_finite_amplified_failure line 210
  23. instance OAI.MatchingFPRAS.Counting.scheduleDecidable line 221
  24. lemma OAI.MatchingFPRAS.Counting.schedule_exists line 223
  25. def OAI.MatchingFPRAS.Counting.leastSchedule line 227
  26. lemma OAI.MatchingFPRAS.Counting.leastSchedule_spec line 229
  27. lemma OAI.MatchingFPRAS.Counting.leastSchedule_le line 231
  28. lemma OAI.MatchingFPRAS.Counting.leastSchedule_log_bound line 233
  29. def OAI.MatchingFPRAS.FiniteTrial.parameters line 239
  30. def OAI.MatchingFPRAS.BitArithmetic.FractionBound line 253
  31. lemma OAI.MatchingFPRAS.BitArithmetic.FractionBound.mono line 255
  32. lemma OAI.MatchingFPRAS.BitArithmetic.FractionBound.zero line 258
  33. lemma OAI.MatchingFPRAS.BitArithmetic.FractionBound.one line 260
  34. lemma OAI.MatchingFPRAS.BitArithmetic.FractionBound.nat line 262
  35. lemma OAI.MatchingFPRAS.BitArithmetic.FractionBound.mul line 264
  36. lemma OAI.MatchingFPRAS.BitArithmetic.FractionBound.div line 271
  37. lemma OAI.MatchingFPRAS.BitArithmetic.FractionBound.add line 282
  38. lemma OAI.MatchingFPRAS.BitArithmetic.FractionBound.sup' line 296
  39. lemma OAI.MatchingFPRAS.BitArithmetic.FractionBound.max line 301
  40. lemma OAI.MatchingFPRAS.BitArithmetic.FractionBound.min line 306
  41. lemma OAI.MatchingFPRAS.Trial.cooling_fraction line 318
  42. lemma OAI.MatchingFPRAS.Trial.ScaleState.edge_ratio line 323
  43. lemma OAI.MatchingFPRAS.Trial.ScaleState.bag_reweight line 338
  44. lemma OAI.MatchingFPRAS.Trial.product_binary_power line 349
  45. lemma OAI.MatchingFPRAS.Trial.ScaleState.pm_card line 361
  46. lemma OAI.MatchingFPRAS.Trial.ScaleState.observable_power line 369
  47. def OAI.MatchingFPRAS.BitArithmetic.GridFraction line 401
  48. lemma OAI.MatchingFPRAS.BitArithmetic.GridFraction.zero line 402
  49. lemma OAI.MatchingFPRAS.BitArithmetic.GridFraction.one line 403
  50. lemma OAI.MatchingFPRAS.BitArithmetic.GridFraction.fractionBound line 405
  51. lemma OAI.MatchingFPRAS.BitArithmetic.GridFraction.average line 409
  52. lemma OAI.MatchingFPRAS.BitArithmetic.GridFraction.cooling_power line 423
  53. lemma OAI.MatchingFPRAS.BitArithmetic.FractionBound.pow line 437
  54. lemma OAI.MatchingFPRAS.BitArithmetic.FractionBound.prod line 442