ThreePrimeMinorArc.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.ThreePrimeMinorArc.prime_sum_norm_le_theta line 12

Source documentation

The prime logarithmic polynomial has global size at most Chebyshev's theta function, for arbitrary phases of norm at most one.

theorem prime_sum_norm_le_theta (u : ℕ) (phase : ℕ → ℂ)
    (hphase : ∀ p ∈ Nat.primesLE u, ‖phase p‖ ≤ 1) :
    ‖∑ p ∈ Nat.primesLE u, (Real.log (p : ℝ) : ℂ) * phase p‖ ≤
      Chebyshev.theta (u : ℝ) := by
…

theorem OAI.Problem337.ThreePrimeMinorArc.prime_sum_norm_le line 26

Source documentation

An unconditional linear global amplitude bound, with an explicit constant.

theorem prime_sum_norm_le (u : ℕ) (phase : ℕ → ℂ)
    (hphase : ∀ p ∈ Nat.primesLE u, ‖phase p‖ ≤ 1) :
    ‖∑ p ∈ Nat.primesLE u, (Real.log (p : ℝ) : ℂ) * phase p‖ ≤
      Real.log 4 * (u : ℝ) :=
…

theorem OAI.Problem337.ThreePrimeMinorArc.cubic_contribution_le_energy line 37

Source documentation

The cubic contribution of any set of frequencies is controlled by a uniform bound on that set and the full Fourier energy. The twist may be any function of norm at most one. This is the elementary minor-arc reduction, not an assertion of a prime exponential-sum estimate.

theorem cubic_contribution_le_energy {q : ℕ} [NeZero q]
    (w : ZMod q → ℂ) (minor : Finset (ZMod q))
    (twist : ZMod q → ℂ) (A : ℝ) (hA : 0 ≤ A)
    (hbound : ∀ r ∈ minor, ‖residueFourier w r‖ ≤ A)
    (htwist : ∀ r ∈ minor, ‖twist r‖ ≤ 1) :
    ‖(∑ r ∈ minor, residueFourier w r ^ 3 * twist r) / (q : ℂ)‖ ≤
      A * ∑ n : ZMod q, ‖w n‖ ^ 2 := by
…

Mentions: OAI.Problem337.residueFourier

theorem OAI.Problem337.ThreePrimeMinorArc.cubic_character_contribution_le_energy line 64

Source documentation

The usual additive-character twist for the coefficient at u.

theorem cubic_character_contribution_le_energy {q : ℕ} [NeZero q]
    (w : ZMod q → ℂ) (minor : Finset (ZMod q)) (u : ZMod q)
    (A : ℝ) (hA : 0 ≤ A)
    (hbound : ∀ r ∈ minor, ‖residueFourier w r‖ ≤ A) :
    ‖(∑ r ∈ minor, residueFourier w r ^ 3 * ZMod.stdAddChar (-(r * u))) /
        (q : ℂ)‖ ≤ A * ∑ n : ZMod q, ‖w n‖ ^ 2 := by
…

Mentions: OAI.Problem337.residueFourier

def OAI.Problem337.ThreePrimeMinorArc.primeLogWeight line 75
Source documentation
Prime logarithmic weights, zero padded in a cyclic group.
```
def primeLogWeight {q : ℕ} [NeZero q] (u : ℕ) (n : ZMod q) : ℂ :=
…
```
theorem OAI.Problem337.ThreePrimeMinorArc.primeLogWeight_energy line 79
Source documentation
Zero padding preserves the exact prime-weight energy when u < q.
```
theorem primeLogWeight_energy {q : ℕ} [NeZero q] (u : ℕ) (huq : u < q) :
    (∑ n : ZMod q, ‖primeLogWeight u n‖ ^ 2) =
      ∑ p ∈ Nat.primesLE u, Real.log (p : ℝ) ^ 2 := by
…
```
Mentions: OAI.Problem337.ThreePrimeMinorArc.primeLogWeight

theorem OAI.Problem337.ThreePrimeMinorArc.residueFourier_primeLogWeight line 103

Source documentation

The zero-padded transform is exactly the usual prime exponential sum.

theorem residueFourier_primeLogWeight {q : ℕ} [NeZero q]
    (u : ℕ) (huq : u < q) (r : ZMod q) :
    residueFourier (primeLogWeight u) r =
      ∑ p ∈ Nat.primesLE u,
        (Real.log (p : ℝ) : ℂ) * ZMod.stdAddChar (r * (p : ZMod q)) := by
…

Mentions: OAI.Problem337.residueFourier, OAI.Problem337.ThreePrimeMinorArc.primeLogWeight

theorem OAI.Problem337.ThreePrimeMinorArc.prime_log_squares_le line 130
Source documentation
A Chebyshev energy bound saves one logarithm compared with the trivial bound obtained by counting all integers up to u.
```
theorem prime_log_squares_le (u : ℕ) (hu : 1 ≤ u) :
    (∑ p ∈ Nat.primesLE u, Real.log (p : ℝ) ^ 2) ≤
      Real.log 4 * (u : ℝ) * Real.log (u : ℝ) := by
…
```

theorem OAI.Problem337.ThreePrimeMinorArc.prime_cubic_contribution_le line 153

Source documentation

A minor-frequency supremum bound for the actual prime sum yields a quadratic error with the Chebyshev constant made explicit.

theorem prime_cubic_contribution_le {q : ℕ} [NeZero q]
    (u : ℕ) (hu : 2 ≤ u) (huq : u < q) (minor : Finset (ZMod q))
    (ε : ℝ) (hε : 0 ≤ ε)
    (hbound : ∀ r ∈ minor,
      ‖∑ p ∈ Nat.primesLE u,
        (Real.log (p : ℝ) : ℂ) * ZMod.stdAddChar (r * (p : ZMod q))‖ ≤
          ε * (u : ℝ) / Real.log (u : ℝ)) :
    ‖(∑ r ∈ minor, (∑ p ∈ Nat.primesLE u,
        (Real.log (p : ℝ) : ℂ) * ZMod.stdAddChar (r * (p : ZMod q))) ^ 3 *
          ZMod.stdAddChar (-(r * (u : ZMod q)))) / (q : ℂ)‖ ≤
      ε * Real.log 4 * (u : ℝ) ^ 2 := by
…