OAI/Probability/ClassicalON/IsingGinibre.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ClassicalON.isingEnergy line 14
  2. def OAI.ClassicalON.isingHamiltonian line 17
  3. def OAI.ClassicalON.isingMean line 20
  4. def OAI.ClassicalON.isingDoubleVariable line 23
  5. def OAI.ClassicalON.isingDoubleEnergy line 26
  6. def OAI.ClassicalON.isingDoubleDifference line 29
  7. theorem OAI.ClassicalON.isingDoubleEnergy_cone line 33
  8. theorem OAI.ClassicalON.isingDoubleDifference_cone line 40
  9. theorem OAI.ClassicalON.isingDoubleVariable_moments line 47
  10. theorem OAI.ClassicalON.isingDoubleEnergy_identity line 56
  11. theorem OAI.ClassicalON.isingDoubleDifference_identity line 63
  12. theorem OAI.ClassicalON.ising_edge_covariance_nonneg line 69