OAI/Probability/InvariantIsing/Fields/SpinHammingBall.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Exponential bounds for Hamming balls and for the fibers of a nearest-slice map. The bound is uniform over the target configuration.

  1. def OAI.InvariantIsing.spinHammingBall line 14
  2. lemma OAI.InvariantIsing.sum_exp_hamming line 17
  3. lemma OAI.InvariantIsing.card_spinHammingBall_le line 33
  4. lemma OAI.InvariantIsing.spin_map_fiber_bound line 55
  5. lemma OAI.InvariantIsing.restrictedSpinLog_le_of_hamming_map line 66