OAI/Analysis/LpDimension/SymmetricMoments.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SubpolynomialLp.symmetric_power_near line 12
2. lemma OAI.SubpolynomialLp.symmetric_power_unit_upper line 43
3. lemma OAI.SubpolynomialLp.sq_rpow_half_abs line 93
4. lemma OAI.SubpolynomialLp.symmetric_power_lower line 98
5. lemma OAI.SubpolynomialLp.symmetric_power_abs line 110
6. lemma OAI.SubpolynomialLp.symmetric_power_upper line 127
7. lemma OAI.SubpolynomialLp.bounded_conv line 162
8. lemma OAI.SubpolynomialLp.bounded_abs_moment_integrable line 171
9. lemma OAI.SubpolynomialLp.bounded_abs_shift_integrable line 179
10. lemma OAI.SubpolynomialLp.symmetric_integral line 187
11. lemma OAI.SubpolynomialLp.bounded_moment_interpolation line 194
12. lemma OAI.SubpolynomialLp.symmetric_conv_moment line 213
13. lemma OAI.SubpolynomialLp.sublinear_absorption line 281
14. lemma OAI.SubpolynomialLp.near_additive_recurrence line 305
15. lemma OAI.SubpolynomialLp.convolutionPower_bounded line 343
16. lemma OAI.SubpolynomialLp.convolutionPower_near_moment line 352