OAI/Combinatorics/KMedian/Geometry/GraphComparison.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedian.GraphComparison.externalMass line 12
  2. def OAI.MetricKMedian.GraphComparison.externalSquare line 14
  3. def OAI.MetricKMedian.GraphComparison.rowType line 16
  4. def OAI.MetricKMedian.GraphComparison.kernel line 18
  5. theorem OAI.MetricKMedian.GraphComparison.external_bounds line 21
  6. theorem OAI.MetricKMedian.GraphComparison.row_type_bounds line 31
  7. theorem OAI.MetricKMedian.GraphComparison.kernel_bound line 43
  8. theorem OAI.MetricKMedian.GraphComparison.kernel_average_bound line 55
  9. theorem OAI.MetricKMedian.GraphComparison.taper_error line 75
  10. theorem OAI.MetricKMedian.GraphComparison.radius_control line 89
  11. def OAI.MetricKMedian.GraphComparison.normalizedDrift line 112
  12. theorem OAI.MetricKMedian.GraphComparison.normalized_drift_le line 120