OAI/MathematicalPhysics/CriticalSK/Gibbs.lean

GitHub source file

57 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CriticalSK.partition_pos line 37
  2. lemma OAI.CriticalSK.gibbs_pos line 41
  3. lemma OAI.CriticalSK.gibbs_nonneg line 44
  4. lemma OAI.CriticalSK.gibbs_sum line 46
  5. lemma OAI.CriticalSK.gibbs_le_one line 51
  6. def OAI.CriticalSK.spinFlip line 55
  7. def OAI.CriticalSK.spinFlipEquiv line 57
  8. lemma OAI.CriticalSK.spinFlipEquiv_apply line 59
  9. lemma OAI.CriticalSK.spinFlip_spinFlip line 61
  10. lemma OAI.CriticalSK.spinValue_not line 65
  11. lemma OAI.CriticalSK.hamiltonian_spinFlip line 68
  12. lemma OAI.CriticalSK.gibbs_spinFlip line 75
  13. lemma OAI.CriticalSK.mean_odd_eq_zero line 78
  14. lemma OAI.CriticalSK.mean_spin line 87
  15. lemma OAI.CriticalSK.linearObservable_spinFlip line 92
  16. lemma OAI.CriticalSK.mean_linearObservable line 96
  17. lemma OAI.CriticalSK.covariance_eq line 100
  18. lemma OAI.CriticalSK.covariance_diag line 104
  19. lemma OAI.CriticalSK.sameExcept_refl line 108
  20. lemma OAI.CriticalSK.sameExcept_symm line 112
  21. lemma OAI.CriticalSK.sameExcept_trans line 117
  22. lemma OAI.CriticalSK.sameExcept_classes line 122
  23. def OAI.CriticalSK.fiberMass line 126
  24. lemma OAI.CriticalSK.fiberMass_pos line 129
  25. lemma OAI.CriticalSK.fiberMass_eq line 138
  26. lemma OAI.CriticalSK.siteKernel_nonneg line 145
  27. lemma OAI.CriticalSK.siteKernel_sum line 151
  28. lemma OAI.CriticalSK.siteKernel_reversible line 161
  29. lemma OAI.CriticalSK.siteKernel_stationary line 172
  30. lemma OAI.CriticalSK.siteKernel_same_row line 177
  31. lemma OAI.CriticalSK.siteKernel_projection line 184
  32. lemma OAI.CriticalSK.mean_nonneg line 201
  33. lemma OAI.CriticalSK.mean_mono line 204
  34. lemma OAI.CriticalSK.mean_const line 207
  35. lemma OAI.CriticalSK.mean_add line 210
  36. lemma OAI.CriticalSK.mean_sub line 214
  37. lemma OAI.CriticalSK.mean_neg line 218
  38. lemma OAI.CriticalSK.mean_mul_const line 221
  39. lemma OAI.CriticalSK.mean_const_mul line 225
  40. lemma OAI.CriticalSK.mean_sum line 229
  41. def OAI.CriticalSK.siteAverage line 234
  42. lemma OAI.CriticalSK.siteAverage_eq line 237
  43. lemma OAI.CriticalSK.siteAverage_add line 240
  44. lemma OAI.CriticalSK.siteAverage_sub line 245
  45. lemma OAI.CriticalSK.siteAverage_idempotent line 251
  46. lemma OAI.CriticalSK.siteAverage_fiber_constant line 256
  47. lemma OAI.CriticalSK.siteAverage_of_fiber_constant line 261
  48. lemma OAI.CriticalSK.siteAverage_selfadjoint line 273
  49. lemma OAI.CriticalSK.siteAverage_orthogonal line 289
  50. theorem OAI.CriticalSK.siteAverage_least_squares line 297
  51. lemma OAI.CriticalSK.siteAverage_form_identity line 317
  52. lemma OAI.CriticalSK.dirichlet_nonneg line 331
  53. lemma OAI.CriticalSK.dirichlet_generator line 336
  54. def OAI.CriticalSK.linearRest line 350
  55. lemma OAI.CriticalSK.linearObservable_split line 353
  56. lemma OAI.CriticalSK.linearRest_fiber_constant line 357
  57. theorem OAI.CriticalSK.dirichlet_linear_le line 363