OAI/Analysis/LpDimension/ClippedMoments.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SubpolynomialLp.tail_measurable line 12
2. lemma OAI.SubpolynomialLp.tail_real_measurable line 16
3. lemma OAI.SubpolynomialLp.integral_power_derivative line 20
4. lemma OAI.SubpolynomialLp.capped_moment_layercake line 26
5. lemma OAI.SubpolynomialLp.capped_moment_lower_log line 81
6. lemma OAI.SubpolynomialLp.excess_first_moment line 128
7. def OAI.SubpolynomialLp.clip line 207
8. lemma OAI.SubpolynomialLp.clip_abs line 209
9. lemma OAI.SubpolynomialLp.clip_error line 219
10. lemma OAI.SubpolynomialLp.clip_measurable line 231
11. lemma OAI.SubpolynomialLp.capped_power_lipschitz line 233
12. lemma OAI.SubpolynomialLp.capped_power_tail_bound line 250
13. lemma OAI.SubpolynomialLp.bounded_power_integrable line 270
14. lemma OAI.SubpolynomialLp.bounded_capped_integrable line 279
15. lemma OAI.SubpolynomialLp.matrix_clip_bounds line 288