OAI/Combinatorics/KMedian/Process/HeavyActions.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MetricKMedian.FixedBatch.HeavyAction line 13
  2. instance OAI.MetricKMedian.FixedBatch.(instance at line 16) line 16
  3. instance OAI.MetricKMedian.FixedBatch.(instance at line 20) line 20
  4. def OAI.MetricKMedian.FixedBatch.heavyParent line 24
  5. def OAI.MetricKMedian.FixedBatch.heavyActions line 28
  6. theorem OAI.MetricKMedian.FixedBatch.ordinary_heavyActions line 35
  7. theorem OAI.MetricKMedian.FixedBatch.heavyParent_membership line 39
  8. theorem OAI.MetricKMedian.FixedBatch.same_parent_eraser line 45
  9. theorem OAI.MetricKMedian.FixedBatch.heavy_partition_disjoint line 66
  10. theorem OAI.MetricKMedian.FixedBatch.heavy_partition_union line 75
  11. theorem OAI.MetricKMedian.FixedBatch.heavy_nonheavy_fiber line 92
  12. theorem OAI.MetricKMedian.FixedBatch.heavy_charge_le line 109
  13. theorem OAI.MetricKMedian.FixedBatch.heavy_incoming_degree line 130
  14. theorem OAI.MetricKMedian.FixedBatch.heavy_ordinary_injective line 141