PrimePowerFourierError.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.norm_mangoldt_sum_sub_prime_sum_le line 14

Source documentation

Removing proper prime powers from a bounded complex-weighted sum costs exactly at most the difference of the Chebyshev functions. The bound is uniform in the phase and requires no cancellation hypothesis.

theorem norm_mangoldt_sum_sub_prime_sum_le (N : ℕ) (f : ℕ → ℂ)
    (hf : ∀ n ∈ Finset.Icc 1 N, ‖f n‖ ≤ 1) :
    ‖(∑ n ∈ Finset.Icc 1 N, (ArithmeticFunction.vonMangoldt n : ℂ) * f n) -
      ∑ n ∈ Finset.Icc 1 N, (primeLogWeight n : ℂ) * f n‖ ≤
        Chebyshev.psi N - Chebyshev.theta N := by
…

Mentions: OAI.Problem337.primeLogWeight

theorem OAI.Problem337.norm_prime_sum_sub_mangoldt_sum_le line 28

Source documentation

The same removal estimate with the prime sum first.

theorem norm_prime_sum_sub_mangoldt_sum_le (N : ℕ) (f : ℕ → ℂ)
    (hf : ∀ n ∈ Finset.Icc 1 N, ‖f n‖ ≤ 1) :
    ‖(∑ n ∈ Finset.Icc 1 N, (primeLogWeight n : ℂ) * f n) -
      ∑ n ∈ Finset.Icc 1 N, (ArithmeticFunction.vonMangoldt n : ℂ) * f n‖ ≤
        Chebyshev.psi N - Chebyshev.theta N := by
…

Mentions: OAI.Problem337.primeLogWeight

theorem OAI.Problem337.norm_prime_sum_le_mangoldt_sum_add line 38

Source documentation

A pointwise prime-sum estimate follows from the corresponding Mangoldt estimate with the elementary prime-power error added.

theorem norm_prime_sum_le_mangoldt_sum_add (N : ℕ) (f : ℕ → ℂ)
    (hf : ∀ n ∈ Finset.Icc 1 N, ‖f n‖ ≤ 1) :
    ‖∑ n ∈ Finset.Icc 1 N, (primeLogWeight n : ℂ) * f n‖ ≤
      ‖∑ n ∈ Finset.Icc 1 N, (ArithmeticFunction.vonMangoldt n : ℂ) * f n‖ +
        (Chebyshev.psi N - Chebyshev.theta N) := by
…

Mentions: OAI.Problem337.primeLogWeight

theorem OAI.Problem337.prime_power_error_mul_log_isLittleO line 53
Source documentation
Every fixed logarithmic loss is negligible compared with the power saving in the elementary prime-power estimate.
```
theorem prime_power_error_mul_log_isLittleO (B : ℕ) :
    (fun x : ℝ => (Chebyshev.psi x - Chebyshev.theta x) * Real.log x ^ B)
      =o[atTop] (fun x : ℝ => x) := by
…
```
theorem OAI.Problem337.eventually_prime_power_error_le_log_budget line 69
Source documentation
A scalar form suited to logarithmic minor-arc budgets. The onset depends only on the desired saving and error, not on any Fourier frequency.
```
theorem eventually_prime_power_error_le_log_budget (B : ℕ) (ε : ℝ) (hε : 0 < ε) :
    ∀ᶠ N : ℕ in atTop,
      Chebyshev.psi N - Chebyshev.theta N ≤
        ε * ((N : ℝ) / Real.log (N : ℝ) ^ B) := by
…
```

theorem OAI.Problem337.eventually_norm_mangoldt_sum_sub_prime_sum_le_log_budget line 90

Source documentation

Uniform removal of proper prime powers at any fixed logarithmic saving. In particular the phase may be chosen after the summation length.

theorem eventually_norm_mangoldt_sum_sub_prime_sum_le_log_budget
    (B : ℕ) (ε : ℝ) (hε : 0 < ε) :
    ∀ᶠ N : ℕ in atTop, ∀ f : ℕ → ℂ,
      (∀ n ∈ Finset.Icc 1 N, ‖f n‖ ≤ 1) →
      ‖(∑ n ∈ Finset.Icc 1 N, (ArithmeticFunction.vonMangoldt n : ℂ) * f n) -
        ∑ n ∈ Finset.Icc 1 N, (primeLogWeight n : ℂ) * f n‖ ≤
          ε * ((N : ℝ) / Real.log (N : ℝ) ^ B) := by
…

Mentions: OAI.Problem337.primeLogWeight

theorem OAI.Problem337.ThreePrimeContinuousFourier.norm_mangoldt_fourier_sub_prime_fourier_le line 104

Source documentation

Specialization to the canonical continuous Fourier phase.

theorem norm_mangoldt_fourier_sub_prime_fourier_le (N : ℕ) (x : ℝ) :
    ‖(∑ n ∈ Finset.Icc 1 N,
        (ArithmeticFunction.vonMangoldt n : ℂ) * phase (n : ℤ) x) -
      ∑ n ∈ Finset.Icc 1 N, (primeLogWeight n : ℂ) * phase (n : ℤ) x‖ ≤
        Chebyshev.psi N - Chebyshev.theta N := by
…

Mentions: OAI.Problem337.ThreePrimeContinuousFourier.phase, OAI.Problem337.primeLogWeight