OAI/Analysis/LpDimension/RampLaws.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SubpolynomialLp.paretoVectorLaw line 14
2. lemma OAI.SubpolynomialLp.paretoVectorLaw_probability line 17
3. lemma OAI.SubpolynomialLp.normalized_coefficients_bounded line 25
4. lemma OAI.SubpolynomialLp.paretoVectorLaw_integrable line 36
5. lemma OAI.SubpolynomialLp.paretoVectorLaw_moment line 46
6. lemma OAI.SubpolynomialLp.paretoVectorLaw_tail_integrable line 63
7. lemma OAI.SubpolynomialLp.paretoVectorLaw_tail_moment line 71
8. lemma OAI.SubpolynomialLp.paretoVectorLaw_ramp_integrable line 85
9. lemma OAI.SubpolynomialLp.paretoVectorLaw_ramp_moment line 97
10. lemma OAI.SubpolynomialLp.paretoVectorLaw_range line 113