PublishedAdditiveSieve.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

The published additive large-sieve input over the Eisenstein integers

M. N. Huxley, The large sieve inequality for algebraic number fields, Mathematika 15 (1968), 178–187. The precise imaginary-quadratic form used here is displayed in P. Gao and L. Zhao, The large sieve with power moduli in imaginary quadratic number fields, IJNT 18 (2022), 1713–1733, arXiv:2101.00811v2, equation (1.2).

This is an explicit hypothesis type. The primitive multiplicative character inequality is to be derived by finite Gauss expansion and orthogonality; it is not assumed here.

def OAI.CubicFirstMoment.huxleyPhase line 26
Source documentation
Gao–Zhao's additive character e_K(nh/q), with sqrt(D_K)=traceLambda.
```
def huxleyPhase (q h n : Eisenstein) : ℂ :=
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein
def OAI.CubicFirstMoment.additiveSievePolynomial line 30
def OAI.CubicFirstMoment.huxleyModulusMass line 34
def OAI.CubicFirstMoment.huxleySieveMass line 39
lemma OAI.CubicFirstMoment.huxleyModulusMass_nonneg line 42
def OAI.CubicFirstMoment.HuxleyAdditiveLargeSieve line 50
Source documentation
Exact Q²+Z input, with neither a conductor power loss nor an invented multiplicative-character estimate hidden in the hypothesis.
```
def HuxleyAdditiveLargeSieve : Prop :=
…
```
lemma OAI.CubicFirstMoment.norm_huxleyPhase line 55