OAI/Analysis/HardSphere/Bridges/Index.lean

GitHub source file

60 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.HardSphere.Wiener.Index line 17
  2. abbrev OAI.HardSphere.Wiener.Noise line 18
  3. abbrev OAI.HardSphere.Wiener.Time line 19
  4. instance OAI.HardSphere.Wiener.(instance at line 20) line 20
  5. instance OAI.HardSphere.Wiener.(instance at line 21) line 21
  6. def OAI.HardSphere.Wiener.law line 23
  7. instance OAI.HardSphere.Wiener.(instance at line 24) line 24
  8. lemma OAI.HardSphere.Wiener.coordinate_preserving line 26
  9. def OAI.HardSphere.Wiener.tent line 30
  10. lemma OAI.HardSphere.Wiener.tent_nonneg line 33
  11. lemma OAI.HardSphere.Wiener.tent_le_one line 36
  12. lemma OAI.HardSphere.Wiener.tent_positive_unique line 40
  13. lemma OAI.HardSphere.Wiener.sum_tent_le_one line 55
  14. def OAI.HardSphere.Wiener.tentMap line 69
  15. def OAI.HardSphere.Wiener.amplitude line 72
  16. lemma OAI.HardSphere.Wiener.amplitude_nonneg line 74
  17. def OAI.HardSphere.Wiener.level line 76
  18. lemma OAI.HardSphere.Wiener.norm_level_le line 79
  19. def OAI.HardSphere.Wiener.moment line 99
  20. lemma OAI.HardSphere.Wiener.moment_ne_top line 101
  21. lemma OAI.HardSphere.Wiener.coordinate_tail line 104
  22. def OAI.HardSphere.Wiener.badLevel line 122
  23. lemma OAI.HardSphere.Wiener.badLevel_bound line 125
  24. lemma OAI.HardSphere.Wiener.ae_eventually_coordinates_small line 148
  25. lemma OAI.HardSphere.Wiener.decay_lt_one line 160
  26. lemma OAI.HardSphere.Wiener.summable_level_bound line 165
  27. lemma OAI.HardSphere.Wiener.ae_summable_level line 176
  28. def OAI.HardSphere.Wiener.path line 182
  29. lemma OAI.HardSphere.Wiener.continuous_level line 185
  30. lemma OAI.HardSphere.Wiener.measurable_path line 189
  31. def OAI.HardSphere.Wiener.wiener line 196
  32. instance OAI.HardSphere.Wiener.(instance at line 197) line 197
  33. lemma OAI.HardSphere.Wiener.path_continuous line 199
  34. lemma OAI.HardSphere.Wiener.tent_at_zero line 201
  35. lemma OAI.HardSphere.Wiener.tent_at_one line 207
  36. lemma OAI.HardSphere.Wiener.level_at_zero line 213
  37. lemma OAI.HardSphere.Wiener.level_at_one line 216
  38. lemma OAI.HardSphere.Wiener.path_at_zero line 219
  39. lemma OAI.HardSphere.Wiener.path_at_one line 228
  40. lemma OAI.HardSphere.Wiener.hasLaw_gaussian_of_ae_tendsto line 238
  41. lemma OAI.HardSphere.Wiener.hasLaw_centered_gaussian_sum line 274
  42. def OAI.HardSphere.Wiener.leftIndex line 294
  43. def OAI.HardSphere.Wiener.rightIndex line 296
  44. lemma OAI.HardSphere.Wiener.sum_split_level line 299
  45. lemma OAI.HardSphere.Wiener.tent_left line 306
  46. lemma OAI.HardSphere.Wiener.tent_right line 313
  47. lemma OAI.HardSphere.Wiener.tent_nonpos line 320
  48. lemma OAI.HardSphere.Wiener.tent_ge_one line 328
  49. def OAI.HardSphere.Wiener.hatKernel line 337
  50. def OAI.HardSphere.Wiener.weight line 339
  51. def OAI.HardSphere.Wiener.partialBridge line 341
  52. lemma OAI.HardSphere.Wiener.hatKernel_rec line 344
  53. lemma OAI.HardSphere.Wiener.partialBridge_zero_left line 350
  54. lemma OAI.HardSphere.Wiener.partialBridge_zero_right line 354
  55. lemma OAI.HardSphere.Wiener.partialBridge_rec line 358
  56. lemma OAI.HardSphere.Wiener.tent_zero_left line 376
  57. lemma OAI.HardSphere.Wiener.tent_zero_right line 381
  58. lemma OAI.HardSphere.Wiener.weight_step line 386
  59. lemma OAI.HardSphere.Wiener.abs_half_mul line 390
  60. lemma OAI.HardSphere.Wiener.partialBridge_error_ordered line 394