OAI/Probability/InvariantIsing/Magnetic/ConstrainedBlockMagneticEstimate.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Finite constrained-block comparison with the actual scalar magnetic functional. Every error term is independent of the cascade depth.

  1. lemma OAI.InvariantIsing.sum_sites_group line 14
  2. lemma OAI.InvariantIsing.spinGroupFieldConstant_of_means line 27
  3. theorem OAI.InvariantIsing.biasedConstrainedBlockValue_gap line 38
  4. lemma OAI.InvariantIsing.magneticBlockGap_eq_biasedGap line 65
  5. theorem OAI.InvariantIsing.magneticBlockGap_estimate line 80