OAI/Combinatorics/KMedian/Analysis/ChargeTransfer.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedian.ChargeTransfer.bit line 9
  2. def OAI.MetricKMedian.ChargeTransfer.c line 10
  3. def OAI.MetricKMedian.ChargeTransfer.F1 line 11
  4. def OAI.MetricKMedian.ChargeTransfer.F2 line 13
  5. def OAI.MetricKMedian.ChargeTransfer.F3 line 15
  6. def OAI.MetricKMedian.ChargeTransfer.F4 line 17
  7. def OAI.MetricKMedian.ChargeTransfer.charge line 19
  8. theorem OAI.MetricKMedian.ChargeTransfer.mul_abs_bound line 22
  9. theorem OAI.MetricKMedian.ChargeTransfer.affine_abs_bound line 27
  10. theorem OAI.MetricKMedian.ChargeTransfer.convex_abs_bound line 36
  11. theorem OAI.MetricKMedian.ChargeTransfer.c_bounds line 46
  12. theorem OAI.MetricKMedian.ChargeTransfer.bit_mul_bounds line 53
  13. theorem OAI.MetricKMedian.ChargeTransfer.factor_bounds line 65
  14. theorem OAI.MetricKMedian.ChargeTransfer.factor_differences line 111
  15. theorem OAI.MetricKMedian.ChargeTransfer.product_difference_bound line 189
  16. theorem OAI.MetricKMedian.ChargeTransfer.charge_error line 195