OAI/Combinatorics/HadwigerCounterexample/OffsetEnergy.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Offset Energy

  1. def OAI.HadwigerCounterexample.unary line 14
  2. def OAI.HadwigerCounterexample.heat line 16
  3. def OAI.HadwigerCounterexample.thermal line 19
  4. def OAI.HadwigerCounterexample.sparks line 23
  5. def OAI.HadwigerCounterexample.glimpse line 27
  6. def OAI.HadwigerCounterexample.hfused line 31
  7. theorem OAI.HadwigerCounterexample.heat_flip line 35
  8. theorem OAI.HadwigerCounterexample.heat_unary line 40
  9. theorem OAI.HadwigerCounterexample.fuse_val line 47
  10. theorem OAI.HadwigerCounterexample.fused_support line 61
  11. theorem OAI.HadwigerCounterexample.fused_inj line 69
  12. theorem OAI.HadwigerCounterexample.hotfused line 83
  13. theorem OAI.HadwigerCounterexample.tone_heat line 90
  14. theorem OAI.HadwigerCounterexample.trace_shift_l line 101
  15. theorem OAI.HadwigerCounterexample.trace_shift_r line 110
  16. theorem OAI.HadwigerCounterexample.tone_offset line 116