OAI/Probability/DilutedSpin/UpperCommonCoefficient.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DilutedSpinGlass.PrescribedTree.mixedLeafAvg line 13
2. lemma OAI.DilutedSpinGlass.PrescribedTree.measurable_mixedLeafAvg line 22
3. lemma OAI.DilutedSpinGlass.PrescribedTree.mixedLeafAvg_bound line 30
4. lemma OAI.DilutedSpinGlass.PrescribedTree.integrable_mixedLeafAvg line 38
5. lemma OAI.DilutedSpinGlass.PrescribedTree.integratedMixedLeaf_identity line 47
6. lemma OAI.DilutedSpinGlass.PrescribedTree.integratedMixedLeaf_combination_nonneg line 61
7. lemma OAI.DilutedSpinGlass.PrescribedTree.qExpect_expect line 73
8. lemma OAI.DilutedSpinGlass.PrescribedTree.qExpect_linear_combination line 83
9. lemma OAI.DilutedSpinGlass.PrescribedTree.mixedQMoment_combination_nonneg line 102