OAI/Probability/FKMaps/InventoryStopping.lean

GitHub source file

67 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.FKCRT.Inventory.revealed line 10
  2. lemma OAI.FKCRT.Inventory.revealed_zero line 13
  3. lemma OAI.FKCRT.Inventory.revealed_succ line 14
  4. lemma OAI.FKCRT.Inventory.revealed_sum line 20
  5. lemma OAI.FKCRT.Inventory.survivor_mono line 25
  6. def OAI.FKCRT.Inventory.rawFiltration line 42
  7. lemma OAI.FKCRT.Inventory.raw_adapted line 45
  8. lemma OAI.FKCRT.Inventory.prefix_measurable line 51
  9. lemma OAI.FKCRT.Inventory.signSum_adapted line 58
  10. lemma OAI.FKCRT.Inventory.raw_sign_martingale line 67
  11. def OAI.FKCRT.Inventory.survivorFlag line 105
  12. def OAI.FKCRT.Inventory.firstSurvivor line 108
  13. lemma OAI.FKCRT.Inventory.survivorFlag_adapted line 110
  14. lemma OAI.FKCRT.Inventory.firstSurvivor_stopping line 114
  15. lemma OAI.FKCRT.Inventory.firstSurvivor_le_iff line 117
  16. lemma OAI.FKCRT.Inventory.firstSurvivor_finite line 129
  17. lemma OAI.FKCRT.Inventory.firstSurvivor_shape line 138
  18. def OAI.FKCRT.Inventory.stoppedDefect line 156
  19. lemma OAI.FKCRT.Inventory.stoppedDefect_martingale line 159
  20. lemma OAI.FKCRT.Inventory.stoppedDefect_nonneg line 165
  21. lemma OAI.FKCRT.Inventory.stoppedDefect_integral line 191
  22. lemma OAI.FKCRT.Inventory.measurableSet_firstSurvivor_eq line 208
  23. lemma OAI.FKCRT.Inventory.measurableSet_firstSurvivor_finite line 212
  24. lemma OAI.FKCRT.Inventory.measurable_firstSurvivor line 220
  25. def OAI.FKCRT.Inventory.K line 229
  26. lemma OAI.FKCRT.Inventory.K_of_hit line 233
  27. lemma OAI.FKCRT.Inventory.measurable_K line 238
  28. lemma OAI.FKCRT.Inventory.stoppedDefect_eq_K line 249
  29. lemma OAI.FKCRT.Inventory.stoppedDefect_tendsto line 265
  30. theorem OAI.FKCRT.Inventory.K_lintegral_le_one line 275

    Source documentation

    The source first optional-stopping bound, without any finite-mean hypothesis on the stopping time.

    theorem K_lintegral_le_one (P : Parameters) :
    ∫⁻ x,ENNReal.ofReal (K x:ℝ) ∂streamLaw P ℕ ≤ 1 := by
…

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

  31. theorem OAI.FKCRT.Inventory.integrable_K line 290
  32. theorem OAI.FKCRT.Inventory.integral_K_le_one line 295
  33. def OAI.FKCRT.Inventory.typeSign line 310
  34. lemma OAI.FKCRT.Inventory.typeSign_not line 311
  35. lemma OAI.FKCRT.Inventory.abs_typeSign line 312
  36. lemma OAI.FKCRT.Inventory.typeSign_sq line 313
  37. def OAI.FKCRT.Inventory.orderType line 315
  38. def OAI.FKCRT.Inventory.assignedSign line 317
  39. lemma OAI.FKCRT.Inventory.abs_assignedSign line 321
  40. structure OAI.FKCRT.Inventory.TypedEvaluation line 325
  41. def OAI.FKCRT.Inventory.TypedEvaluation.erase line 329
  42. def OAI.FKCRT.Inventory.typedStep line 332
  43. def OAI.FKCRT.Inventory.typedRun line 338
  44. def OAI.FKCRT.Inventory.validStep line 342
  45. def OAI.FKCRT.Inventory.ValidTyping line 345
  46. lemma OAI.FKCRT.Inventory.erase_typedStep line 349
  47. lemma OAI.FKCRT.Inventory.erase_typedRun line 358
  48. lemma OAI.FKCRT.Inventory.typedStep_burgers line 364
  49. lemma OAI.FKCRT.Inventory.pop_sign_sum line 371
  50. def OAI.FKCRT.Inventory.typedImbalance line 399
  51. lemma OAI.FKCRT.Inventory.typedStep_imbalance line 402
  52. lemma OAI.FKCRT.Inventory.typedRun_imbalance line 418
  53. lemma OAI.FKCRT.Inventory.sum_typeSign_abs_le line 428
  54. lemma OAI.FKCRT.Inventory.typed_orders_sum_abs_le line 435
  55. lemma OAI.FKCRT.Inventory.typedRun_no_survivor_bound line 440
  56. lemma OAI.FKCRT.Inventory.typed_orders_opposite_sum line 454
  57. lemma OAI.FKCRT.Inventory.typedRun_first_survivor_sum line 465
  58. lemma OAI.FKCRT.Inventory.ValidTyping_append line 485
  59. def OAI.FKCRT.Inventory.Letter.flip line 503
  60. lemma OAI.FKCRT.Inventory.Letter.flip_flip line 507
  61. lemma OAI.FKCRT.Inventory.eligible_flip line 512
  62. lemma OAI.FKCRT.Inventory.pop_flip line 517
  63. def OAI.FKCRT.Inventory.Evaluation.flip line 525
  64. lemma OAI.FKCRT.Inventory.step_flip line 528
  65. lemma OAI.FKCRT.Inventory.run_flip line 535
  66. lemma OAI.FKCRT.Inventory.reduce_flip line 541
  67. lemma OAI.FKCRT.Inventory.burgers_flip_empty_iff line 544