OAI/Analysis/LpDimension/CoordinateLaws.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SubpolynomialLp.coordinateLaw line 14
2. instance OAI.SubpolynomialLp.coordinateLaw_probability line 16
3. lemma OAI.SubpolynomialLp.coordinateLaw_integral line 21
4. lemma OAI.SubpolynomialLp.coordinateLaw_abs_moment line 25
5. lemma OAI.SubpolynomialLp.coordinateLaw_sq_moment line 29
6. lemma OAI.SubpolynomialLp.coordinateLaw_exp_moment line 33
7. lemma OAI.SubpolynomialLp.coordinateLaw_integrable line 37
8. lemma OAI.SubpolynomialLp.coordinateLaw_ae line 41
9. lemma OAI.SubpolynomialLp.coordinateLaw_symmetric line 45
10. lemma OAI.SubpolynomialLp.coordinateLaw_convolutionPower line 52
11. lemma OAI.SubpolynomialLp.convolutionPower_submodule line 57
12. lemma OAI.SubpolynomialLp.bounded_coordinate_power_integrable line 71
13. lemma OAI.SubpolynomialLp.bounded_symmetric_coordinate_exp line 79