OAI/Combinatorics/HadwigerCounterexample/RelativeEntropy.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Relative Entropy

  1. def OAI.HadwigerCounterexample.lsupp line 14
  2. def OAI.HadwigerCounterexample.tension line 16
  3. def OAI.HadwigerCounterexample.varOne line 17
  4. theorem OAI.HadwigerCounterexample.tension_of_ratio line 19
  5. theorem OAI.HadwigerCounterexample.tension_as_diff line 23
  6. theorem OAI.HadwigerCounterexample.tension_mix line 26
  7. theorem OAI.HadwigerCounterexample.tension_le_cap line 36
  8. theorem OAI.HadwigerCounterexample.tension_cell line 52
  9. theorem OAI.HadwigerCounterexample.var_tension line 67
  10. theorem OAI.HadwigerCounterexample.tension_nonneg line 102