OAI/Probability/FKMaps/Vervaat.lean

GitHub source file

99 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.FKCRT.TreeCoding.clipTime line 13
  2. lemma OAI.FKCRT.TreeCoding.continuous_clipTime line 15
  3. lemma OAI.FKCRT.TreeCoding.clipTime_coe line 17
  4. lemma OAI.FKCRT.TreeCoding.clipTime_of_nonpos line 20
  5. lemma OAI.FKCRT.TreeCoding.clipTime_of_one_le line 23
  6. def OAI.FKCRT.TreeCoding.cyclePath line 26
  7. lemma OAI.FKCRT.TreeCoding.cyclePath_zero line 35
  8. lemma OAI.FKCRT.TreeCoding.cyclePath_one line 40
  9. lemma OAI.FKCRT.TreeCoding.cyclePath_apply_left line 46
  10. lemma OAI.FKCRT.TreeCoding.cyclePath_apply_right line 55
  11. lemma OAI.FKCRT.TreeCoding.continuous_cyclePath line 65
  12. lemma OAI.FKCRT.TreeCoding.cyclePath_nonneg line 80
  13. lemma OAI.FKCRT.TreeCoding.exists_minTime line 89
  14. lemma OAI.FKCRT.TreeCoding.exists_firstMinimum line 94
  15. def OAI.FKCRT.TreeCoding.minTime line 103
  16. lemma OAI.FKCRT.TreeCoding.minTime_spec line 105
  17. lemma OAI.FKCRT.TreeCoding.minTime_first line 108
  18. def OAI.FKCRT.TreeCoding.UniqueMinimum line 111
  19. lemma OAI.FKCRT.TreeCoding.minimum_stable line 114
  20. lemma OAI.FKCRT.TreeCoding.continuousAt_minTime line 142
  21. def OAI.FKCRT.TreeCoding.vervaat line 150
  22. lemma OAI.FKCRT.TreeCoding.continuousAt_vervaat line 152
  23. lemma OAI.FKCRT.TreeCoding.vervaat_zero line 156
  24. lemma OAI.FKCRT.TreeCoding.vervaat_one line 158
  25. lemma OAI.FKCRT.TreeCoding.vervaat_nonneg line 160
  26. def OAI.FKCRT.TreeCoding.restrictedMin line 163
  27. lemma OAI.FKCRT.TreeCoding.restrictedMin_spec line 167
  28. lemma OAI.FKCRT.TreeCoding.restrictedMin_lipschitz line 173
  29. lemma OAI.FKCRT.TreeCoding.minTime_le_iff line 189
  30. lemma OAI.FKCRT.TreeCoding.measurable_minTime line 205
  31. lemma OAI.FKCRT.TreeCoding.measurable_vervaat line 217
  32. def OAI.FKCRT.TreeCoding.reversePath line 220
  33. lemma OAI.FKCRT.TreeCoding.reversePath_apply line 223
  34. lemma OAI.FKCRT.TreeCoding.reversePath_lipschitz line 226
  35. def OAI.FKCRT.TreeCoding.lastMinTime line 234
  36. lemma OAI.FKCRT.TreeCoding.lastMinTime_spec line 237
  37. lemma OAI.FKCRT.TreeCoding.lastMinTime_last line 242
  38. lemma OAI.FKCRT.TreeCoding.measurable_lastMinTime line 250
  39. def OAI.FKCRT.TreeCoding.HasUniqueMinimum line 253
  40. lemma OAI.FKCRT.TreeCoding.hasUniqueMinimum_iff line 255
  41. lemma OAI.FKCRT.TreeCoding.measurableSet_hasUniqueMinimum line 268
  42. def OAI.FKCRT.TreeCoding.tiltPath line 272
  43. lemma OAI.FKCRT.TreeCoding.tiltPath_apply line 275
  44. lemma OAI.FKCRT.TreeCoding.continuous_tiltPath line 278
  45. def OAI.FKCRT.TreeCoding.TiltMinimum line 281
  46. lemma OAI.FKCRT.TreeCoding.tiltMinimum_antitone line 284
  47. theorem OAI.FKCRT.TreeCoding.countable_badTilts line 293
  48. lemma OAI.FKCRT.TreeCoding.not_unique_iff_two_minima line 319
  49. theorem OAI.FKCRT.TreeCoding.ae_unique_minimum_tilt line 332
  50. theorem OAI.FKCRT.TreeCoding.IndepFun.ae_unique_minimum_tilt line 347
  51. theorem OAI.FKCRT.TreeCoding.brownian_unique_minimum line 358
  52. lemma OAI.FKCRT.TreeCoding.indepFun_path_of_coords line 372
  53. def OAI.FKCRT.TreeCoding.prefixTimePath line 389
  54. lemma OAI.FKCRT.TreeCoding.prefixTimePath_apply line 392
  55. lemma OAI.FKCRT.TreeCoding.prefixTimePath_lipschitz line 395
  56. def OAI.FKCRT.TreeCoding.prefixResidual line 403
  57. def OAI.FKCRT.TreeCoding.bridgeAt line 407
  58. lemma OAI.FKCRT.TreeCoding.prefixResidual_aemeasurable line 410
  59. lemma OAI.FKCRT.TreeCoding.prefixResidual_ae_eq line 416
  60. lemma OAI.FKCRT.TreeCoding.prefixResidual_joint_gaussian line 426
  61. lemma OAI.FKCRT.TreeCoding.prefixResidual_covariance_bridgeAt line 455
  62. lemma OAI.FKCRT.TreeCoding.prefixResidual_indep_bridgeAt line 476
  63. lemma OAI.FKCRT.TreeCoding.variance_bridgeAt line 489
  64. lemma OAI.FKCRT.TreeCoding.bridgeAt_nullSingletonClass line 504
  65. theorem OAI.FKCRT.TreeCoding.bridge_prefix_unique_minimum line 513
  66. theorem OAI.FKCRT.TreeCoding.gaussianProcess_map_eq line 531
  67. lemma OAI.FKCRT.TreeCoding.path_law_eq_of_coords line 573
  68. def OAI.FKCRT.TreeCoding.circleTime line 593
  69. lemma OAI.FKCRT.TreeCoding.cyclePath_apply_closed line 598
  70. def OAI.FKCRT.TreeCoding.bbCov line 607
  71. lemma OAI.FKCRT.TreeCoding.bbCov_comm line 609
  72. lemma OAI.FKCRT.TreeCoding.circleTime_covariance line 611
  73. lemma OAI.FKCRT.TreeCoding.circleTime_surj_mod_endpoints line 642
  74. lemma OAI.FKCRT.TreeCoding.cycle_min_zero_iff line 669
  75. lemma OAI.FKCRT.TreeCoding.bridgeAt_gaussian line 685
  76. lemma OAI.FKCRT.TreeCoding.integral_bridgeAt line 690
  77. lemma OAI.FKCRT.TreeCoding.covariance_bridgeAt line 699
  78. lemma OAI.FKCRT.TreeCoding.cyclicBridge_gaussian line 718
  79. lemma OAI.FKCRT.TreeCoding.bridgePath_closed line 731
  80. theorem OAI.FKCRT.TreeCoding.bridgePath_cycle_invariant line 743
  81. def OAI.FKCRT.TreeCoding.minAtSet line 781
  82. lemma OAI.FKCRT.TreeCoding.isClosed_minAtSet line 783
  83. lemma OAI.FKCRT.TreeCoding.measurableSet_minAtSet line 789
  84. lemma OAI.FKCRT.TreeCoding.measure_minAt_eq line 792
  85. lemma OAI.FKCRT.TreeCoding.eq_of_minima_in_unique_prefix line 806
  86. def OAI.FKCRT.TreeCoding.reciprocalTime line 820
  87. lemma OAI.FKCRT.TreeCoding.reciprocalTime_le_half line 823
  88. lemma OAI.FKCRT.TreeCoding.reciprocalTime_injective line 827
  89. lemma OAI.FKCRT.TreeCoding.minAt_zero_null_of_cyclic_prefix line 834
  90. lemma OAI.FKCRT.TreeCoding.bridgePath_law_cyclic line 863
  91. theorem OAI.FKCRT.TreeCoding.bridge_not_minimum_zero line 872
  92. def OAI.FKCRT.TreeCoding.innerCut line 895
  93. lemma OAI.FKCRT.TreeCoding.innerCut_pos line 899
  94. lemma OAI.FKCRT.TreeCoding.innerCut_lt_one line 903
  95. lemma OAI.FKCRT.TreeCoding.exists_lt_innerCut line 908
  96. theorem OAI.FKCRT.TreeCoding.bridge_unique_minimum line 916
  97. theorem OAI.FKCRT.TreeCoding.probabilityMeasure_tendsto_map_aeContinuous line 950
  98. theorem OAI.FKCRT.TreeCoding.TendstoInDistribution.aeContinuous_comp line 981
  99. theorem OAI.FKCRT.TreeCoding.CriticalEvenOffspring.iidVervaat_CLT line 1009