OAI/Probability/DilutedSpin/RootPatternProduct.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DilutedSpinGlass.HeterogeneousMarks.rootSitePattern line 21
2. lemma OAI.DilutedSpinGlass.HeterogeneousMarks.measurable_rootSitePattern line 26
3. lemma OAI.DilutedSpinGlass.HeterogeneousMarks.rootSitePattern_bound line 36
4. lemma OAI.DilutedSpinGlass.HeterogeneousMarks.rootSitePattern_eq line 42
5. lemma OAI.DilutedSpinGlass.HeterogeneousMarks.integral_rootSitePattern line 51
6. lemma OAI.DilutedSpinGlass.HeterogeneousMarks.integral_independent_patterns line 69