OAI/Combinatorics/KMedian/Analysis/RowComparison.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MetricKMedian.FiniteComparison.positive_row_location line 10
  2. theorem OAI.MetricKMedian.FiniteComparison.d_lower line 46
  3. theorem OAI.MetricKMedian.FiniteComparison.H_bounds line 48
  4. theorem OAI.MetricKMedian.FiniteComparison.small_linear_nonpos line 54
  5. theorem OAI.MetricKMedian.FiniteComparison.centered_affine line 65
  6. theorem OAI.MetricKMedian.FiniteComparison.incoming_pointwise line 71
  7. def OAI.MetricKMedian.FiniteComparison.uprime line 116
  8. theorem OAI.MetricKMedian.FiniteComparison.uprime_mul line 119
  9. theorem OAI.MetricKMedian.FiniteComparison.uprime_decompose line 125
  10. theorem OAI.MetricKMedian.FiniteComparison.uprime_first line 134
  11. theorem OAI.MetricKMedian.FiniteComparison.row_le_uprime line 156
  12. theorem OAI.MetricKMedian.FiniteComparison.positive_uprime_le_radius line 169
  13. theorem OAI.MetricKMedian.FiniteComparison.row_le_excess line 198
  14. theorem OAI.MetricKMedian.FiniteComparison.uprime_charge_bound line 224
  15. theorem OAI.MetricKMedian.FiniteComparison.finite_charge line 256
  16. def OAI.MetricKMedian.FiniteComparison.rawRow line 325
  17. theorem OAI.MetricKMedian.FiniteComparison.rawRow_affine line 332
  18. theorem OAI.MetricKMedian.FiniteComparison.affine_le_max line 338
  19. theorem OAI.MetricKMedian.FiniteComparison.rawRow_mono_y line 344
  20. def OAI.MetricKMedian.FiniteComparison.endpoint line 363
  21. theorem OAI.MetricKMedian.FiniteComparison.rawRow_eq_rowValue line 365
  22. theorem OAI.MetricKMedian.FiniteComparison.finite_raw_of_scalar line 372