OAI/Probability/FreeIsing/Ising/WalkObstruction.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem367.IsingWalk.conjugateRoot line 11
  2. def OAI.Problem367.IsingWalk.eigenRate line 13
  3. def OAI.Problem367.IsingWalk.eigenWeight line 15
  4. theorem OAI.Problem367.IsingWalk.conjugateRoot_pos line 19
  5. theorem OAI.Problem367.IsingWalk.conjugateRoot_lt line 23
  6. theorem OAI.Problem367.IsingWalk.theta_le_eigenRate line 30
  7. theorem OAI.Problem367.IsingWalk.eigenRate_pos line 40
  8. theorem OAI.Problem367.IsingWalk.theta_characteristic line 45
  9. theorem OAI.Problem367.IsingWalk.conjugate_characteristic line 51
  10. theorem OAI.Problem367.IsingWalk.eigenWeight_zero line 57
  11. theorem OAI.Problem367.IsingWalk.eigenWeight_one line 61
  12. theorem OAI.Problem367.IsingWalk.eigenWeight_recurrence line 66
  13. theorem OAI.Problem367.IsingWalk.eigenWeight_le line 78
  14. theorem OAI.Problem367.IsingWalk.critical_square_lt line 86
  15. theorem OAI.Problem367.IsingWalk.eigenRate_gt_critical line 95
  16. def OAI.Problem367.IsingWalk.treeEigenWeight line 109
  17. theorem OAI.Problem367.IsingWalk.average_treeEigenWeight line 112
  18. theorem OAI.Problem367.IsingWalk.iterate_eigenfunction line 137
  19. theorem OAI.Problem367.IsingWalk.ising_walk_lower_bound line 150
  20. theorem OAI.Problem367.IsingWalk.le_of_exponential_bound line 167
  21. theorem OAI.Problem367.IsingWalk.threshold_of_ising_walk_bound line 178
  22. theorem OAI.Problem367.IsingWalk.threshold_of_operatorAverage_norm line 217