OAI/Probability/InvariantIsing/Fields/FieldMagnetizationModulus.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A uniform modulus for the actual finite-field magnetization levels. Small height gaps force small overlap gaps, including near tied levels.

  1. lemma OAI.InvariantIsing.fieldMagnetizationLevel_increment_le line 15
  2. theorem OAI.InvariantIsing.fieldMagnetizationLevel_sub_le line 47
  3. theorem OAI.InvariantIsing.fieldMagnetizationLevel_abs_sub_le line 61