OAI/Probability/InvariantIsing/Magnetic/MagneticBlockModulus.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Height continuity after block averaging, uniformly in block size and in every optimizing root bias.

  1. lemma OAI.InvariantIsing.magneticBlockLevel_abs_sub_le line 13
  2. lemma OAI.InvariantIsing.magneticBlockPath_on_cell line 32