OAI/Probability/InvariantIsing/Magnetic/MagneticLevelDerivative.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Differentiability of the physical conditional square levels at fixed magnetization, including the change in the optimizing bias.

  1. def OAI.InvariantIsing.magneticHeightLevel line 15
  2. def OAI.InvariantIsing.magneticHeightSchur line 20
  3. lemma OAI.InvariantIsing.magneticHeightSchur_symmetric line 27
  4. lemma OAI.InvariantIsing.hasDerivAt_magneticHeightP_line line 35
  5. lemma OAI.InvariantIsing.hasDerivAt_magneticHeightLevel_line line 63