OAI/NumberTheory/CubicMoment/Estimates/PrimeMellinTransfer.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The prime comparison through a common-height integral

The angular Gauss-minus-model coefficients are uniformly bounded. The actual sharp dyadic prime sum differs negligibly from the same finite polynomial integrated against the constructed Mellin cutoff.

  1. def OAI.CubicFirstMoment.primeComparisonCoefficient line 19
  2. lemma OAI.CubicFirstMoment.primeComparisonCoefficient_bound line 22
  3. def OAI.CubicFirstMoment.sharpDyadicPrimeComparison line 35
  4. def OAI.CubicFirstMoment.smoothedDyadicPrimeComparison line 38
  5. def OAI.CubicFirstMoment.comparisonMellinIntegral line 42
  6. lemma OAI.CubicFirstMoment.smoothedDyadicPrimeComparison_eq_integral line 46
  7. lemma OAI.CubicFirstMoment.sharpDyadicPrimeComparison_sub_smooth line 52
  8. theorem OAI.CubicFirstMoment.sharpDyadicPrimeComparison_sub_integral_isLittleO line 61

    Source documentation

    The exact inverse-transform integral approximates the actual angular Gauss-minus-model prime sum at the required first-moment scale.

    theorem sharpDyadicPrimeComparison_sub_integral_isLittleO (ℓ : ℤ) {ρ : ℝ}
    (hρ : 0 < ρ) (hρ₁ : ρ ≤ 5/6) :
    (fun X : ℝ => sharpDyadicPrimeComparison ℓ X - comparisonMellinIntegral ℓ ρ X)
      =o[Filter.atTop] firstMomentScale := by
…

    Mentions: OAI.CubicFirstMoment.sharpDyadicPrimeComparison, OAI.CubicFirstMoment.comparisonMellinIntegral, OAI.CubicFirstMoment.firstMomentScale