OAI/Analysis/LpDimension/FourierTails.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SubpolynomialLp.fourierCutoff line 12
2. lemma OAI.SubpolynomialLp.fourierCutoff_nonneg line 14
3. lemma OAI.SubpolynomialLp.fourierCutoff_le_two line 17
4. lemma OAI.SubpolynomialLp.fourierCutoff_eq line 28
5. lemma OAI.SubpolynomialLp.fourierCutoff_ge_half line 36
6. lemma OAI.SubpolynomialLp.fourierCutoff_continuous line 48
7. lemma OAI.SubpolynomialLp.real_charFun line 61
8. lemma OAI.SubpolynomialLp.fourierCutoff_average line 70
9. lemma OAI.SubpolynomialLp.stable_tail_upper line 90
10. lemma OAI.SubpolynomialLp.one_sub_cos_quadratic_lower line 134
11. lemma OAI.SubpolynomialLp.fourierCutoff_quadratic line 154
12. lemma OAI.SubpolynomialLp.stable_fourier_average_upper line 179
13. lemma OAI.SubpolynomialLp.stable_capped_second_upper line 200
14. lemma OAI.SubpolynomialLp.charFun_defect_le_capped line 235
15. lemma OAI.SubpolynomialLp.exp_defect_lower line 267
16. lemma OAI.SubpolynomialLp.exists_small_power line 275
17. lemma OAI.SubpolynomialLp.stable_tail_lower line 284