MinorArcBudget.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.ThreePrimeAnalysis.vaughan_envelope_le_log_budget line 12

Source documentation

Explicit arithmetic loss budget for a standard Vaughan-type envelope. This is a scalar inequality: it does not assume or assert an exponential-sum estimate for primes.

theorem vaughan_envelope_le_log_budget (N q C : ℝ)
    (hN : 1 < N) (hC : 0 ≤ C)
    (hconstant : 3 * C ≤ Real.log N ^ 2)
    (hsmall : Real.log N ^ 11 ≤ N ^ (1 / 5 : ℝ))
    (hqlow : Real.log N ^ 22 ≤ q)
    (hqup : q ≤ N / Real.log N ^ 22) :
    C * (N / Real.sqrt q + N ^ (4 / 5 : ℝ) + Real.sqrt (N * q)) *
        Real.log N ^ 4 ≤ N / Real.log N ^ 5 := by
…

theorem OAI.Problem337.ThreePrimeAnalysis.eventually_vaughan_envelope_le_log_budget line 55

Source documentation

A fixed envelope coefficient is absorbed uniformly over the entire minor rational-denominator window. The onset depends only on C.

theorem eventually_vaughan_envelope_le_log_budget (C : ℝ) (hC : 0 ≤ C) :
    ∀ᶠ N : ℝ in atTop, ∀ q : ℝ,
      Real.log N ^ 22 ≤ q → q ≤ N / Real.log N ^ 22 →
      C * (N / Real.sqrt q + N ^ (4 / 5 : ℝ) + Real.sqrt (N * q)) *
        Real.log N ^ 4 ≤ N / Real.log N ^ 5 := by
…

theorem OAI.Problem337.ThreePrimeAnalysis.eventually_minor_cubic_log_budget line 78
Source documentation
Combining a N/log(N)^5 pointwise minor-arc bound with any fixed A*N*log(N) energy budget gives an arbitrarily small quadratic error.
```
theorem eventually_minor_cubic_log_budget (A ε : ℝ) (hA : 0 ≤ A) (hε : 0 < ε) :
    ∀ᶠ N : ℝ in atTop,
      (N / Real.log N ^ 5) * (A * N * Real.log N) ≤ ε * N ^ 2 := by
…
```

theorem OAI.Problem337.ThreePrimeAnalysis.vaughan_envelope_le_power_log_budget line 99

Source documentation

Variable logarithmic losses need only a correspondingly wider rational cutoff. This form is useful when a coefficient moment yields an unspecified but fixed power of the logarithm.

theorem vaughan_envelope_le_power_log_budget (B D : ℕ) (N q C : ℝ)
    (hN : 1 < N) (hC : 0 ≤ C)
    (hconstant : 3 * C ≤ Real.log N ^ 2)
    (hsmall : Real.log N ^ (B + D + 2) ≤ N ^ (1 / 5 : ℝ))
    (hqlow : Real.log N ^ (2 * (B + D + 2)) ≤ q)
    (hqup : q ≤ N / Real.log N ^ (2 * (B + D + 2))) :
    C * (N / Real.sqrt q + N ^ (4 / 5 : ℝ) + Real.sqrt (N * q)) *
        Real.log N ^ B ≤ N / Real.log N ^ D := by
…

Mentions: OAI.Problem337.D

theorem OAI.Problem337.ThreePrimeAnalysis.eventually_vaughan_envelope_le_power_log_budget line 146

Source documentation

Any fixed polynomial logarithmic loss has a uniform minor-window budget. Neither the fixed log exponents nor the implied constant depend on N or q.

theorem eventually_vaughan_envelope_le_power_log_budget (B D : ℕ) (C : ℝ) (hC : 0 ≤ C) :
    ∀ᶠ N : ℝ in atTop, ∀ q : ℝ,
      Real.log N ^ (2 * (B + D + 2)) ≤ q →
      q ≤ N / Real.log N ^ (2 * (B + D + 2)) →
      C * (N / Real.sqrt q + N ^ (4 / 5 : ℝ) + Real.sqrt (N * q)) *
        Real.log N ^ B ≤ N / Real.log N ^ D := by
…

Mentions: OAI.Problem337.D