OAI/Probability/FKMaps/InventoryDrift.lean

GitHub source file

81 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.FKCRT.Inventory.tail line 10
  2. lemma OAI.FKCRT.Inventory.tail_zero line 11
  3. lemma OAI.FKCRT.Inventory.tail_tail line 12
  4. lemma OAI.FKCRT.Inventory.measurable_tail line 15
  5. lemma OAI.FKCRT.Inventory.tail_preserving line 18
  6. lemma OAI.FKCRT.Inventory.revealed_add line 22
  7. lemma OAI.FKCRT.Inventory.revealed_append_newest line 30
  8. lemma OAI.FKCRT.Inventory.revealed_extension line 35
  9. def OAI.FKCRT.Inventory.firstType line 40
  10. lemma OAI.FKCRT.Inventory.firstType_of_hit line 43
  11. lemma OAI.FKCRT.Inventory.firstType_of_survivor line 49
  12. lemma OAI.FKCRT.Inventory.measurable_firstType line 67
  13. def OAI.FKCRT.Inventory.typedRevealed line 76
  14. lemma OAI.FKCRT.Inventory.typedRevealed_erase line 79
  15. lemma OAI.FKCRT.Inventory.typedRevealed_append_newest line 83
  16. lemma OAI.FKCRT.Inventory.typedRevealed_valid line 98
  17. def OAI.FKCRT.Inventory.D line 118
  18. def OAI.FKCRT.Inventory.Dsum line 119
  19. lemma OAI.FKCRT.Inventory.abs_D line 121
  20. lemma OAI.FKCRT.Inventory.measurable_D line 122
  21. lemma OAI.FKCRT.Inventory.measurable_Dsum line 125
  22. lemma OAI.FKCRT.Inventory.typedRevealed_sum line 128
  23. lemma OAI.FKCRT.Inventory.D_shift line 133
  24. lemma OAI.FKCRT.Inventory.Dsum_add line 135
  25. lemma OAI.FKCRT.Inventory.Dsum_no_survivor line 138
  26. lemma OAI.FKCRT.Inventory.Dsum_at_hit line 148
  27. lemma OAI.FKCRT.Inventory.abs_Dsum_le line 159
  28. lemma OAI.FKCRT.Inventory.law_flip_preserving line 172
  29. def OAI.FKCRT.Inventory.flipStream line 192
  30. lemma OAI.FKCRT.Inventory.measurable_flipStream line 193
  31. lemma OAI.FKCRT.Inventory.flipStream_preserving line 195
  32. lemma OAI.FKCRT.Inventory.revealed_flip line 202
  33. lemma OAI.FKCRT.Inventory.firstSurvivor_flip line 205
  34. lemma OAI.FKCRT.Inventory.firstType_flip_of_hit line 214
  35. lemma OAI.FKCRT.Inventory.raw_indep_tail line 221
  36. lemma OAI.FKCRT.Inventory.raw_fun_indep_tail line 239
  37. lemma OAI.FKCRT.Inventory.integrable_Dsum line 244
  38. def OAI.FKCRT.Inventory.hitType line 253

    Source documentation

    Signed first-survivor event. Unlike the totalized first type, this is raw-prefix measurable.

    def hitType (n : ℕ) (x : ℕ → Letter) : ℝ :=
…

    Mentions: OAI.FKCRT.Inventory.Letter

  39. lemma OAI.FKCRT.Inventory.measurable_hitType_raw line 256
  40. lemma OAI.FKCRT.Inventory.measurable_hitType line 268
  41. lemma OAI.FKCRT.Inventory.abs_hitType_le line 270
  42. lemma OAI.FKCRT.Inventory.integrable_hitType line 275
  43. lemma OAI.FKCRT.Inventory.hitType_flip line 278
  44. lemma OAI.FKCRT.Inventory.integral_hitType line 284
  45. lemma OAI.FKCRT.Inventory.integral_hitType_mul_older line 290
  46. def OAI.FKCRT.Inventory.T line 311
  47. lemma OAI.FKCRT.Inventory.measurable_T line 312
  48. lemma OAI.FKCRT.Inventory.abs_T line 314
  49. lemma OAI.FKCRT.Inventory.T_sq line 317
  50. lemma OAI.FKCRT.Inventory.bounded_integrable line 320
  51. lemma OAI.FKCRT.Inventory.measurable_Dsum_real line 324
  52. lemma OAI.FKCRT.Inventory.abs_Dsum_real_le line 326
  53. lemma OAI.FKCRT.Inventory.integrable_T_Dsum line 328
  54. def OAI.FKCRT.Inventory.truncK line 336
  55. lemma OAI.FKCRT.Inventory.measurable_truncK line 338
  56. lemma OAI.FKCRT.Inventory.integrable_truncK line 341
  57. lemma OAI.FKCRT.Inventory.truncK_nonneg line 348
  58. lemma OAI.FKCRT.Inventory.truncK_le line 351
  59. lemma OAI.FKCRT.Inventory.truncK_tendsto line 356
  60. def OAI.FKCRT.Inventory.olderCorrection line 371

    Source documentation

    The signed contribution of letters strictly older than the first survivor.

    def olderCorrection (m : ℕ) (x : ℕ → Letter) : ℝ :=
…

    Mentions: OAI.FKCRT.Inventory.Letter

  61. lemma OAI.FKCRT.Inventory.integrable_older_term line 373
  62. lemma OAI.FKCRT.Inventory.integrable_olderCorrection line 381
  63. lemma OAI.FKCRT.Inventory.integral_olderCorrection line 383
  64. lemma OAI.FKCRT.Inventory.olderCorrection_hit line 387
  65. lemma OAI.FKCRT.Inventory.olderCorrection_nohit line 399
  66. lemma OAI.FKCRT.Inventory.covariance_pointwise line 408
  67. def OAI.FKCRT.Inventory.covariance line 440
  68. lemma OAI.FKCRT.Inventory.covariance_lower line 441
  69. lemma OAI.FKCRT.Inventory.integral_assignedSign line 469
  70. lemma OAI.FKCRT.Inventory.abs_assignedSign_real line 473
  71. lemma OAI.FKCRT.Inventory.measurable_D_real line 475
  72. lemma OAI.FKCRT.Inventory.Dsum_newest line 477
  73. lemma OAI.FKCRT.Inventory.integral_newest_older line 481
  74. def OAI.FKCRT.Inventory.varianceSum line 507
  75. lemma OAI.FKCRT.Inventory.varianceSum_nonneg line 508
  76. lemma OAI.FKCRT.Inventory.integrable_Dsum_sq line 510
  77. lemma OAI.FKCRT.Inventory.integrable_newest_older line 516
  78. lemma OAI.FKCRT.Inventory.varianceSum_increment line 525
  79. lemma OAI.FKCRT.Inventory.varianceSum_increment_le line 546
  80. theorem OAI.FKCRT.Inventory.integral_K_strict_drift line 553

    Source documentation

    Strict drift of the actual iid inventory word, without assuming a finite mean stopping time.

    theorem integral_K_strict_drift (P : Parameters) :
    (∫ x,(K x:ℝ) ∂streamLaw P ℕ) ≤ 1/(2*P.p) := by
…

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

  81. theorem OAI.FKCRT.Inventory.integral_K_lt_one line 582