OAI/Probability/FKMaps/InventoryRenewal.lean

GitHub source file

122 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.FKCRT.Inventory.survivorTail line 11
  2. def OAI.FKCRT.Inventory.survivorData line 12
  3. def OAI.FKCRT.Inventory.prefixData line 13
  4. lemma OAI.FKCRT.Inventory.measurable_prefixData line 15
  5. lemma OAI.FKCRT.Inventory.measurable_survivorData line 18
  6. lemma OAI.FKCRT.Inventory.measurable_survivorTail line 19
  7. lemma OAI.FKCRT.Inventory.survivorData_of_hit line 25
  8. lemma OAI.FKCRT.Inventory.survivorTail_of_hit line 28
  9. lemma OAI.FKCRT.Inventory.survivor_rectangle_sum line 33
  10. lemma OAI.FKCRT.Inventory.survivor_rectangle line 68
  11. lemma OAI.FKCRT.Inventory.survivorTail_preserving line 76
  12. lemma OAI.FKCRT.Inventory.survivorData_indep_tail line 83
  13. def OAI.FKCRT.Inventory.parsingData line 89
  14. lemma OAI.FKCRT.Inventory.parsingData_iid line 90
  15. lemma OAI.FKCRT.Inventory.parsingData_identDistrib line 93
  16. def OAI.FKCRT.DefectHitting.walk line 112
  17. def OAI.FKCRT.DefectHitting.alive line 113
  18. def OAI.FKCRT.DefectHitting.stoppedSum line 114
  19. lemma OAI.FKCRT.DefectHitting.walk_succ line 117
  20. lemma OAI.FKCRT.DefectHitting.alive_zero line 119
  21. lemma OAI.FKCRT.DefectHitting.alive_succ line 120
  22. lemma OAI.FKCRT.DefectHitting.stoppedSum_eq line 128
  23. lemma OAI.FKCRT.DefectHitting.stoppedSum_le_one line 152
  24. def OAI.FKCRT.DefectHitting.past line 161
  25. lemma OAI.FKCRT.DefectHitting.past_le line 163
  26. lemma OAI.FKCRT.DefectHitting.measurable_walk_prefix line 166
  27. lemma OAI.FKCRT.DefectHitting.measurableSet_alive_prefix line 174
  28. lemma OAI.FKCRT.DefectHitting.measurableSet_alive line 178
  29. lemma OAI.FKCRT.DefectHitting.alive_indep_next line 180
  30. lemma OAI.FKCRT.DefectHitting.integral_alive_increment line 189
  31. theorem OAI.FKCRT.DefectHitting.bounded_wald_bound line 210
  32. lemma OAI.FKCRT.DefectHitting.integral_alive_length line 227
  33. def OAI.FKCRT.DefectHitting.totalLength line 248
  34. lemma OAI.FKCRT.DefectHitting.measurable_totalLength line 251
  35. lemma OAI.FKCRT.DefectHitting.totalLength_expectation line 256
  36. lemma OAI.FKCRT.DefectHitting.totalLength_finite line 296
  37. lemma OAI.FKCRT.DefectHitting.hit_of_totalLength_finite line 305
  38. lemma OAI.FKCRT.DefectHitting.integrable_totalLength line 315
  39. lemma OAI.FKCRT.DefectHitting.alive_antitone line 325
  40. def OAI.FKCRT.DefectHitting.stopPredicate line 328
  41. lemma OAI.FKCRT.DefectHitting.stop_exists line 331
  42. def OAI.FKCRT.DefectHitting.stopIndex line 335
  43. lemma OAI.FKCRT.DefectHitting.measurable_stopIndex line 337
  44. lemma OAI.FKCRT.DefectHitting.stop_spec line 344
  45. lemma OAI.FKCRT.DefectHitting.stop_eq_zero_of_no_hit line 353
  46. lemma OAI.FKCRT.DefectHitting.walk_at_stop line 357
  47. lemma OAI.FKCRT.DefectHitting.totalLength_eq_sum line 373
  48. def OAI.FKCRT.DefectHitting.stoppedLength line 381
  49. lemma OAI.FKCRT.DefectHitting.measurable_stoppedLength line 384
  50. lemma OAI.FKCRT.DefectHitting.totalLength_toReal line 392
  51. lemma OAI.FKCRT.DefectHitting.integrable_stoppedLength line 409
  52. instance OAI.FKCRT.Inventory.(instance at line 425) line 425
  53. instance OAI.FKCRT.Inventory.(instance at line 426) line 426
  54. def OAI.FKCRT.Inventory.parsingK line 428
  55. lemma OAI.FKCRT.Inventory.measurable_parsingK line 429
  56. lemma OAI.FKCRT.Inventory.parsingK_iid line 431
  57. lemma OAI.FKCRT.Inventory.parsingK_identDistrib line 433
  58. lemma OAI.FKCRT.Inventory.integrable_parsingK line 436
  59. lemma OAI.FKCRT.Inventory.integral_parsingK line 439
  60. def OAI.FKCRT.Inventory.allParsingFinite line 443
  61. lemma OAI.FKCRT.Inventory.ae_allParsingFinite line 444
  62. def OAI.FKCRT.Inventory.parsingLength line 449
  63. def OAI.FKCRT.Inventory.parsingOffset line 450
  64. def OAI.FKCRT.Inventory.rawChunk line 453
  65. def OAI.FKCRT.Inventory.shortPrefix line 455
  66. def OAI.FKCRT.Inventory.leftSteps line 459
  67. def OAI.FKCRT.Inventory.leftWord line 460
  68. def OAI.FKCRT.Inventory.shortLeftWord line 461
  69. lemma OAI.FKCRT.Inventory.parsingTail_eq line 463
  70. lemma OAI.FKCRT.Inventory.revealed_offset_succ line 472
  71. lemma OAI.FKCRT.Inventory.run_shortPrefix line 476
  72. lemma OAI.FKCRT.Inventory.run_shortLeftWord line 481
  73. lemma OAI.FKCRT.Inventory.parsing_shape line 484
  74. lemma OAI.FKCRT.Inventory.normal_parsing_length line 495
  75. lemma OAI.FKCRT.Inventory.signSum_add line 501
  76. lemma OAI.FKCRT.Inventory.signSum_parsing line 504
  77. lemma OAI.FKCRT.Inventory.signSum_before_parsing line 510
  78. lemma OAI.FKCRT.Inventory.signSum_offset line 525
  79. lemma OAI.FKCRT.Inventory.shortPrefix_length line 533
  80. lemma OAI.FKCRT.Inventory.shortLeftWord_length line 542
  81. lemma OAI.FKCRT.Inventory.signSum_nonpos_prefix line 545
  82. lemma OAI.FKCRT.Inventory.ae_left_first_hit line 560
  83. lemma OAI.FKCRT.Inventory.measurable_shortLeftWord line 572
  84. theorem OAI.FKCRT.Inventory.integrable_shortLeftWord_length line 591

    Source documentation

    Source ladder:short-length for the actual first-hit left ladder word, shortened by the proved reduction-preserving parsing. No E J is used.

    theorem integrable_shortLeftWord_length (P : Parameters) :
    Integrable (fun x => ((shortLeftWord x).length:ℝ)) (streamLaw P ℕ) := by
