OAI/Analysis/FreeEntropy/TensorHermite.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.FiniteEntropySeparation.productGaussian line 12
  2. instance OAI.FiniteEntropySeparation.(instance at line 14) line 14
  3. def OAI.FiniteEntropySeparation.tensorHermite line 16
  4. def OAI.FiniteEntropySeparation.tensorWeight line 17
  5. theorem OAI.FiniteEntropySeparation.tensorHermite_zero line 18
  6. theorem OAI.FiniteEntropySeparation.tensorHermite_integrable line 20
  7. theorem OAI.FiniteEntropySeparation.tensorHermite_mul_integrable line 22
  8. theorem OAI.FiniteEntropySeparation.tensorHermite_mean line 27
  9. theorem OAI.FiniteEntropySeparation.tensorHermite_inner line 40
  10. theorem OAI.FiniteEntropySeparation.tensorWeight_pos line 56
  11. theorem OAI.FiniteEntropySeparation.tensorHermite_update line 59
  12. theorem OAI.FiniteEntropySeparation.tensorHermite_mul_coord line 69
  13. def OAI.FiniteEntropySeparation.tensorHermiteSpan line 88
  14. theorem OAI.FiniteEntropySeparation.tensorHermite_mem line 90
  15. theorem OAI.FiniteEntropySeparation.tensorHermiteSpan_coord line 92
  16. theorem OAI.FiniteEntropySeparation.mvPolynomial_hermite_span line 112
  17. theorem OAI.FiniteEntropySeparation.mvPolynomial_hermite_expansion line 123