OAI/Combinatorics/KMedian/CookLevin/CookLevin.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MetricKMedian.PCP.CookLevin.polynomial_mono line 14
  2. def OAI.MetricKMedian.PCP.CookLevin.firstWord line 26
  3. def OAI.MetricKMedian.PCP.CookLevin.inputPrefix line 27
  4. def OAI.MetricKMedian.PCP.CookLevin.inputSize line 28
  5. def OAI.MetricKMedian.PCP.CookLevin.time line 29
  6. def OAI.MetricKMedian.PCP.CookLevin.space line 30
  7. def OAI.MetricKMedian.PCP.CookLevin.boundary line 31
  8. def OAI.MetricKMedian.PCP.CookLevin.system line 36
  9. lemma OAI.MetricKMedian.PCP.CookLevin.last_length line 39
  10. lemma OAI.MetricKMedian.PCP.CookLevin.init_length line 48
  11. lemma OAI.MetricKMedian.PCP.CookLevin.initial_prefix line 56
  12. lemma OAI.MetricKMedian.PCP.CookLevin.complete line 67
  13. lemma OAI.MetricKMedian.PCP.CookLevin.initial_decode line 92
  14. lemma OAI.MetricKMedian.PCP.CookLevin.sound line 116
  15. lemma OAI.MetricKMedian.PCP.CookLevin.correct line 128