OAI/Probability/DilutedSpin/CompoundSample.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DilutedSpinGlass.measurable_compound_sample line 14
2. lemma OAI.DilutedSpinGlass.compound_sample_integrable line 22
3. lemma OAI.DilutedSpinGlass.integral_compound_sample line 37
4. lemma OAI.DilutedSpinGlass.iid_sample_norm_bound line 54
5. lemma OAI.DilutedSpinGlass.integral_compound_finite_sample line 61