OAI/Computability/MeanPayoff/Allocation.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MeanPayoff.TreeDevice.Certified.Allocation.double line 15
  2. def OAI.MeanPayoff.TreeDevice.Certified.Allocation.init line 16
  3. def OAI.MeanPayoff.TreeDevice.Certified.Allocation.device line 17
  4. theorem OAI.MeanPayoff.TreeDevice.Certified.Allocation.fold_length line 20
  5. theorem OAI.MeanPayoff.TreeDevice.Certified.Allocation.exact line 28
  6. theorem OAI.MeanPayoff.TreeDevice.Certified.Allocation.fold_bound line 32
  7. def OAI.MeanPayoff.PolyBound line 75
  8. theorem OAI.MeanPayoff.PolyBound.mono line 79
  9. theorem OAI.MeanPayoff.PolyBound.base line 82
  10. theorem OAI.MeanPayoff.PolyBound.const line 83
  11. theorem OAI.MeanPayoff.PolyBound.add line 84
  12. theorem OAI.MeanPayoff.PolyBound.mul line 92
  13. theorem OAI.MeanPayoff.PolyBound.pow line 99
  14. theorem OAI.MeanPayoff.PolyBound.apply line 103
  15. theorem OAI.MeanPayoff.TreeDevice.polynomial_limit line 110
  16. theorem OAI.MeanPayoff.TreeDevice.polynomial_output line 115