OAI/Probability/DilutedSpin/UpperCountMean.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.DilutedSpinGlass.PrescribedTree.upperDatumLaw_probability line 13
2. lemma OAI.DilutedSpinGlass.PrescribedTree.upperDatumLaw_ae line 19
3. def OAI.DilutedSpinGlass.PrescribedTree.realCountEnergy line 24
4. def OAI.DilutedSpinGlass.PrescribedTree.datumRoot line 29
5. lemma OAI.DilutedSpinGlass.PrescribedTree.measurable_datumRoot line 38
6. lemma OAI.DilutedSpinGlass.PrescribedTree.datumRoot_bound line 64
7. lemma OAI.DilutedSpinGlass.PrescribedTree.datumRoot_integrable line 87
8. def OAI.DilutedSpinGlass.PrescribedTree.upperCountMean line 101
9. lemma OAI.DilutedSpinGlass.PrescribedTree.upperCountMean_bound line 108