…

    Mentions: OAI.FKCRT.Inventory.Parameters, OAI.FKCRT.Inventory.shortLeftWord, OAI.FKCRT.Inventory.streamLaw

  85. lemma OAI.FKCRT.Inventory.K_flip line 606
  86. lemma OAI.FKCRT.Inventory.tail_flip line 608
  87. lemma OAI.FKCRT.Inventory.survivorTail_flip line 609
  88. lemma OAI.FKCRT.Inventory.iterate_survivorTail_flip line 611
  89. lemma OAI.FKCRT.Inventory.parsingK_flip line 616
  90. lemma OAI.FKCRT.Inventory.leftSteps_flip line 619
  91. lemma OAI.FKCRT.Inventory.normalWord_flip line 625
  92. lemma OAI.FKCRT.Inventory.rawChunk_flip line 628
  93. lemma OAI.FKCRT.Inventory.shortPrefix_flip line 630
  94. lemma OAI.FKCRT.Inventory.shortLeftWord_flip line 634
  95. def OAI.FKCRT.Inventory.Letter.typeNet line 637
  96. def OAI.FKCRT.Inventory.typeNet line 642
  97. def OAI.FKCRT.Inventory.FixedWord line 644
  98. lemma OAI.FKCRT.Inventory.Letter.typeNet_flip line 646
  99. lemma OAI.FKCRT.Inventory.typeNet_flip line 652
  100. lemma OAI.FKCRT.Inventory.Letter.abs_typeNet_le line 654
  101. lemma OAI.FKCRT.Inventory.abs_typeNet_le line 660
  102. lemma OAI.FKCRT.Inventory.typeNet_total line 669
  103. lemma OAI.FKCRT.Inventory.fixed_normal_parsing line 685
  104. lemma OAI.FKCRT.Inventory.fixed_shortPrefix line 690
  105. lemma OAI.FKCRT.Inventory.fixed_shortLeftWord line 696
  106. lemma OAI.FKCRT.Inventory.shortLeftWord_sign line 698
  107. lemma OAI.FKCRT.Inventory.ae_short_typeNet_total line 703
  108. lemma OAI.FKCRT.Inventory.integrable_short_typeNet line 707
  109. theorem OAI.FKCRT.Inventory.integral_short_typeNet line 717

    Source documentation

    Each genuine shortened L-piece has expected net count 1/2 of either type.

    theorem integral_short_typeNet (P : Parameters) (b : Bool) :
    (∫ x,(typeNet b (shortLeftWord x):ℝ) ∂streamLaw P ℕ)=1/2 := by
…

    Mentions: OAI.FKCRT.Inventory.Parameters, OAI.FKCRT.Inventory.typeNet, OAI.FKCRT.Inventory.shortLeftWord, OAI.FKCRT.Inventory.streamLaw

  110. def OAI.FKCRT.Inventory.shortLeftLaw line 740
  111. lemma OAI.FKCRT.Inventory.shortLeft_hasLaw line 742
  112. instance OAI.FKCRT.Inventory.shortLeftLaw_probability line 744
  113. lemma OAI.FKCRT.Inventory.shortLeftLaw_length_integrable line 748
  114. lemma OAI.FKCRT.Inventory.shortLeftLaw_typeNet_integrable line 752
  115. lemma OAI.FKCRT.Inventory.shortLeftLaw_typeNet_mean line 756
  116. lemma OAI.FKCRT.Inventory.shortLeftLaw_fixed line 760
  117. lemma OAI.FKCRT.Inventory.firstSurvivor_of_burger line 764
  118. lemma OAI.FKCRT.Inventory.parsingLength_of_burger line 770
  119. lemma OAI.FKCRT.Inventory.K_of_burger line 772
  120. lemma OAI.FKCRT.Inventory.leftSteps_of_burger line 775
  121. lemma OAI.FKCRT.Inventory.shortLeftWord_of_burger line 795
  122. lemma OAI.FKCRT.Inventory.shortLeftLaw_burger_positive line 800