OAI/Probability/SKBarriers/Interpolation/RestrictedConcentration.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SK.Analytic.restrictedLogPartition_subGaussian line 14
2. theorem OAI.SK.Analytic.restrictedLogPartition_integrable line 27
3. theorem OAI.SK.Analytic.restrictedLogPartition_upper_tail line 36
4. def OAI.SK.Analytic.replicaGibbsMass line 43
5. theorem OAI.SK.Analytic.replicaGibbsMass_nonneg line 46
6. theorem OAI.SK.Analytic.replicaGibbsMass_le_one line 50
7. theorem OAI.SK.Analytic.replicaGibbsMass_eq_ratio line 58
8. theorem OAI.SK.Analytic.replicaGibbsMass_eq_exp line 68
9. theorem OAI.SK.Analytic.continuous_replicaGibbsMass line 74
10. theorem OAI.SK.Analytic.replicaGibbsMass_integrable line 80