OAI/Probability/DilutedSpin/ShapeRoot.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DilutedSpinGlass.UniversalDictionary.externalShapeHistory line 15
2. lemma OAI.DilutedSpinGlass.UniversalDictionary.externalShapeHistory_expansion line 31
3. def OAI.DilutedSpinGlass.UniversalDictionary.rootShapeHistory line 46
4. lemma OAI.DilutedSpinGlass.UniversalDictionary.rootShapeHistory_expansion line 58
5. def OAI.DilutedSpinGlass.UniversalDictionary.shapeAverage line 85
6. def OAI.DilutedSpinGlass.UniversalDictionary.shapeCovariance line 90
7. lemma OAI.DilutedSpinGlass.UniversalDictionary.shapeAverage_expansion line 101
8. lemma OAI.DilutedSpinGlass.UniversalDictionary.shapeCovariance_expansion line 117