NoncubePowerBounds.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

Exact normalization of the three numerical sieve bounds, and a quantitative uniform power saving away from the exceptional configurations.

def OAI.CubicFirstMoment.pSieveRatio line 12
Source documentation
The actual cubic-sieve bound, divided by the dispersion benchmark.
```
def pSieveRatio (B P Q : ℝ) : ℝ :=
…
```
def OAI.CubicFirstMoment.qSieveRatio line 15
def OAI.CubicFirstMoment.ordinarySieveRatio line 18
lemma OAI.CubicFirstMoment.sieve_power_mul_div line 21
lemma OAI.CubicFirstMoment.sieve_power_denominator line 25
lemma OAI.CubicFirstMoment.pSieveRatio_eq_powers line 36
lemma OAI.CubicFirstMoment.qSieveRatio_eq_powers line 61
lemma OAI.CubicFirstMoment.ordinarySieveRatio_eq_powers line 86
lemma OAI.CubicFirstMoment.sieve_three_power_le line 103
lemma OAI.CubicFirstMoment.pSieveRatio_le line 112
lemma OAI.CubicFirstMoment.qSieveRatio_le line 117
lemma OAI.CubicFirstMoment.ordinarySieveRatio_le line 122
theorem OAI.CubicFirstMoment.noncubeSieveRatio_le line 136
Source documentation
This is the numerical bound used after normalizing the concrete sieve estimates; the exponent is the limiting exponent.
```
theorem noncubeSieveRatio_le {B : ℝ} (hB : 1 ≤ B) (p q : ℝ) :
    min (pSieveRatio B (B^p) (B^q))
      (min (qSieveRatio B (B^p) (B^q)) (ordinarySieveRatio B (B^p) (B^q))) ≤
      3*B^(noncubeSieveExponent p q) := by
…
```
Mentions: OAI.CubicFirstMoment.pSieveRatio, OAI.CubicFirstMoment.qSieveRatio, OAI.CubicFirstMoment.ordinarySieveRatio, OAI.CubicFirstMoment.noncubeSieveExponent

theorem OAI.CubicFirstMoment.uniform_noncube_ratio_saving line 153

Source documentation

A uniform power saving survives all additional losses with exponent at most half the compactness gap.

theorem uniform_noncube_ratio_saving {κ δ : ℝ} (hκ : 0 < κ) (hδ : 0 < δ) :
    ∃ γ : ℝ, 0 < γ ∧ ∀ (B p q η : ℝ), 1 ≤ B →
      0 ≤ p → 0 ≤ q → p+2*q ≤ 1 → κ ≤ p+2*q →
      δ ≤ |p-1|+|q| → δ ≤ |p-1/3|+|q-1/3| → η ≤ γ/2 →
      B^η * min (pSieveRatio B (B^p) (B^q))
        (min (qSieveRatio B (B^p) (B^q)) (ordinarySieveRatio B (B^p) (B^q))) ≤
          3*B^(-γ/2) := by
…

Mentions: OAI.CubicFirstMoment.pSieveRatio, OAI.CubicFirstMoment.qSieveRatio, OAI.CubicFirstMoment.ordinarySieveRatio