OAI/Probability/InvariantIsing/Magnetic/MagneticVariationalContinuity.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Field-alphabet stability of the magnetic variational formula. These bounds are uniform over all rational interior magnetizations.

  1. lemma OAI.InvariantIsing.magnetic_field_term_difference line 13
  2. lemma OAI.InvariantIsing.finiteMagneticFunctional_le_add line 27
  3. lemma OAI.InvariantIsing.finiteMagneticFunctional_ne_top_bot line 52
  4. theorem OAI.InvariantIsing.abs_finiteMagneticFunctional_sub_le line 61