OAI/Probability/InvariantIsing/Magnetic/MagneticFieldRadial.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Radial monotonicity of the finite prescribed-magnetization overlap. The root bias is chosen at the fixed prescribed magnetization at every scale.

  1. lemma OAI.InvariantIsing.squareContinuation_congr_list line 16
  2. lemma OAI.InvariantIsing.magneticFieldLevel_eq_scaled line 27
  3. theorem OAI.InvariantIsing.magneticFieldLevel_radial line 40