OAI/Probability/FreeIsing/Ising/CopyStationarity.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem367.IsingCopyStationarity.copyRelabel line 19
  2. theorem OAI.Problem367.IsingCopyStationarity.measurable_copyRelabel line 23
  3. theorem OAI.Problem367.IsingCopyStationarity.measurePreserving_copies_relabel line 26
  4. theorem OAI.Problem367.IsingCopyStationarity.posterior_relabel_ae line 45
  5. theorem OAI.Problem367.IsingCopyStationarity.field_array_relabel_ae line 65
  6. theorem OAI.Problem367.IsingCopyStationarity.measurePreserving_observations line 73
  7. def OAI.Problem367.IsingCopyStationarity.sitePair line 82
  8. theorem OAI.Problem367.IsingCopyStationarity.measurable_sitePair line 86
  9. theorem OAI.Problem367.IsingCopyStationarity.measurePreserving_sitePair_relabel line 97
  10. theorem OAI.Problem367.IsingCopyStationarity.fieldDifference_identDistrib line 111
  11. theorem OAI.Problem367.IsingCopyStationarity.integral_fieldDifference_sq_eq line 129