OAI/Probability/DilutedSpin/PhysicalPairConnection.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DilutedSpinGlass.ConcreteReservoir.integral_siteLaw line 12
2. def OAI.DilutedSpinGlass.UniversalDictionary.pairSplitTest line 25
3. def OAI.DilutedSpinGlass.UniversalDictionary.readVector line 28
4. lemma OAI.DilutedSpinGlass.UniversalDictionary.readVector_bound line 32
5. lemma OAI.DilutedSpinGlass.UniversalDictionary.rootShapeHistory_pair line 43
6. lemma OAI.DilutedSpinGlass.UniversalDictionary.integral_rootShapeHistory_pair line 53
7. lemma OAI.DilutedSpinGlass.UniversalDictionary.measurable_rootShapeHistory_pair_slice line 68
8. lemma OAI.DilutedSpinGlass.UniversalDictionary.measurable_rootShapeHistory_pair line 79
9. lemma OAI.DilutedSpinGlass.UniversalDictionary.rootShapeHistory_pair_bound line 85
10. lemma OAI.DilutedSpinGlass.UniversalDictionary.integrable_rootShapeHistory_pair line 92
11. lemma OAI.DilutedSpinGlass.UniversalDictionary.shapeAverage_pair line 103