OAI/Probability/InvariantIsing/Gaussian/GordonCurveMean.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Differentiation under the finite Gaussian minimum--maximum interpolation.

  1. def OAI.InvariantIsing.gordonCurveMean line 12
  2. def OAI.InvariantIsing.gordonCurveSlope line 16
  3. lemma OAI.InvariantIsing.gordonCurveMean_hasDerivAt line 21