OAI/Probability/Ising/GibbsMeasure.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BufferedIsing.DSS.sgn line 15

    Source documentation

    Directed pair couplings. Both directions are counted; diagonal terms are constants. This intermediate presentation allows exact restriction without re-enumerating edges.

    def sgn (b : Bool) : ℝ := if b then 1 else -1
  2. def OAI.BufferedIsing.DSS.hamiltonian line 17
  3. def OAI.BufferedIsing.DSS.mass line 20
  4. def OAI.BufferedIsing.DSS.part line 23
  5. def OAI.BufferedIsing.DSS.average line 25
  6. def OAI.BufferedIsing.DSS.mean line 28
  7. lemma OAI.BufferedIsing.DSS.mass_pos line 31
  8. lemma OAI.BufferedIsing.DSS.part_pos line 34
  9. lemma OAI.BufferedIsing.DSS.sgn_neg line 38
  10. lemma OAI.BufferedIsing.DSS.sgn_sq line 39
  11. lemma OAI.BufferedIsing.DSS.sgn_le_one line 40
  12. lemma OAI.BufferedIsing.DSS.neg_one_le_sgn line 41
  13. lemma OAI.BufferedIsing.DSS.sgn_mono line 42
  14. lemma OAI.BufferedIsing.DSS.average_add line 47
  15. lemma OAI.BufferedIsing.DSS.average_sub line 51
  16. lemma OAI.BufferedIsing.DSS.average_const line 55
  17. lemma OAI.BufferedIsing.DSS.mean_lt_one line 61
  18. lemma OAI.BufferedIsing.DSS.neg_one_lt_mean line 71
  19. lemma OAI.BufferedIsing.DSS.sgn_modular line 82
  20. lemma OAI.BufferedIsing.DSS.sgn_product_supermodular line 85
  21. lemma OAI.BufferedIsing.DSS.mass_lattice line 90
  22. lemma OAI.BufferedIsing.DSS.hamiltonian_field_add line 115
  23. lemma OAI.BufferedIsing.DSS.mass_field_add line 120
  24. lemma OAI.BufferedIsing.DSS.mean_mono line 124