OAI/NumberTheory/CubicGauss/DualGram.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Gaussian smoothing, transformed cubic Gram sums and dual operator bounds.

  1. lemma OAI.CubicFirstMoment.real_gaussian_summable line 17
  2. lemma OAI.CubicFirstMoment.gaussian_pair_summable line 29
  3. lemma OAI.CubicFirstMoment.gaussian_kernel_summable line 52
  4. theorem OAI.CubicFirstMoment.gaussian_lattice_gram_bound line 83
  5. def OAI.CubicFirstMoment.cubicG line 108
  6. lemma OAI.CubicFirstMoment.cubicG_eq line 111
  7. lemma OAI.CubicFirstMoment.norm_cubicG line 115
  8. def OAI.CubicFirstMoment.sieveFiber line 120
  9. lemma OAI.CubicFirstMoment.mem_sieveFiber line 123
  10. lemma OAI.CubicFirstMoment.sum_product_explicit line 127
  11. lemma OAI.CubicFirstMoment.sum_common_by_fiber line 131
  12. def OAI.CubicFirstMoment.cubicDualPair line 150
  13. theorem OAI.CubicFirstMoment.cubic_gaussian_gram_transform line 158
  14. def OAI.CubicFirstMoment.cubicDualForm line 232
  15. theorem OAI.CubicFirstMoment.cubic_dual_form_bound line 237