OAI/Probability/RadialTransition/PackingLimit.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RadialTransition.IsPacking line 12
  2. theorem OAI.RadialTransition.dist_lt_one_of_coordinate_half line 15
  3. theorem OAI.RadialTransition.packing_card_bound line 29
  4. theorem OAI.RadialTransition.packing_card_set_bddAbove line 57
  5. theorem OAI.RadialTransition.packingNumber_attained line 63
  6. theorem OAI.RadialTransition.packing_card_le line 68
  7. theorem OAI.RadialTransition.packingNumber_bound line 72
  8. theorem OAI.RadialTransition.packingNumber_pos line 77
  9. def OAI.RadialTransition.packingTranslate line 92
  10. theorem OAI.RadialTransition.packingTranslate_apply line 95
  11. theorem OAI.RadialTransition.packingTranslate_mem_cube line 98
  12. theorem OAI.RadialTransition.packingTranslate_dist_same line 111
  13. theorem OAI.RadialTransition.packingTranslate_separated line 119
  14. theorem OAI.RadialTransition.packingNumber_replication line 143
  15. def OAI.RadialTransition.packingDensity line 180
  16. theorem OAI.RadialTransition.packing_ratio_bound line 183
  17. theorem OAI.RadialTransition.packing_ratios_bdd line 194
  18. theorem OAI.RadialTransition.packing_ratios_nonempty line 200
  19. theorem OAI.RadialTransition.packing_ratio_le_density line 204
  20. theorem OAI.RadialTransition.packingDensity_pos line 208
  21. theorem OAI.RadialTransition.packing_lower_approximation line 214
  22. theorem OAI.RadialTransition.packing_lower_approximation_le line 221
  23. theorem OAI.RadialTransition.packing_upper_approximation_le line 234
  24. theorem OAI.RadialTransition.packingDensity_limit line 244