OAI/NumberTheory/CubicGauss/GaussianKernel.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Gaussian lattice decay, shell bounds and integral estimates.

  1. lemma OAI.CubicFirstMoment.SieveKernel.norm_weighted_pair_sum line 14
  2. abbrev OAI.CubicFirstMoment.SieveKernel.Index line 38
  3. def OAI.CubicFirstMoment.SieveKernel.coefficient line 39
  4. def OAI.CubicFirstMoment.SieveKernel.majorant line 43
  5. lemma OAI.CubicFirstMoment.SieveKernel.exp_series_complex line 47
  6. lemma OAI.CubicFirstMoment.SieveKernel.exp_series_real line 50
  7. lemma OAI.CubicFirstMoment.SieveKernel.hasSum_mul_complex line 53
  8. lemma OAI.CubicFirstMoment.SieveKernel.hasSum_mul_real line 59
  9. lemma OAI.CubicFirstMoment.SieveKernel.kernel_hasSum line 65
  10. lemma OAI.CubicFirstMoment.SieveKernel.majorant_hasSum line 84
  11. lemma OAI.CubicFirstMoment.SieveKernel.coefficient_norm_le line 99
  12. lemma OAI.CubicFirstMoment.SieveKernel.power_coefficient_energy line 108
  13. theorem OAI.CubicFirstMoment.SieveKernel.gaussian_gram_bound line 133
  14. lemma OAI.CubicFirstMoment.SieveKernel.gaussian_gram_envelope line 191