OAI/Computability/MeanPayoff/InputSize.lean

GitHub source file

54 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MeanPayoff.encodeNat_length line 9
  2. theorem OAI.MeanPayoff.encodeInt_length line 14
  3. theorem OAI.MeanPayoff.input_n_le line 18
  4. theorem OAI.MeanPayoff.length_le_flatten line 22
  5. theorem OAI.MeanPayoff.input_weight_size_le line 34
  6. theorem OAI.MeanPayoff.input_weight_lt_pow line 45
  7. theorem OAI.MeanPayoff.input_weightBound_le line 51
  8. theorem OAI.MeanPayoff.width_growth_bound line 71
  9. theorem OAI.MeanPayoff.input_topWidth_le line 92
  10. theorem OAI.MeanPayoff.input_globalG_le line 105
  11. theorem OAI.MeanPayoff.globalS_upper line 116
  12. def OAI.MeanPayoff.inputScale line 130
  13. theorem OAI.MeanPayoff.inputScale_large line 132
  14. theorem OAI.MeanPayoff.inputScale_n line 134
  15. theorem OAI.MeanPayoff.inputScale_g line 139
  16. theorem OAI.MeanPayoff.inputScale_s line 144
  17. theorem OAI.MeanPayoff.inputScale_log line 150
  18. theorem OAI.MeanPayoff.globalJ_scale line 160
  19. theorem OAI.MeanPayoff.chainBound_scale line 174
  20. theorem OAI.MeanPayoff.globalListBound_scale line 183
  21. theorem OAI.MeanPayoff.auxiliaryCalls_scale line 190
  22. theorem OAI.MeanPayoff.callBase_scale line 218
  23. structure OAI.MeanPayoff.BudgetCode line 240
  24. def OAI.MeanPayoff.BudgetCode.depth line 250
  25. def OAI.MeanPayoff.BudgetCode.Good line 252
  26. def OAI.MeanPayoff.BudgetCode.zero line 254
  27. def OAI.MeanPayoff.BudgetCode.value line 256
  28. def OAI.MeanPayoff.BudgetCode.reduceK line 270
  29. def OAI.MeanPayoff.BudgetCode.reduceM line 271
  30. def OAI.MeanPayoff.BudgetCode.reweightK line 272
  31. def OAI.MeanPayoff.BudgetCode.reweightM line 274
  32. theorem OAI.MeanPayoff.BudgetCode.value_zero line 277
  33. theorem OAI.MeanPayoff.BudgetCode.value_reduceK line 281
  34. theorem OAI.MeanPayoff.BudgetCode.value_reduceM line 288
  35. theorem OAI.MeanPayoff.BudgetCode.value_reweightK line 295
  36. theorem OAI.MeanPayoff.BudgetCode.value_reweightM line 305
  37. theorem OAI.MeanPayoff.BudgetCode.depth_zero line 315
  38. theorem OAI.MeanPayoff.BudgetCode.depth_reduceK line 316
  39. theorem OAI.MeanPayoff.BudgetCode.depth_reduceM line 318
  40. theorem OAI.MeanPayoff.BudgetCode.depth_reweightK line 320
  41. theorem OAI.MeanPayoff.BudgetCode.depth_reweightM line 322
  42. theorem OAI.MeanPayoff.BudgetCode.good_zero line 325
  43. theorem OAI.MeanPayoff.BudgetCode.good_reduceK line 326
  44. theorem OAI.MeanPayoff.BudgetCode.good_reduceM line 327
  45. theorem OAI.MeanPayoff.BudgetCode.good_reweightK line 329
  46. theorem OAI.MeanPayoff.BudgetCode.good_reweightM line 336
  47. theorem OAI.MeanPayoff.BudgetCode.coordinate_depth line 343
  48. theorem OAI.MeanPayoff.BudgetCode.value_k_fraction line 349
  49. theorem OAI.MeanPayoff.BudgetCode.value_m_fraction line 354
  50. theorem OAI.MeanPayoff.BudgetCode.value_density line 359
  51. theorem OAI.MeanPayoff.BudgetCode.value_density_sum_bound line 364
  52. inductive OAI.MeanPayoff.ReachableBudget line 380
  53. theorem OAI.MeanPayoff.ReachableBudget.depth_rank line 391
  54. theorem OAI.MeanPayoff.ReachableBudget.presentation line 400