CubePairAsymptotic.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The actual cube part of a Gram entry, with the multiplicity three and the coprimality error retained.

lemma OAI.CubicFirstMoment.gramDualTerm_cube line 15
lemma OAI.CubicFirstMoment.cube_gram_series line 25

theorem OAI.CubicFirstMoment.cube_gram_asymptotic line 59

Source documentation

A fixed radial weight has a uniform principal-frequency expansion. The two errors are the bounded lattice error and the explicit rough-prime exclusion error. The lattice scale is linked to the actual Poisson scale.

theorem cube_gram_asymptotic (W : ℝ → ℂ)
    (hW : HasCompactSupport W) (hW' : ContDiff ℝ ∞ W) :
    ∃ C K : ℝ, 0 < C ∧ 0 < K ∧ ∀ (a b : Eisenstein),
      primary a → Squarefree a → primary b → Squarefree b →
      ∀ A q : ℝ, 0 ≤ A → 0 < q → q ≤ 1 → q^3 = A/(27*norm (b*a)) →
      ‖(∑' h : Eisenstein, if h ≠ 0 ∧ (∃ j : Eisenstein, j^3 = h) then
          gramDualTerm b a W A h else 0) -
        (1/(3*q):ℝ) • cubeProfileIntegral W‖ ≤
        (C+K/q*∑ p ∈ primaryPrimeFactors a ∪ primaryPrimeFactors b, 1/norm p)/3 := by
…

Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.gramDualTerm, OAI.CubicFirstMoment.cubeProfileIntegral, OAI.CubicFirstMoment.primaryPrimeFactors