OAI/Combinatorics/KMedian/PCP/Hadamard.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MetricKMedian.PCP.Bit line 12
  2. abbrev OAI.MetricKMedian.PCP.BitVector line 13
  3. theorem OAI.MetricKMedian.PCP.bit_cases line 15
  4. theorem OAI.MetricKMedian.PCP.bit_add_one_ne_zero line 22
  5. theorem OAI.MetricKMedian.PCP.linear_nonzero_rate line 28
  6. theorem OAI.MetricKMedian.PCP.bilinear_nonzero_rate line 46
  7. def OAI.MetricKMedian.PCP.dot line 80
  8. def OAI.MetricKMedian.PCP.tensor line 82
  9. theorem OAI.MetricKMedian.PCP.dot_add_left line 85
  10. theorem OAI.MetricKMedian.PCP.dot_add_right line 87
  11. theorem OAI.MetricKMedian.PCP.dot_zero_left line 89
  12. theorem OAI.MetricKMedian.PCP.dot_zero_right line 90
  13. def OAI.MetricKMedian.PCP.dotHom line 92
  14. theorem OAI.MetricKMedian.PCP.tensor_add_left line 98
  15. theorem OAI.MetricKMedian.PCP.tensor_add_right line 101
  16. theorem OAI.MetricKMedian.PCP.tensor_zero_left line 104
  17. theorem OAI.MetricKMedian.PCP.tensor_zero_right line 107
  18. theorem OAI.MetricKMedian.PCP.dot_tensor line 110
  19. def OAI.MetricKMedian.PCP.coordinates line 119
  20. theorem OAI.MetricKMedian.PCP.linear_representation line 123
  21. def OAI.MetricKMedian.PCP.multiplicationDiscrepancy line 139
  22. theorem OAI.MetricKMedian.PCP.multiplication_identifies_tensor line 149