OAI/Probability/DilutedSpin/UpperFreshLocal.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DilutedSpinGlass.PrescribedTree.realCountEnergy_succ line 13
2. lemma OAI.DilutedSpinGlass.PrescribedTree.datumRoot_real_succ line 23
3. lemma OAI.DilutedSpinGlass.PrescribedTree.datumRoot_head_bound line 41
4. def OAI.DilutedSpinGlass.PrescribedTree.freshRoot line 73
5. lemma OAI.DilutedSpinGlass.PrescribedTree.measurable_freshRoot line 81
6. lemma OAI.DilutedSpinGlass.PrescribedTree.freshRoot_bound line 94
7. lemma OAI.DilutedSpinGlass.PrescribedTree.freshRoot_mean_sub line 103
8. lemma OAI.DilutedSpinGlass.PrescribedTree.freshRoot_replacement line 136