PublishedPrimitiveHecke.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The classical primitive Hecke input on the actual finite residue characters constructed here. Completion/functional equation: Watkins (2011), §3.6, p.123; entire order-one completion: Thorner–Zaman (2019), §2C, p.1049, Eq.(2-15). This is a conditional input, not an axiom. No character sum estimate or new-paper conclusion is included.

def OAI.CubicFirstMoment.residueHeckeScale line 16
lemma OAI.CubicFirstMoment.residueHeckeScale_pos line 18
def OAI.CubicFirstMoment.PrimitiveResidueHeckeInput line 26
Source documentation
The standard analytic continuation and functional equation for a primitive nonprincipal finite Hecke character with trivial infinity type. The two Dirichlet series are literally those of the residue character and its complex conjugate on the complete ideal exponent lattice.
```
def PrimitiveResidueHeckeInput : Prop :=
…
```
theorem OAI.CubicFirstMoment.primitive_residue_analytic_data line 39
Source documentation
The published continuation/functional-equation input supplies the analytic properties of the primitive residue character. The growth needed for contour shifts follows by the Phragmén–Lindelöf theorem.
```
theorem primitive_residue_analytic_data (hpub : PrimitiveResidueHeckeInput)
    {q : Eisenstein} (hq : q ≠ 0) (χ : MulChar (Residues q) ℂ)
    (hp : PrimitiveResidueCharacter q χ) (hn : χ ≠ 1)
    (hu : ∀ u : Eisensteinˣ, χ (Ideal.Quotient.mk (modulus q) u) = 1)
    (hGamma : ∀ m : ℕ, GammaInverseFiniteOrder (1/2-(m:ℝ)) 2) :
    ∃ (root : ℂ) (L Ldual : ℂ → ℂ), ‖root‖ = 1 ∧
      PrimitiveHeckeAnalyticData (residueIdealChar q χ) (residueIdealChar q (star χ))
        (residueHeckeScale q) root L Ldual := by
…
```
Mentions: OAI.CubicFirstMoment.PrimitiveResidueHeckeInput, OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.Residues, OAI.CubicFirstMoment.PrimitiveResidueCharacter, OAI.CubicFirstMoment.modulus, OAI.CubicFirstMoment.GammaInverseFiniteOrder, OAI.CubicFirstMoment.PrimitiveHeckeAnalyticData, OAI.CubicFirstMoment.residueIdealChar, OAI.CubicFirstMoment.residueHeckeScale

theorem OAI.CubicFirstMoment.primitive_residue_smooth_approximation line 55

Source documentation

An actual primitive residue character has the full smooth dual approximation with a uniform error, from the published input above and the explicit weak Gamma bounds.

theorem primitive_residue_smooth_approximation (hpub : PrimitiveResidueHeckeInput)
    (W : ℝ → ℂ) (hW : HasCompactSupport W) (hpos : tsupport W ⊆ Ioi 0)
    (hsm : ContDiff ℝ ∞ W) {δ : ℝ} (hδ : 0 < δ) (H R : ℝ)
    (hGI : ∀ m : ℕ, GammaInverseFiniteOrder (1/2-(m:ℝ)) 2)
    (hGQ : ∀ m : ℕ, GammaQuotientStripBound (1/2-(m:ℝ))) :
    ∃ C : ℝ, 0 ≤ C ∧ ∀ (q : Eisenstein), q ≠ 0 →
      ∀ χ : MulChar (Residues q) ℂ, PrimitiveResidueCharacter q χ → χ ≠ 1 →
      (∀ u : Eisensteinˣ, χ (Ideal.Quotient.mk (modulus q) u) = 1) →
      ∃ root : ℂ, ‖root‖ = 1 ∧ ∀ (Y Z J t : ℝ),
      1 ≤ Y → 1 ≤ Z → 0 < J → Z ≤ Y^H → J ≤ Y^H →
      ((residueHeckeScale q)^2*(1+|t|)^2)/(Z*J) ≤ Y^(-δ) →
      ‖(∑' ν, residueIdealChar q χ ν*mellinPhase t (idealExponentNorm ν)*W (idealExponentNorm ν/Z))-
…

Mentions: OAI.CubicFirstMoment.PrimitiveResidueHeckeInput, OAI.CubicFirstMoment.GammaInverseFiniteOrder, OAI.CubicFirstMoment.GammaQuotientStripBound, OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.Residues, OAI.CubicFirstMoment.PrimitiveResidueCharacter, OAI.CubicFirstMoment.modulus, OAI.CubicFirstMoment.residueHeckeScale, OAI.CubicFirstMoment.residueIdealChar, OAI.CubicFirstMoment.mellinPhase, OAI.CubicFirstMoment.idealExponentNorm