OAI/NumberTheory/CubicGauss/LaplaceBounds.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Weighted Gaussian tails and Laplace estimates for sieve kernels.

  1. lemma OAI.CubicFirstMoment.SieveKernel.factorial_term_le line 15
  2. lemma OAI.CubicFirstMoment.SieveKernel.damped_coefficient_bound line 22
  3. lemma OAI.CubicFirstMoment.SieveKernel.damping_cancel line 44
  4. def OAI.CubicFirstMoment.SieveKernel.geometricMajorant line 52
  5. lemma OAI.CubicFirstMoment.SieveKernel.geometricMajorant_hasSum line 55
  6. theorem OAI.CubicFirstMoment.SieveKernel.gaussian_weighted_gram_bound line 64
  7. lemma OAI.CubicFirstMoment.SieveKernel.exp_tail_indicator_integrable line 158
  8. lemma OAI.CubicFirstMoment.SieveKernel.exp_tail_indicator line 162
  9. lemma OAI.CubicFirstMoment.SieveKernel.finite_laplace_identity line 170
  10. theorem OAI.CubicFirstMoment.SieveKernel.finite_laplace_bound line 188
  11. lemma OAI.CubicFirstMoment.SieveKernel.laplace_rpow_integrable line 219
  12. lemma OAI.CubicFirstMoment.SieveKernel.laplace_rpow_integral line 229
  13. theorem OAI.CubicFirstMoment.SieveKernel.finite_laplace_power_bound line 245
  14. theorem OAI.CubicFirstMoment.SieveKernel.finite_laplace_polynomial_bound line 273
  15. lemma OAI.CubicFirstMoment.SieveKernel.finite_laplace_three_bound line 302