OAI/Probability/FKMaps/SeamLengths.lean

GitHub source file

65 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.FKCRT.Inventory.upPath line 9
  2. def OAI.FKCRT.Inventory.firstUp line 10
  3. lemma OAI.FKCRT.Inventory.upPath_adapted line 11
  4. lemma OAI.FKCRT.Inventory.firstUp_stopping line 16
  5. lemma OAI.FKCRT.Inventory.firstUp_measurable line 18
  6. lemma OAI.FKCRT.Inventory.upPath_step line 19
  7. lemma OAI.FKCRT.Inventory.upPath_initial line 24
  8. lemma OAI.FKCRT.Inventory.upPath_martingale line 28
  9. lemma OAI.FKCRT.Inventory.firstUp_finite line 33
  10. lemma OAI.FKCRT.Inventory.firstUp_of_hit_iff line 47
  11. lemma OAI.FKCRT.Inventory.firstUp_prefix_lt line 56
  12. lemma OAI.FKCRT.Inventory.stoppedWord_up_eq_leftWord line 70
  13. def OAI.FKCRT.Inventory.rawLeftLaw line 90
  14. instance OAI.FKCRT.Inventory.rawLeftLaw_probability line 91
  15. lemma OAI.FKCRT.Inventory.rawLeftLaw_normal line 93
  16. lemma OAI.FKCRT.Inventory.firstUp_add line 112
  17. lemma OAI.FKCRT.Inventory.stoppedWord_up_add line 134
  18. def OAI.FKCRT.Inventory.leftPieces line 140
  19. lemma OAI.FKCRT.Inventory.leftPieces_measurable line 141
  20. lemma OAI.FKCRT.Inventory.leftPieces_preserving line 145
  21. lemma OAI.FKCRT.Inventory.leftPieces_tail line 159
  22. lemma OAI.FKCRT.Inventory.stoppedWord_up_pieces line 165
  23. lemma OAI.FKCRT.Inventory.leftPrefix_identDistrib line 183
  24. def OAI.FKCRT.Inventory.mappedPieceLaw line 208
  25. instance OAI.FKCRT.Inventory.mappedPieceLaw_probability line 209
  26. def OAI.FKCRT.Inventory.mapPieces line 211
  27. lemma OAI.FKCRT.Inventory.mapPieces_preserving line 212
  28. lemma OAI.FKCRT.Inventory.run_normalPieces line 216
  29. lemma OAI.FKCRT.Inventory.pieceSeamEvent_normal_preimage line 222
  30. lemma OAI.FKCRT.Inventory.pieceSeam_normal_measure line 230
  31. lemma OAI.FKCRT.Inventory.reverse_reversePiecesPrefix line 246
  32. lemma OAI.FKCRT.Inventory.chronologicalRight_identDistrib line 250
  33. def OAI.FKCRT.Inventory.rawSeamWord line 260
  34. lemma OAI.FKCRT.Inventory.rawSeamWord_measurable line 262
  35. lemma OAI.FKCRT.Inventory.rawSeam_measure line 266
  36. theorem OAI.FKCRT.Inventory.raw_seam_uniform line 287

    Source documentation

    Source ladder:uniform for the actual two independent raw hit intervals. No conditioning on success or stopping-length moment is assumed.

    theorem raw_seam_uniform (P : Parameters) : ∃ δ : ℝ,0<δ ∧ ∀ h : ℕ,0<h →
    ENNReal.ofReal δ≤((streamLaw P ℕ).prod (streamLaw P ℕ)) {z | EmptyReducing (rawSeamWord h z)} := by
