OAI/Analysis/LpDimension/ProjectedRamps.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SubpolynomialLp.integrated_power_perturbation line 12
2. def OAI.SubpolynomialLp.projectedRampLaw line 34
3. instance OAI.SubpolynomialLp.projectedRampLaw_probability line 37
4. lemma OAI.SubpolynomialLp.projectedRampLaw_symmetry line 44
5. lemma OAI.SubpolynomialLp.projectedRampLaw_bounded line 47
6. lemma OAI.SubpolynomialLp.projectedRampLaw_range line 62
7. lemma OAI.SubpolynomialLp.projectedRampLaw_moment line 75
8. lemma OAI.SubpolynomialLp.ramp_jump_law line 89