UniformNoncubeGap.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Compactness makes the nonexceptional conductor saving uniform.

theorem OAI.CubicFirstMoment.uniform_noncube_exponent_gap line 14
Source documentation
With a positive conductor threshold and fixed neighborhoods of the two exceptional shapes removed, one of the three sieve bounds saves a single uniform positive power.
```
theorem uniform_noncube_exponent_gap {κ δ : ℝ} (hκ : 0 < κ) (hδ : 0 < δ) :
    ∃ γ : ℝ, 0 < γ ∧ ∀ p q : ℝ, 0 ≤ p → 0 ≤ q → p+2*q ≤ 1 →
      κ ≤ p+2*q → δ ≤ |p-1|+|q| → δ ≤ |p-1/3|+|q-1/3| →
      noncubeSieveExponent p q ≤ -γ := by
…
```
Mentions: OAI.CubicFirstMoment.noncubeSieveExponent