OAI/Probability/DilutedSpin/RootCoefficients.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DilutedSpinGlass.HeterogeneousMarks.sameTreeCoefficient line 22
2. lemma OAI.DilutedSpinGlass.HeterogeneousMarks.sameTreeCoefficient_patterns line 30
3. lemma OAI.DilutedSpinGlass.HeterogeneousMarks.measurable_sameTreeCoefficient line 40
4. lemma OAI.DilutedSpinGlass.HeterogeneousMarks.sameTreeCoefficient_bound line 50
5. def OAI.DilutedSpinGlass.HeterogeneousMarks.independentTreeCoefficient line 56
6. lemma OAI.DilutedSpinGlass.HeterogeneousMarks.independentTreeCoefficient_patterns line 64
7. lemma OAI.DilutedSpinGlass.HeterogeneousMarks.measurable_independentTreeCoefficient line 76
8. lemma OAI.DilutedSpinGlass.HeterogeneousMarks.independentTreeCoefficient_bound line 90
9. lemma OAI.DilutedSpinGlass.HeterogeneousMarks.integral_treeCoefficient_comparison line 96
10. lemma OAI.DilutedSpinGlass.PrescribedTree.expect_qExpect line 118
11. lemma OAI.DilutedSpinGlass.PrescribedTree.normalized_backwardLog_tail line 125
12. lemma OAI.DilutedSpinGlass.integral_expansion_tail line 138
13. lemma OAI.DilutedSpinGlass.PrescribedTree.qExpect_leaf_power line 162
14. lemma OAI.DilutedSpinGlass.PrescribedTree.qMoment_neg line 176
15. lemma OAI.DilutedSpinGlass.PrescribedTree.logInsertion_negative_tail line 190