OAI/Combinatorics/KMedian/PCP/Boundary.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MetricKMedian.PCP.table_distance_triangle line 15
  2. theorem OAI.MetricKMedian.PCP.table_distance_symm line 24
  3. theorem OAI.MetricKMedian.PCP.derivative_distance line 32
  4. theorem OAI.MetricKMedian.PCP.dot_single line 53
  5. theorem OAI.MetricKMedian.PCP.hadamard_distance line 57
  6. theorem OAI.MetricKMedian.PCP.exists_nearest line 73
  7. def OAI.MetricKMedian.PCP.nearestLabel line 81
  8. theorem OAI.MetricKMedian.PCP.nearestLabel_min line 84
  9. theorem OAI.MetricKMedian.PCP.nearestLabel_robust line 88
  10. def OAI.MetricKMedian.PCP.liftQuery line 101
  11. theorem OAI.MetricKMedian.PCP.dot_liftQuery line 105
  12. def OAI.MetricKMedian.PCP.boundaryRate line 113
  13. theorem OAI.MetricKMedian.PCP.boundary_transfer line 118