OAI/Computability/MeanPayoff/BitDepth.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MeanPayoff.RandomTree.bitDepth line 11
  2. def OAI.MeanPayoff.RandomTree.read line 15
  3. def OAI.MeanPayoff.RandomTree.readPrefix line 20
  4. theorem OAI.MeanPayoff.RandomTree.padBits_cons_zero line 23
  5. theorem OAI.MeanPayoff.RandomTree.padBits_cons_succ line 26
  6. theorem OAI.MeanPayoff.RandomTree.readPrefix_leaf line 33
  7. theorem OAI.MeanPayoff.RandomTree.readPrefix_coin_cons line 36
  8. theorem OAI.MeanPayoff.RandomTree.prefix_sum line 42
  9. theorem OAI.MeanPayoff.RandomTree.prefix_probability line 66
  10. theorem OAI.MeanPayoff.RandomTree.game_prefix_success line 74
  11. def OAI.MeanPayoff.rootInvocationBound line 92
  12. theorem OAI.MeanPayoff.rootInvocationBound_nat line 95
  13. theorem OAI.MeanPayoff.clog_real_le_twice_logb line 125
  14. theorem OAI.MeanPayoff.rootInvocationBound_real line 138
  15. inductive OAI.MeanPayoff.RandomTree.Path line 157
  16. theorem OAI.MeanPayoff.RandomTree.Path.all line 162
  17. theorem OAI.MeanPayoff.RandomTree.Path.depth_le line 169
  18. theorem OAI.MeanPayoff.RandomTree.depth_attained line 176
  19. theorem OAI.MeanPayoff.RandomTree.path_bind_iff line 186
  20. theorem OAI.MeanPayoff.RandomTree.path_map_iff line 217
  21. theorem OAI.MeanPayoff.RandomTree.bitDepth_map line 227
  22. theorem OAI.MeanPayoff.RandomTree.bitDepth_uniformBelow line 233
  23. def OAI.MeanPayoff.Counted.Resource line 242
  24. theorem OAI.MeanPayoff.Counted.resource_pure line 245
  25. theorem OAI.MeanPayoff.Counted.resource_mono line 250
  26. theorem OAI.MeanPayoff.Counted.resource_map line 255
  27. theorem OAI.MeanPayoff.Counted.resource_bind line 261
  28. theorem OAI.MeanPayoff.Counted.resource_lift line 272
  29. theorem OAI.MeanPayoff.Counted.resource_charge line 278
  30. theorem OAI.MeanPayoff.Counted.resource_trials line 287
  31. theorem OAI.MeanPayoff.Counted.resource_traverse line 295
  32. theorem OAI.MeanPayoff.Counted.depth_le line 301