OAI/Analysis/BoundedHochschild/Martingales.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

Hilbert-valued martingale limits and random-walk mean-square convergence.

  1. lemma OAI.HochschildMartingale.energy_identity line 21
  2. theorem OAI.HochschildMartingale.exists_limit_of_bounded_orthogonal_increments line 31
  3. theorem OAI.HochschildMartingale.uniform_cauchy_error line 69
  4. lemma OAI.HochschildMartingale.martingale_L2_orthogonal line 85
  5. theorem OAI.HochschildMartingale.martingale_L2_convergence line 100
  6. def OAI.HochschildWalk.pathMeasure line 118
  7. instance OAI.HochschildWalk.(instance at line 119) line 119
  8. def OAI.HochschildWalk.takePath line 121
  9. def OAI.HochschildWalk.word line 123
  10. def OAI.HochschildWalk.walk line 125
  11. lemma OAI.HochschildWalk.walk_succ line 128
  12. lemma OAI.HochschildWalk.takePath_measurable line 134
  13. lemma OAI.HochschildWalk.takePath_law line 138
  14. lemma OAI.HochschildWalk.walk_measurable line 144
  15. lemma OAI.HochschildWalk.takePath_integral line 148
  16. lemma OAI.HochschildWalk.last_integral line 156
  17. lemma OAI.HochschildWalk.integrable_of_countable_bound line 180
  18. lemma OAI.HochschildWalk.increment_inner_integral line 187
  19. lemma OAI.HochschildWalk.process_memLp line 222
  20. def OAI.HochschildWalk.processLp line 228
  21. lemma OAI.HochschildWalk.processLp_ae line 232
  22. lemma OAI.HochschildWalk.processLp_norm_le line 237
  23. lemma OAI.HochschildWalk.processLp_step_orthogonal line 246
  24. lemma OAI.HochschildWalk.processLp_orthogonal line 262
  25. lemma OAI.HochschildWalk.processLp_sq_error line 284
  26. lemma OAI.HochschildWalk.limitLp_sq_error line 294
  27. theorem OAI.HochschildWalk.harmonic_mean_square_convergence line 306