OAI/Combinatorics/KMedianRecovery/Recovery/Blocks.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BlueSubsetDP.blocks line 10
  2. lemma OAI.BlueSubsetDP.mem_blocks line 12
  3. inductive OAI.BlueSubsetDP.Partition line 15
  4. lemma OAI.BlueSubsetDP.Partition.subset line 21
  5. lemma OAI.BlueSubsetDP.Partition.nonempty line 31
  6. lemma OAI.BlueSubsetDP.Partition.pairwise line 41
  7. lemma OAI.BlueSubsetDP.Partition.union line 52
  8. lemma OAI.BlueSubsetDP.Partition.length_le line 60
  9. def OAI.BlueSubsetDP.value line 70
  10. lemma OAI.BlueSubsetDP.value_zero line 74
  11. lemma OAI.BlueSubsetDP.value_le_partition line 77
  12. lemma OAI.BlueSubsetDP.value_attained line 86
  13. lemma OAI.BlueSubsetDP.value_le_iff_partition line 113
  14. def OAI.BlueSubsetDP.best line 124
  15. lemma OAI.BlueSubsetDP.best_attained line 127
  16. lemma OAI.BlueSubsetDP.best_le_partition line 142
  17. def OAI.BlueSubsetDP.blockCost line 161
  18. lemma OAI.BlueSubsetDP.blockCost_le line 166
  19. lemma OAI.BlueSubsetDP.blockCost_attained line 178
  20. lemma OAI.BlueSubsetDP.Partition.cost_sum line 208
  21. lemma OAI.BlueSubsetDP.partition_by_destination line 217
  22. lemma OAI.BlueSubsetDP.best_le_routing line 249
  23. lemma OAI.BlueSubsetDP.partition_routing line 272
  24. lemma OAI.BlueSubsetDP.best_routing line 323
  25. lemma OAI.BlueSubsetDP.layer_transition_bound line 339
  26. lemma OAI.BlueSubsetDP.all_layers_transition_bound line 350