OAI/Probability/FreeIsing/Estimates/FiniteSpinCoupling.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem367.FiniteSpinCoupling.energy line 14
  2. def OAI.Problem367.FiniteSpinCoupling.partition line 18
  3. def OAI.Problem367.FiniteSpinCoupling.numerator line 20
  4. def OAI.Problem367.FiniteSpinCoupling.mean line 23
  5. lemma OAI.Problem367.FiniteSpinCoupling.mean_eq line 26
  6. lemma OAI.Problem367.FiniteSpinCoupling.partition_pos line 31
  7. lemma OAI.Problem367.FiniteSpinCoupling.exp_interaction line 35
  8. lemma OAI.Problem367.FiniteSpinCoupling.exp_energy line 42
  9. theorem OAI.Problem367.FiniteSpinCoupling.partition_energy line 51
  10. theorem OAI.Problem367.FiniteSpinCoupling.numerator_energy_fst line 59
  11. theorem OAI.Problem367.FiniteSpinCoupling.mean_energy_fst line 74
  12. theorem OAI.Problem367.FiniteSpinCoupling.mean_equiv line 87
  13. theorem OAI.Problem367.FiniteSpinCoupling.mean_energy_snd line 94
  14. theorem OAI.Problem367.FiniteSpinCoupling.mean_of_energy_split line 111