OAI/Analysis/FreeEntropy/GaussianMvStein.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.FiniteEntropySeparation.tensorHermite_coord_eq line 12
2. theorem OAI.FiniteEntropySeparation.tensorHermite_coord_integrable line 25
3. theorem OAI.FiniteEntropySeparation.tensorHermite_stein line 29
4. theorem OAI.FiniteEntropySeparation.linearExpand_coord line 41
5. theorem OAI.FiniteEntropySeparation.tensorExpansion_stein line 48
6. theorem OAI.FiniteEntropySeparation.gaussian_mvPolynomial_stein line 55