OAI/Combinatorics/KMedian/Analysis/ScalarTransfer.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedian.ScalarTransfer.bit line 9
  2. def OAI.MetricKMedian.ScalarTransfer.d line 10
  3. def OAI.MetricKMedian.ScalarTransfer.hh line 11
  4. def OAI.MetricKMedian.ScalarTransfer.uZero line 12
  5. def OAI.MetricKMedian.ScalarTransfer.uOne line 13
  6. def OAI.MetricKMedian.ScalarTransfer.c line 14
  7. def OAI.MetricKMedian.ScalarTransfer.N line 15
  8. def OAI.MetricKMedian.ScalarTransfer.ell line 16
  9. def OAI.MetricKMedian.ScalarTransfer.T1 line 17
  10. def OAI.MetricKMedian.ScalarTransfer.T2 line 19
  11. def OAI.MetricKMedian.ScalarTransfer.Q0 line 21
  12. def OAI.MetricKMedian.ScalarTransfer.Q1 line 23
  13. def OAI.MetricKMedian.ScalarTransfer.Y line 25
  14. def OAI.MetricKMedian.ScalarTransfer.Yprime line 27
  15. theorem OAI.MetricKMedian.ScalarTransfer.mul_abs_bound line 30
  16. theorem OAI.MetricKMedian.ScalarTransfer.add_product_abs_bound line 35
  17. theorem OAI.MetricKMedian.ScalarTransfer.T1_error line 43
  18. theorem OAI.MetricKMedian.ScalarTransfer.T2_error line 61
  19. theorem OAI.MetricKMedian.ScalarTransfer.Q0_error line 80
  20. theorem OAI.MetricKMedian.ScalarTransfer.Q1_error line 97
  21. theorem OAI.MetricKMedian.ScalarTransfer.Y_error line 116
  22. theorem OAI.MetricKMedian.ScalarTransfer.Yprime_error line 129