OAI/Probability/InvariantIsing/Fields/SpinGroupProjectionMoment.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The expected number of flips in the nearest group-slice projection. The input consists of ordinary count variances, which can be checked under the independent canonical site law.

  1. lemma OAI.InvariantIsing.cast_nat_distance_eq_abs line 15
  2. lemma OAI.InvariantIsing.spinGroupProjection_distance_real line 25
  3. theorem OAI.InvariantIsing.spinGroupProjection_expected_distance line 35
  4. theorem OAI.InvariantIsing.spinGroupProjection_expected_distance_le line 51