OAI/Probability/FKMaps/TreeCode.lean

GitHub source file

125 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.FKCRT.TreeCoding.walk line 13
  2. def OAI.FKCRT.TreeCoding.IsTreeCode line 17
  3. abbrev OAI.FKCRT.TreeCoding.Code line 21
  4. instance OAI.FKCRT.TreeCoding.(instance at line 24) line 24
  5. def OAI.FKCRT.TreeCoding.height line 27
  6. def OAI.FKCRT.TreeCoding.jointCode line 32
  7. def OAI.FKCRT.TreeCoding.codeWeight line 37
  8. def OAI.FKCRT.TreeCoding.codePartition line 41
  9. def OAI.FKCRT.TreeCoding.codeExpectation line 45
  10. lemma OAI.FKCRT.TreeCoding.walk_zero line 50
  11. lemma OAI.FKCRT.TreeCoding.codeWeight_nonneg line 53
  12. lemma OAI.FKCRT.TreeCoding.codePartition_nonneg line 57
  13. lemma OAI.FKCRT.TreeCoding.height_terminal line 61
  14. lemma OAI.FKCRT.TreeCoding.walk_step line 71
  15. def OAI.FKCRT.TreeCoding.binaryCombDegrees line 88
  16. lemma OAI.FKCRT.TreeCoding.walk_binaryComb line 92
  17. def OAI.FKCRT.TreeCoding.binaryComb line 102
  18. lemma OAI.FKCRT.TreeCoding.codeWeight_binaryComb_pos line 113
  19. lemma OAI.FKCRT.TreeCoding.codePartition_odd_pos line 123
  20. lemma OAI.FKCRT.TreeCoding.Code.sum_degrees line 129
  21. lemma OAI.FKCRT.TreeCoding.codeWeight_eq_zero_of_not_odd line 140
  22. lemma OAI.FKCRT.TreeCoding.codePartition_eq_zero_of_not_odd line 157
  23. lemma OAI.FKCRT.TreeCoding.codeExpectation_one line 162
  24. def OAI.FKCRT.TreeCoding.prefixSum line 168
  25. def OAI.FKCRT.TreeCoding.IsExcursionList line 171
  26. def OAI.FKCRT.TreeCoding.FirstMinimum line 175
  27. lemma OAI.FKCRT.TreeCoding.prefixSum_zero line 180
  28. lemma OAI.FKCRT.TreeCoding.prefixSum_length line 183
  29. lemma OAI.FKCRT.TreeCoding.prefixSum_drop line 187
  30. lemma OAI.FKCRT.TreeCoding.sum_drop line 193
  31. lemma OAI.FKCRT.TreeCoding.prefixSum_rotate_left line 201
  32. lemma OAI.FKCRT.TreeCoding.prefixSum_rotate_right line 209
  33. lemma OAI.FKCRT.TreeCoding.exists_firstListMinimum line 221
  34. lemma OAI.FKCRT.TreeCoding.FirstMinimum.unique line 239
  35. lemma OAI.FKCRT.TreeCoding.isExcursionList_rotate_of_firstMinimum line 251
  36. lemma OAI.FKCRT.TreeCoding.firstMinimum_of_isExcursionList_rotate line 264
  37. theorem OAI.FKCRT.TreeCoding.existsUnique_excursion_rotation line 287
  38. lemma OAI.FKCRT.TreeCoding.weighted_unique_rotation line 296
  39. abbrev OAI.FKCRT.TreeCoding.Bridge line 322
  40. instance OAI.FKCRT.TreeCoding.(instance at line 325) line 325
  41. def OAI.FKCRT.TreeCoding.degreeList line 328
  42. lemma OAI.FKCRT.TreeCoding.degreeList_length line 332
  43. lemma OAI.FKCRT.TreeCoding.degreeList_prefixSum line 336
  44. lemma OAI.FKCRT.TreeCoding.degreeList_sum line 341
  45. lemma OAI.FKCRT.TreeCoding.isTreeCode_iff line 346
  46. def OAI.FKCRT.TreeCoding.rotateDegrees line 351
  47. lemma OAI.FKCRT.TreeCoding.degreeList_rotate line 358
  48. lemma OAI.FKCRT.TreeCoding.walk_rotate_terminal line 367
  49. def OAI.FKCRT.TreeCoding.rotateBridge line 372
  50. lemma OAI.FKCRT.TreeCoding.Bridge.unique_good_rotation line 376
  51. def OAI.FKCRT.TreeCoding.bridgeWeight line 392
  52. def OAI.FKCRT.TreeCoding.bridgePartition line 396
  53. lemma OAI.FKCRT.TreeCoding.bridgeWeight_rotate line 400
  54. theorem OAI.FKCRT.TreeCoding.codePartition_cyclic line 405
  55. def OAI.FKCRT.TreeCoding.bridgeEmbedding line 427
  56. lemma OAI.FKCRT.TreeCoding.totalStep_bridge line 436
  57. lemma OAI.FKCRT.TreeCoding.totalStep_bridge_range line 443
  58. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.bridgePartition_eq_iid line 463
  59. lemma OAI.FKCRT.TreeCoding.rotateBridge_zero line 483
  60. lemma OAI.FKCRT.TreeCoding.rotateBridge_add line 490
  61. def OAI.FKCRT.TreeCoding.goodRotation line 497
  62. lemma OAI.FKCRT.TreeCoding.goodRotation_spec line 501
  63. def OAI.FKCRT.TreeCoding.canonicalCode line 506
  64. lemma OAI.FKCRT.TreeCoding.goodRotation_of_code line 510
  65. lemma OAI.FKCRT.TreeCoding.canonicalCode_of_code line 516
  66. lemma OAI.FKCRT.TreeCoding.goodRotation_add line 523
  67. lemma OAI.FKCRT.TreeCoding.canonicalCode_rotate line 530
  68. theorem OAI.FKCRT.TreeCoding.canonicalCode_weighted_sum line 537
  69. theorem OAI.FKCRT.TreeCoding.canonicalCode_expectation line 566
  70. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.iid_bridge_singleton line 578
  71. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.bridge_integral_eq line 586
  72. def OAI.FKCRT.TreeCoding.bridgeFromArray line 610
  73. lemma OAI.FKCRT.TreeCoding.bridgeFromArray_spec line 614
  74. lemma OAI.FKCRT.TreeCoding.bridgeFromArray_embedding line 619
  75. def OAI.FKCRT.TreeCoding.arrayTree line 624
  76. lemma OAI.FKCRT.TreeCoding.arrayTree_embedding line 629
  77. theorem OAI.FKCRT.TreeCoding.CriticalEvenOffspring.arrayTree_expectation line 634
  78. lemma OAI.FKCRT.TreeCoding.interpolation_interval_formula line 643
  79. lemma OAI.FKCRT.TreeCoding.interpolation_ge line 686
  80. lemma OAI.FKCRT.TreeCoding.interpolation_strict_before line 694
  81. lemma OAI.FKCRT.TreeCoding.exists_grid_interval line 715
  82. lemma OAI.FKCRT.TreeCoding.cyclePath_interpolation line 736
  83. lemma OAI.FKCRT.TreeCoding.minTime_interpolation line 789
  84. lemma OAI.FKCRT.TreeCoding.cyclePath_one_time line 805
  85. lemma OAI.FKCRT.TreeCoding.goodRotation_firstMinimum line 814
  86. def OAI.FKCRT.TreeCoding.walkPolygon line 822
  87. lemma OAI.FKCRT.TreeCoding.walkPolygon_cycle line 826
  88. theorem OAI.FKCRT.TreeCoding.vervaat_walkPolygon line 851
  89. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.iidWalk_bridgeEmbedding line 906
  90. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.vervaat_arrayTree line 923
  91. theorem OAI.FKCRT.TreeCoding.CriticalEvenOffspring.codeWalk_CLT line 934
  92. def OAI.FKCRT.TreeCoding.firstZero line 958
  93. lemma OAI.FKCRT.TreeCoding.firstZero_le_iff line 963
  94. lemma OAI.FKCRT.TreeCoding.firstZero_isStoppingTime line 975
  95. lemma OAI.FKCRT.TreeCoding.integer_path_nonneg_before_zero line 990
  96. lemma OAI.FKCRT.TreeCoding.stopped_firstZero_nonneg line 1000
  97. lemma OAI.FKCRT.TreeCoding.martingale_stoppedProcess_real line 1017
  98. theorem OAI.FKCRT.TreeCoding.integer_martingale_hits_zero line 1029
  99. def OAI.FKCRT.TreeCoding.integerSum line 1070
  100. lemma OAI.FKCRT.TreeCoding.integerSum_zero line 1074
  101. lemma OAI.FKCRT.TreeCoding.integerSum_succ line 1077
  102. theorem OAI.FKCRT.TreeCoding.CriticalEvenOffspring.stream_hits_negative line 1083
  103. def OAI.FKCRT.TreeCoding.reverseIndex line 1134
  104. def OAI.FKCRT.TreeCoding.reverseFirst line 1137
  105. lemma OAI.FKCRT.TreeCoding.reverseIndex_involutive line 1140
  106. lemma OAI.FKCRT.TreeCoding.reverseFirst_preserving line 1149
  107. lemma OAI.FKCRT.TreeCoding.integerSum_reverseFirst line 1155
  108. def OAI.FKCRT.TreeCoding.negativeSurvival line 1169
  109. def OAI.FKCRT.TreeCoding.firstHitBelow line 1173
  110. lemma OAI.FKCRT.TreeCoding.firstHitBelow_iff_reverse_survival line 1177
  111. lemma OAI.FKCRT.TreeCoding.measurable_integerSum line 1200
  112. lemma OAI.FKCRT.TreeCoding.measurableSet_firstHitBelow line 1205
  113. lemma OAI.FKCRT.TreeCoding.measurableSet_survival_endpoint line 1213
  114. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.survival_endpoint_eq_firstHit line 1222
  115. lemma OAI.FKCRT.TreeCoding.exists_firstHitBelow line 1232
  116. lemma OAI.FKCRT.TreeCoding.firstHitBelow_disjoint line 1250
  117. theorem OAI.FKCRT.TreeCoding.CriticalEvenOffspring.negative_potential_one line 1264
  118. def OAI.FKCRT.TreeCoding.truncateStream line 1275
  119. lemma OAI.FKCRT.TreeCoding.measurable_truncateStream line 1278
  120. lemma OAI.FKCRT.TreeCoding.integerSum_truncateStream line 1285
  121. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.truncate_indep_next line 1293
  122. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.prefix_inter_next line 1311
  123. lemma OAI.FKCRT.TreeCoding.survival_endpoint_truncate line 1325
  124. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.negative_potential_zero line 1338
  125. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.negative_potential line 1357