OAI/Combinatorics/HadwigerCounterexample/ProbePointMasses.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Probe Point Masses

  1. def OAI.HadwigerCounterexample.initCap line 13
  2. def OAI.HadwigerCounterexample.bySide line 16
  3. theorem OAI.HadwigerCounterexample.side_same line 20
  4. def OAI.HadwigerCounterexample.basisFrom line 39
  5. def OAI.HadwigerCounterexample.ctot line 43
  6. abbrev OAI.HadwigerCounterexample.Among line 44
  7. def OAI.HadwigerCounterexample.csignal line 46
  8. def OAI.HadwigerCounterexample.poke line 50
  9. theorem OAI.HadwigerCounterexample.poke_cap line 57
  10. def OAI.HadwigerCounterexample.heatRate line 97
  11. instance OAI.HadwigerCounterexample.amongFintype line 100
  12. theorem OAI.HadwigerCounterexample.format_size line 103
  13. theorem OAI.HadwigerCounterexample.heat_rate line 124
  14. theorem OAI.HadwigerCounterexample.heat_one line 176
  15. theorem OAI.HadwigerCounterexample.heat_none line 190