OAI/Probability/FKMaps/LadderCuts.lean

GitHub source file

78 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.FKCRT.Inventory.firstDown_add line 10
2. lemma OAI.FKCRT.Inventory.stoppedWord_down_add line 32
3. def OAI.FKCRT.Inventory.rightPieces line 38
4. lemma OAI.FKCRT.Inventory.rightPieces_measurable line 39
5. lemma OAI.FKCRT.Inventory.rightPieces_preserving line 43
6. def OAI.FKCRT.Inventory.reversePiecesPrefix line 57
7. lemma OAI.FKCRT.Inventory.reversePiecesPrefix_succ line 59
8. lemma OAI.FKCRT.Inventory.rightPieces_tail line 65
9. lemma OAI.FKCRT.Inventory.stoppedWord_down_pieces line 71
10. def OAI.FKCRT.Inventory.reverseFirstPieces line 89
11. lemma OAI.FKCRT.Inventory.reverseFirstPieces_preserving line 91
12. lemma OAI.FKCRT.Inventory.reversePiecesPrefix_eq line 95
13. lemma OAI.FKCRT.Inventory.rightPrefix_identDistrib line 106
14. lemma OAI.FKCRT.Inventory.piecesPrefix_measurable line 129
15. def OAI.FKCRT.Inventory.NonemptyPieces line 136
16. lemma OAI.FKCRT.Inventory.reverseRightLaw_nonempty line 137
17. lemma OAI.FKCRT.Inventory.rightPieces_nonempty line 142
18. lemma OAI.FKCRT.Inventory.piecesPrefix_length line 147
19. lemma OAI.FKCRT.Inventory.piecesPrefix_extension line 155
20. def OAI.FKCRT.Inventory.pieceScan line 160
21. lemma OAI.FKCRT.Inventory.pieceScan_measurable line 162
22. lemma OAI.FKCRT.Inventory.pieceScan_get line 166
23. lemma OAI.FKCRT.Inventory.rawWord_pieceScan line 172
24. lemma OAI.FKCRT.Inventory.rawWord_measurable line 191
25. lemma OAI.FKCRT.Inventory.wordWeight_reverse line 193
26. lemma OAI.FKCRT.Inventory.rawWord_reverse line 195
27. lemma OAI.FKCRT.Inventory.increment_sum_bounds line 196
28. lemma OAI.FKCRT.Inventory.rightDensity_signSum_bounds line 204
29. lemma OAI.FKCRT.Inventory.firstDown_length line 208
30. lemma OAI.FKCRT.Inventory.rawKilled_preimage line 213
31. lemma OAI.FKCRT.Inventory.rightDensity_rawKilled_measurable line 225
32. lemma OAI.FKCRT.Inventory.rawPrefix_tail_rectangle line 228
33. lemma OAI.FKCRT.Inventory.rawKilled_block_rectangle line 253
34. lemma OAI.FKCRT.Inventory.stoppedWord_suffix_witness line 265

    Source documentation

    A specified reversed terminal string of a first-downcrossing word leaves a genuine killed-walk prefix and an independent raw suffix.

    lemma stoppedWord_suffix_witness {h t : ℕ} {x : ℕ → Letter} {w : List Letter}
        (hwpos : 0<w.length) (hh : w.length<h) (hx : firstDown h x=WithTop.some t)
        (hw : (stoppedWord (firstDown h) x).take w.length=w) :
        ∃ r n : ℕ,0<r ∧ (r:ℤ)= -(w.map Letter.increment).sum ∧
          x∈rawKilled (h-1) (r-1) n ∧ rawWord (tail n x) w.length=w.reverse := by
    …

    Mentions: OAI.FKCRT.Inventory.Letter, OAI.FKCRT.Inventory.firstDown, OAI.FKCRT.Inventory.stoppedWord, OAI.FKCRT.Inventory.Letter.increment, OAI.FKCRT.Inventory.rawKilled, OAI.FKCRT.Inventory.rawWord, OAI.FKCRT.Inventory.tail

35. def OAI.FKCRT.Inventory.terminalDeficit line 300
36. theorem OAI.FKCRT.Inventory.stoppedWord_prefix_density_bound line 304

    Source documentation

    The only density estimate used is a sum of finite-prefix cylinders. No integrability of the raw downcrossing length is asserted.

    theorem stoppedWord_prefix_density_bound (P : Parameters) (h : ℕ) (w : List Letter)
        (hwpos : 0<w.length) (hh : w.length<h) :
        streamLaw P ℕ {x | (stoppedWord (firstDown h) x).take w.length=w} ≤
          2*(terminalDeficit w:ℝ≥0∞)*wordWeight P w := by
    …

    Mentions: OAI.FKCRT.Inventory.Parameters, OAI.FKCRT.Inventory.Letter, OAI.FKCRT.Inventory.streamLaw, OAI.FKCRT.Inventory.stoppedWord, OAI.FKCRT.Inventory.firstDown, OAI.FKCRT.Inventory.terminalDeficit, OAI.FKCRT.Inventory.wordWeight

