OAI/Probability/DilutedSpin/FunctionalContinuity.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DilutedSpinGlass.trialSiteField line 13
2. def OAI.DilutedSpinGlass.trialSiteDisorder line 15
3. lemma OAI.DilutedSpinGlass.integrable_trial_site_field line 19
4. lemma OAI.DilutedSpinGlass.trialSiteField_bound line 27
5. lemma OAI.DilutedSpinGlass.stronglyMeasurable_trialSiteField line 37
6. lemma OAI.DilutedSpinGlass.trialSiteField_continuous line 43
7. lemma OAI.DilutedSpinGlass.interaction_sum_integrable line 55
8. lemma OAI.DilutedSpinGlass.integral_interaction_sum line 60
9. lemma OAI.DilutedSpinGlass.integrable_trialSiteField line 68
10. lemma OAI.DilutedSpinGlass.trialSiteDisorder_bound line 76
11. lemma OAI.DilutedSpinGlass.trialSiteDisorder_continuous line 86
12. lemma OAI.DilutedSpinGlass.functional_continuous line 97