OAI/Probability/InvariantIsing/Fields/FieldSpinVariance.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

A quantitative conditional-variance bound for a Lipschitz spin mean. The constant depends only on an upper bound for the Gaussian variance, rather than on the depth of the scalar recursion.

  1. lemma OAI.InvariantIsing.fieldGaussianMomentCap_nonneg line 16
  2. lemma OAI.InvariantIsing.field_centered_spin_variance line 21
  3. lemma OAI.InvariantIsing.fieldSpinTransition_centered_standard line 59
  4. lemma OAI.InvariantIsing.fieldSpinTransition_variance_bound line 69
  5. lemma OAI.InvariantIsing.fieldSpinTransition_variance_le line 98