OAI/Analysis/FreeEntropy/PolynomialFunctions.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.FiniteEntropySeparation.IsRealPolynomial line 11
  2. theorem OAI.FiniteEntropySeparation.mvPolynomial_hasCoordinateDeriv line 12
  3. theorem OAI.FiniteEntropySeparation.IsRealPolynomial.const line 31
  4. theorem OAI.FiniteEntropySeparation.IsRealPolynomial.coord line 32
  5. theorem OAI.FiniteEntropySeparation.IsRealPolynomial.add line 33
  6. theorem OAI.FiniteEntropySeparation.IsRealPolynomial.sub line 37
  7. theorem OAI.FiniteEntropySeparation.IsRealPolynomial.mul line 41
  8. theorem OAI.FiniteEntropySeparation.IsRealPolynomial.const_mul line 45
  9. theorem OAI.FiniteEntropySeparation.IsRealPolynomial.mul_const line 47
  10. theorem OAI.FiniteEntropySeparation.IsRealPolynomial.neg line 49
  11. theorem OAI.FiniteEntropySeparation.IsRealPolynomial.pow line 51
  12. theorem OAI.FiniteEntropySeparation.IsRealPolynomial.finset_sum line 54
  13. theorem OAI.FiniteEntropySeparation.IsRealPolynomial.continuous line 61
  14. theorem OAI.FiniteEntropySeparation.IsRealPolynomial.integrable line 64
  15. theorem OAI.FiniteEntropySeparation.IsRealPolynomial.derivative line 67
  16. theorem OAI.FiniteEntropySeparation.IsRealPolynomial.hasDerivAt line 73
  17. theorem OAI.FiniteEntropySeparation.IsRealPolynomial.stein line 78
  18. theorem OAI.FiniteEntropySeparation.IsRealPolynomial.poincare line 82