OAI/Probability/InvariantIsing/Fields/SpinGroupCountVariance.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Count fluctuations under the independent canonical site law. The result applies to the averaged Gaussian spin kernels as soon as their bias equations give the prescribed group means.

  1. def OAI.InvariantIsing.spinGroupCountSummand line 16
  2. lemma OAI.InvariantIsing.sum_spinGroupCountSummand line 20
  3. lemma OAI.InvariantIsing.spinGroupCountSummand_memLp line 25
  4. lemma OAI.InvariantIsing.variance_spinGroupCountSummand_le line 34
  5. theorem OAI.InvariantIsing.spinGroupCount_variance_le line 50
  6. theorem OAI.InvariantIsing.spinGroupCount_centered_sq_le line 65
  7. theorem OAI.InvariantIsing.spinGroupProjection_product_mean_distance line 75