OAI/Analysis/FreeEntropy/TensorPoincare.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.FiniteEntropySeparation.coordinateDerivative line 11
  2. theorem OAI.FiniteEntropySeparation.tensorExpansion_hasDerivAt line 13
  3. theorem OAI.FiniteEntropySeparation.tensorExpansion_derivative line 18
  4. theorem OAI.FiniteEntropySeparation.tensorExpansion_mean line 22
  5. theorem OAI.FiniteEntropySeparation.tensorExpansion_energy line 27
  6. theorem OAI.FiniteEntropySeparation.tensorExpansion_variance line 37
  7. theorem OAI.FiniteEntropySeparation.tensorDegree_ge_one line 45
  8. theorem OAI.FiniteEntropySeparation.tensorExpansion_poincare line 56
  9. theorem OAI.FiniteEntropySeparation.gaussian_mvPolynomial_poincare line 76
  10. theorem OAI.FiniteEntropySeparation.gaussian_mvPolynomial_integrable line 82