OAI/Analysis/LpDimension/ConvolutionError.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.SubpolynomialLp.interval_moment_errorline 12 - lemma
OAI.SubpolynomialLp.weighted_variance_powerline 21 - lemma
OAI.SubpolynomialLp.variance_power_algebraline 34 - lemma
OAI.SubpolynomialLp.convolutionLaw_weighted_errorline 51 - lemma
OAI.SubpolynomialLp.convolutionLaw_exp_boundline 93