OAI/Computability/Scheduling/PolynomialLoops.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.ThreeMachine.StackCompiler.Poly.Pool line 14
  2. theorem OAI.ThreeMachine.StackCompiler.Poly.reparam line 16
  3. theorem OAI.ThreeMachine.StackCompiler.Poly.powerBase line 25
  4. theorem OAI.ThreeMachine.StackCompiler.Poly.volumeMap line 29
  5. theorem OAI.ThreeMachine.StackCompiler.Poly.mapTime line 42
  6. theorem OAI.ThreeMachine.StackCompiler.Poly.filterTime line 58
  7. theorem OAI.ThreeMachine.StackCompiler.Poly.anyTime line 71
  8. theorem OAI.ThreeMachine.StackCompiler.Poly.allTime line 84
  9. theorem OAI.ThreeMachine.StackCompiler.Poly.volumeFinRange line 103
  10. theorem OAI.ThreeMachine.StackCompiler.Poly.finVal line 108
  11. theorem OAI.ThreeMachine.StackCompiler.Poly.finsetCard line 111
  12. theorem OAI.ThreeMachine.StackCompiler.Poly.lengthVolume line 118
  13. theorem OAI.ThreeMachine.StackCompiler.Poly.volumePool line 122
  14. theorem OAI.ThreeMachine.StackCompiler.Poly.volumeMapSimple line 127
  15. theorem OAI.ThreeMachine.StackCompiler.Poly.volumeFilter line 140
  16. theorem OAI.ThreeMachine.StackCompiler.Poly.lengthFinRange line 150
  17. theorem OAI.ThreeMachine.StackCompiler.Poly.lengthSort line 153
  18. theorem OAI.ThreeMachine.StackCompiler.Poly.lengthOfFn line 157
  19. theorem OAI.ThreeMachine.StackCompiler.Poly.timeReparam line 163
  20. def OAI.ThreeMachine.StackCompiler.Poly.FinPool line 173
  21. theorem OAI.ThreeMachine.StackCompiler.Poly.volumeFunction line 175
  22. theorem OAI.ThreeMachine.StackCompiler.Poly.iteNat line 185
  23. theorem OAI.ThreeMachine.StackCompiler.Poly.natFunctionApply line 189
  24. theorem OAI.ThreeMachine.StackCompiler.Poly.volumeFilterMap line 200
  25. theorem OAI.ThreeMachine.StackCompiler.Poly.filterMapTime line 216
  26. theorem OAI.ThreeMachine.StackCompiler.Poly.firstResultTime line 234
  27. theorem OAI.ThreeMachine.StackCompiler.Poly.lengthMap line 256
  28. theorem OAI.ThreeMachine.StackCompiler.Poly.lengthProduct line 261
  29. theorem OAI.ThreeMachine.StackCompiler.Poly.lengthFilter line 269
  30. abbrev OAI.ThreeMachine.StackCompiler.Poly.ListPool line 277
  31. theorem OAI.ThreeMachine.StackCompiler.Poly.listVolume line 278