OAI/NumberTheory/CubicMoment/Estimates/PrimeHeightDecomposition.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Exact low-height and dyadic-window decomposition of the sharp prime comparison. The large-height model is controlled before any factorization of the Gauss sum is used.

  1. def OAI.CubicFirstMoment.finiteHeightLow line 14
  2. def OAI.CubicFirstMoment.finiteHeightTail line 20
  3. lemma OAI.CubicFirstMoment.heightFourierIntegral_partition line 27
  4. lemma OAI.CubicFirstMoment.finite_height_partition line 44
  5. lemma OAI.CubicFirstMoment.finite_smooth_low_tail line 54
  6. lemma OAI.CubicFirstMoment.finiteHeightTail_linear line 66
  7. def OAI.CubicFirstMoment.primeComparisonLowHeight line 73
  8. def OAI.CubicFirstMoment.primeGaussHeightTail line 76
  9. lemma OAI.CubicFirstMoment.sharp_prime_comparison_low_tail line 79
  10. theorem OAI.CubicFirstMoment.actual_prime_model_height_tail_isLittleO line 116
  11. theorem OAI.CubicFirstMoment.sharp_prime_comparison_sub_low_and_gauss_tail line 128