ArithmeticInputs.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Published arithmetic inputs at the strength needed here

The fixed-order Selberg–Delange expansion is Granville–Koukoulopoulos, Beyond the LSD method (2019), Theorem 1, specialized to μ²(n) z^ω(n), or Koukoulopoulos, The Distribution of Prime Numbers, Theorem 13.2. The expansion concerns squarefree weights and contains no character estimates.

def OAI.JointDickman.squarefreeSummatory line 23
def OAI.JointDickman.squarefreeLeadingConstant line 27
Source documentation
The convergent Euler-product normalization of the first LSD coefficient.
```
noncomputable def squarefreeLeadingConstant (z : ℝ) : ℝ :=
…
```
def OAI.JointDickman.PublishedInputs.SquarefreeSelbergDelangeInput line 35
Source documentation
Only the two positive exponents used by the paper, with all fixed expansion orders and the actual leading coefficient.
```
def SquarefreeSelbergDelangeInput : Prop :=
…
```
def OAI.JointDickman.PublishedInputs.PrimeReciprocalMertensInput line 46
Source documentation
The classical reciprocal-prime Mertens estimate, at its usual O(1/log x) strength: Montgomery–Vaughan, Multiplicative Number Theory I, Theorem 2.7(d).
```
def PrimeReciprocalMertensInput : Prop :=
…
```
def OAI.JointDickman.PublishedInputs.PrimeProductMertensInput line 53
Source documentation
Mertens' product theorem, with its normalized limiting constant: Montgomery–Vaughan, Multiplicative Number Theory I, Theorem 2.7(e).
```
def PrimeProductMertensInput : Prop :=
…
```
theorem OAI.JointDickman.squarefreeSummatory_one_term line 62
Source documentation
The fixed-order expansion in particular supplies the leading term with one full logarithmic saving, with no uniformity in an unbounded order.
```
theorem squarefreeSummatory_one_term
    (hSD : PublishedInputs.SquarefreeSelbergDelangeInput) {z : ℝ}
    (hz : z = 1 / 4 ∨ z = 1 / 2) :
    ∃ C : ℝ, 0 ≤ C ∧ ∀ Y : ℝ, 3 ≤ Y →
      |squarefreeSummatory z Y -
        Y * squarefreeLeadingConstant z * (Real.log Y) ^ (z - 1)| ≤
          C * Y * (Real.log Y) ^ (z - 2) := by
…
```
Mentions: OAI.JointDickman.PublishedInputs.SquarefreeSelbergDelangeInput, OAI.JointDickman.squarefreeSummatory, OAI.JointDickman.squarefreeLeadingConstant
theorem OAI.JointDickman.squarefreeSummatory_normalized_tendsto line 75
Source documentation
The leading normalized asymptotic, proved from the cited expansion.
```
theorem squarefreeSummatory_normalized_tendsto
    (hSD : PublishedInputs.SquarefreeSelbergDelangeInput) {z : ℝ}
    (hz : z = 1 / 4 ∨ z = 1 / 2) :
    Tendsto (fun Y : ℝ => squarefreeSummatory z Y /
      (Y * (Real.log Y) ^ (z - 1))) atTop (𝓝 (squarefreeLeadingConstant z)) := by
…
```
Mentions: OAI.JointDickman.PublishedInputs.SquarefreeSelbergDelangeInput, OAI.JointDickman.squarefreeSummatory, OAI.JointDickman.squarefreeLeadingConstant