OAI/Combinatorics/KMedian/Process/SourceBalance.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedian.SourceBalance.positive line 11
  2. def OAI.MetricKMedian.SourceBalance.negative line 12
  3. def OAI.MetricKMedian.SourceBalance.nonzero line 13
  4. def OAI.MetricKMedian.SourceBalance.amount line 14
  5. theorem OAI.MetricKMedian.SourceBalance.amount_nonneg line 16
  6. theorem OAI.MetricKMedian.SourceBalance.amount_eq_positive line 18
  7. theorem OAI.MetricKMedian.SourceBalance.amount_eq_negative line 26
  8. theorem OAI.MetricKMedian.SourceBalance.abs_sum line 47
  9. theorem OAI.MetricKMedian.SourceBalance.nonzero_card line 70
  10. theorem OAI.MetricKMedian.SourceBalance.nonzero_mass line 80
  11. theorem OAI.MetricKMedian.SourceBalance.grid_imbalance line 99
  12. theorem OAI.MetricKMedian.SourceBalance.heavy_card line 112