Documentation

LeanPool.SpherePacking.GammaAnalysis

GammaAnalysis #

Gamma-kernel estimates and radial asymptotics.

theorem CohnElkies.upper_laplace_monomial_integral {η : } ( : 0 < η) (k : ) :
(a : ) in Set.Ioi 0, a ^ k * Real.exp (-η * a) = k.factorial / η ^ (k + 1)

Evaluates a monomial against a positive exponential Laplace weight.