OAI/Probability/DilutedSpin/MixedPatterns.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DilutedSpinGlass.HeterogeneousMarks.rootInsertion line 26
2. lemma OAI.DilutedSpinGlass.HeterogeneousMarks.measurable_rootInsertion line 32
3. def OAI.DilutedSpinGlass.HeterogeneousMarks.independentInsertion line 53
4. lemma OAI.DilutedSpinGlass.HeterogeneousMarks.independentInsertion_encode line 61
5. lemma OAI.DilutedSpinGlass.HeterogeneousMarks.measurable_independentInsertion line 75
6. def OAI.DilutedSpinGlass.Pattern.mixedMass line 106
7. lemma OAI.DilutedSpinGlass.Pattern.mixedMass_nonneg line 110
8. lemma OAI.DilutedSpinGlass.Pattern.mixedMass_total line 114
9. lemma OAI.DilutedSpinGlass.Pattern.mixedMass_moment line 125
10. lemma OAI.DilutedSpinGlass.Pattern.mixed_pattern_replacement line 137
11. lemma OAI.DilutedSpinGlass.exponents_nonempty line 205
12. def OAI.DilutedSpinGlass.zeroHierarchy line 218