WeightedPrimeInput.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Applying the published prime input to smooth prime weights

Prime elements of equal norm are collected without identifying conjugate prime ideals. Complex Abel summation then derives the smooth-weighted estimate from CubicPrimeSiegelWalfisz. The weighted estimate follows by partial summation.

def OAI.CubicFirstMoment.primeNormCoefficient line 21
Source documentation
Coefficients collected by integer norm, on a finite ambient prime set.
```
def primeNormCoefficient (R : ℝ) (χ : Eisenstein → ℂ) (n : ℕ) : ℂ :=
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein
lemma OAI.CubicFirstMoment.primeNormCoefficient_cumulative line 24
lemma OAI.CubicFirstMoment.primeNormCoefficient_weighted line 45

theorem OAI.CubicFirstMoment.weighted_prime_bound line 60

Source documentation

Weighted interval sums inherit a uniform bound for all their unweighted prime prefixes, at the explicit cost of total variation of the weight.

theorem weighted_prime_bound (χ : Eisenstein → ℂ) (f : ℝ → ℂ)
    {a b H : ℝ} (ha : 0 ≤ a) (hab : a ≤ b)
    (hdiff : ∀ t ∈ Set.Icc a b, DifferentiableAt ℝ f t)
    (hderiv : IntegrableOn (deriv f) (Set.Icc a b))
    (hχ : ∀ t ∈ Set.Icc a b, ‖primeCutoffSum χ t‖ ≤ H) :
    ‖∑ p ∈ (primeCutoff b).filter (fun p => a < norm p), f (norm p) * χ p‖ ≤
      H * (‖f a‖ + ‖f b‖ + ∫ t in Set.Ioc a b, ‖deriv f t‖) := by
…

Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primeCutoffSum, OAI.CubicFirstMoment.primeCutoff, OAI.CubicFirstMoment.norm

theorem OAI.CubicFirstMoment.weighted_cubic_prime_bound line 75

Source documentation

The smooth-weighted form used for prime constituents in the new decomposition, derived solely from the cited unweighted Hecke input.

theorem weighted_cubic_prime_bound (hSW : CubicPrimeSiegelWalfisz)
    (A D : ℝ) (hA : 0 < A) (hD : 0 < D) :
    ∃ C X₀ : ℝ, 0 < C ∧ 1 < X₀ ∧
      ∀ a b : ℝ, X₀ ≤ a → a ≤ b →
        ∀ q₁ q₂ : Eisenstein,
          primary q₁ → primary q₂ → Squarefree q₁ → Squarefree q₂ →
          IsCoprime q₁ q₂ → MixedCubicNonprincipal q₁ q₂ →
          norm (q₁ * q₂) ≤ (Real.log a) ^ A →
          ∀ f : ℝ → ℂ,
            (∀ t ∈ Set.Icc a b, DifferentiableAt ℝ f t) →
            IntegrableOn (deriv f) (Set.Icc a b) →
            ‖∑ p ∈ (primeCutoff b).filter (fun p => a < norm p),
…

Mentions: OAI.CubicFirstMoment.CubicPrimeSiegelWalfisz, OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.MixedCubicNonprincipal, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.primeCutoff