OAI/Probability/DilutedSpin/MixedEnergy.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DilutedSpinGlass.mixedSpinLaw line 10
2. lemma OAI.DilutedSpinGlass.mixedSpinLaw_factor line 14
3. def OAI.DilutedSpinGlass.mixedEnergy line 27
4. lemma OAI.DilutedSpinGlass.mixedEnergy_bound line 31
5. lemma OAI.DilutedSpinGlass.measurable_mixedEnergy line 39
6. def OAI.DilutedSpinGlass.PrescribedTree.mixedTreeEnergy line 47
7. def OAI.DilutedSpinGlass.PrescribedTree.mixedEnergyAvg line 53
8. lemma OAI.DilutedSpinGlass.PrescribedTree.measurable_mixedEnergyAvg line 62
9. lemma OAI.DilutedSpinGlass.PrescribedTree.mixedEnergyAvg_bound line 75
10. lemma OAI.DilutedSpinGlass.PrescribedTree.integrable_mixedEnergyAvg line 87