OAI/Probability/DilutedSpin/QSubsetDeviation.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DilutedSpinGlass.PrescribedTree.shapeDeviation line 17
2. lemma OAI.DilutedSpinGlass.PrescribedTree.shapeDeviation_nonneg line 22
3. lemma OAI.DilutedSpinGlass.PrescribedTree.shapeDeviation_le_subtree line 32
4. lemma OAI.DilutedSpinGlass.PrescribedTree.qExpect_add line 55
5. lemma OAI.DilutedSpinGlass.PrescribedTree.qExpect_div_const line 62
6. lemma OAI.DilutedSpinGlass.PrescribedTree.subtreePotential_le_card line 67
7. lemma OAI.DilutedSpinGlass.PrescribedTree.qExpect_subtree_bounded line 80
8. lemma OAI.DilutedSpinGlass.PrescribedTree.qExpect_shapeDeviation_le line 90