OAI/Analysis/LpDimension/PowerEstimates.lean
3 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.SubpolynomialLp.power_difference_epsilonline 12 - lemma
OAI.SubpolynomialLp.rpow_le_constant_expline 61 - lemma
OAI.SubpolynomialLp.symmetric_exp_quadraticline 82