OAI/Analysis/Daugavet/HeavyTails.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ExactModuli.KW.coefficientNorm line 16
2. lemma OAI.ExactModuli.KW.coefficientNorm_nonneg line 18
3. lemma OAI.ExactModuli.KW.coefficientNorm_rpow line 22
4. lemma OAI.ExactModuli.KW.abs_le_coefficientNorm line 29
5. lemma OAI.ExactModuli.KW.sum_scaled_coefficients line 35
6. lemma OAI.ExactModuli.KW.difference_law_tail line 45
7. lemma OAI.ExactModuli.KW.scaled_difference_tail_upper line 51
8. lemma OAI.ExactModuli.KW.scaled_difference_tail_lower line 69
9. lemma OAI.ExactModuli.KW.scaled_difference_symmetric line 90
10. theorem OAI.ExactModuli.KW.heavy_tail_upper line 97
11. lemma OAI.ExactModuli.KW.scaled_difference_max_tail line 122
12. theorem OAI.ExactModuli.KW.heavy_tail_lower line 153
13. theorem OAI.ExactModuli.KW.heavy_tail line 196