Exponential saving from high distinct-prime-factor beta support

The cutoff is real. The elementary Rankin weight is 2 ^ omega(n); its absorption only doubles the fixed divisor order, with no power of the ambient scale lost.

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.betaLowOmega (β : ℕ → ℝ) (ξ : ℝ) (n : ℕ) : ℝ

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.betaLowOmega β ξ n = if ↑n.primeFactors.card ≤ ξ then β n else 0

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.betaHighOmega (β : ℕ → ℝ) (ξ : ℝ) (n : ℕ) : ℝ

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.betaHighOmega β ξ n = if ξ < ↑n.primeFactors.card then β n else 0

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.beta_eq_lowOmega_add_highOmega (β : ℕ → ℝ) (ξ : ℝ) (n : ℕ) : β n = betaLowOmega β ξ n + betaHighOmega β ξ n

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.abs_betaLowOmega_le (β : ℕ → ℝ) (ξ : ℝ) (n : ℕ) : |betaLowOmega β ξ n| ≤ |β n|

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.abs_betaHighOmega_le (β : ℕ → ℝ) (ξ : ℝ) (n : ℕ) : |betaHighOmega β ξ n| ≤ |β n|

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.betaLowOmega_nonzero_card_le {β : ℕ → ℝ} {ξ : ℝ} {n : ℕ} (h : betaLowOmega β ξ n ≠ 0) : ↑n.primeFactors.card ≤ ξ

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.two_pow_card_primeFactors_le_tau {n : ℕ} (hn : n ≠ 0) : 2 ^ n.primeFactors.card ≤ (fouvryTau 2) n

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.highOmega_rankin_bound (k : ℕ) {n : ℕ} (hn : n ≠ 0) {ξ : ℝ} (hξ : ξ < ↑n.primeFactors.card) : ↑((fouvryTau k) n) ≤ 2 ^ (-ξ) * ↑((fouvryTau (2 * k)) n)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.abs_betaHighOmega_le_rankin (k : ℕ) {N : Finset ℕ} {β : ℕ → ℝ} (hβ : ∀ n ∈ N, |β n| ≤ ↑((fouvryTau k) n)) (ξ : ℝ) {n : ℕ} (hn : n ∈ N) : |betaHighOmega β ξ n| ≤ 2 ^ (-ξ) * ↑((fouvryTau (2 * k)) n)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.highOmega_sum_tau_le (k : ℕ) {x : ℝ} (hx : 1 ≤ x) (N : Finset ℕ) (hN : N ⊆ Finset.Ioc 0 ⌊x⌋₊) : ∑ n ∈ N, ↑((fouvryTau k) n) ≤ x * (1 + Real.log x) ^ k

A convenient all-orders global mean; increasing the order by one also treats order zero without exceptional cases.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.sum_abs_betaHighOmega_le (k : ℕ) {T : ℝ} (hT : 1 ≤ T) (N : Finset ℕ) (hN : N ⊆ Finset.Ioc 0 ⌊T⌋₊) (β : ℕ → ℝ) (hβ : ∀ n ∈ N, |β n| ≤ ↑((fouvryTau k) n)) (ξ : ℝ) : ∑ n ∈ N, |betaHighOmega β ξ n| ≤ 2 ^ (-ξ) * T * (1 + Real.log T) ^ (2 * k)