OAI/Probability/FKMaps/UniformSeams.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FKCRT.Inventory.leftCutDensity line 11
2. lemma OAI.FKCRT.Inventory.leftCutDensity_pos line 12
3. lemma OAI.FKCRT.Inventory.leftCut_density line 14
4. def OAI.FKCRT.Inventory.forwardTypeSum line 31
5. lemma OAI.FKCRT.Inventory.left_type_averages line 33
6. def OAI.FKCRT.Inventory.leftBurgers line 40
7. lemma OAI.FKCRT.Inventory.leftBurgers_length line 41
8. lemma OAI.FKCRT.Inventory.leftBurgers_append line 47
9. lemma OAI.FKCRT.Inventory.forwardTypeSum_burgers line 55
10. def OAI.FKCRT.Inventory.bottomBurgerCount line 64
11. lemma OAI.FKCRT.Inventory.bottomBurgerCount_bounds line 66
12. theorem OAI.FKCRT.Inventory.left_uniform_counts line 81

    Source documentation

    Source uniform bottom counts, for genuine shortened +1 pieces.

    theorem left_uniform_counts (P : Parameters) (b : Bool) :
        ∀ᵐ x ∂Stationary.seqLaw (shortLeftLaw P),leftCutAt x 0 →
          ∀ ε>0,∀ᶠ k : ℕ in atTop,∀ h≥k,
            |(bottomBurgerCount x b h k:ℝ)/(k:ℝ)-1/2|<ε := by
    …

    Mentions: OAI.FKCRT.Inventory.Parameters, OAI.FKCRT.Stationary.seqLaw, OAI.FKCRT.Inventory.shortLeftLaw, OAI.FKCRT.Inventory.leftCutAt, OAI.FKCRT.Inventory.bottomBurgerCount

13. def OAI.FKCRT.Inventory.backwardOutputSum line 129
14. lemma OAI.FKCRT.Inventory.backwardOutputSum_eq line 131
15. def OAI.FKCRT.Inventory.terminalOrderCount line 152
16. lemma OAI.FKCRT.Inventory.terminalOrderCount_bounds line 154
17. theorem OAI.FKCRT.Inventory.right_uniform_counts line 176

    Source documentation

    Uniform terminal counts on the actual R-cut event; the h variable is unbounded and is not fixed before the limit.

    theorem right_uniform_counts (P : Parameters) (o : Order) :
        ∀ᵐ x ∂Stationary.seqLaw (rightLaw P),rightCutAt x 0 →
          ∀ ε>0,∀ᶠ k : ℕ in atTop,∀ h≥k,
            |(terminalOrderCount x o h k:ℝ)/(k:ℝ)-outputMass P o|<ε := by
    …

    Mentions: OAI.FKCRT.Inventory.Parameters, OAI.FKCRT.Inventory.Order, OAI.FKCRT.Stationary.seqLaw, OAI.FKCRT.Inventory.rightLaw, OAI.FKCRT.Inventory.rightCutAt, OAI.FKCRT.Inventory.terminalOrderCount, OAI.FKCRT.Inventory.outputMass

18. lemma OAI.FKCRT.Inventory.outputMass_nonneg line 226
19. lemma OAI.FKCRT.Inventory.seam_alpha line 229
20. def OAI.FKCRT.Inventory.GoodLeft line 239
21. def OAI.FKCRT.Inventory.GoodRight line 241
22. lemma OAI.FKCRT.Inventory.GoodLeft.mono line 243
23. lemma OAI.FKCRT.Inventory.GoodRight.mono line 245
24. lemma OAI.FKCRT.Inventory.exists_measure_pos_of_ae_cover line 248
25. lemma OAI.FKCRT.Inventory.goodLeft_positive line 257
26. lemma OAI.FKCRT.Inventory.goodRight_positive line 274
27. lemma OAI.FKCRT.Inventory.intervalWord_measurable_coords line 293
28. lemma OAI.FKCRT.Inventory.goodLeft_measurable line 306
29. lemma OAI.FKCRT.Inventory.goodRight_past_measurable line 314
30. lemma OAI.FKCRT.Inventory.goodRight_measurable line 324
31. def OAI.FKCRT.Inventory.FlexiblePrefix line 336
32. lemma OAI.FKCRT.Inventory.intervalWord_flexible line 338
33. lemma OAI.FKCRT.Inventory.reduce_flexible line 349
34. lemma OAI.FKCRT.Inventory.forcedRight_shape line 352
35. lemma OAI.FKCRT.Inventory.count_bottom_flexible line 368
36. lemma OAI.FKCRT.Inventory.count_bottom_flexible_append line 371
37. lemma OAI.FKCRT.Inventory.count_bottom_flexible_append_small line 375
38. theorem OAI.FKCRT.Inventory.seam_matching line 383

    Source documentation

    Deterministic source seam criterion, including every small k.

    theorem seam_matching {x y : ℤ → List Letter} {α : ℝ} {B D h : ℕ}
        (hα : 0≤α) (hBD : B≤D) (hD : (B:ℝ)≤α*D)
        (hl : GoodLeft α B x) (hr : GoodRight α B y) (hf : FlexiblePrefix y D)
        (hdl : ∀ j,((x j).map Letter.increment).sum=1)
        (hdr : ∀ j,((y j).map Letter.increment).sum= -1) :
        EmptyReducing (intervalWord x 0 h++intervalWord y ((D:ℤ)-h) h) := by
    …

    Mentions: OAI.FKCRT.Inventory.Letter, OAI.FKCRT.Inventory.D, OAI.FKCRT.Inventory.GoodLeft, OAI.FKCRT.Inventory.GoodRight, OAI.FKCRT.Inventory.FlexiblePrefix, OAI.FKCRT.Inventory.Letter.increment, OAI.FKCRT.Inventory.EmptyReducing, OAI.FKCRT.Inventory.intervalWord

39. lemma OAI.FKCRT.Inventory.flexiblePrefix_future_measurable line 449
40. lemma OAI.FKCRT.Inventory.flexiblePrefix_measurable line 460
41. lemma OAI.FKCRT.Inventory.flexiblePrefix_positive line 462
42. lemma OAI.FKCRT.Inventory.goodRight_forced_positive line 478
43. def OAI.FKCRT.Inventory.piecesFrom line 489
44. lemma OAI.FKCRT.Inventory.piecesFrom_preserving line 490
45. def OAI.FKCRT.Inventory.pieceSeamEvent line 495
46. lemma OAI.FKCRT.Inventory.pieceSeamEvent_measurable line 497
47. theorem OAI.FKCRT.Inventory.piece_seam_uniform line 504

    Source documentation

    Uniform success for the actual independent shortened-L and genuine-R laws. Raw stopping-word transport is separate: no finite stopping-length mean is used.

    theorem piece_seam_uniform (P : Parameters) : ∃ δ : ℝ,0<δ ∧ ∀ h : ℕ,
        ENNReal.ofReal δ≤((naturalPiecesLaw (shortLeftLaw P)).prod (naturalPiecesLaw (rightLaw P))) (pieceSeamEvent h) := by
    …

    Mentions: OAI.FKCRT.Inventory.Parameters, OAI.FKCRT.Inventory.naturalPiecesLaw, OAI.FKCRT.Inventory.shortLeftLaw, OAI.FKCRT.Inventory.rightLaw, OAI.FKCRT.Inventory.pieceSeamEvent