OAI/Combinatorics/KMedianRecovery/Machines/FirstSize.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.RadiusMenus.firstSize line 7
  2. def OAI.MetricKMedianRecovery.RadiusMenus.thirdSize line 8
  3. def OAI.MetricKMedianRecovery.RadiusMenus.upwardIndex line 9
  4. def OAI.MetricKMedianRecovery.RadiusMenus.additiveRadius line 10
  5. lemma OAI.MetricKMedianRecovery.RadiusMenus.additiveRadius_pos line 12
  6. lemma OAI.MetricKMedianRecovery.RadiusMenus.upward_radius_bounds line 16
  7. lemma OAI.MetricKMedianRecovery.RadiusMenus.first_menu_available line 40
  8. lemma OAI.MetricKMedianRecovery.RadiusMenus.third_menu_available line 55
  9. lemma OAI.MetricKMedianRecovery.RadiusMenus.geometric_exists line 75
  10. def OAI.MetricKMedianRecovery.RadiusMenus.geometricCap line 79
  11. lemma OAI.MetricKMedianRecovery.RadiusMenus.geometricCap_spec line 82
  12. lemma OAI.MetricKMedianRecovery.RadiusMenus.geometric_menu_available line 85
  13. def OAI.MetricKMedianRecovery.RadiusMenus.thirdNormalizer line 109
  14. lemma OAI.MetricKMedianRecovery.RadiusMenus.thirdNormalizer_eq line 112
  15. lemma OAI.MetricKMedianRecovery.RadiusMenus.thirdNormalizer_pos line 120
  16. lemma OAI.MetricKMedianRecovery.RadiusMenus.thirdNormalizer_lt_one line 125
  17. def OAI.MetricKMedianRecovery.RadiusMenus.menuConstant line 130
  18. lemma OAI.MetricKMedianRecovery.RadiusMenus.menuConstant_pos line 134
  19. lemma OAI.MetricKMedianRecovery.RadiusMenus.menuConstant_le_one line 142
  20. lemma OAI.MetricKMedianRecovery.RadiusMenus.first_entry_lower line 145
  21. lemma OAI.MetricKMedianRecovery.RadiusMenus.second_entry_lower line 148
  22. lemma OAI.MetricKMedianRecovery.RadiusMenus.third_entry_lower line 152
  23. def OAI.MetricKMedianRecovery.RadiusMenus.menuWeight line 164
  24. lemma OAI.MetricKMedianRecovery.RadiusMenus.menuWeight_total line 169
  25. theorem OAI.MetricKMedianRecovery.RadiusMenus.menu_product_budget line 185