OAI/Combinatorics/KMedian/Hardness/Analysis.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedian.Coverage.Input.selectedMask line 12
  2. theorem OAI.MetricKMedian.Coverage.Input.selectedMask_eq_selected line 15
  3. def OAI.MetricKMedian.Coverage.Input.comparisonCost line 21
  4. def OAI.MetricKMedian.Coverage.Input.accepts line 24
  5. theorem OAI.MetricKMedian.Coverage.Input.comparisonCost_eq_cost line 27
  6. theorem OAI.MetricKMedian.Coverage.Input.accepts_of_perfect line 34
  7. theorem OAI.MetricKMedian.Coverage.Input.rejects_of_sound line 46
  8. theorem OAI.MetricKMedian.exists_coverage_margin line 63
  9. theorem OAI.MetricKMedian.factor_above_threshold line 72
  10. theorem OAI.MetricKMedian.approximationFactors_nonempty line 77
  11. def OAI.MetricKMedian.unitCoverage line 80
  12. theorem OAI.MetricKMedian.unitCoverage_perfect line 89
  13. theorem OAI.MetricKMedian.factor_ge_one line 100
  14. theorem OAI.MetricKMedian.approximationFactors_bddBelow line 110
  15. theorem OAI.MetricKMedian.approximationFactors_upward line 113
  16. theorem OAI.MetricKMedian.infimum_le_threshold line 122
  17. theorem OAI.MetricKMedian.one_le_infimum line 128