OAI/Probability/FKMaps/BridgeLimit.lean

GitHub source file

61 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.FKCRT.TreeCoding.bridgePath line 13
  2. lemma OAI.FKCRT.TreeCoding.bridgePath_aemeasurable line 16
  3. lemma OAI.FKCRT.TreeCoding.bridgePath_ae_eq line 21
  4. lemma OAI.FKCRT.TreeCoding.bridge_joint_gaussian line 30
  5. lemma OAI.FKCRT.TreeCoding.bridge_covariance_endpoint line 55
  6. lemma OAI.FKCRT.TreeCoding.bridge_process_indep_endpoint line 69
  7. lemma OAI.FKCRT.TreeCoding.indepFun_of_measurableEmbedding_left line 78
  8. lemma OAI.FKCRT.TreeCoding.bridgePath_indep_endpoint line 86
  9. lemma OAI.FKCRT.TreeCoding.gaussian_softCutoff_pos line 109
  10. lemma OAI.FKCRT.TreeCoding.brownian_softCutoff_pos line 118
  11. lemma OAI.FKCRT.TreeCoding.brownian_dist_bridge_le line 125
  12. theorem OAI.FKCRT.TreeCoding.brownian_soft_bridge_bound line 137
  13. lemma OAI.FKCRT.TreeCoding.integral_tendsto_of_tendstoInDistribution line 207
  14. theorem OAI.FKCRT.TreeCoding.soft_weighted_tendsto line 223
  15. lemma OAI.FKCRT.TreeCoding.tendsto_of_soft_windows line 245
  16. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.iid_endpoint_positive line 266
  17. def OAI.FKCRT.TreeCoding.CriticalEvenOffspring.iidBridgeLaw line 295
  18. instance OAI.FKCRT.TreeCoding.(instance at line 298) line 298
  19. def OAI.FKCRT.TreeCoding.CriticalEvenOffspring.bridgeConstant line 302
  20. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.bridgeConstant_pos line 305
  21. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.iid_endpoint_limit line 309
  22. lemma OAI.FKCRT.TreeCoding.bridge_soft_numeric line 344
  23. lemma OAI.FKCRT.TreeCoding.exists_bridge_cutoff line 372
  24. lemma OAI.FKCRT.TreeCoding.bridge_split_parameters line 388
  25. lemma OAI.FKCRT.TreeCoding.bridge_suffix_tendsto line 421
  26. theorem OAI.FKCRT.TreeCoding.CriticalEvenOffspring.stopped_soft_error line 429
  27. theorem OAI.FKCRT.TreeCoding.CriticalEvenOffspring.stopped_bridge_integral_limit line 496
  28. theorem OAI.FKCRT.TreeCoding.CriticalEvenOffspring.stopped_bridge_CLT line 539
  29. lemma OAI.FKCRT.TreeCoding.hat_reverse line 562
  30. lemma OAI.FKCRT.TreeCoding.interpolation_reverse line 572
  31. lemma OAI.FKCRT.TreeCoding.reverse_partial_sum line 586
  32. lemma OAI.FKCRT.TreeCoding.interpolation_increments_reverse line 599
  33. lemma OAI.FKCRT.TreeCoding.measurePreserving_cond line 608
  34. def OAI.FKCRT.TreeCoding.reverseArray line 621
  35. lemma OAI.FKCRT.TreeCoding.reverseArray_apply line 624
  36. lemma OAI.FKCRT.TreeCoding.reverseArray_preserving line 629
  37. lemma OAI.FKCRT.TreeCoding.reverseArray_sum line 634
  38. lemma OAI.FKCRT.TreeCoding.reverseArray_cond_preserving line 638
  39. lemma OAI.FKCRT.TreeCoding.stopPath_one line 647
  40. lemma OAI.FKCRT.TreeCoding.stopPath_zero line 651
  41. lemma OAI.FKCRT.TreeCoding.continuous_stopPath_time line 655
  42. lemma OAI.FKCRT.TreeCoding.dist_stop_reverse_le line 659
  43. def OAI.FKCRT.TreeCoding.earlyTime line 682
  44. lemma OAI.FKCRT.TreeCoding.earlyTime_pos line 685
  45. lemma OAI.FKCRT.TreeCoding.earlyTime_lt_one line 687
  46. lemma OAI.FKCRT.TreeCoding.earlyTime_tendsto line 692
  47. lemma OAI.FKCRT.TreeCoding.lateTime_tendsto line 697
  48. lemma OAI.FKCRT.TreeCoding.norm_stop_early_tendsto line 700
  49. lemma OAI.FKCRT.TreeCoding.stop_late_tendsto line 705
  50. def OAI.FKCRT.TreeCoding.freezeGauge line 709
  51. lemma OAI.FKCRT.TreeCoding.freezeGauge_continuous line 712
  52. lemma OAI.FKCRT.TreeCoding.freezeGauge_nonneg line 716
  53. lemma OAI.FKCRT.TreeCoding.freezeGauge_abs_le line 719
  54. lemma OAI.FKCRT.TreeCoding.integral_reverse_freeze_bound line 724
  55. lemma OAI.FKCRT.TreeCoding.early_gauge_integral_tendsto line 767
  56. lemma OAI.FKCRT.TreeCoding.late_integral_tendsto line 781
  57. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.iidWalk_reverse line 793
  58. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.bridge_reverse_preserving line 802
  59. lemma OAI.FKCRT.TreeCoding.bridgePath_zero_ae line 806
  60. theorem OAI.FKCRT.TreeCoding.CriticalEvenOffspring.bridge_integral_limit line 814
  61. theorem OAI.FKCRT.TreeCoding.CriticalEvenOffspring.iidBridge_CLT line 866