OAI/Probability/InvariantIsing/Magnetic/MagneticInverseCurvature.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

First and second spatial derivatives of the actual curvature in the physical mean-spin coordinate. The root exponent remains zero.

  1. lemma OAI.InvariantIsing.magnetic_tanh_measurable line 16
  2. lemma OAI.InvariantIsing.magnetic_third_terminal_measurable line 21
  3. lemma OAI.InvariantIsing.magnetic_tail_third_regular line 26
  4. lemma OAI.InvariantIsing.magnetic_tail_fourth_regular line 38
  5. def OAI.InvariantIsing.fieldBiasThird line 54
  6. def OAI.InvariantIsing.fieldBiasFourth line 61
  7. lemma OAI.InvariantIsing.hasDerivAt_fieldBiasCurvature line 68
  8. lemma OAI.InvariantIsing.hasDerivAt_fieldBiasThird line 84
  9. def OAI.InvariantIsing.magneticCurvature line 100
  10. def OAI.InvariantIsing.magneticCurvatureSlope line 103
  11. def OAI.InvariantIsing.magneticCurvatureSecond line 106
  12. lemma OAI.InvariantIsing.magneticCurvature_pos line 110
  13. lemma OAI.InvariantIsing.hasDerivAt_magneticCurvature line 113
  14. lemma OAI.InvariantIsing.hasDerivAt_magneticCurvatureSlope line 121
  15. lemma OAI.InvariantIsing.hasDerivAt_deriv_magneticCurvature line 131