37. def OAI.FKCRT.Inventory.rightScanLaw line 359
38. instance OAI.FKCRT.Inventory.(instance at line 361) line 361
39. lemma OAI.FKCRT.Inventory.rightScan_cylinder_bound line 364
40. lemma OAI.FKCRT.Inventory.rightScan_first_order line 382
41. def OAI.FKCRT.Inventory.rightRemainderLaw line 396
42. instance OAI.FKCRT.Inventory.(instance at line 397) line 397
43. lemma OAI.FKCRT.Inventory.rawWord_succ_head line 400
44. lemma OAI.FKCRT.Inventory.wordWeight_cons line 408
45. lemma OAI.FKCRT.Inventory.terminalDeficit_order line 410
46. lemma OAI.FKCRT.Inventory.order_mass_sum line 414
47. theorem OAI.FKCRT.Inventory.rightRemainder_cylinder_bound line 420
48. lemma OAI.FKCRT.Inventory.rawFiltration_eq_comap line 459
49. lemma OAI.FKCRT.Inventory.rawPrefix_atom line 472
50. lemma OAI.FKCRT.Inventory.rightRemainder_prefix_bound line 476
51. lemma OAI.FKCRT.Inventory.rightRemainder_prefix_event line 484
52. lemma OAI.FKCRT.Inventory.K_signSum_of_hit line 526
53. theorem OAI.FKCRT.Inventory.rightRemainder_hit_bound line 537
54. theorem OAI.FKCRT.Inventory.rightRemainder_survivor_bound line 550
55. def OAI.FKCRT.Inventory.RightCut line 575
56. lemma OAI.FKCRT.Inventory.measurableSet_rightCut line 576
57. lemma OAI.FKCRT.Inventory.rawWord_pieceScan_prefix line 582
58. lemma OAI.FKCRT.Inventory.noSurvivor_burgers line 590
59. lemma OAI.FKCRT.Inventory.append_order_no_burgers line 599
60. lemma OAI.FKCRT.Inventory.remainder_noSurvivor_implies_cut line 605
61. lemma OAI.FKCRT.Inventory.K_lintegral_lt_one line 620
62. lemma OAI.FKCRT.Inventory.rightRemainder_noSurvivor_pos line 627
63. theorem OAI.FKCRT.Inventory.positive_rightCut line 638
64. lemma OAI.FKCRT.Inventory.orders_step_sublist line 661
65. lemma OAI.FKCRT.Inventory.orders_run_sublist line 665
66. def OAI.FKCRT.Inventory.LeftCut line 670
67. lemma OAI.FKCRT.Inventory.measurable_piecesPrefix line 671
68. lemma OAI.FKCRT.Inventory.measurableSet_leftCut line 676
69. def OAI.FKCRT.Inventory.supplyPieces line 681
70. def OAI.FKCRT.Inventory.startingSupply line 683
71. lemma OAI.FKCRT.Inventory.supplyPieces_flatten line 684
72. lemma OAI.FKCRT.Inventory.run_supplyPieces line 690
73. lemma OAI.FKCRT.Inventory.startingSupply_count line 693
74. lemma OAI.FKCRT.Inventory.supplyPieces_mem line 695
75. lemma OAI.FKCRT.Inventory.leftCut_of_buffer_prefix line 701
76. lemma OAI.FKCRT.Inventory.iid_all_fixed line 725
77. theorem OAI.FKCRT.Inventory.positive_leftCut_general line 733

    Source documentation

    Positive L-cut probability using only shortened-piece integrability, positive type-drift and the two genuine one-burger atoms.

    theorem positive_leftCut_general (ν : Measure (List Letter)) [IsProbabilityMeasure ν]
        (hlen : Integrable (fun w : List Letter => (w.length:ℝ)) ν)
        (hnet : ∀ b,Integrable (fun w => (typeNet b w:ℝ)) ν)
        (hmean : ∀ b,(∫ w,(typeNet b w:ℝ) ∂ν)=1/2)
        (hf : ∀ᵐ w ∂ν,FixedWord w)
        (hburger : ∀ b,0<ν {[Letter.burger b]}) :
        0<naturalPiecesLaw ν {x | LeftCut x} := by
    …

    Mentions: OAI.FKCRT.Inventory.Letter, OAI.FKCRT.Inventory.typeNet, OAI.FKCRT.Inventory.FixedWord, OAI.FKCRT.Inventory.naturalPiecesLaw, OAI.FKCRT.Inventory.LeftCut

78. theorem OAI.FKCRT.Inventory.shortLeft_positive_cut line 767

    Source documentation

    Source ladder:cuts, L side, for the actual shortened first +1 pieces.

    theorem shortLeft_positive_cut (P : Parameters) :
        0<naturalPiecesLaw (shortLeftLaw P) {x | LeftCut x} :=
    …

    Mentions: OAI.FKCRT.Inventory.Parameters, OAI.FKCRT.Inventory.naturalPiecesLaw, OAI.FKCRT.Inventory.shortLeftLaw, OAI.FKCRT.Inventory.LeftCut