OAI/Probability/InvariantIsing/Magnetic/MagneticFieldCurvature.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Strict bias convexity follows from the positive terminal curvature and the nonnegative conditional variance terms in the actual recursion.

  1. lemma OAI.InvariantIsing.fieldSpinTransition_pos line 15
  2. lemma OAI.InvariantIsing.fieldScalarLogCoshSecond_pos line 34
  3. def OAI.InvariantIsing.fieldBiasCurvature line 58

    Source documentation

    Actual second bias derivative, with the root exponent fixed at zero.

    def fieldBiasCurvature (h : FieldStep) : ℝ → ℝ :=
…

    Mentions: OAI.InvariantIsing.FieldStep

  4. lemma OAI.InvariantIsing.fieldBiasCurvature_pos line 64
  5. lemma OAI.InvariantIsing.hasDerivAt_fieldBiasMean line 72
  6. lemma OAI.InvariantIsing.strictMono_fieldBiasMean line 91
  7. lemma OAI.InvariantIsing.strictConvexOn_fieldValue_bias line 97
  8. lemma OAI.InvariantIsing.magneticBias_minimum_unique line 106