OAI/Probability/SKRatio/Calculus/GradientMoments.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKRatio.Calculus.integral_exp_decay_le line 13
2. lemma OAI.SKRatio.Calculus.gradient_envelope_bounds line 28
3. lemma OAI.SKRatio.Calculus.moments_of_gradient_envelope line 49
4. lemma OAI.SKRatio.Calculus.gradient_envelope_of_small_set line 70
5. theorem OAI.SKRatio.Calculus.uniform_gradient_moments_of_small_set line 95
6. lemma OAI.SKRatio.Calculus.row_squares_le_opNorm line 155
7. theorem OAI.SKRatio.Calculus.uniform_field_tails_of_small_set line 174