OAI/NumberTheory/CubicMoment/Estimates/GaussianDerivativeFactors.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Polynomially controlled factors of all derivatives of the radial Gaussian.

  1. lemma OAI.CubicFirstMoment.temperate_fderiv line 11
  2. lemma OAI.CubicFirstMoment.temperate_smulRight line 19
  3. def OAI.CubicFirstMoment.radialGaussian line 25
  4. def OAI.CubicFirstMoment.gaussianLogDerivative line 27
  5. lemma OAI.CubicFirstMoment.radialGaussian_smooth line 30
  6. lemma OAI.CubicFirstMoment.radialGaussian_fderiv line 33
  7. lemma OAI.CubicFirstMoment.radialGaussian_derivative_factor line 43