OAI/Analysis/LpDimension/Pareto.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SubpolynomialLp.powerIntensity_scaling line 12
2. lemma OAI.SubpolynomialLp.powerIntensity_even_scaling line 28
3. def OAI.SubpolynomialLp.pareto line 39
4. lemma OAI.SubpolynomialLp.pareto_probability line 41
5. lemma OAI.SubpolynomialLp.powerIntensity_supported_positive line 45
6. lemma OAI.SubpolynomialLp.pareto_integral_eq_full line 48
7. lemma OAI.SubpolynomialLp.pareto_even_scaling line 62