Covering prefixes by logarithmic prime bands

theorem NairTenenbaum.primeSelect_mem_dyadic_band {r : ℕ} (n : Tuple r) (q : ℕ) {x u w₀ : ℝ} (hx : 1 < x) (hw₀ : 1 ≤ w₀) (hupper : ∀ (i : Fin r), ∀ p ∈ (↑(primeSelect n (Finset.range q) i)).primeFactors, ↑p ≤ x ^ u) (hlower : ∃ (i : Fin r), ∃ p ∈ (↑(primeSelect n (Finset.range q) i)).primeFactors, w₀ < ↑p) : ∃ (j : ℕ), w₀ < x ^ (2 * (u / 2 ^ (j + 1))) ∧ x ^ (u / 2 ^ (j + 1)) < ↑q ∧ ∀ (i : Fin r), ↑(primeSelect n (Finset.range q) i) ∈ Nat.factoredNumbers (Finset.Icc 0 ⌊x ^ (2 * (u / 2 ^ (j + 1)))⌋₊)

A prefix with a prime factor above w₀, all of whose primes are at most x^u, lies in an eligible dyadic band. Its existing next-prime cutoff is already large enough to sift at the lower edge of that band.

def NairTenenbaum.PolynomialSystem.HasIntermediatePrefix {k r : ℕ} (P : PolynomialSystem k r) (N : ℕ+) (X w₀ x u : ℝ) (t : ℤ) : Prop

The middle range of largest prefix primes. The two outside ranges will be handled by the bounded-smoothness and large-next-prime estimates respectively.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def NairTenenbaum.PolynomialSystem.intermediatePrefixContribution {k r : ℕ} (P : PolynomialSystem k r) (F : ArithmeticMap k) (N : ℕ+) (X w₀ x u : ℝ) (a b : ℤ) : ℝ

The weighted contribution of prefixes in the intermediate prime range.

Equations

• One or more equations did not get rendered due to their size.

theorem NairTenenbaum.PolynomialSystem.HasIntermediatePrefix.exists_band {k r : ℕ} {P : PolynomialSystem k r} {N : ℕ+} {X w₀ x u : ℝ} {t : ℤ} (h : P.HasIntermediatePrefix N X w₀ x u t) (hx : 1 < x) (hw₀ : 1 ≤ w₀) : ∃ (j : ℕ), w₀ < x ^ (2 * (u / 2 ^ (j + 1))) ∧ P.HasSmoothTailPrefix N (Finset.Icc 0 ⌊x ^ (2 * (u / 2 ^ (j + 1)))⌋₊) X (x ^ (u / 2 ^ (j + 1))) t

theorem NairTenenbaum.exists_finset_sum_le_cover {ι : Type u_1} {κ : Type u_2} [Nonempty κ] (T : Finset ι) (U : κ → Finset ι) (eligible : κ → Prop) (w : ι → ℝ) (hw : ∀ (i : ι), 0 ≤ w i) (hcover : ∀ i ∈ T, ∃ (j : κ), eligible j ∧ i ∈ U j) : ∃ (J : Finset κ), (∀ j ∈ J, eligible j) ∧ ∑ i ∈ T, w i ≤ ∑ j ∈ J, ∑ i ∈ U j, w i

A finite weighted set covered by eligible finite sets uses only finitely many of them. Overlap is harmless for nonnegative weights.

theorem NairTenenbaum.PolynomialSystem.intermediatePrefixContribution_le_bands {k r : ℕ} (P : PolynomialSystem k r) {F : ArithmeticMap k} (hF : ∀ (n : Tuple k), 0 ≤ F n) (N : ℕ+) (X w₀ x u : ℝ) (a b : ℤ) (hx : 1 < x) (hw₀ : 1 ≤ w₀) : ∃ (J : Finset ℕ), (∀ j ∈ J, w₀ < x ^ (2 * (u / 2 ^ (j + 1)))) ∧ P.intermediatePrefixContribution F N X w₀ x u a b ≤ ∑ j ∈ J, P.smoothTailPrefixContribution F N (Finset.Icc 0 ⌊x ^ (2 * (u / 2 ^ (j + 1)))⌋₊) X a b (x ^ (u / 2 ^ (j + 1)))

The finite interval needs only finitely many eligible bands. Overlap causes no loss because all arithmetic weights are nonnegative.