OAI/Combinatorics/KMedianRecovery/Recovery/CommonL.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.IntegralAssembly.commonL line 10
  2. def OAI.MetricKMedianRecovery.IntegralAssembly.countBound line 13
  3. def OAI.MetricKMedianRecovery.IntegralAssembly.repetitions line 16
  4. theorem OAI.MetricKMedianRecovery.IntegralAssembly.uniform_finite_experiment line 19
  5. lemma OAI.MetricKMedianRecovery.IntegralAssembly.commonL_bound line 57
  6. lemma OAI.MetricKMedianRecovery.IntegralAssembly.countBound_bound line 80
  7. def OAI.MetricKMedianRecovery.Rounding.edge line 101
  8. lemma OAI.MetricKMedianRecovery.Rounding.edge_self line 104
  9. lemma OAI.MetricKMedianRecovery.Rounding.edge_symm line 105
  10. lemma OAI.MetricKMedianRecovery.Rounding.edge_le_cap line 107
  11. lemma OAI.MetricKMedianRecovery.Rounding.edge_pos line 112
  12. lemma OAI.MetricKMedianRecovery.Rounding.edge_triangle line 117
  13. def OAI.MetricKMedianRecovery.Rounding.metric line 134
  14. lemma OAI.MetricKMedianRecovery.Rounding.edge_upper line 146
  15. lemma OAI.MetricKMedianRecovery.Rounding.original_le_uncapped line 159
  16. def OAI.MetricKMedianRecovery.Rounding.connection line 171
  17. def OAI.MetricKMedianRecovery.Rounding.cost line 173
  18. def OAI.MetricKMedianRecovery.Rounding.nearest line 175
  19. lemma OAI.MetricKMedianRecovery.Rounding.nearest_mem line 177
  20. lemma OAI.MetricKMedianRecovery.Rounding.nearest_edge line 180
  21. lemma OAI.MetricKMedianRecovery.Rounding.connection_le line 186
  22. lemma OAI.MetricKMedianRecovery.Rounding.rounded_cost_upper line 191
  23. lemma OAI.MetricKMedianRecovery.Rounding.original_cost_le line 203