Removing the divisors of a changing nonzero residue from beta

The deleted mass is bounded by one divisor sum, including at order zero. The subpolynomial constant precedes the residue, scale, support and sequence.

def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.betaClean (β : ℕ → ℝ) (a : ℤ) (n : ℕ) : ℝ

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.betaClean β a n = if ↑n ∣ a then 0 else β n

def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.betaDivisorPart (β : ℕ → ℝ) (a : ℤ) (n : ℕ) : ℝ

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.betaDivisorPart β a n = if ↑n ∣ a then β n else 0

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.beta_eq_clean_add_divisorPart (β : ℕ → ℝ) (a : ℤ) (n : ℕ) : β n = betaClean β a n + betaDivisorPart β a n

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.abs_betaClean_le (β : ℕ → ℝ) (a : ℤ) (n : ℕ) : |betaClean β a n| ≤ |β n|

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.abs_betaDivisorPart_le (β : ℕ → ℝ) (a : ℤ) (n : ℕ) : |betaDivisorPart β a n| ≤ |β n|

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.betaClean_nonzero_not_dvd {β : ℕ → ℝ} {a : ℤ} {n : ℕ} (hn : betaClean β a n ≠ 0) : ¬↑n ∣ a

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.support_betaClean_subset (β : ℕ → ℝ) (a : ℤ) : Function.support (betaClean β a) ⊆ Function.support β

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.support_betaDivisorPart_subset (β : ℕ → ℝ) (a : ℤ) : Function.support (betaDivisorPart β a) ⊆ Function.support β

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.betaClean_abs_le_fouvryTau {k : ℕ} {N : Finset ℕ} {β : ℕ → ℝ} (hβ : ∀ n ∈ N, |β n| ≤ ↑((fouvryTau k) n)) (a : ℤ) (n : ℕ) : n ∈ N → |betaClean β a n| ≤ ↑((fouvryTau k) n)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.fouvryTau_le_succ (k n : ℕ) : (fouvryTau k) n ≤ (fouvryTau (k + 1)) n

The summand indexed by n proves monotonicity even when the lower order is zero; at n = 0 both sides vanish.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.sum_abs_betaDivisorPart_le (k : ℕ) (N : Finset ℕ) (β : ℕ → ℝ) {a : ℤ} (ha : a ≠ 0) (hβ : ∀ n ∈ N, |β n| ≤ ↑((fouvryTau k) n)) : ∑ n ∈ N, |betaDivisorPart β a n| ≤ ↑((fouvryTau (k + 1)) a.natAbs)

No positivity or interval-support assumption on N is required: zero is not a divisor of a nonzero residue.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.sum_abs_betaDivisorPart_uniform_rpow (k : ℕ) {δ : ℝ} (hδ : 0 < δ) : ∃ (C : ℝ), 0 < C ∧ ∀ (x : ℝ), 1 ≤ x → ∀ (a : ℤ), a ≠ 0 → ↑a.natAbs ≤ x → ∀ (N : Finset ℕ) (β : ℕ → ℝ), (∀ n ∈ N, |β n| ≤ ↑((fouvryTau k) n)) → ∑ n ∈ N, |betaDivisorPart β a n| ≤ C * x ^ δ

A single constant works for all changing sequences and residues of size at most x. In particular the beta order may be zero.