OAI/Combinatorics/KMedian/PCP/QuadraticEncoding.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MetricKMedian.PCP.bit_mul_self line 15
  2. theorem OAI.MetricKMedian.PCP.dot_sum line 18
  3. theorem OAI.MetricKMedian.PCP.dot_smul line 21
  4. def OAI.MetricKMedian.PCP.unitForm line 24
  5. theorem OAI.MetricKMedian.PCP.dot_unitForm line 26
  6. theorem OAI.MetricKMedian.PCP.quadratic_diagonal line 30
  7. abbrev OAI.MetricKMedian.PCP.RelationEncoding.Variable line 38
  8. abbrev OAI.MetricKMedian.PCP.RelationEncoding.Equation line 39
  9. def OAI.MetricKMedian.PCP.RelationEncoding.system line 41
  10. theorem OAI.MetricKMedian.PCP.RelationEncoding.satisfies_iff line 49
  11. def OAI.MetricKMedian.PCP.RelationEncoding.witness line 71
  12. theorem OAI.MetricKMedian.PCP.RelationEncoding.witness_left line 75
  13. theorem OAI.MetricKMedian.PCP.RelationEncoding.witness_right line 79
  14. theorem OAI.MetricKMedian.PCP.RelationEncoding.complete line 83
  15. theorem OAI.MetricKMedian.PCP.RelationEncoding.sound line 94
  16. theorem OAI.MetricKMedian.PCP.RelationEncoding.exact line 120