OAI/Probability/InvariantIsing/Magnetic/MagneticBoundaryContinuity.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Continuity of the prescribed-magnetization functional along the strict height regularization, including coincident heights and zero root variance.

  1. lemma OAI.InvariantIsing.fieldRegularized_depth line 16
  2. lemma OAI.InvariantIsing.continuous_fieldRegularizedValue_bias line 19
  3. lemma OAI.InvariantIsing.continuous_fieldRegularizedMean_bias line 50
  4. lemma OAI.InvariantIsing.continuous_fieldRegularizedLevel_bias line 77
  5. lemma OAI.InvariantIsing.continuous_fieldRegularizedMagneticBias line 119
  6. lemma OAI.InvariantIsing.continuous_fieldRegularizedConstrainedValue line 132
  7. lemma OAI.InvariantIsing.continuous_fieldRegularizedMagneticLevel line 140