OAI/Probability/FreeIsing/Ising/CopyPathBounds.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem367.IsingCopyPathBounds.edgeLogDifference line 18
  2. def OAI.Problem367.IsingCopyPathBounds.edgeLogBound line 27
  3. theorem OAI.Problem367.IsingCopyPathBounds.edgeLogBound_nonneg line 30
  4. theorem OAI.Problem367.IsingCopyPathBounds.measurable_edgeLogDifference line 36
  5. theorem OAI.Problem367.IsingCopyPathBounds.ae_all_siteDifference_bound line 46
  6. theorem OAI.Problem367.IsingCopyPathBounds.ae_edgeLogDifference_bound line 62
  7. def OAI.Problem367.IsingCopyPathBounds.pathLogDifference line 81
  8. theorem OAI.Problem367.IsingCopyPathBounds.measurable_pathLogDifference line 86
  9. theorem OAI.Problem367.IsingCopyPathBounds.ae_pathLogDifference_bound line 93
  10. theorem OAI.Problem367.IsingCopyPathBounds.ae_pathLogDifference_sq_bound line 112
  11. theorem OAI.Problem367.IsingCopyPathBounds.memLp_pathLogDifference line 124
  12. theorem OAI.Problem367.IsingCopyPathBounds.integrable_pathLogDifference_sq line 132