OAI/Probability/InvariantIsing/Magnetic/MagneticCurvatureBound.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The physical curvature is bounded by the remaining spin variance. Consequently its mean-coordinate representative vanishes at both endpoints.

  1. lemma OAI.InvariantIsing.fieldCurvatureTransform_le_spin_variance line 15
  2. lemma OAI.InvariantIsing.field_logCosh_spin_variance line 42
  3. lemma OAI.InvariantIsing.fieldScalarLogCoshSecond_le_spin_variance line 50
  4. lemma OAI.InvariantIsing.fieldBiasCurvature_le_spin_variance line 78
  5. lemma OAI.InvariantIsing.magneticCurvature_le_spin_variance line 104