OAI/Computability/MeanPayoff/Sampling.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MeanPayoff.RandomTree.badCount_eq_countP line 11
  2. theorem OAI.MeanPayoff.RandomTree.badCount_perm line 17
  3. theorem OAI.MeanPayoff.RandomTree.badCount_sublist line 21
  4. theorem OAI.MeanPayoff.RandomTree.badCount_eq_length line 26
  5. theorem OAI.MeanPayoff.RandomTree.badCount_map_le line 31
  6. def OAI.MeanPayoff.medianInt line 40
  7. def OAI.MeanPayoff.median line 46
  8. theorem OAI.MeanPayoff.medianInt_mem line 49
  9. theorem OAI.MeanPayoff.median_inBox line 53
  10. theorem OAI.MeanPayoff.medianInt_lower_failure line 68
  11. theorem OAI.MeanPayoff.medianInt_upper_failure line 89
  12. theorem OAI.MeanPayoff.median_lower_failure line 109
  13. theorem OAI.MeanPayoff.median_upper_failure line 122
  14. theorem OAI.MeanPayoff.RandomTree.probability_map line 139
  15. theorem OAI.MeanPayoff.RandomTree.probability_mono_all line 144
  16. theorem OAI.MeanPayoff.RandomTree.probability_union line 152
  17. theorem OAI.MeanPayoff.RandomTree.probability_of_all_not line 161
  18. def OAI.MeanPayoff.RandomTree.ask line 169
  19. theorem OAI.MeanPayoff.RandomTree.ask_lower line 172
  20. theorem OAI.MeanPayoff.RandomTree.ask_upper line 183
  21. theorem OAI.MeanPayoff.RandomTree.trials_all line 194
  22. theorem OAI.MeanPayoff.RandomTree.all_and line 207
  23. theorem OAI.MeanPayoff.RandomTree.ask_inBox line 213
  24. def OAI.MeanPayoff.globalG line 223
  25. def OAI.MeanPayoff.sampleExponent line 224
  26. def OAI.MeanPayoff.globalS line 225
  27. def OAI.MeanPayoff.globalJ line 226
  28. theorem OAI.MeanPayoff.globalS_lower line 228
  29. theorem OAI.MeanPayoff.globalS_minimal line 231
  30. theorem OAI.MeanPayoff.globalS_large line 236
  31. theorem OAI.MeanPayoff.globalJ_positive line 242
  32. theorem OAI.MeanPayoff.globalJ_odd line 244
  33. structure OAI.MeanPayoff.SolveBox line 247
  34. abbrev OAI.MeanPayoff.BoxVector line 256
  35. def OAI.MeanPayoff.SolveBox.bottom line 260
  36. def OAI.MeanPayoff.SolveBox.top line 261
  37. def OAI.MeanPayoff.SolveBox.medianBox line 263
  38. def OAI.MeanPayoff.SolveBox.repeated line 271
  39. theorem OAI.MeanPayoff.SolveBox.repeated_lower line 274
  40. theorem OAI.MeanPayoff.SolveBox.repeated_upper line 291
  41. def OAI.MeanPayoff.SolveBox.withFloor line 308
  42. def OAI.MeanPayoff.SolveBox.withCeiling line 317
  43. def OAI.MeanPayoff.SolveBox.capLow line 326
  44. def OAI.MeanPayoff.SolveBox.capHigh line 339
  45. def OAI.MeanPayoff.SolveBox.centered line 352
  46. def OAI.MeanPayoff.SolveBox.exactVector line 364
  47. def OAI.MeanPayoff.SolveBox.smallVector line 367
  48. def OAI.MeanPayoff.SolveBox.midpoint line 377
  49. def OAI.MeanPayoff.SolveBox.averageClipped line 389
  50. def OAI.MeanPayoff.RandomTree.uniformBelow line 406
  51. theorem OAI.MeanPayoff.RandomTree.uniformBelow_lt line 410
  52. theorem OAI.MeanPayoff.RandomTree.expect_uniformBelow line 419