OAI/Probability/InvariantIsing/Magnetic/MagneticScalarInverse.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Spatial and variance derivatives of the genuine finite-tail inverse curvature. The minimizing bias is constructed by coercivity, and no inverse-regularity assumption remains in these statements.

  1. lemma OAI.InvariantIsing.magneticScalarSlabBias_continuousAt_spin line 16
  2. lemma OAI.InvariantIsing.magneticScalarSlabBias_hasDerivAt_spin line 41
  3. def OAI.InvariantIsing.magneticScalarInverseCurvature line 55
  4. lemma OAI.InvariantIsing.magneticScalarInverseCurvature_eq line 61
  5. lemma OAI.InvariantIsing.magneticScalarInverseCurvature_variance_hasDerivAt line 71