OAI/Probability/FKMaps/PieceLaws.lean

GitHub source file

107 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.FKCRT.Inventory.(instance at line 11) line 11
  2. instance OAI.FKCRT.Inventory.(instance at line 12) line 12
  3. instance OAI.FKCRT.Inventory.(instance at line 13) line 13
  4. instance OAI.FKCRT.Inventory.(instance at line 14) line 14
  5. def OAI.FKCRT.Inventory.intervalWord line 17

    Source documentation

    Chronological concatenation between whole-piece boundaries.

    def intervalWord (x : ℤ → List Letter) (a : ℤ) (n : ℕ) : List Letter :=
…

    Mentions: OAI.FKCRT.Inventory.Letter

  6. lemma OAI.FKCRT.Inventory.intervalWord_zero line 19
  7. lemma OAI.FKCRT.Inventory.intervalWord_succ line 20
  8. lemma OAI.FKCRT.Inventory.intervalWord_add line 22
  9. lemma OAI.FKCRT.Inventory.intervalWord_measurable line 31
  10. lemma OAI.FKCRT.Inventory.intervalWord_shift line 33
  11. lemma OAI.FKCRT.Inventory.intervalWord_net line 41
  12. lemma OAI.FKCRT.Inventory.reduce_append_no_burgers line 48
  13. lemma OAI.FKCRT.Inventory.reduce_append_no_orders line 55
  14. def OAI.FKCRT.Inventory.leftCutAt line 63
  15. def OAI.FKCRT.Inventory.rightCutAt line 64
  16. lemma OAI.FKCRT.Inventory.leftCutAt_measurable line 65
  17. lemma OAI.FKCRT.Inventory.rightCutAt_measurable line 68
  18. lemma OAI.FKCRT.Inventory.leftCutAt_shift line 71
  19. lemma OAI.FKCRT.Inventory.rightCutAt_shift line 74
  20. lemma OAI.FKCRT.Inventory.no_burgers_interval line 79
  21. def OAI.FKCRT.Inventory.rightOrders line 82
  22. lemma OAI.FKCRT.Inventory.rightOrders_length line 83
  23. lemma OAI.FKCRT.Inventory.rightOrders_append line 90
  24. def OAI.FKCRT.Inventory.rightOutput line 93
  25. lemma OAI.FKCRT.Inventory.rightOutput_measurable line 94
  26. lemma OAI.FKCRT.Inventory.rightOutput_shift line 98
  27. def OAI.FKCRT.Inventory.rightOutputData line 106
  28. lemma OAI.FKCRT.Inventory.rightOutput_segment line 111
  29. def OAI.FKCRT.Inventory.rightWord line 125
  30. def OAI.FKCRT.Inventory.rightLaw line 126
  31. lemma OAI.FKCRT.Inventory.rightWord_measurable line 127
  32. lemma OAI.FKCRT.Inventory.rightLaw_eq line 128
  33. instance OAI.FKCRT.Inventory.rightLaw_probability line 131
  34. lemma OAI.FKCRT.Inventory.rightLaw_reverse line 133
  35. lemma OAI.FKCRT.Inventory.rightLaw_net line 137
  36. lemma OAI.FKCRT.Inventory.rightSeq_net line 140
  37. def OAI.FKCRT.Inventory.reversedPast line 145
  38. lemma OAI.FKCRT.Inventory.reversedPast_measurable line 146
  39. lemma OAI.FKCRT.Inventory.reversedPast_preserving line 148
  40. lemma OAI.FKCRT.Inventory.intervalWord_first line 161
  41. lemma OAI.FKCRT.Inventory.reversedPast_prefix line 165
  42. lemma OAI.FKCRT.Inventory.rightCutAt_zero_iff line 174
  43. lemma OAI.FKCRT.Inventory.rightCutAt_positive line 176
  44. lemma OAI.FKCRT.Inventory.rightWord_of_order line 182
  45. lemma OAI.FKCRT.Inventory.rightLaw_order_positive line 190
  46. lemma OAI.FKCRT.Inventory.increment_flip line 200
  47. lemma OAI.FKCRT.Inventory.signSum_flip line 201
  48. lemma OAI.FKCRT.Inventory.firstDown_flip line 203
  49. lemma OAI.FKCRT.Inventory.rightWord_flip line 209
  50. lemma OAI.FKCRT.Inventory.rightLaw_flip_preserving line 211
  51. def OAI.FKCRT.Inventory.flipPieceSeq line 227
  52. lemma OAI.FKCRT.Inventory.flipPieceSeq_measurable line 228
  53. lemma OAI.FKCRT.Inventory.flipPieceSeq_preserving line 230
  54. lemma OAI.FKCRT.Inventory.intervalWord_flip line 236
  55. lemma OAI.FKCRT.Inventory.rightCutAt_flip line 241
  56. lemma OAI.FKCRT.Inventory.rightOrders_flip line 243
  57. lemma OAI.FKCRT.Inventory.rightOutput_flip line 246
  58. lemma OAI.FKCRT.Inventory.rightCutAt_zero_past_measurable line 253
  59. lemma OAI.FKCRT.Inventory.rightCutAt_one_of_order line 265
  60. lemma OAI.FKCRT.Inventory.rightOutput_of_cut_order line 278
  61. lemma OAI.FKCRT.Inventory.rightOutput_flexible_positive line 288
  62. def OAI.FKCRT.Inventory.outputIndicator line 309
  63. lemma OAI.FKCRT.Inventory.outputIndicator_measurable line 310
  64. lemma OAI.FKCRT.Inventory.outputIndicator_integrable line 312
  65. def OAI.FKCRT.Inventory.outputMass line 318
  66. lemma OAI.FKCRT.Inventory.outputMass_eq_measure line 319
  67. lemma OAI.FKCRT.Inventory.outputMass_flexible_pos line 324
  68. lemma OAI.FKCRT.Inventory.outputMass_fixed_eq line 327
  69. lemma OAI.FKCRT.Inventory.outputMass_sum line 335
  70. lemma OAI.FKCRT.Inventory.outputMass_fixed line 350
  71. theorem OAI.FKCRT.Inventory.rightOutput_frequencies line 355
  72. def OAI.FKCRT.CutOutput.count line 373

    Source documentation

    Number of marked boundaries before n.

    def count (C : ℕ → Prop) (n : ℕ) : ℕ := by
