OAI/Combinatorics/KMedian/PCP/Linearity.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedian.PCP.derivative line 14
  2. def OAI.MetricKMedian.PCP.linearityRejects line 16
  3. def OAI.MetricKMedian.PCP.correctionErrors line 20
  4. theorem OAI.MetricKMedian.PCP.exists_best_anchor line 24
  5. def OAI.MetricKMedian.PCP.corrected line 33
  6. theorem OAI.MetricKMedian.PCP.corrected_min line 36
  7. def OAI.MetricKMedian.PCP.derivativePairEquiv line 41
  8. theorem OAI.MetricKMedian.PCP.shifted_reject_count line 47
  9. theorem OAI.MetricKMedian.PCP.different_derivatives_bound line 58
  10. theorem OAI.MetricKMedian.PCP.correction_error_bound line 82
  11. theorem OAI.MetricKMedian.PCP.count_translate line 100
  12. theorem OAI.MetricKMedian.PCP.card_le_of_three_cover line 106
  13. theorem OAI.MetricKMedian.PCP.corrected_add line 121
  14. def OAI.MetricKMedian.PCP.correctedHom line 148
  15. def OAI.MetricKMedian.PCP.tableErrors line 157
  16. theorem OAI.MetricKMedian.PCP.sum_point_rejects line 161
  17. theorem OAI.MetricKMedian.PCP.corrected_close line 174
  18. theorem OAI.MetricKMedian.PCP.linearity_test_sound line 207
  19. theorem OAI.MetricKMedian.PCP.linearity_test_complete line 212