OAI/Combinatorics/KMedian/Analysis/NormalizedTransfer.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MetricKMedian.ScalarTransfer.reciprocal_quadratic line 10
  2. theorem OAI.MetricKMedian.ScalarTransfer.first_gap_identity line 18
  3. theorem OAI.MetricKMedian.ScalarTransfer.first_scalar line 27
  4. def OAI.MetricKMedian.ScalarTransfer.stdB line 81
  5. def OAI.MetricKMedian.ScalarTransfer.stdL line 82
  6. def OAI.MetricKMedian.ScalarTransfer.stdM line 84
  7. def OAI.MetricKMedian.ScalarTransfer.stdK line 86
  8. theorem OAI.MetricKMedian.ScalarTransfer.Q0_difference line 89
  9. theorem OAI.MetricKMedian.ScalarTransfer.Q0_minimum line 94
  10. theorem OAI.MetricKMedian.ScalarTransfer.linear_gap_identity line 111
  11. theorem OAI.MetricKMedian.ScalarTransfer.linear_scalar line 117
  12. theorem OAI.MetricKMedian.ScalarTransfer.Y_le_base line 129
  13. theorem OAI.MetricKMedian.ScalarTransfer.Yprime_le_base line 136