OAI/Analysis/LpDimension/CompoundPoisson.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SubpolynomialLp.convolutionPower line 15
2. instance OAI.SubpolynomialLp.convolutionPower_probability line 19
3. def OAI.SubpolynomialLp.compoundPoisson line 25
4. instance OAI.SubpolynomialLp.compoundPoisson_probability line 28
5. lemma OAI.SubpolynomialLp.integral_compoundPoisson line 39
6. lemma OAI.SubpolynomialLp.convolutionPower_map line 47
7. lemma OAI.SubpolynomialLp.charFun_convolutionPower line 62
8. lemma OAI.SubpolynomialLp.charFun_compoundPoisson line 68
9. lemma OAI.SubpolynomialLp.exp_integrable_conv line 90
10. lemma OAI.SubpolynomialLp.exp_integral_conv line 102
11. lemma OAI.SubpolynomialLp.exp_convolutionPower line 110
12. lemma OAI.SubpolynomialLp.bounded_exp_integrable line 121
13. def OAI.SubpolynomialLp.symmetrize line 132
14. instance OAI.SubpolynomialLp.symmetrize_probability line 135
15. lemma OAI.SubpolynomialLp.integral_symmetrize line 142
16. lemma OAI.SubpolynomialLp.charFun_symmetrize line 153