CharacterInputs.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The published character estimate

The input is the Siegel–Walfisz specialization of Singha Roy, The Landau–Selberg–Delange method for products of Dirichlet L-functions, and applications, I, arXiv:2511.15928v1, Theorem 1.1 and Corollary 1.2, with Siegel's bound (Koukoulopoulos, Theorem 12.10). Take ν = 1, the exponent z at one nonprincipal character, and zero at every other character. The Euler correction is absolutely convergent for Re(s)>1/2; the principal exponent is zero, so all the main coefficients vanish. This is an explicit conditional input, not a proof of that analytic result.

def OAI.JointDickman.squarefreeCharacterSum line 24
Source documentation
Twist the squarefree coefficients, before removing any small primes.
```
noncomputable def squarefreeCharacterSum {q : ℕ}
    (χ : DirichletCharacter ℂ q) (z Y : ℝ) : ℂ :=
…
```
def OAI.JointDickman.PublishedInputs.SquarefreeCharacterEstimateInput line 32
Source documentation
Only the two exponents and the arbitrary fixed logarithmic saving needed for the moving-cutoff argument are retained.
```
def SquarefreeCharacterEstimateInput : Prop :=
…
```