OAI/Probability/FKMaps/Offspring.lean

GitHub source file

123 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.FKCRT.TreeCoding.CriticalEvenOffspring line 13
  2. def OAI.FKCRT.TreeCoding.CriticalEvenOffspring.variance line 24
  3. def OAI.FKCRT.TreeCoding.CriticalEvenOffspring.sigma line 28
  4. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.summable_variance line 32
  5. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.variance_pos line 42
  6. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.sigma_pos line 49
  7. def OAI.FKCRT.TreeCoding.CriticalEvenOffspring.law line 53
  8. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.law_apply line 60
  9. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.law_singleton line 66
  10. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.law_real_singleton line 71
  11. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.integrable_iff line 76
  12. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.integral_eq_tsum line 85
  13. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.integrable_id line 93
  14. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.integrable_sq line 99
  15. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.integral_id line 105
  16. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.integrable_step line 111
  17. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.integral_step line 116
  18. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.integrable_step_sq line 122
  19. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.integral_step_sq line 128
  20. def OAI.FKCRT.TreeCoding.CriticalEvenOffspring.standardStep line 134
  21. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.integral_standardStep line 138
  22. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.integral_standardStep_sq line 143
  23. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.charFun_power_limit line 149
  24. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.charFun_gaussian_bound line 157
  25. def OAI.FKCRT.TreeCoding.CriticalEvenOffspring.iidLaw line 187
  26. instance OAI.FKCRT.TreeCoding.(instance at line 191) line 191
  27. def OAI.FKCRT.TreeCoding.totalStep line 196
  28. lemma OAI.FKCRT.TreeCoding.totalStep_eq_sum_sub line 199
  29. lemma OAI.FKCRT.TreeCoding.totalStep_measurable line 204
  30. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.ae_even line 209
  31. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.iid_ae_even line 218
  32. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.iid_totalStep_parity line 225
  33. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.iid_marginal_map line 234
  34. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.charFun_step_scale line 243
  35. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.iid_charFun line 256
  36. def OAI.FKCRT.TreeCoding.CriticalEvenOffspring.streamLaw line 276
  37. instance OAI.FKCRT.TreeCoding.(instance at line 280) line 280
  38. def OAI.FKCRT.TreeCoding.CriticalEvenOffspring.streamStep line 285
  39. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.standardStep_memLp line 289
  40. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.streamStep_memLp line 295
  41. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.streamStep_indep line 301
  42. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.streamStep_ident line 306
  43. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.streamStep_integral line 313
  44. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.streamStep_integral_sq line 322
  45. theorem OAI.FKCRT.TreeCoding.CriticalEvenOffspring.streamWalk_CLT line 331
  46. def OAI.FKCRT.TreeCoding.CriticalEvenOffspring.iidWalk line 341
  47. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.iidWalk_measurable line 347
  48. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.stream_restrict_law line 352
  49. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.iidWalk_restrict line 360
  50. theorem OAI.FKCRT.TreeCoding.CriticalEvenOffspring.iidWalk_CLT line 379
  51. def OAI.FKCRT.TreeCoding.iidSplit line 395
  52. lemma OAI.FKCRT.TreeCoding.iidSplit_fst line 400
  53. lemma OAI.FKCRT.TreeCoding.iidSplit_snd line 404
  54. def OAI.FKCRT.TreeCoding.stopTime line 408
  55. def OAI.FKCRT.TreeCoding.stopPath line 413
  56. lemma OAI.FKCRT.TreeCoding.stopPath_apply line 417
  57. lemma OAI.FKCRT.TreeCoding.stopPath_lipschitz line 421
  58. lemma OAI.FKCRT.TreeCoding.continuous_stopPath line 430
  59. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.iidWalk_endpoint line 434
  60. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.iidWalk_agree_prefix line 450
  61. def OAI.FKCRT.TreeCoding.CriticalEvenOffspring.prefixWalk line 478
  62. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.prefixWalk_eq line 483
  63. lemma OAI.FKCRT.TreeCoding.norm_tsum_smul_lt_one line 495
  64. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.charFun_tsum line 528
  65. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.charFun_lt_one line 537
  66. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.charFun_compact_gap line 573
  67. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.charFun_global_gaussian line 602
  68. def OAI.FKCRT.TreeCoding.CriticalEvenOffspring.fourierCutoff line 628
  69. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.cutoff_measurable line 634
  70. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.cutoff_pointwise line 641
  71. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.cutoff_gaussian_bound line 656
  72. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.cutoff_L1_limit line 681
  73. lemma OAI.FKCRT.TreeCoding.integral_exp_even_int line 705
  74. lemma OAI.FKCRT.TreeCoding.integral_exp_even_int' line 729
  75. lemma OAI.FKCRT.TreeCoding.spanTwo_inversion line 737
  76. def OAI.FKCRT.TreeCoding.CriticalEvenOffspring.siteFourier line 787
  77. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.siteFourier_integral line 793
  78. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.siteFourier_probability line 834
  79. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.iid_site_incompatible line 847
  80. theorem OAI.FKCRT.TreeCoding.CriticalEvenOffspring.iid_site_uniform_bound line 863
  81. lemma OAI.FKCRT.TreeCoding.totalStep_succAbove line 887
  82. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.iid_coordinate_site line 892
  83. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.law_real_set line 913
  84. lemma OAI.FKCRT.TreeCoding.real_measure_coordinate_decomposition line 925
  85. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.iid_coordinate_tail_sum line 942
  86. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.iid_coordinate_tail_bound line 971
  87. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.iid_max_tail_bound line 1003
  88. lemma OAI.FKCRT.TreeCoding.gaussian_fourier_shift line 1028
  89. lemma OAI.FKCRT.TreeCoding.gaussian_phase_integrable line 1049
  90. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.siteFourier_integrable line 1061
  91. def OAI.FKCRT.TreeCoding.CriticalEvenOffspring.localCLTError line 1071
  92. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.siteFourier_gaussian_error line 1075
  93. theorem OAI.FKCRT.TreeCoding.CriticalEvenOffspring.uniform_local_limit line 1099
  94. lemma OAI.FKCRT.TreeCoding.gaussianProfile_hasDerivAt line 1125
  95. lemma OAI.FKCRT.TreeCoding.gaussianProfile_deriv_bound line 1132
  96. lemma OAI.FKCRT.TreeCoding.gaussianProfile_lipschitz line 1142
  97. lemma OAI.FKCRT.TreeCoding.gaussianProfile_sub_bound line 1150
  98. theorem OAI.FKCRT.TreeCoding.CriticalEvenOffspring.local_limit_oscillation line 1155
  99. theorem OAI.FKCRT.TreeCoding.CriticalEvenOffspring.suffix_site_oscillation line 1191
  100. lemma OAI.FKCRT.TreeCoding.totalStep_split line 1229
  101. lemma OAI.FKCRT.TreeCoding.iidSplit_preserving line 1234
  102. lemma OAI.FKCRT.TreeCoding.iid_prefix_test_endpoint line 1241
  103. lemma OAI.FKCRT.TreeCoding.integral_cond_eq_div line 1277
  104. def OAI.FKCRT.TreeCoding.endpointWindow line 1284
  105. lemma OAI.FKCRT.TreeCoding.endpointWindow_apply line 1288
  106. lemma OAI.FKCRT.TreeCoding.iid_prefix_test_window line 1294
  107. lemma OAI.FKCRT.TreeCoding.normalized_integral_stability line 1341
  108. lemma OAI.FKCRT.TreeCoding.finite_window_stability line 1415
  109. lemma OAI.FKCRT.TreeCoding.iid_site_convolution line 1481
  110. theorem OAI.FKCRT.TreeCoding.iid_prefix_window_bound line 1495
  111. def OAI.FKCRT.TreeCoding.softCutoff line 1549
  112. lemma OAI.FKCRT.TreeCoding.softCutoff_continuous line 1552
  113. lemma OAI.FKCRT.TreeCoding.softCutoff_nonneg line 1557
  114. lemma OAI.FKCRT.TreeCoding.softCutoff_le_one line 1560
  115. lemma OAI.FKCRT.TreeCoding.softCutoff_pos_iff line 1566
  116. lemma OAI.FKCRT.TreeCoding.softCutoff_support line 1572
  117. lemma OAI.FKCRT.TreeCoding.softCutoff_integrable line 1579
  118. def OAI.FKCRT.TreeCoding.latticeWindow line 1590
  119. lemma OAI.FKCRT.TreeCoding.mem_latticeWindow_iff line 1595
  120. lemma OAI.FKCRT.TreeCoding.softCutoff_scaled_pos_iff line 1609
  121. lemma OAI.FKCRT.TreeCoding.endpointWindow_softCutoff line 1614
  122. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.iid_endpointWindow_ae line 1626
  123. theorem OAI.FKCRT.TreeCoding.CriticalEvenOffspring.prefix_soft_bound line 1639