…

    Mentions: OAI.FKCRT.Inventory.Parameters, OAI.FKCRT.Inventory.streamLaw, OAI.FKCRT.Inventory.EmptyReducing, OAI.FKCRT.Inventory.rawSeamWord

  37. lemma OAI.FKCRT.SimpleWalk.sign_not line 304
  38. def OAI.FKCRT.SimpleWalk.reflectPath line 305
  39. lemma OAI.FKCRT.SimpleWalk.reflectPath_sum line 306
  40. lemma OAI.FKCRT.SimpleWalk.not_coin_preserving line 312
  41. lemma OAI.FKCRT.SimpleWalk.reflectPath_preserving line 319
  42. def OAI.FKCRT.Inventory.rawUpperSurvival line 329
  43. lemma OAI.FKCRT.Inventory.rawUpperSurvival_measure line 330
  44. lemma OAI.FKCRT.Inventory.stoppedWord_length_of_hit line 358
  45. lemma OAI.FKCRT.Inventory.stoppedWord_length_top line 362
  46. lemma OAI.FKCRT.Inventory.down_length_tail_subset line 364
  47. lemma OAI.FKCRT.Inventory.up_length_tail_subset line 377
  48. theorem OAI.FKCRT.Inventory.stopped_lengths_tail line 392

    Source documentation

    Both actual first-passage lengths obey the same uniform square-root tail.

    theorem stopped_lengths_tail : ∃ C : ℝ,0<C ∧ ∀ (P : Parameters) (h n : ℕ),0<h → 0<n →
    (streamLaw P ℕ).real {x | n<(stoppedWord (firstDown h) x).length} ≤ C*h/Real.sqrt n ∧
    (streamLaw P ℕ).real {x | n<(stoppedWord (firstUp h) x).length} ≤ C*h/Real.sqrt n := by
…

    Mentions: OAI.FKCRT.Inventory.Parameters, OAI.FKCRT.Inventory.streamLaw, OAI.FKCRT.Inventory.stoppedWord, OAI.FKCRT.Inventory.firstDown, OAI.FKCRT.Inventory.firstUp

  49. lemma OAI.FKCRT.Inventory.rawSeamWord_length line 415
  50. lemma OAI.FKCRT.Inventory.rawSeam_length_tail line 418
  51. theorem OAI.FKCRT.Inventory.short_seam_uniform line 450

    Source documentation

    Successful genuine seam intervals have a uniform positive probability of quadratic length; no independence of length and success is used.

    theorem short_seam_uniform (P : Parameters) : ∃ (δ : ℝ) (A : ℕ),0<δ ∧ 0<A ∧ ∀ h : ℕ,0<h →
    δ ≤ ((streamLaw P ℕ).prod (streamLaw P ℕ)).real
      {z | EmptyReducing (rawSeamWord h z) ∧ (rawSeamWord h z).length≤2*A*h^2} := by
…

    Mentions: OAI.FKCRT.Inventory.Parameters, OAI.FKCRT.Inventory.streamLaw, OAI.FKCRT.Inventory.EmptyReducing, OAI.FKCRT.Inventory.rawSeamWord

  52. def OAI.FKCRT.Inventory.letterSplit line 502
  53. lemma OAI.FKCRT.Inventory.letterSplit_preserving line 505
  54. lemma OAI.FKCRT.Inventory.letterSplit_word line 510
  55. def OAI.FKCRT.Inventory.reverseLetters line 514
  56. lemma OAI.FKCRT.Inventory.reverseLetters_apply line 516
  57. lemma OAI.FKCRT.Inventory.reverseLetters_word line 519
  58. lemma OAI.FKCRT.Inventory.reverseLetters_preserving line 529
  59. def OAI.FKCRT.Inventory.seamWord line 533
  60. lemma OAI.FKCRT.Inventory.seamWord_measurable line 534
  61. lemma OAI.FKCRT.Inventory.seamWord_length line 538
  62. lemma OAI.FKCRT.Inventory.seamWord_preserving line 540
  63. def OAI.FKCRT.Inventory.emptyProb line 559
  64. lemma OAI.FKCRT.Inventory.emptyProb_nonneg line 560
  65. lemma OAI.FKCRT.Inventory.seamWord_empty_measure line 561