PrimePowerPhaseError.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.norm_mangoldt_sub_prime_phase_sum_le line 12

Source documentation

Removing higher prime powers from any bounded complex phase costs at most exactly the elementary Chebyshev error. No distribution of primes is assumed.

theorem norm_mangoldt_sub_prime_phase_sum_le (N : ℕ) (w : ℕ → ℂ)
    (hw : ∀ n ∈ Finset.Icc 1 N, ‖w n‖ ≤ 1) :
    ‖(∑ n ∈ Finset.Icc 1 N, (ArithmeticFunction.vonMangoldt n : ℂ) * w n) -
      ∑ n ∈ (Finset.Icc 1 N).filter Nat.Prime, (Real.log (n : ℝ) : ℂ) * w n‖ ≤
      Chebyshev.psi N - Chebyshev.theta N := by
…

theorem OAI.Problem337.primePowerError_mul_log_isLittleO line 30
Source documentation
The prime-power discrepancy remains negligible after multiplying by any fixed real power of the logarithm.
```
theorem primePowerError_mul_log_isLittleO (D : ℝ) :
    (fun x : ℝ => (Chebyshev.psi x - Chebyshev.theta x) * Real.log x ^ D)
      =o[atTop] (fun x : ℝ => x) := by
…
```
Mentions: OAI.Problem337.D

theorem OAI.Problem337.eventually_norm_mangoldt_sub_prime_phase_sum_le line 44

Source documentation

Uniform prime-power deletion with an arbitrary logarithmic saving. The onset is independent of the complex phases.

theorem eventually_norm_mangoldt_sub_prime_phase_sum_le
    (D ε : ℝ) (hε : 0 < ε) :
    ∀ᶠ N : ℕ in atTop, ∀ w : ℕ → ℂ,
      (∀ n ∈ Finset.Icc 1 N, ‖w n‖ ≤ 1) →
      ‖(∑ n ∈ Finset.Icc 1 N, (ArithmeticFunction.vonMangoldt n : ℂ) * w n) -
        ∑ n ∈ (Finset.Icc 1 N).filter Nat.Prime, (Real.log (n : ℝ) : ℂ) * w n‖ ≤
        ε * (N : ℝ) / Real.log (N : ℝ) ^ D := by
…

Mentions: OAI.Problem337.D

theorem OAI.Problem337.norm_prime_phase_sum_le_mangoldt_add_error line 67

Source documentation

Any upper bound for the Mangoldt phase sum transfers to the prime-only logarithmically weighted sum with the explicit prime-power error.

theorem norm_prime_phase_sum_le_mangoldt_add_error (N : ℕ) (w : ℕ → ℂ)
    (hw : ∀ n ∈ Finset.Icc 1 N, ‖w n‖ ≤ 1) :
    ‖∑ n ∈ (Finset.Icc 1 N).filter Nat.Prime, (Real.log (n : ℝ) : ℂ) * w n‖ ≤
      ‖∑ n ∈ Finset.Icc 1 N, (ArithmeticFunction.vonMangoldt n : ℂ) * w n‖ +
        (Chebyshev.psi N - Chebyshev.theta N) := by
…

theorem OAI.Problem337.prime_phase_log_bound_of_mangoldt line 82

Source documentation

Uniform transfer of logarithmic minor-arc estimates. The set of allowed phases may vary arbitrarily with the summation length.

theorem prime_phase_log_bound_of_mangoldt {ι : Type*}
    (w : ℕ → ι → ℕ → ℂ) (minor : ℕ → Set ι) (D ε : ℝ) (hε : 0 < ε)
    (hw : ∀ N t, t ∈ minor N → ∀ n ∈ Finset.Icc 1 N, ‖w N t n‖ ≤ 1)
    (hbound : ∀ᶠ N : ℕ in atTop, ∀ t ∈ minor N,
      ‖∑ n ∈ Finset.Icc 1 N, (ArithmeticFunction.vonMangoldt n : ℂ) * w N t n‖ ≤
        (ε / 2) * (N : ℝ) / Real.log (N : ℝ) ^ D) :
    ∀ᶠ N : ℕ in atTop, ∀ t ∈ minor N,
      ‖∑ n ∈ (Finset.Icc 1 N).filter Nat.Prime,
        (Real.log (n : ℝ) : ℂ) * w N t n‖ ≤
        ε * (N : ℝ) / Real.log (N : ℝ) ^ D := by
…

Mentions: OAI.Problem337.D