OAI/Probability/SKValue/GroundState/WeakGuerra.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKValueG.profile_penalty_mono line 13
2. lemma OAI.SKValueG.weak_profile_guerra_upper line 24
3. lemma OAI.SKValue.logCoshTerminal_ge_abs line 76
4. lemma OAI.SKValue.OrderParameter.weighted_cutoff_integral line 82
5. lemma OAI.SKValue.OrderParameter.weighted_grid_error line 90
6. lemma OAI.SKValue.OrderParameter.weighted_grid_tendsto line 109
7. theorem OAI.SKValue.expectedMaximum_le_parisi line 117
8. theorem OAI.SKValue.groundStateValue_le_parisi line 129