OAI/Probability/InvariantIsing/Magnetic/MagneticCenteredMoments.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Centered bounded-spin moments used to control the coefficients of the inverse-mean diffusion. These estimates apply to the actual tilted Gaussian law, including zero covariance.

  1. lemma OAI.InvariantIsing.magnetic_bounded_integrable line 14
  2. lemma OAI.InvariantIsing.magnetic_spin_mean_bound line 20
  3. lemma OAI.InvariantIsing.magnetic_centered_spin_bound line 26
  4. lemma OAI.InvariantIsing.magnetic_centered_power_integrable line 31
  5. lemma OAI.InvariantIsing.magnetic_centered_second line 39
  6. lemma OAI.InvariantIsing.magnetic_centered_second_bounds line 62
  7. lemma OAI.InvariantIsing.magnetic_centered_third line 76
  8. lemma OAI.InvariantIsing.magnetic_centered_fourth line 104
  9. lemma OAI.InvariantIsing.magnetic_weighted_centered_second line 140
  10. lemma OAI.InvariantIsing.magnetic_centered_third_bound line 167
  11. lemma OAI.InvariantIsing.magnetic_centered_fourth_cumulant_bound line 185
  12. lemma OAI.InvariantIsing.magnetic_weighted_centered_bound line 211
  13. lemma OAI.InvariantIsing.magnetic_nonnegative_spin_variance_bound line 246
  14. lemma OAI.InvariantIsing.magnetic_weighted_variance_bound line 262