OAI/Probability/InvariantIsing/Magnetic/MagneticBlockError.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The finite block error vanishes uniformly over field partitions with bounded final height and magnetizations in a fixed interior interval.

  1. def OAI.InvariantIsing.magneticUniformBiasBound line 16
  2. lemma OAI.InvariantIsing.magneticBias_uniform_bound line 18
  3. lemma OAI.InvariantIsing.normalized_magneticBlockError line 26
  4. lemma OAI.InvariantIsing.log_one_add_exp_neg_tendsto line 36
  5. theorem OAI.InvariantIsing.tendsto_zero_of_magneticBlockError line 42