OAI/Analysis/LpDimension/GradientLaws.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SubpolynomialLp.weighted_gradient_measure_samples line 12
2. def OAI.SubpolynomialLp.globalCutLaw line 58
3. instance OAI.SubpolynomialLp.globalCutLaw_probability line 60
4. lemma OAI.SubpolynomialLp.globalCutLaw_moment line 65
5. lemma OAI.SubpolynomialLp.globalCutLaw_bound line 69
6. lemma OAI.SubpolynomialLp.globalCutLaw_submodule line 76
7. lemma OAI.SubpolynomialLp.convolutionPower_coordinate_integrable line 82