OAI/Probability/SKBarriers/SpinGlass/SpinHessianFormula.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SK.Analytic.rootPair line 16
2. theorem OAI.SK.Analytic.rootPair_continuous line 20
3. theorem OAI.SK.Analytic.rootPair_bound line 25
4. theorem OAI.SK.Analytic.rootPair_shift_bound line 34
5. theorem OAI.SK.Analytic.hierarchyPressure_rootHessian_spin_formula line 59