OAI/Probability/DilutedSpin/FirstMomentUpper.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DilutedSpinGlass.integrable_rootArray_sum line 10
2. lemma OAI.DilutedSpinGlass.integral_rootArray_sum line 19
3. lemma OAI.DilutedSpinGlass.PrescribedTree.datumRoot_norm_bound line 34
4. lemma OAI.DilutedSpinGlass.PrescribedTree.upperDatum_integrable_norm line 50
5. lemma OAI.DilutedSpinGlass.PrescribedTree.datumRoot_integrable_firstMoment line 54
6. lemma OAI.DilutedSpinGlass.PrescribedTree.upperCountMean_bound_firstMoment line 68