OAI/Combinatorics/KMedian/Process/PhysicalPotential.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedian.PhysicalPotential.mass line 12
  2. def OAI.MetricKMedian.PhysicalPotential.cost line 13
  3. def OAI.MetricKMedian.PhysicalPotential.potential line 15
  4. theorem OAI.MetricKMedian.PhysicalPotential.mass_nonneg line 20
  5. theorem OAI.MetricKMedian.PhysicalPotential.cost_nonneg line 23
  6. theorem OAI.MetricKMedian.PhysicalPotential.mass_mono line 27
  7. theorem OAI.MetricKMedian.PhysicalPotential.cost_mono line 32
  8. theorem OAI.MetricKMedian.PhysicalPotential.mass_sdiff line 36
  9. theorem OAI.MetricKMedian.PhysicalPotential.cost_sdiff line 42
  10. theorem OAI.MetricKMedian.PhysicalPotential.cost_ge_mass_mul line 46
  11. theorem OAI.MetricKMedian.PhysicalPotential.point_cost_le line 51
  12. theorem OAI.MetricKMedian.PhysicalPotential.B_nonneg line 55
  13. theorem OAI.MetricKMedian.PhysicalPotential.removal_identity line 57
  14. theorem OAI.MetricKMedian.PhysicalPotential.external_update_le line 66
  15. def OAI.MetricKMedian.PhysicalPotential.retained line 74
  16. theorem OAI.MetricKMedian.PhysicalPotential.retained_subset line 77
  17. theorem OAI.MetricKMedian.PhysicalPotential.retained_hinge_identity line 80
  18. theorem OAI.MetricKMedian.PhysicalPotential.internal_update_le line 99
  19. theorem OAI.MetricKMedian.PhysicalPotential.force_savings line 120
  20. theorem OAI.MetricKMedian.PhysicalPotential.force_cap_bound line 135
  21. def OAI.MetricKMedian.PhysicalPotential.savingsFraction line 144
  22. theorem OAI.MetricKMedian.PhysicalPotential.savingsFraction_pos line 147
  23. theorem OAI.MetricKMedian.PhysicalPotential.force_fraction line 152
  24. theorem OAI.MetricKMedian.PhysicalPotential.chunks_le_full line 188