…
  73. def OAI.FKCRT.CutOutput.last line 376
  74. lemma OAI.FKCRT.CutOutput.last_le line 379
  75. lemma OAI.FKCRT.CutOutput.last_spec line 380
  76. lemma OAI.FKCRT.CutOutput.count_le line 381
  77. lemma OAI.FKCRT.CutOutput.count_at_last line 386
  78. lemma OAI.FKCRT.CutOutput.countReal line 394
  79. lemma OAI.FKCRT.CutOutput.last_tendsto line 403

    Source documentation

    Positive density is enough; no independence between cuts is used.

    lemma last_tendsto (C : ℕ → Prop) {δ : ℝ} (hδ : 0<δ)
    (hd : Tendsto (fun n => (count C n:ℝ)/(n:ℝ)) atTop (𝓝 δ)) :
    Tendsto (fun n => last C n+1) atTop atTop := by
…

    Mentions: OAI.FKCRT.CutOutput.count, OAI.FKCRT.CutOutput.last

  80. lemma OAI.FKCRT.CutOutput.last_ratio line 417
  81. lemma OAI.FKCRT.CutOutput.last_gap_ratio line 433
  82. lemma OAI.FKCRT.CutOutput.last_gap_div line 445
  83. lemma OAI.FKCRT.CutOutput.last_div line 456
  84. lemma OAI.FKCRT.Stationary.shift_neg_iterate line 478
  85. lemma OAI.FKCRT.Inventory.rightOutput_reverse_frequencies line 490
  86. def OAI.FKCRT.Inventory.rightCutDensity line 502
  87. lemma OAI.FKCRT.Inventory.rightCutDensity_pos line 503
  88. lemma OAI.FKCRT.Inventory.rightCut_reverse_density line 505
  89. lemma OAI.FKCRT.Inventory.rightCut_last_gap line 521
  90. lemma OAI.FKCRT.Inventory.bottom_append line 537
  91. lemma OAI.FKCRT.Inventory.bottom_append_bounds line 543
  92. lemma OAI.FKCRT.Inventory.count_real_sum line 554
  93. lemma OAI.FKCRT.Inventory.count_ofFn_real line 563
  94. def OAI.FKCRT.Inventory.typeBalance line 577
  95. lemma OAI.FKCRT.Inventory.typeBalance_step line 578
  96. lemma OAI.FKCRT.Inventory.typeBalance_run line 606
  97. lemma OAI.FKCRT.Inventory.burger_count_eq_typeNet line 616
  98. lemma OAI.FKCRT.Inventory.intervalWord_fixed line 621
  99. lemma OAI.FKCRT.Inventory.typeNet_intervalWord line 627
  100. lemma OAI.FKCRT.Inventory.shortLeftLaw_net line 635
  101. lemma OAI.FKCRT.Inventory.leftSeq_net line 639
  102. lemma OAI.FKCRT.Inventory.leftSeq_fixed line 643
  103. def OAI.FKCRT.Inventory.futurePieces line 648
  104. lemma OAI.FKCRT.Inventory.futurePieces_preserving line 649
  105. lemma OAI.FKCRT.Inventory.futurePieces_prefix line 653
  106. lemma OAI.FKCRT.Inventory.leftCutAt_zero_iff line 656
  107. lemma OAI.FKCRT.Inventory.leftCutAt_positive line 658