OAI/Analysis/BoundedHochschild/WalkLabels.lean

GitHub source file

74 declarations, 0 contain sorry, 0 declared as axioms

Bad-path probability bounds and symmetric rare-label random walks.

  1. lemma OAI.HochschildRare.finite_coordinates_mass line 27
  2. lemma OAI.HochschildRare.some_coordinate_mass_le line 33
  3. lemma OAI.HochschildRare.label_collision_mass_le line 48
  4. lemma OAI.HochschildRare.uniform_label_collision_mass_le line 77
  5. lemma OAI.HochschildRare.path_miss_mass line 89
  6. lemma OAI.HochschildRare.some_path_miss_mass_le line 102
  7. def OAI.HochschildRare.badPaths line 114
  8. theorem OAI.HochschildRare.badPaths_mass_le line 121
  9. def OAI.HochschildRare.baseMass line 153
  10. lemma OAI.HochschildRare.baseMass_le_one line 154
  11. lemma OAI.HochschildRare.baseMass_pos line 158
  12. def OAI.HochschildRare.baseWeight line 160
  13. lemma OAI.HochschildRare.baseWeight_pos line 161
  14. lemma OAI.HochschildRare.summable_baseWeight line 162
  15. lemma OAI.HochschildRare.sum_baseWeight line 165
  16. abbrev OAI.HochschildRare.Label line 171
  17. instance OAI.HochschildRare.(instance at line 172) line 172
  18. instance OAI.HochschildRare.(instance at line 173) line 173
  19. def OAI.HochschildRare.labelWeight line 175
  20. lemma OAI.HochschildRare.sum_uniform_weight line 179
  21. lemma OAI.HochschildRare.tsum_labelWeight line 187
  22. def OAI.HochschildRare.labelPMF line 199
  23. def OAI.HochschildRare.labelLaw line 201
  24. instance OAI.HochschildRare.(instance at line 202) line 202
  25. lemma OAI.HochschildRare.labelLaw_singleton line 204
  26. lemma OAI.HochschildRare.stage_label_mass line 207
  27. lemma OAI.HochschildRare.stage_mass line 212
  28. def OAI.HochschildRare.stageSet line 227
  29. def OAI.HochschildRare.tailSet line 228
  30. def OAI.HochschildRare.baseTail line 229
  31. lemma OAI.HochschildRare.stageSet_disjoint line 231
  32. lemma OAI.HochschildRare.tail_mass line 237
  33. lemma OAI.HochschildRare.base_label_mass line 254
  34. lemma OAI.HochschildRare.base_tail_mass line 258
  35. lemma OAI.HochschildRare.exists_base_cut line 280
  36. def OAI.HochschildRare.signLaw line 288
  37. instance OAI.HochschildRare.(instance at line 289) line 289
  38. lemma OAI.HochschildRare.signLaw_singleton line 291
  39. lemma OAI.HochschildRare.sign_flip_preserving line 295
  40. abbrev OAI.HochschildRare.Increment line 301
  41. def OAI.HochschildRare.incrementLaw line 302
  42. instance OAI.HochschildRare.(instance at line 303) line 303
  43. lemma OAI.HochschildRare.increment_fst_preserving line 305
  44. lemma OAI.HochschildRare.increment_flip_preserving line 307
  45. lemma OAI.HochschildRare.increment_label_mass line 311
  46. abbrev OAI.HochschildRare.WalkGroup line 315
  47. instance OAI.HochschildRare.(instance at line 316) line 316
  48. instance OAI.HochschildRare.(instance at line 317) line 317
  49. def OAI.HochschildRare.incrementValue line 319
  50. def OAI.HochschildRare.walkLaw line 322
  51. instance OAI.HochschildRare.(instance at line 323) line 323
  52. lemma OAI.HochschildRare.incrementValue_preserving line 326
  53. lemma OAI.HochschildRare.walkLaw_symmetric line 329
  54. lemma OAI.HochschildRare.base_atom_pos line 341
  55. def OAI.HochschildRare.badBound line 361
  56. lemma OAI.HochschildRare.badBound_tendsto line 365
  57. lemma OAI.HochschildRare.rare_four_terms_le line 367
  58. theorem OAI.HochschildRare.rare_badPaths_le line 403
  59. def OAI.HochschildRare.baseCut line 422
  60. lemma OAI.HochschildRare.baseCut_spec line 423
  61. def OAI.HochschildRare.stageBad line 426
  62. lemma OAI.HochschildRare.stageBad_mass_le line 430
  63. def OAI.HochschildRare.StageTests line 448
  64. lemma OAI.HochschildRare.stages_time_atTop line 453
  65. theorem OAI.HochschildRare.finite_tests_freeMoments line 461
  66. lemma OAI.HochschildRare.countable_atom_sum line 494
  67. lemma OAI.HochschildRare.countable_real_atom_sum line 501
  68. lemma OAI.HochschildRare.probability_eq_atomicLaw line 508
  69. instance OAI.HochschildRare.(instance at line 515) line 515
  70. def OAI.HochschildRare.walkEnum line 517
  71. def OAI.HochschildRare.walkWeights line 518
  72. lemma OAI.HochschildRare.walkWeights_nonneg line 519
  73. lemma OAI.HochschildRare.walkWeights_sum line 520
  74. lemma OAI.HochschildRare.walkLaw_eq_atomic line 522