OAI/Combinatorics/KMedian/PCP/BinaryReduction.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MetricKMedian.PCP.testRate_singleton line 12
  2. theorem OAI.MetricKMedian.PCP.testRate_ge_atom line 22
  3. abbrev OAI.MetricKMedian.PCP.IncidenceReduction.Label line 30
  4. abbrev OAI.MetricKMedian.PCP.IncidenceReduction.Position line 31
  5. abbrev OAI.MetricKMedian.PCP.IncidenceReduction.Test line 32
  6. def OAI.MetricKMedian.PCP.IncidenceReduction.reduced line 34
  7. theorem OAI.MetricKMedian.PCP.IncidenceReduction.allowed_iff line 40
  8. def OAI.MetricKMedian.PCP.IncidenceReduction.decoded line 44
  9. theorem OAI.MetricKMedian.PCP.IncidenceReduction.bad_incidence line 47
  10. theorem OAI.MetricKMedian.PCP.IncidenceReduction.sound line 60
  11. theorem OAI.MetricKMedian.PCP.IncidenceReduction.complete line 83
  12. instance OAI.MetricKMedian.PCP.AlphabetReduction.positionFintype line 97
  13. def OAI.MetricKMedian.PCP.AlphabetReduction.binary line 99
  14. theorem OAI.MetricKMedian.PCP.AlphabetReduction.binary_sound line 102
  15. theorem OAI.MetricKMedian.PCP.AlphabetReduction.binary_complete line 110
  16. def OAI.MetricKMedian.PCP.AlphabetReduction.interiorBound line 115
  17. theorem OAI.MetricKMedian.PCP.AlphabetReduction.interior_card_le line 121
  18. theorem OAI.MetricKMedian.PCP.AlphabetReduction.position_card_le line 131
  19. theorem OAI.MetricKMedian.PCP.AlphabetReduction.test_card line 141
  20. theorem OAI.MetricKMedian.PCP.AlphabetReduction.binary_card_bounds line 144