OAI/Probability/InvariantIsing/Magnetic/MagneticGroupParameterBound.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The finite-group magnetic field value has a parameter modulus uniform in all covariance partitions of bounded height.

  1. lemma OAI.InvariantIsing.constrainedFieldValue_abs_le_height line 12
  2. lemma OAI.InvariantIsing.magneticGroupValue_parameter_modulus line 20
  3. lemma OAI.InvariantIsing.magneticGroupValue_parameters_uniform line 49