OAI/Computability/RandomMean/SizeBounds.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MeanPayoff.TreeDevice.Certified.Size.randomBool line 10
  2. theorem OAI.MeanPayoff.TreeDevice.Certified.Size.mask line 11
  3. theorem OAI.MeanPayoff.TreeDevice.Certified.Size.digits line 14
  4. theorem OAI.MeanPayoff.TreeDevice.Certified.Array.randomSmallOfSize line 17
  5. theorem OAI.MeanPayoff.TreeDevice.Certified.Array.Small.randomSize line 19
  6. theorem OAI.MeanPayoff.TreeDevice.Certified.RawBudget.small_of_size line 23
  7. theorem OAI.MeanPayoff.TreeDevice.Certified.RawBox.small_of_size line 33
  8. theorem OAI.MeanPayoff.TreeDevice.Certified.RawOrientation.small_of_size line 39
  9. theorem OAI.MeanPayoff.TreeDevice.Certified.RawOrientation.listMass_size line 42
  10. theorem OAI.MeanPayoff.TreeDevice.Certified.RawOrientation.small_size line 52
  11. theorem OAI.MeanPayoff.TreeDevice.Certified.RawOrientation.many_size line 59
  12. theorem OAI.MeanPayoff.TreeDevice.Certified.RawControl.Pack.fields_size line 78
  13. theorem OAI.MeanPayoff.TreeDevice.Certified.RawControl.Pack.small_of_size line 98
  14. theorem OAI.MeanPayoff.TreeDevice.Certified.RawControl.Pack.mass_size line 105
  15. theorem OAI.MeanPayoff.TreeDevice.Certified.RawControl.Pack.small_size line 112
  16. def OAI.MeanPayoff.TreeDevice.Certified.RawControl.StackTags line 170
  17. def OAI.MeanPayoff.TreeDevice.Certified.RawControl.StateTags line 171
  18. theorem OAI.MeanPayoff.TreeDevice.Certified.RawControl.stackTags_nil line 172
  19. theorem OAI.MeanPayoff.TreeDevice.Certified.RawControl.stackTags_cons line 173
  20. theorem OAI.MeanPayoff.TreeDevice.Certified.RawControl.StackTags.tail line 174
  21. theorem OAI.MeanPayoff.TreeDevice.Certified.RawControl.JobLabel.tags line 175
  22. theorem OAI.MeanPayoff.TreeDevice.Certified.RawControl.FrameLabel.tags line 182
  23. theorem OAI.MeanPayoff.TreeDevice.Certified.RawControl.dispatch_tags line 191
  24. theorem OAI.MeanPayoff.TreeDevice.Certified.Size.cons line 208
  25. theorem OAI.MeanPayoff.TreeDevice.Certified.RawControl.stackMass_mem line 212
  26. theorem OAI.MeanPayoff.TreeDevice.Certified.RawControl.stackMass_size line 220
  27. theorem OAI.MeanPayoff.TreeDevice.Certified.RawControl.stateMass_size line 228
  28. theorem OAI.MeanPayoff.TreeDevice.Certified.RawControl.stateSmall_of_size line 234
  29. theorem OAI.MeanPayoff.TreeDevice.Certified.RawControl.stateTags_of_size line 237
  30. theorem OAI.MeanPayoff.TreeDevice.Certified.RawControl.StateTags.mono line 240
  31. theorem OAI.MeanPayoff.TreeDevice.Certified.RawControl.state_small_size line 242