MetaplecticAuxiliary.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

The auxiliary functions in Heath-Brown (2000), §3, equations (14) and (19), and the finite-divisor estimate on author-manuscript p.14. Only fixed-level strip growth is needed here, so the finite-divisor estimate drops its factors at most one. All polynomial estimates below are derived from the stated auxiliary bound and convergent Euler inverse.

def OAI.CubicFirstMoment.metaplecticPsiSeries line 17
def OAI.CubicFirstMoment.metaplecticZetaInverse line 21
def OAI.CubicFirstMoment.metaplecticPrimaryDivisors line 25
def OAI.CubicFirstMoment.HeathBrownZBound line 30
Source documentation
HB §3 (19), at large height only. The parameter e is retained literally; the application below uses just e = 1/10.
```
def HeathBrownZBound (Z : Eisenstein → ℂ → ℂ) : Prop :=
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein
def OAI.CubicFirstMoment.HeathBrownZFactorization line 38
Source documentation
Equation (14), after division by its absolutely convergent Euler factor. The reciprocal is the literal primary Möbius series above.
```
def HeathBrownZFactorization (Ψ Z : Eisenstein → ℂ → ℂ) : Prop :=
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein
def OAI.CubicFirstMoment.HeathBrownFiniteDivisor line 48
Source documentation
The finite-divisor inequality following the exact identity on HB p.14. Since Nr, Nd ≥ 1, its factors (Nr)^(-1/2) and (Nd)^(-1/2) are discarded, and complementary divisors are reindexed. This weaker fixed-level version suffices solely to justify a contour shift.
```
def HeathBrownFiniteDivisor (F Ψ : Eisenstein → ℂ → ℂ) : Prop :=
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein
lemma OAI.CubicFirstMoment.norm_idealMoebius_le_one line 55
Distinct definitions of this name: OAI/NumberTheory/CubicGram/CubicOperator.lean:407 (different declaration text). Qualify references as OAI.CubicFirstMoment.norm_idealMoebius_le_one@path.
lemma OAI.CubicFirstMoment.metaplecticZetaInverse_uniform line 62
lemma OAI.CubicFirstMoment.heathBrown_Z_polynomial line 81
lemma OAI.CubicFirstMoment.heathBrown_psi_polynomial line 102
lemma OAI.CubicFirstMoment.heathBrown_left_strip_polynomial line 123
Source documentation
Fixed-level growth on the left part of the contour strip, derived from HB's auxiliary bound rather than assumed for the original series.
```
lemma heathBrown_left_strip_polynomial {F Ψ Z : Eisenstein → ℂ → ℂ}
    (hZ : HeathBrownZBound Z) (hfac : HeathBrownZFactorization Ψ Z)
    (hdiv : HeathBrownFiniteDivisor F Ψ) {δ : ℝ} (hδ : 0 < δ)
    {r : Eisenstein} (hr : primary r) (hs : Squarefree r) :
    MetaplecticStripPolynomial (F r) (1/2+δ) (9/10) := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.HeathBrownZBound, OAI.CubicFirstMoment.HeathBrownZFactorization, OAI.CubicFirstMoment.HeathBrownFiniteDivisor, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.MetaplecticStripPolynomial