OAI/Combinatorics/HadwigerCounterexample/ProjectionEnergy.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Projection Energy

  1. theorem OAI.HadwigerCounterexample.map_mass line 13
  2. theorem OAI.HadwigerCounterexample.map_nz line 16
  3. theorem OAI.HadwigerCounterexample.lsupp_witness line 19
  4. theorem OAI.HadwigerCounterexample.lsupp_hit line 30
  5. theorem OAI.HadwigerCounterexample.lsupp.map line 38
  6. theorem OAI.HadwigerCounterexample.map_nested line 45
  7. theorem OAI.HadwigerCounterexample.map_mix line 49
  8. theorem OAI.HadwigerCounterexample.map_resize line 53
  9. def OAI.HadwigerCounterexample.pour line 64
  10. theorem OAI.HadwigerCounterexample.map_pour line 68
  11. def OAI.HadwigerCounterexample.bucket line 78
  12. theorem OAI.HadwigerCounterexample.pour_nz line 81
  13. theorem OAI.HadwigerCounterexample.bucket_scale line 86
  14. theorem OAI.HadwigerCounterexample.bucket_law line 89
  15. theorem OAI.HadwigerCounterexample.lsupp_bucket line 96
  16. theorem OAI.HadwigerCounterexample.bucket_nested line 101
  17. theorem OAI.HadwigerCounterexample.bucket_mix line 109
  18. theorem OAI.HadwigerCounterexample.tension_stage line 115