OAI/Probability/InvariantIsing/Magnetic/MagneticCurvatureLower.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

A positive exponential lower bound for the actual finite-step curvature. The constant depends only on the finite covariance data, not on the bias.

  1. def OAI.InvariantIsing.magneticGaussianLowerFactor line 14
  2. lemma OAI.InvariantIsing.magneticGaussianLowerFactor_pos line 18
  3. lemma OAI.InvariantIsing.fieldSpinTransition_exponential_lower line 27
  4. lemma OAI.InvariantIsing.fieldScalarLogCosh_lipschitz line 98
  5. lemma OAI.InvariantIsing.field_logCosh_curvature_exponential_lower line 114
  6. def OAI.InvariantIsing.magneticCurvatureLowerCap line 127
  7. lemma OAI.InvariantIsing.magneticCurvatureLowerCap_pos line 131
  8. lemma OAI.InvariantIsing.fieldScalarLogCoshSecond_exponential_lower line 137
  9. lemma OAI.InvariantIsing.fieldBiasCurvature_exponential_lower line 164