OAI/Probability/DilutedSpin/CavityOldNewMean.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DilutedSpinGlass.cavityLaw_mean_eq line 12
2. lemma OAI.DilutedSpinGlass.PrescribedTree.pathFst_tail line 71
3. lemma OAI.DilutedSpinGlass.PrescribedTree.singleBlockEnergy_pack line 78
4. lemma OAI.DilutedSpinGlass.PrescribedTree.activeEnergy_pack line 89
5. lemma OAI.DilutedSpinGlass.PrescribedTree.activeRoot_flat line 108