OAI/Probability/InvariantIsing/Magnetic/MagneticSlabInitial.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Exact zero-variance data for the inverse-coordinate slab equations. The continued square starts at s², and the final tanh curvature at 1-s².

  1. lemma OAI.InvariantIsing.magneticScalarSlabMean_zero line 14
  2. lemma OAI.InvariantIsing.magneticScalarSlabBias_zero line 19
  3. lemma OAI.InvariantIsing.magneticScalarSlab_square_initial line 26
  4. lemma OAI.InvariantIsing.magneticScalarInverseCurvature_nil_initial line 40