OAI/Probability/SKBarriers/Scalar/ScalarResponseBounds.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SK.Analytic.scalarPrefixVariance_nonneg line 16
2. theorem OAI.SK.Analytic.scalarPrefixVariance_monotone line 19
3. theorem OAI.SK.Analytic.scalarFiniteResponse_origin_le line 30
4. theorem OAI.SK.Analytic.scalarHierarchyAverage_spin_square_lipschitz line 56
5. theorem OAI.SK.Analytic.scalarMomentSquare_spin_spatial_bound line 74
6. theorem OAI.SK.Analytic.scalarFiniteResponse_spatial_bound line 97