OAI/Combinatorics/HadwigerCounterexample/PhaseParameters.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

Phase Parameters

  1. def OAI.HadwigerCounterexample.mstep line 14
  2. def OAI.HadwigerCounterexample.Bstep line 15
  3. def OAI.HadwigerCounterexample.denomStep line 16
  4. theorem OAI.HadwigerCounterexample.Bstep_pos line 17
  5. theorem OAI.HadwigerCounterexample.denom_pos line 18
  6. def OAI.HadwigerCounterexample.stage line 20
  7. def OAI.HadwigerCounterexample.pcoef line 21
  8. def OAI.HadwigerCounterexample.tinyPhase line 23
  9. def OAI.HadwigerCounterexample.warn line 24
  10. def OAI.HadwigerCounterexample.coin line 25
  11. def OAI.HadwigerCounterexample.heatloss line 26
  12. theorem OAI.HadwigerCounterexample.row_le line 28
  13. theorem OAI.HadwigerCounterexample.tinyPhase_pos line 34
  14. theorem OAI.HadwigerCounterexample.tinyPhase_le line 36
  15. theorem OAI.HadwigerCounterexample.heatloss_pos line 42
  16. theorem OAI.HadwigerCounterexample.bp_nat_vanish line 44
  17. theorem OAI.HadwigerCounterexample.eventually_grid line 48
  18. theorem OAI.HadwigerCounterexample.absorb_pow line 55
  19. theorem OAI.HadwigerCounterexample.limit_pow line 81
  20. theorem OAI.HadwigerCounterexample.span_stage line 113
  21. theorem OAI.HadwigerCounterexample.atlas_stage line 126
  22. theorem OAI.HadwigerCounterexample.price_bound line 149
  23. theorem OAI.HadwigerCounterexample.early_spend line 178
  24. theorem OAI.HadwigerCounterexample.glimpses_stage line 183
  25. theorem OAI.HadwigerCounterexample.phase_calendar line 203