OAI/Probability/DilutedSpin/FirstMomentFresh.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DilutedSpinGlass.integral_root_prod_finite_integrable line 9
2. lemma OAI.DilutedSpinGlass.PrescribedTree.upperCountMean_real_firstMoment line 30
3. lemma OAI.DilutedSpinGlass.PrescribedTree.integral_upperDatumLaw_integrable line 97
4. lemma OAI.DilutedSpinGlass.PrescribedTree.freshRoot_mean_sub_firstMoment line 117
5. lemma OAI.DilutedSpinGlass.PrescribedTree.freshRoot_replacement_firstMoment line 150