OAI/Computability/MeanPayoff/SizeBounds.lean

GitHub source file

70 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MeanPayoff.TreeDevice.Certified.Word.sub_length line 10
  2. theorem OAI.MeanPayoff.TreeDevice.Certified.Word.average_length line 13
  3. theorem OAI.MeanPayoff.TreeDevice.Certified.Word.unsignedMul_length line 16
  4. theorem OAI.MeanPayoff.TreeDevice.Certified.Word.mul_length line 20
  5. theorem OAI.MeanPayoff.TreeDevice.Certified.Word.shiftRight_length line 29
  6. theorem OAI.MeanPayoff.TreeDevice.Certified.Array.Bounded.mono line 39
  7. theorem OAI.MeanPayoff.TreeDevice.Certified.Array.Bounded.nil line 41
  8. theorem OAI.MeanPayoff.TreeDevice.Certified.Array.Bounded.cons line 42
  9. theorem OAI.MeanPayoff.TreeDevice.Certified.Array.bounded_zip_general line 46
  10. theorem OAI.MeanPayoff.TreeDevice.Certified.Array.add_bound line 60
  11. theorem OAI.MeanPayoff.TreeDevice.Certified.Array.sub_bound line 62
  12. theorem OAI.MeanPayoff.TreeDevice.Certified.Array.average_bound line 64
  13. theorem OAI.MeanPayoff.TreeDevice.Certified.Array.min_bound line 66
  14. theorem OAI.MeanPayoff.TreeDevice.Certified.Array.max_bound line 68
  15. theorem OAI.MeanPayoff.TreeDevice.Certified.Array.translate_bound line 70
  16. theorem OAI.MeanPayoff.TreeDevice.Certified.Array.Bounded.headD line 77
  17. theorem OAI.MeanPayoff.TreeDevice.Certified.Array.Bounded.getD line 81
  18. structure OAI.MeanPayoff.TreeDevice.Certified.Array.Small line 95
  19. theorem OAI.MeanPayoff.TreeDevice.Certified.Array.Small.mono line 98
  20. theorem OAI.MeanPayoff.TreeDevice.Certified.Array.Small.nil line 99
  21. theorem OAI.MeanPayoff.TreeDevice.Certified.Array.Small.zip line 100
  22. theorem OAI.MeanPayoff.TreeDevice.Certified.Array.Small.min line 103
  23. theorem OAI.MeanPayoff.TreeDevice.Certified.Array.Small.max line 104
  24. theorem OAI.MeanPayoff.TreeDevice.Certified.Array.Small.average line 105
  25. theorem OAI.MeanPayoff.TreeDevice.Certified.Array.Small.translate line 107
  26. theorem OAI.MeanPayoff.TreeDevice.Certified.Array.Small.getD line 109
  27. theorem OAI.MeanPayoff.TreeDevice.Certified.Array.Small.doubleOn line 116
  28. structure OAI.MeanPayoff.TreeDevice.Certified.RawBudget.Small line 140
  29. theorem OAI.MeanPayoff.TreeDevice.Certified.RawBudget.Small.mono line 147
  30. theorem OAI.MeanPayoff.TreeDevice.Certified.RawBudget.times_length line 149
  31. theorem OAI.MeanPayoff.TreeDevice.Certified.RawBudget.encodedWord_length_nonneg line 150
  32. theorem OAI.MeanPayoff.TreeDevice.Certified.RawBudget.constant_short line 155
  33. theorem OAI.MeanPayoff.TreeDevice.Certified.RawBudget.times_short line 157
  34. theorem OAI.MeanPayoff.TreeDevice.Certified.RawBudget.Small.reduceK line 159
  35. theorem OAI.MeanPayoff.TreeDevice.Certified.RawBudget.Small.reduceM line 161
  36. theorem OAI.MeanPayoff.TreeDevice.Certified.RawBudget.Small.reweightK line 163
  37. theorem OAI.MeanPayoff.TreeDevice.Certified.RawBudget.Small.reweightM line 165
  38. structure OAI.MeanPayoff.TreeDevice.Certified.RawBox.Small line 169
  39. theorem OAI.MeanPayoff.TreeDevice.Certified.RawBox.Small.mono line 173
  40. theorem OAI.MeanPayoff.TreeDevice.Certified.RawBox.Small.midpoint line 174
  41. theorem OAI.MeanPayoff.TreeDevice.Certified.RawBox.Small.withFloor line 175
  42. theorem OAI.MeanPayoff.TreeDevice.Certified.RawBox.Small.withCeiling line 176
  43. theorem OAI.MeanPayoff.TreeDevice.Certified.RawBox.Small.clip line 177
  44. theorem OAI.MeanPayoff.TreeDevice.Certified.RawBox.Small.averageClipped line 178
  45. theorem OAI.MeanPayoff.TreeDevice.Certified.RawBox.centered_small line 179
  46. theorem OAI.MeanPayoff.TreeDevice.Certified.RawBox.Small.capLow line 185
  47. theorem OAI.MeanPayoff.TreeDevice.Certified.RawBox.Small.capHigh line 187
  48. theorem OAI.MeanPayoff.TreeDevice.Certified.Array.choose_bound line 200
  49. theorem OAI.MeanPayoff.TreeDevice.Certified.Array.choose_small line 225
  50. structure OAI.MeanPayoff.TreeDevice.Certified.DetMass.Small line 231
  51. theorem OAI.MeanPayoff.TreeDevice.Certified.DetMass.Small.mono line 235
  52. theorem OAI.MeanPayoff.TreeDevice.Certified.DetMass.short line 238
  53. theorem OAI.MeanPayoff.TreeDevice.Certified.DetMass.times_bound line 243
  54. theorem OAI.MeanPayoff.TreeDevice.Certified.DetMass.scale_small line 250
  55. theorem OAI.MeanPayoff.TreeDevice.Certified.DetMass.reweight_small line 258
  56. structure OAI.MeanPayoff.TreeDevice.Certified.DetRaw.Small line 285
  57. theorem OAI.MeanPayoff.TreeDevice.Certified.DetRaw.Small.mono line 291
  58. theorem OAI.MeanPayoff.TreeDevice.Certified.DetRaw.piece_bound line 294
  59. theorem OAI.MeanPayoff.TreeDevice.Certified.DetRaw.amount_bound line 297
  60. theorem OAI.MeanPayoff.TreeDevice.Certified.DetRaw.center_small line 300
  61. theorem OAI.MeanPayoff.TreeDevice.Certified.DetRaw.child_small line 303
  62. theorem OAI.MeanPayoff.TreeDevice.Certified.DetRaw.provisional_small line 315
  63. theorem OAI.MeanPayoff.TreeDevice.Certified.DetRaw.continuation_small line 324
  64. theorem OAI.MeanPayoff.TreeDevice.Certified.DetRaw.minus_small line 330
  65. theorem OAI.MeanPayoff.TreeDevice.Certified.DetRaw.plus_small line 341
  66. theorem OAI.MeanPayoff.TreeDevice.Certified.DetRaw.down_small line 348
  67. theorem OAI.MeanPayoff.TreeDevice.Certified.DetRaw.up_small line 353
  68. theorem OAI.MeanPayoff.TreeDevice.Certified.DetRaw.baseLabels_length line 358
  69. theorem OAI.MeanPayoff.TreeDevice.Certified.DetRaw.basic_length line 361
  70. theorem OAI.MeanPayoff.TreeDevice.Certified.DetRaw.finish_length line 368