OAI/Computability/MeanPayoff/FiniteIteration.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MeanPayoff.TreeDevice.Certified.Array.choose line 11
  2. def OAI.MeanPayoff.TreeDevice.Certified.Array.replicate line 14
  3. def OAI.MeanPayoff.TreeDevice.Certified.Array.anyLE line 15
  4. def OAI.MeanPayoff.TreeDevice.Certified.Array.anyGE line 16
  5. theorem OAI.MeanPayoff.TreeDevice.Certified.Array.map_rep line 18
  6. theorem OAI.MeanPayoff.TreeDevice.Certified.Array.scale_rep line 26
  7. theorem OAI.MeanPayoff.TreeDevice.Certified.Array.translate_rep line 33
  8. theorem OAI.MeanPayoff.TreeDevice.Certified.Array.choose_rep line 40
  9. theorem OAI.MeanPayoff.TreeDevice.Certified.Array.lt_rep line 56
  10. theorem OAI.MeanPayoff.TreeDevice.Certified.Array.le_rep line 64
  11. theorem OAI.MeanPayoff.TreeDevice.Certified.Array.complement_rep line 73
  12. theorem OAI.MeanPayoff.TreeDevice.Certified.Array.repeat_rep line 78
  13. theorem OAI.MeanPayoff.TreeDevice.Certified.Array.anyLE_eq line 83
  14. theorem OAI.MeanPayoff.TreeDevice.Certified.Array.anyGE_eq line 88
  15. theorem OAI.MeanPayoff.TreeDevice.Certified.RawBudget.smallMask_eq line 95
  16. abbrev OAI.MeanPayoff.TreeDevice.Certified.RawBox.Data line 122
  17. def OAI.MeanPayoff.TreeDevice.Certified.RawBox.width line 123
  18. def OAI.MeanPayoff.TreeDevice.Certified.RawBox.lower line 124
  19. def OAI.MeanPayoff.TreeDevice.Certified.RawBox.upper line 125
  20. def OAI.MeanPayoff.TreeDevice.Certified.RawBox.withFloor line 126
  21. def OAI.MeanPayoff.TreeDevice.Certified.RawBox.withCeiling line 128
  22. def OAI.MeanPayoff.TreeDevice.Certified.RawBox.clip line 130
  23. def OAI.MeanPayoff.TreeDevice.Certified.RawBox.midpoint line 132
  24. def OAI.MeanPayoff.TreeDevice.Certified.RawBox.averageClipped line 133
  25. def OAI.MeanPayoff.TreeDevice.Certified.RawBox.centered line 135
  26. def OAI.MeanPayoff.TreeDevice.Certified.RawBox.capLow line 138
  27. def OAI.MeanPayoff.TreeDevice.Certified.RawBox.capHigh line 141
  28. def OAI.MeanPayoff.TreeDevice.Certified.RawBox.smallVector line 144
  29. def OAI.MeanPayoff.TreeDevice.Certified.RawBox.dividedWidth line 146
  30. def OAI.MeanPayoff.TreeDevice.Certified.RawBox.remainderWidth line 147
  31. def OAI.MeanPayoff.TreeDevice.Certified.RawBox.movedFloor line 149
  32. def OAI.MeanPayoff.TreeDevice.Certified.RawBox.movedCeiling line 151
  33. structure OAI.MeanPayoff.TreeDevice.Certified.RawBox.Rep line 154
  34. theorem OAI.MeanPayoff.TreeDevice.Certified.RawBox.floor_rep line 159
  35. theorem OAI.MeanPayoff.TreeDevice.Certified.RawBox.ceiling_rep line 162
  36. theorem OAI.MeanPayoff.TreeDevice.Certified.RawBox.clip_rep line 166
  37. theorem OAI.MeanPayoff.TreeDevice.Certified.RawBox.midpoint_rep line 172
  38. theorem OAI.MeanPayoff.TreeDevice.Certified.RawBox.average_rep line 176
  39. theorem OAI.MeanPayoff.TreeDevice.Certified.RawBox.centered_rep line 182
  40. theorem OAI.MeanPayoff.TreeDevice.Certified.RawBox.capLow_rep line 195
  41. theorem OAI.MeanPayoff.TreeDevice.Certified.RawBox.capHigh_rep line 204
  42. theorem OAI.MeanPayoff.TreeDevice.Certified.RawBox.smallVector_rep line 213
  43. theorem OAI.MeanPayoff.TreeDevice.Certified.RawBox.dividedWidth_eq line 220
  44. theorem OAI.MeanPayoff.TreeDevice.Certified.RawBox.dividedWidth_nat line 224
  45. theorem OAI.MeanPayoff.TreeDevice.Certified.RawBox.remainderWidth_nat line 231
  46. theorem OAI.MeanPayoff.TreeDevice.Certified.RawBox.movedFloor_eq line 237
  47. theorem OAI.MeanPayoff.TreeDevice.Certified.RawBox.movedCeiling_eq line 241
  48. theorem OAI.MeanPayoff.box_iterate_fixed line 253
  49. theorem OAI.MeanPayoff.SolveBox.volume_bound line 274
  50. theorem OAI.MeanPayoff.SolveBox.iterate_exact line 283