OAI/Combinatorics/KMedian/Amplification/RegularPrograms.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MetricKMedian.PCP.Compiler.RegularProgram.RPort line 15
  2. abbrev OAI.MetricKMedian.PCP.Compiler.RegularProgram.Port line 16
  3. lemma OAI.MetricKMedian.PCP.Compiler.RegularProgram.poly_zeroBranch line 17
  4. def OAI.MetricKMedian.PCP.Compiler.RegularProgram.matchStep line 18
  5. def OAI.MetricKMedian.PCP.Compiler.RegularProgram.matchAllowed line 26
  6. def OAI.MetricKMedian.PCP.Compiler.RegularProgram.localRotate line 33
  7. def OAI.MetricKMedian.PCP.Compiler.RegularProgram.localAllowed line 37
  8. def OAI.MetricKMedian.PCP.Compiler.RegularProgram.paddedRotate line 39
  9. def OAI.MetricKMedian.PCP.Compiler.RegularProgram.paddedAllowed line 45
  10. def OAI.MetricKMedian.PCP.Compiler.RegularProgram.strongRotate line 47
  11. def OAI.MetricKMedian.PCP.Compiler.RegularProgram.rotate line 49
  12. def OAI.MetricKMedian.PCP.Compiler.RegularProgram.allowed line 56
  13. lemma OAI.MetricKMedian.PCP.Compiler.RegularProgram.poly_matchStep line 58
  14. lemma OAI.MetricKMedian.PCP.Compiler.RegularProgram.poly_matchAllowed line 72
  15. lemma OAI.MetricKMedian.PCP.Compiler.RegularProgram.poly_localRotate line 77
  16. lemma OAI.MetricKMedian.PCP.Compiler.RegularProgram.poly_localAllowed line 86
  17. lemma OAI.MetricKMedian.PCP.Compiler.RegularProgram.poly_paddedRotate line 92
  18. lemma OAI.MetricKMedian.PCP.Compiler.RegularProgram.poly_paddedAllowed line 101
  19. lemma OAI.MetricKMedian.PCP.Compiler.RegularProgram.poly_strongRotate line 108
  20. lemma OAI.MetricKMedian.PCP.Compiler.RegularProgram.poly_rotate line 114
  21. lemma OAI.MetricKMedian.PCP.Compiler.RegularProgram.poly_allowed line 117