Arithmetic.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Arithmetic estimates for prime-degree torus packets

The real-variable comparison controls the contribution of a nontrivial zero after applying Stark (1974), Lemmas 3 and 8. The discriminant and local-moment estimates relate the arithmetic counting scales.

theorem OAI.DukePrimeDegree.zero_contribution_comparison line 24
Source documentation
Uniform comparison of a zero's contribution to the logarithmic derivative, once its rescaled distance from 1 is bounded below. The constant is slightly larger than the manuscript's, which is harmless.
```
theorem zero_contribution_comparison
    {X Y U c : ℝ} (hX : 0 ≤ X) (hU : 0 < U) (hU4 : U ≤ 4)
    (hc : 0 < c) (hgap : c ^ 2 ≤ X ^ 2 + Y ^ 2) :
    (X + U) / ((X + U) ^ 2 + Y ^ 2) ≤
      (8 + 8 / c ^ 2) * ((X + 1) / ((X + 1) ^ 2 + Y ^ 2)) := by
…
```
theorem OAI.DukePrimeDegree.scale_tendsto_atTop line 51
Source documentation
The packet discriminant bound suffices to transfer divergence from the multiplier-order discriminant to the counting scale.
```
theorem scale_tendsto_atTop {D Q : ℕ → ℝ} {k : ℕ}
    (hQ : ∀ i, 0 ≤ Q i) (hbound : ∀ i, D i ≤ Q i ^ k)
    (hD : Tendsto D atTop atTop) : Tendsto Q atTop atTop := by
…
```
theorem OAI.DukePrimeDegree.weighted_tail_le_moment line 66
Source documentation
Markov's estimate for arbitrary (possibly correlated) local shells. All sums are extended nonnegative sums, so no convergence hypothesis is needed. This is the tail extraction used in lem:local-moment.
```
theorem weighted_tail_le_moment {α : Type*} (mass size : α → ℝ≥0∞)
    (R : ℝ≥0∞) (s : ℝ) (hs : 0 ≤ s) (hR : R ≠ 0) (hRtop : R ≠ ∞) :
    (∑' i, if R < size i then mass i else 0) ≤
      (R ^ s)⁻¹ * ∑' i, mass i * size i ^ s := by
…
```
theorem OAI.DukePrimeDegree.tail_exponent_absorption line 91
Source documentation
Absorb the harmless q^(s/16) loss in the moment bound into the cutoff Q^(1/8). This is the exponent calculation giving Q^(-s/16) in the local-weight tail estimate, using only q ≤ Q.
```
theorem tail_exponent_absorption {q Q s : ℝ} (hq : 0 ≤ q) (hQ : 0 < Q)
    (hqQ : q ≤ Q) (hs : 0 ≤ s) :
    Q ^ (-s / 8) * q ^ (s / 16) ≤ Q ^ (-s / 16) := by
…
```