Documentation

LeanPool.SpherePacking.GammaAnalysis

GammaAnalysis #

Gamma-kernel estimates and radial asymptotics.

theorem CohnElkies.upper_laplace_monomial_integral {η : ℝ} (hη : 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.