OAI/Probability/InvariantIsing/Magnetic/MagneticSlabCoefficient.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Uniform bounded potential for the actual finite-slab inverse-curvature comparison. The cap depends on exponents, not on the variance parameter.

  1. lemma OAI.InvariantIsing.magneticScalarSlabJet_eq_cons line 17
  2. def OAI.InvariantIsing.magneticSlabPotentialCap line 27
  3. lemma OAI.InvariantIsing.magneticScalarInverse_weighted_second_bound line 30