OAI/Probability/InvariantIsing/Magnetic/MagneticL1.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The constrained field functional is one-half Lipschitz in the L1 distance between arbitrary bounded monotone field paths.

  1. lemma OAI.InvariantIsing.field_height_difference_integral line 16
  2. lemma OAI.InvariantIsing.constrainedFieldValue_lipschitz_equal_cutList line 31
  3. theorem OAI.InvariantIsing.abs_constrainedFieldValue_sub_le_L1 line 39
  4. lemma OAI.InvariantIsing.constrainedFieldValue_eq_of_ae line 52