OAI/Probability/FreeIsing/Estimates/RadialWalk.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem367.RadialWalk.average line 12
  2. theorem OAI.Problem367.RadialWalk.average_mono line 15
  3. theorem OAI.Problem367.RadialWalk.average_mul line 21
  4. theorem OAI.Problem367.RadialWalk.iterate_bound line 27
  5. theorem OAI.Problem367.RadialWalk.average_nonneg line 42
  6. theorem OAI.Problem367.RadialWalk.abs_average_le line 47
  7. theorem OAI.Problem367.RadialWalk.abs_iterate_average_le line 53
  8. theorem OAI.Problem367.RadialWalk.iterate_average_mono line 63
  9. theorem OAI.Problem367.RadialWalk.iterate_average_mul line 72
  10. def OAI.Problem367.RadialWalk.vectorAverage line 84
  11. theorem OAI.Problem367.RadialWalk.inner_vectorAverage line 87
  12. theorem OAI.Problem367.RadialWalk.inner_iterate_vectorAverage line 92
  13. theorem OAI.Problem367.RadialWalk.inner_iterate_bound line 103
  14. def OAI.Problem367.RadialWalk.weight line 120
  15. def OAI.Problem367.RadialWalk.rate line 123
  16. theorem OAI.Problem367.RadialWalk.rate_nonneg line 125
  17. theorem OAI.Problem367.RadialWalk.rate_lt_one line 128
  18. theorem OAI.Problem367.RadialWalk.root_bound line 137
  19. theorem OAI.Problem367.RadialWalk.recurrence line 147
  20. def OAI.Problem367.RadialWalk.treeWeight line 159
  21. theorem OAI.Problem367.RadialWalk.average_treeWeight_le line 161
  22. theorem OAI.Problem367.RadialWalk.iterate_treeWeight_le line 179
  23. theorem OAI.Problem367.RadialWalk.covariance_walk_bound line 183