OAI/Probability/InvariantIsing/Cavity/CavityGaussianRotationCurve.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The trigonometric interpolation between independent Gaussian fields, with the cavity-size penalty removed along the same path.

  1. def OAI.InvariantIsing.cavityGaussianCurve line 14
  2. def OAI.InvariantIsing.cavityGaussianCurveDerivative line 18
  3. def OAI.InvariantIsing.cavityPenaltyCurve line 22
  4. lemma OAI.InvariantIsing.cavityGaussianCurve_linear line 25
  5. lemma OAI.InvariantIsing.cavityGaussianCurveDerivative_linear line 32
  6. lemma OAI.InvariantIsing.cavityGaussianCurve_hasDerivAt line 39
  7. lemma OAI.InvariantIsing.cavityPenaltyCurve_hasDerivAt line 46
  8. lemma OAI.InvariantIsing.cavityGaussianCurveDerivative_bound line 55
  9. lemma OAI.InvariantIsing.cavityGaussianCurve_cross line 68
  10. lemma OAI.InvariantIsing.cavityGaussianCurve_cross_bound line 88