OAI/Probability/SKBarriers/SpinGlass/SpinCovarianceVariation.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.SK.Analytic.hierarchySpinMean_const_mulline 20 - theorem
OAI.SK.Analytic.hierarchyLevel_coordinate_gradientline 33 - theorem
OAI.SK.Analytic.hierarchyPotential_coordinate_gradientline 51 - theorem
OAI.SK.Analytic.hierarchyGaussian_coordinate_spinline 69