OAI/Analysis/FreeEntropy/GaussianIBP.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.FiniteEntropySeparation.gaussian_weight_integrableline 11 - theorem
OAI.FiniteEntropySeparation.hasDerivAt_gaussianPDFRealline 17 - theorem
OAI.FiniteEntropySeparation.gaussian_integrationByPartsline 32 - theorem
OAI.FiniteEntropySeparation.gaussian_pow_integrableline 63 - theorem
OAI.FiniteEntropySeparation.gaussian_polynomial_integrableline 70 - theorem
OAI.FiniteEntropySeparation.gaussian_polynomial_steinline 75