OAI/Probability/SKRatio/Matrices/Spin.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SKRatioGaussian.Spin line 12
  2. abbrev OAI.SKRatioGaussian.Edge line 13
  3. abbrev OAI.SKRatioGaussian.Disorder line 14
  4. def OAI.SKRatioGaussian.spinValue line 16
  5. def OAI.SKRatioGaussian.coupling line 18
  6. def OAI.SKRatioGaussian.hamiltonian line 22
  7. def OAI.SKRatioGaussian.weight line 26
  8. def OAI.SKRatioGaussian.partition line 29
  9. def OAI.SKRatioGaussian.mass line 32
  10. def OAI.SKRatioGaussian.expectation line 35
  11. def OAI.SKRatioGaussian.variance line 38
  12. def OAI.SKRatioGaussian.flip line 41
  13. def OAI.SKRatioGaussian.conditionalExpectation line 44
  14. def OAI.SKRatioGaussian.dirichlet line 49
  15. def OAI.SKRatioGaussian.disorderLaw line 52
  16. def OAI.SKRatioGaussian.poincareEvent line 55
  17. def OAI.SKRatioGaussian.discreteGap line 58
  18. def OAI.SKRatioGaussian.MainStatement line 62
  19. theorem OAI.SKRatioGaussian.spinValue_true line 72
  20. theorem OAI.SKRatioGaussian.spinValue_false line 73
  21. theorem OAI.SKRatioGaussian.spinValue_not line 74
  22. theorem OAI.SKRatioGaussian.spinValue_sq line 76
  23. theorem OAI.SKRatioGaussian.coupling_diag line 79
  24. theorem OAI.SKRatioGaussian.coupling_symm line 82
  25. theorem OAI.SKRatioGaussian.flip_same line 88
  26. theorem OAI.SKRatioGaussian.flip_other line 91
  27. theorem OAI.SKRatioGaussian.flip_flip line 94
  28. def OAI.SKRatioGaussian.flipEquiv line 100
  29. theorem OAI.SKRatioGaussian.sum_flip line 103
  30. theorem OAI.SKRatioGaussian.weight_pos line 106
  31. theorem OAI.SKRatioGaussian.partition_pos line 109
  32. theorem OAI.SKRatioGaussian.mass_pos line 112
  33. theorem OAI.SKRatioGaussian.mass_nonneg line 115
  34. theorem OAI.SKRatioGaussian.sum_mass line 118
  35. theorem OAI.SKRatioGaussian.expectation_const line 122
  36. theorem OAI.SKRatioGaussian.expectation_add line 126
  37. theorem OAI.SKRatioGaussian.expectation_sub line 130
  38. theorem OAI.SKRatioGaussian.expectation_mul_const line 134
  39. theorem OAI.SKRatioGaussian.expectation_const_mul line 138
  40. theorem OAI.SKRatioGaussian.expectation_nonneg line 142
  41. theorem OAI.SKRatioGaussian.variance_nonneg line 146
  42. theorem OAI.SKRatioGaussian.dirichlet_nonneg line 149
  43. theorem OAI.SKRatioGaussian.variance_eq_zero_iff line 153
  44. theorem OAI.SKRatioGaussian.variance_pos_of_ne line 161
  45. theorem OAI.SKRatioGaussian.exists_positive_variance line 168
  46. theorem OAI.SKRatioGaussian.lower_bound_discreteGap line 175
  47. instance OAI.SKRatioGaussian.disorderLaw_probability line 186
  48. theorem OAI.SKRatioGaussian.gap_probability_of_poincare line 190