OAI/Probability/SKBarriers/Parisi/QuantileScalarOverlap.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SK.Analytic.hierarchyMeanOverlap_oneSite line 17
2. theorem OAI.SK.Analytic.blockExponent_singleSite line 48
3. theorem OAI.SK.Analytic.quantileOverlapMean_eq_scalar_block line 62
4. theorem OAI.SK.Analytic.blockDimension_oneSite line 70
5. theorem OAI.SK.Analytic.scalarMomentSquare_cast line 72
6. theorem OAI.SK.Analytic.blockMass_oneSite_cast line 79
7. theorem OAI.SK.Analytic.siteScalarCoefficients_oneSite_cast line 87
8. theorem OAI.SK.Analytic.quantileOverlapMean_eq_scalar line 95