OAI/Probability/FreeIsing/Spins/Moments.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem367.IsingSpin.toReal line 13
  2. lemma OAI.Problem367.IsingSpin.toReal_neg line 17
  3. lemma OAI.Problem367.IsingSpin.toReal_pos line 18
  4. lemma OAI.Problem367.measurable_spinToReal line 23
  5. lemma OAI.Problem367.measurable_spinEvent line 25
  6. lemma OAI.Problem367.HasFreeIsingLaw.isProbabilityMeasure line 29
  7. lemma OAI.Problem367.norm_spinToReal line 49
  8. lemma OAI.Problem367.integrable_spin line 52
  9. lemma OAI.Problem367.HasFreeIsingLaw.integral_spin line 58
  10. lemma OAI.Problem367.HasFreeIsingLaw.integral_spin_sq line 73
  11. lemma OAI.Problem367.memLp_spin line 83
  12. lemma OAI.Problem367.HasFreeIsingLaw.variance_spin line 89
  13. lemma OAI.Problem367.HasFreeIsingLaw.integral_factor_spin line 97
  14. lemma OAI.Problem367.HasFreeIsingLaw.integral_factor_spin_sq line 107
  15. lemma OAI.Problem367.integral_spin_mul_of_diagonal line 117
  16. theorem OAI.Problem367.IsingSpin.toReal_eq_spinSign line 159
  17. lemma OAI.Problem367.HasFreeIsingLaw.integral_spinSign line 162
  18. lemma OAI.Problem367.HasFreeIsingLaw.integral_spinSign_sq line 167
  19. lemma OAI.Problem367.HasFreeIsingLaw.variance_spinSign line 172
  20. lemma OAI.Problem367.HasFreeIsingLaw.integral_edge_spin line 177
  21. lemma OAI.Problem367.HasFreeIsingLaw.integral_edge_spinSign line 186