PrimeSharpCutoff.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Sharp Fourier cutoff for actual prime sums

A fixed integer norm contains at most a conjugate pair of primary primes. Thus collecting prime coefficients by norm supplies the coefficient bound needed in the endpoint-kernel argument, without a norm-counting hypothesis.

lemma OAI.CubicFirstMoment.primaryPrime_eq_or_conjugate_of_norm_eq line 20
Distinct definitions of this name: OAI/NumberTheory/CubicMoment/Estimates/PrimeNormEndpoints.lean:13 (same statement text; different proof or body). Qualify references as OAI.CubicFirstMoment.primaryPrime_eq_or_conjugate_of_norm_eq@path.
lemma OAI.CubicFirstMoment.prime_norm_fiber_card_le_two line 34
def OAI.CubicFirstMoment.collectedPrimeCoefficient line 58
lemma OAI.CubicFirstMoment.collectedPrimeCoefficient_bound line 61
theorem OAI.CubicFirstMoment.prime_sharp_interval_sum_error line 75
Source documentation
An actual prime sum has the claimed endpoint cost after collecting both conjugates at each integer norm.
```
theorem prime_sharp_interval_sum_error (P : Finset Eisenstein)
    (hP : ∀ p ∈ P, primaryPrime p) (c : Eisenstein → ℂ)
    {X T M : ℝ} (hX : 0 < X) (hT : 0 < T) (hM : 0 ≤ M)
    (hPX : ∀ p ∈ P, norm p ≤ 4*X) (hc : ∀ p ∈ P, ‖c p‖ ≤ M) :
    ‖∑ p ∈ P, c p*sharpIntervalError X T (norm p)‖ ≤
      128*kernelMoment truncationKernel 1*M*(1+X/T) := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primaryPrime, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.sharpIntervalError, OAI.CubicFirstMoment.kernelMoment, OAI.CubicFirstMoment.truncationKernel

theorem OAI.CubicFirstMoment.prime_sharp_interval_error_isLittleO line 110

Source documentation

The endpoint error for uniformly bounded prime coefficients is negligible at the Patterson scale for every positive extra height.

theorem prime_sharp_interval_error_isLittleO {ρ M : ℝ} (hρ : 0 < ρ) (hρ₁ : ρ ≤ 5/6)
    (hM : 0 ≤ M) (P : ℝ → Finset Eisenstein) (c : ℝ → Eisenstein → ℂ)
    (hP : ∀ X, 1 ≤ X → ∀ p ∈ P X, primaryPrime p ∧ norm p ≤ 4*X)
    (hc : ∀ X, 1 ≤ X → ∀ p ∈ P X, ‖c X p‖ ≤ M) :
    (fun X : ℝ => ∑ p ∈ P X, c X p*
      sharpIntervalError X (X^(1/6+ρ : ℝ)) (norm p)) =o[Filter.atTop] firstMomentScale := by
…

Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primaryPrime, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.sharpIntervalError, OAI.CubicFirstMoment.firstMomentScale