OAI/Analysis/FreeEntropy/PolynomialGrowth.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.FiniteEntropySeparation.mvPolynomial_norm_bound line 13
2. theorem OAI.FiniteEntropySeparation.IsRealPolynomial.norm_bound line 42
3. theorem OAI.FiniteEntropySeparation.IsRealPolynomial.smoothed_integrable line 46
4. theorem OAI.FiniteEntropySeparation.IsRealPolynomial.smoothedGradient_integrable line 57
5. theorem OAI.FiniteEntropySeparation.IsRealPolynomial.hasDerivAt_line line 71