OAI/Combinatorics/KMedianRecovery/Refined/Endpoint.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

Comparison-cluster prices and the geometric data and stopping conditions of two-stage endpoints.

  1. def OAI.MetricKMedianRecovery.RefinedRecovery.Certificate.price line 14
  2. def OAI.MetricKMedianRecovery.RefinedRecovery.Certificate.group line 15
  3. def OAI.MetricKMedianRecovery.RefinedRecovery.Certificate.partCost line 17
  4. def OAI.MetricKMedianRecovery.RefinedRecovery.Certificate.mean line 19
  5. def OAI.MetricKMedianRecovery.RefinedRecovery.Certificate.near line 21
  6. def OAI.MetricKMedianRecovery.RefinedRecovery.Certificate.populationRadius line 23
  7. lemma OAI.MetricKMedianRecovery.RefinedRecovery.Certificate.partCost_nonneg line 27
  8. lemma OAI.MetricKMedianRecovery.RefinedRecovery.Certificate.partCost_sum line 30
  9. lemma OAI.MetricKMedianRecovery.RefinedRecovery.Certificate.mean_mul_card line 33
  10. lemma OAI.MetricKMedianRecovery.RefinedRecovery.Certificate.mean_nonneg line 41
  11. lemma OAI.MetricKMedianRecovery.RefinedRecovery.Certificate.partCost_subsum line 44
  12. lemma OAI.MetricKMedianRecovery.RefinedRecovery.Certificate.cluster_subsum line 49
  13. lemma OAI.MetricKMedianRecovery.RefinedRecovery.Certificate.partCost_empty line 62
  14. lemma OAI.MetricKMedianRecovery.RefinedRecovery.Certificate.populationRadius_nonneg line 68
  15. structure OAI.MetricKMedianRecovery.RefinedRecovery.EndpointData line 75
  16. def OAI.MetricKMedianRecovery.RefinedRecovery.EndpointData.final line 87
  17. def OAI.MetricKMedianRecovery.RefinedRecovery.EndpointData.covered line 88
  18. def OAI.MetricKMedianRecovery.RefinedRecovery.EndpointData.firstRemaining line 89
  19. def OAI.MetricKMedianRecovery.RefinedRecovery.EndpointData.remaining line 90
  20. def OAI.MetricKMedianRecovery.RefinedRecovery.EndpointData.firstReference line 91
  21. def OAI.MetricKMedianRecovery.RefinedRecovery.EndpointData.finalReference line 94
  22. def OAI.MetricKMedianRecovery.RefinedRecovery.EndpointData.firstInternal line 97
  23. def OAI.MetricKMedianRecovery.RefinedRecovery.EndpointData.finalInternal line 100
  24. def OAI.MetricKMedianRecovery.RefinedRecovery.EndpointData.large line 103
  25. def OAI.MetricKMedianRecovery.RefinedRecovery.EndpointData.small line 105
  26. def OAI.MetricKMedianRecovery.RefinedRecovery.EndpointData.firstMass line 106
  27. def OAI.MetricKMedianRecovery.RefinedRecovery.EndpointData.secondMass line 108
  28. def OAI.MetricKMedianRecovery.RefinedRecovery.EndpointData.fraction line 110
  29. def OAI.MetricKMedianRecovery.RefinedRecovery.EndpointData.baseCharge line 113
  30. def OAI.MetricKMedianRecovery.RefinedRecovery.EndpointData.internalCharge line 116
  31. def OAI.MetricKMedianRecovery.RefinedRecovery.EndpointData.clusterCharge line 122
  32. def OAI.MetricKMedianRecovery.RefinedRecovery.EndpointData.totalCharge line 125
  33. structure OAI.MetricKMedianRecovery.RefinedRecovery.EndpointConditions line 130