OAI/Probability/InvariantIsing/Magnetic/MagneticMeanShift.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A uniform mean-shift estimate from the Ising variance bound.

  1. lemma OAI.InvariantIsing.magnetic_mean_shift_deficit line 13
  2. lemma OAI.InvariantIsing.magnetic_mean_shift_tendsto_one line 52
  3. lemma OAI.InvariantIsing.magnetic_mean_shift_tendsto_neg_one line 68