OAI/Computability/MeanPayoff/Budgets.lean

GitHub source file

69 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.MeanPayoff.Budgets line 8
  2. def OAI.MeanPayoff.AdmissibleSub line 18
  3. def OAI.MeanPayoff.AdmissibleSuper line 22
  4. def OAI.MeanPayoff.Budgets.density line 26
  5. def OAI.MeanPayoff.Budgets.totalDensity line 27
  6. def OAI.MeanPayoff.Budgets.parameter line 28
  7. def OAI.MeanPayoff.Budgets.measure line 29
  8. theorem OAI.MeanPayoff.Budgets.density_pos line 32
  9. theorem OAI.MeanPayoff.Budgets.totalDensity_pos line 35
  10. theorem OAI.MeanPayoff.Budgets.parameter_pos line 39
  11. theorem OAI.MeanPayoff.Budgets.measure_nonneg line 42
  12. theorem OAI.MeanPayoff.Budgets.measure_univ line 46
  13. theorem OAI.MeanPayoff.Budgets.measure_compl line 49
  14. def OAI.MeanPayoff.smallRankAnswer line 59
  15. theorem OAI.MeanPayoff.small_rank_comparisons line 62
  16. def OAI.MeanPayoff.halve line 101
  17. theorem OAI.MeanPayoff.halve_pos line 104
  18. theorem OAI.MeanPayoff.mass_halve line 111
  19. def OAI.MeanPayoff.Budgets.reduceK line 121
  20. def OAI.MeanPayoff.Budgets.reduceM line 123
  21. def OAI.MeanPayoff.Budgets.reweightK line 125
  22. def OAI.MeanPayoff.Budgets.reweightM line 131
  23. theorem OAI.MeanPayoff.Budgets.reduceK_parameter line 138
  24. theorem OAI.MeanPayoff.Budgets.reduceM_parameter line 143
  25. theorem OAI.MeanPayoff.density_reweightK line 148
  26. theorem OAI.MeanPayoff.density_reweightM line 153
  27. theorem OAI.MeanPayoff.reweight_admissible_sub line 158
  28. theorem OAI.MeanPayoff.reweight_admissible_super line 168
  29. theorem OAI.MeanPayoff.Budgets.reweightK_totalDensity line 178
  30. theorem OAI.MeanPayoff.Budgets.reweightM_totalDensity line 184
  31. theorem OAI.MeanPayoff.Budgets.reweightK_contraction line 190
  32. theorem OAI.MeanPayoff.Budgets.reweightM_contraction line 200
  33. theorem OAI.MeanPayoff.parameter_rank_exists line 210
  34. def OAI.MeanPayoff.parameterRank line 217
  35. theorem OAI.MeanPayoff.parameterRank_spec line 219
  36. theorem OAI.MeanPayoff.parameterRank_zero_iff line 222
  37. theorem OAI.MeanPayoff.parameterRank_decreases line 226
  38. inductive OAI.MeanPayoff.RandomTree line 243
  39. def OAI.MeanPayoff.RandomTree.bind line 249
  40. def OAI.MeanPayoff.RandomTree.map line 253
  41. def OAI.MeanPayoff.RandomTree.expect line 256
  42. def OAI.MeanPayoff.RandomTree.All line 260
  43. theorem OAI.MeanPayoff.RandomTree.expect_leaf line 264
  44. theorem OAI.MeanPayoff.RandomTree.expect_coin line 266
  45. theorem OAI.MeanPayoff.RandomTree.expect_bind line 269
  46. theorem OAI.MeanPayoff.RandomTree.expect_map line 276
  47. theorem OAI.MeanPayoff.RandomTree.expect_const line 280
  48. theorem OAI.MeanPayoff.RandomTree.expect_add line 286
  49. theorem OAI.MeanPayoff.RandomTree.expect_mul line 292
  50. theorem OAI.MeanPayoff.RandomTree.expect_mono_all line 298
  51. theorem OAI.MeanPayoff.RandomTree.all_of_forall line 308
  52. theorem OAI.MeanPayoff.RandomTree.expect_mono line 314
  53. theorem OAI.MeanPayoff.RandomTree.expect_nonneg line 318
  54. theorem OAI.MeanPayoff.RandomTree.all_bind line 322
  55. theorem OAI.MeanPayoff.RandomTree.all_mono line 329
  56. def OAI.MeanPayoff.RandomTree.probability line 335
  57. theorem OAI.MeanPayoff.RandomTree.probability_nonneg line 339
  58. theorem OAI.MeanPayoff.RandomTree.probability_le_one line 344
  59. theorem OAI.MeanPayoff.RandomTree.probability_mono line 351
  60. theorem OAI.MeanPayoff.RandomTree.probability_compl line 358
  61. theorem OAI.MeanPayoff.RandomTree.qualified_bind_error line 370
  62. def OAI.MeanPayoff.RandomTree.badCount line 388
  63. def OAI.MeanPayoff.RandomTree.trials line 392
  64. theorem OAI.MeanPayoff.RandomTree.trials_length line 396
  65. def OAI.MeanPayoff.RandomTree.moment line 407
  66. theorem OAI.MeanPayoff.RandomTree.moment_cons line 410
  67. theorem OAI.MeanPayoff.RandomTree.failure_moment line 415
  68. theorem OAI.MeanPayoff.RandomTree.amplification_moment line 427
  69. theorem OAI.MeanPayoff.RandomTree.amplification line 449