OAI/Probability/DilutedSpin/SameInsertionAverage.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DilutedSpinGlass.HeterogeneousMarks.sameInsertionAverage line 20
2. lemma OAI.DilutedSpinGlass.HeterogeneousMarks.measurable_sameInsertionAverage line 25
3. lemma OAI.DilutedSpinGlass.HeterogeneousMarks.sameInsertionAverage_bound line 34
4. lemma OAI.DilutedSpinGlass.HeterogeneousMarks.independentInsertion_bound line 43
5. lemma OAI.DilutedSpinGlass.HeterogeneousMarks.same_qMoment line 52
6. lemma OAI.DilutedSpinGlass.HeterogeneousMarks.sameInsertionAverage_tail line 64
7. lemma OAI.DilutedSpinGlass.HeterogeneousMarks.independentInsertion_tail line 93