OAI/Combinatorics/KMedian/PCP/FiniteTest.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedian.PCP.testRate line 12
  2. theorem OAI.MetricKMedian.PCP.testRate_nonneg line 19
  3. theorem OAI.MetricKMedian.PCP.testRate_le_one line 23
  4. theorem OAI.MetricKMedian.PCP.testRate_congr line 27
  5. theorem OAI.MetricKMedian.PCP.testRate_mono line 33
  6. theorem OAI.MetricKMedian.PCP.testRate_or_le line 41
  7. theorem OAI.MetricKMedian.PCP.testRate_union_bound line 50
  8. theorem OAI.MetricKMedian.PCP.testRate_false line 54
  9. theorem OAI.MetricKMedian.PCP.testRate_true line 58
  10. theorem OAI.MetricKMedian.PCP.testRate_complement line 62
  11. theorem OAI.MetricKMedian.PCP.testRate_equiv line 72
  12. theorem OAI.MetricKMedian.PCP.testRate_eq_count line 77
  13. theorem OAI.MetricKMedian.PCP.testRate_prod line 87
  14. theorem OAI.MetricKMedian.PCP.testRate_fst line 93
  15. theorem OAI.MetricKMedian.PCP.testRate_snd line 100
  16. theorem OAI.MetricKMedian.PCP.testRate_fibers_le line 106
  17. def OAI.MetricKMedian.PCP.linearityRate line 118
  18. theorem OAI.MetricKMedian.PCP.linearityRate_eq line 121
  19. theorem OAI.MetricKMedian.PCP.linearityRate_small line 127
  20. theorem OAI.MetricKMedian.PCP.corrective_query_error line 135
  21. theorem OAI.MetricKMedian.PCP.corrected_distance line 150