OAI/Probability/InvariantIsing/Magnetic/MagneticFieldInverse.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The unique interior minimizing bias is the inverse physical mean-spin map. Its derivative and the magnetization envelope formula are actual consequences of the scalar Gaussian recursion.

  1. def OAI.InvariantIsing.magneticBias line 15
  2. lemma OAI.InvariantIsing.fieldBiasMean_magneticBias line 17
  3. lemma OAI.InvariantIsing.magneticBias_minimizes line 22
  4. lemma OAI.InvariantIsing.constrainedFieldValue_magneticBias line 29
  5. lemma OAI.InvariantIsing.continuousAt_magneticBias line 33
  6. lemma OAI.InvariantIsing.hasDerivAt_magneticBias line 56
  7. lemma OAI.InvariantIsing.hasDerivAt_constrainedFieldValue_magnetization line 65