OAI/Combinatorics/KMedianRecovery/Branching/BlueDPValue.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BlueDP.merge line 9
  2. lemma OAI.MetricKMedianRecovery.BlueDP.value_merge line 12
  3. def OAI.MetricKMedianRecovery.BlueDP.collect line 19
  4. lemma OAI.MetricKMedianRecovery.BlueDP.value_collect line 20
  5. lemma OAI.MetricKMedianRecovery.BlueDP.collect_some line 24
  6. lemma OAI.MetricKMedianRecovery.BlueDP.list_min_inf line 43
  7. lemma OAI.MetricKMedianRecovery.BlueDP.select_finset line 48
  8. def OAI.MetricKMedianRecovery.BlueDP.enumBlocks line 54
  9. lemma OAI.MetricKMedianRecovery.BlueDP.enumBlocks_set line 56
  10. def OAI.MetricKMedianRecovery.BlueDP.recurrence line 70
  11. lemma OAI.MetricKMedianRecovery.BlueDP.recurrence_value line 73
  12. def OAI.MetricKMedianRecovery.BlueDP.best line 80
  13. lemma OAI.MetricKMedianRecovery.BlueDP.range_succ_set line 82
  14. lemma OAI.MetricKMedianRecovery.BlueDP.best_value line 88
  15. abbrev OAI.MetricKMedianRecovery.BlueDP.Atom line 101
  16. def OAI.MetricKMedianRecovery.BlueDP.item line 103
  17. def OAI.MetricKMedianRecovery.BlueDP.blockAt line 105
  18. def OAI.MetricKMedianRecovery.BlueDP.block line 107
  19. lemma OAI.MetricKMedianRecovery.BlueDP.item_value line 110
  20. lemma OAI.MetricKMedianRecovery.BlueDP.blockAt_value line 115
  21. lemma OAI.MetricKMedianRecovery.BlueDP.block_value line 120
  22. lemma OAI.MetricKMedianRecovery.BlueDP.optimizer_value line 124