OAI/Probability/DilutedSpin/UpperDatum.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DilutedSpinGlass.rootMap line 11
2. lemma OAI.DilutedSpinGlass.rootArray_rootMap line 15
3. lemma OAI.DilutedSpinGlass.measurable_rootMap line 23
4. lemma OAI.DilutedSpinGlass.rootLaw_ae_every line 29
5. lemma OAI.DilutedSpinGlass.PrescribedTree.measurable_cavityEnergy line 41
6. lemma OAI.DilutedSpinGlass.PrescribedTree.measurable_cavityRoot line 55
7. abbrev OAI.DilutedSpinGlass.PrescribedTree.UpperDatum line 64
8. def OAI.DilutedSpinGlass.PrescribedTree.upperDatumLaw line 66