OAI/Probability/FKMaps/LadderRecords.lean

GitHub source file

101 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.FKCRT.TreeCoding.weakLadderHit line 13
  2. lemma OAI.FKCRT.TreeCoding.measurableSet_weakLadderHit line 17
  3. lemma OAI.FKCRT.TreeCoding.weakLadderHit_decomposition line 25
  4. lemma OAI.FKCRT.TreeCoding.weakLadderHit_decomposition_disjoint line 49
  5. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.weakLadderHit_mass line 59
  6. theorem OAI.FKCRT.TreeCoding.CriticalEvenOffspring.weakLadder_overshoot_mass line 72
  7. lemma OAI.FKCRT.TreeCoding.tail_tsum_ite line 81
  8. lemma OAI.FKCRT.TreeCoding.tail_tsum_total line 92
  9. lemma OAI.FKCRT.TreeCoding.sum_range_cast_nat line 107
  10. lemma OAI.FKCRT.TreeCoding.tail_tsum_first_moment line 117
  11. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.ladder_total line 135
  12. def OAI.FKCRT.TreeCoding.CriticalEvenOffspring.ladderLaw line 144
  13. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.ladderLaw_apply line 148
  14. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.variance_eq_second_sub_one line 152
  15. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.ladder_first_moment line 164
  16. def OAI.FKCRT.TreeCoding.streamShift line 195
  17. lemma OAI.FKCRT.TreeCoding.measurable_streamShift line 198
  18. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.streamShift_preserving line 204
  19. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.truncate_indep_shift line 219
  20. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.prefix_inter_shift line 247
  21. lemma OAI.FKCRT.TreeCoding.weakLadderHit_truncate line 256
  22. lemma OAI.FKCRT.TreeCoding.weakLadderHit_unique line 268
  23. lemma OAI.FKCRT.TreeCoding.weakLadderHit_pairwise line 286
  24. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.ae_weakLadderHit line 295
  25. lemma OAI.FKCRT.TreeCoding.measurableSet_hasWeakLadder line 308
  26. def OAI.FKCRT.TreeCoding.ladderPredicate line 313
  27. lemma OAI.FKCRT.TreeCoding.ladderPredicate_exists line 317
  28. def OAI.FKCRT.TreeCoding.ladderIndex line 324
  29. lemma OAI.FKCRT.TreeCoding.measurable_ladderIndex line 329
  30. lemma OAI.FKCRT.TreeCoding.ladderIndex_eq_of_hit line 339
  31. def OAI.FKCRT.TreeCoding.ladderOvershoot line 351
  32. def OAI.FKCRT.TreeCoding.ladderTail line 354
  33. lemma OAI.FKCRT.TreeCoding.measurable_ladderOvershoot line 357
  34. lemma OAI.FKCRT.TreeCoding.measurable_ladderTail line 367
  35. lemma OAI.FKCRT.TreeCoding.ladderOvershoot_of_hit line 379
  36. lemma OAI.FKCRT.TreeCoding.ladderTail_of_hit line 384
  37. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.ladder_slice_mass line 389
  38. lemma OAI.FKCRT.TreeCoding.countable_slice_rectangle line 419
  39. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.ladder_rectangle line 447
  40. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.ladder_hasLaw line 455
  41. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.ladderTail_preserving line 464
  42. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.ladder_indep_tail line 473
  43. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.ladder_integrable line 483
  44. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.ladder_integral line 493
  45. lemma OAI.FKCRT.TreeCoding.regenerative_cylinder line 502
  46. lemma OAI.FKCRT.TreeCoding.regenerative_iIndepFun line 535
  47. def OAI.FKCRT.TreeCoding.renewalIncrement line 580
  48. lemma OAI.FKCRT.TreeCoding.measurable_renewalIncrement line 584
  49. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.renewal_iid line 588
  50. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.renewal_hasLaw line 594
  51. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.renewal_strong_law line 599
  52. def OAI.FKCRT.TreeCoding.renewalCount line 618
  53. lemma OAI.FKCRT.TreeCoding.renewalCount_spec line 621
  54. lemma OAI.FKCRT.TreeCoding.le_renewalCount_iff line 626
  55. lemma OAI.FKCRT.TreeCoding.renewalCount_succ_gt line 635
  56. lemma OAI.FKCRT.TreeCoding.renewalCount_mono line 641
  57. lemma OAI.FKCRT.TreeCoding.renewalCount_at line 648
  58. lemma OAI.FKCRT.TreeCoding.renewalCount_tendsto line 655
  59. structure OAI.FKCRT.TreeCoding.LadderEnumeration line 663
  60. lemma OAI.FKCRT.TreeCoding.LadderEnumeration.le_level line 670
  61. lemma OAI.FKCRT.TreeCoding.LadderEnumeration.maximum line 678
  62. lemma OAI.FKCRT.TreeCoding.LadderEnumeration.record_at line 684
  63. def OAI.FKCRT.TreeCoding.weakRecords line 690
  64. lemma OAI.FKCRT.TreeCoding.mem_weakRecords line 694
  65. lemma OAI.FKCRT.TreeCoding.LadderEnumeration.records line 699
  66. lemma OAI.FKCRT.TreeCoding.LadderEnumeration.card_records line 725
  67. lemma OAI.FKCRT.TreeCoding.LadderEnumeration.first_records_below line 733
  68. def OAI.FKCRT.TreeCoding.ladderTime line 750
  69. lemma OAI.FKCRT.TreeCoding.ladderTime_zero line 755
  70. lemma OAI.FKCRT.TreeCoding.ladderTime_strictMono line 758
  71. lemma OAI.FKCRT.TreeCoding.streamShift_add line 765
  72. lemma OAI.FKCRT.TreeCoding.ladderTail_iterate line 772
  73. lemma OAI.FKCRT.TreeCoding.integerSum_shift line 783
  74. def OAI.FKCRT.TreeCoding.HasAllLadders line 790
  75. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.ae_all_ladders line 794
  76. lemma OAI.FKCRT.TreeCoding.ladderTime_step_level line 802
  77. lemma OAI.FKCRT.TreeCoding.ladderTime_between line 813
  78. lemma OAI.FKCRT.TreeCoding.ladderTime_enumeration line 824
  79. lemma OAI.FKCRT.TreeCoding.ladderTime_level_sum line 834
  80. lemma OAI.FKCRT.TreeCoding.linear_remainder_of_ratio line 844
  81. lemma OAI.FKCRT.TreeCoding.uniform_remainder_probability line 873
  82. lemma OAI.FKCRT.TreeCoding.integrable_neg_exp_nat line 898
  83. lemma OAI.FKCRT.TreeCoding.nat_laplace_lt_one line 908
  84. lemma OAI.FKCRT.TreeCoding.iid_nat_laplace_sum line 928
  85. lemma OAI.FKCRT.TreeCoding.iid_nat_lower_tail line 949
  86. def OAI.FKCRT.TreeCoding.renewalLevel line 1002
  87. lemma OAI.FKCRT.TreeCoding.measurable_renewalLevel line 1006
  88. lemma OAI.FKCRT.TreeCoding.renewalLevel_nonneg line 1012
  89. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.renewal_uniform_remainder line 1016
  90. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.renewal_remainder_probability line 1025
  91. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.renewal_lower_tail line 1033
  92. lemma OAI.FKCRT.TreeCoding.ladderTime_level_real line 1047
  93. lemma OAI.FKCRT.TreeCoding.record_count_remainder line 1053
  94. def OAI.FKCRT.TreeCoding.reverseRecords line 1062
  95. def OAI.FKCRT.TreeCoding.recordHeight line 1066
  96. lemma OAI.FKCRT.TreeCoding.mem_reverseRecords line 1070
  97. lemma OAI.FKCRT.TreeCoding.exists_first_path_minimum line 1075
  98. lemma OAI.FKCRT.TreeCoding.reverseRecords_at_first_minimum line 1093
  99. lemma OAI.FKCRT.TreeCoding.reverseRecords_split line 1114
  100. lemma OAI.FKCRT.TreeCoding.reverseRecords_shared_prefix_subset line 1130
  101. theorem OAI.FKCRT.TreeCoding.recordHeight_interval_identity line 1140