OAI/Probability/DilutedSpin/CavityAllocatedMean.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DilutedSpinGlass.energyInsertionFunctional line 15
2. lemma OAI.DilutedSpinGlass.energyInsertion_integrable line 19
3. lemma OAI.DilutedSpinGlass.energyInsertionFunctional_lipschitz line 26
4. lemma OAI.DilutedSpinGlass.energyInsertionFunctional_bound line 39
5. lemma OAI.DilutedSpinGlass.integral_energyInsertionFunctional line 47
6. def OAI.DilutedSpinGlass.PrescribedTree.activeCountMean line 70
7. lemma OAI.DilutedSpinGlass.PrescribedTree.allocatedDatumRoot_bound line 78
8. lemma OAI.DilutedSpinGlass.PrescribedTree.allocatedDatumRoot_integrable line 89
9. lemma OAI.DilutedSpinGlass.PrescribedTree.upperAllocatedMean line 107