OAI/Probability/SKBarriers/SpinGlass/SpinMonomials.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SK.spinMonomial line 24
2. theorem OAI.SK.spinMonomial_sq line 27
3. theorem OAI.SK.spinMonomial_gauge line 31
4. def OAI.SK.monomialSign line 35
5. theorem OAI.SK.scalarSign_monomial line 38
6. def OAI.SK.spinExponent line 44
7. theorem OAI.SK.spinExponent_axis line 48
8. theorem OAI.SK.spinExponent_gauge line 52
9. theorem OAI.SK.spinExponent_sq_le line 62
10. theorem OAI.SK.hierarchy_spin_variance line 68