OAI/Combinatorics/HadwigerCounterexample/RefinementEnergy.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Refinement Energy

  1. theorem OAI.HadwigerCounterexample.var_nonneg line 13
  2. theorem OAI.HadwigerCounterexample.var_tri line 14
  3. theorem OAI.HadwigerCounterexample.var_pr line 18
  4. theorem OAI.HadwigerCounterexample.var_event line 27
  5. theorem OAI.HadwigerCounterexample.var_mix line 41
  6. theorem OAI.HadwigerCounterexample.bucket_m line 48
  7. theorem OAI.HadwigerCounterexample.tariffs_monotone line 56
  8. theorem OAI.HadwigerCounterexample.budget_nonneg line 60
  9. theorem OAI.HadwigerCounterexample.budget_progress line 68