OAI/Probability/FKMaps/PathCLT.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.FKCRT.TreeCoding.pathApprox_random_tendstoInMeasure line 13
  2. lemma OAI.FKCRT.TreeCoding.hat_gridPoint line 25
  3. lemma OAI.FKCRT.TreeCoding.interpolation_gridPoint line 44
  4. def OAI.FKCRT.TreeCoding.coarseWalk line 50
  5. def OAI.FKCRT.TreeCoding.coarseIndex line 53
  6. lemma OAI.FKCRT.TreeCoding.coarseWalk_vertex line 57
  7. lemma OAI.FKCRT.TreeCoding.coarse_grid_dist_le line 64
  8. lemma OAI.FKCRT.TreeCoding.coarseWalk_error_le line 82
  9. def OAI.FKCRT.TreeCoding.cumulative line 107
  10. lemma OAI.FKCRT.TreeCoding.continuous_cumulative line 110
  11. lemma OAI.FKCRT.TreeCoding.cumulative_nat line 118
  12. lemma OAI.FKCRT.TreeCoding.cumulative_div line 125
  13. lemma OAI.FKCRT.TreeCoding.sum_range_blocks line 132
  14. lemma OAI.FKCRT.TreeCoding.cumulative_blocks line 140
  15. lemma OAI.FKCRT.TreeCoding.coarseWalk_eq_cumulative line 149
  16. lemma OAI.FKCRT.TreeCoding.map_uncurry_pi line 157
  17. lemma OAI.FKCRT.TreeCoding.iIndepFun_uncurry_pi line 174
  18. lemma OAI.FKCRT.TreeCoding.tendstoInDistribution_pi_indep line 207
  19. lemma OAI.FKCRT.TreeCoding.identDistrib_pi_indep line 237
  20. lemma OAI.FKCRT.TreeCoding.blockIndex_injective line 252
  21. lemma OAI.FKCRT.TreeCoding.identDistrib_iid_blocks line 268
  22. lemma OAI.FKCRT.TreeCoding.tendstoInDistribution_transport line 297
  23. lemma OAI.FKCRT.TreeCoding.tendstoInDistribution_reindex line 318
  24. lemma OAI.FKCRT.TreeCoding.identDistrib_comp_measurePreserving line 327
  25. lemma OAI.FKCRT.TreeCoding.iid_block_standard_CLT line 336
  26. lemma OAI.FKCRT.TreeCoding.nat_div_ratio_tendsto line 372
  27. lemma OAI.FKCRT.TreeCoding.sqrt_nat_div_ratio_tendsto line 386
  28. lemma OAI.FKCRT.TreeCoding.iid_block_scaled_CLT line 391
  29. def OAI.FKCRT.TreeCoding.gridTime line 426
  30. lemma OAI.FKCRT.TreeCoding.gridTime_mono line 428
  31. def OAI.FKCRT.TreeCoding.meshIncrement line 433
  32. lemma OAI.FKCRT.TreeCoding.brownian_mesh_independent line 436
  33. lemma OAI.FKCRT.TreeCoding.brownian_mesh_hasLaw line 441
  34. lemma OAI.FKCRT.TreeCoding.brownian_normalized_mesh_hasLaw line 453
  35. def OAI.FKCRT.TreeCoding.brownianPath line 463
  36. lemma OAI.FKCRT.TreeCoding.brownianPath_ae_eq line 466
  37. lemma OAI.FKCRT.TreeCoding.brownianPath_aemeasurable line 473
  38. lemma OAI.FKCRT.TreeCoding.cumulative_mesh line 493
  39. lemma OAI.FKCRT.TreeCoding.coarseWalk_CLT line 503
  40. lemma OAI.FKCRT.TreeCoding.integral_lipschitz_approx_bound line 531
  41. theorem OAI.FKCRT.TreeCoding.tendstoInDistribution_of_approximations line 582
  42. theorem OAI.FKCRT.TreeCoding.iid_scaledWalk_CLT line 634