An upper bound for the unassigned terms.
Only an upper bound is needed here. We enclose the unassigned
arguments in a set of smooth numbers and count that larger set. There is
no claim that every smooth argument is unassigned.
Proposition 12.6 (A one-sided bound for the
unassigned terms). Fix ℎ,𝑠 and
choose the admissible depth 𝐿
minimally for each large 𝑋. Put
𝑡 =𝐿 −𝑠 +1 =𝑂ℎ,𝑠(log𝑋) and 𝑦𝑋 =4√𝑋 +2𝑡/√𝑋. If 𝑛 =𝑁 +𝑡 is unassigned, then its largest
prime factor satisfies 𝑃(𝑛) ≤𝑦𝑋.
Consequently
#{𝑁∈[𝑋,2𝑋):𝑁∉A}≤Ψ(2𝑋+𝑡−1,𝑦𝑋)−Ψ(𝑋+𝑡−1,𝑦𝑋)=(1−log2+𝑜(1))𝑋<825𝑋
for all sufficiently large 𝑋. Here Ψ(𝑥,𝑦) counts the positive integers at
most 𝑥 whose prime factors are all
at most 𝑦. This is an upper bound
for the unassigned count, not an asymptotic equality for that
count.
Proof. Let 𝑝 =𝑃(𝑛) and
𝑚 =𝑛/𝑝. Since 𝑛 >1, failure of the assignment
condition means either 𝑝 ≤2⌊√𝑋⌋ or 𝑚 >⌊√𝑋/2⌋. In the second case 𝑚 >√𝑋/2, so
𝑝=𝑛𝑚<2(2𝑋+𝑡)√𝑋=𝑦𝑋.
The first case also gives 𝑝 ≤𝑦𝑋. Counting the resulting smooth
integers in [𝑋 +𝑡,2𝑋 +𝑡) proves the
first inequality.
For completeness, the classical fixed-parameter asymptotic Ψ(𝑥,𝑥1/𝑢) ∼𝑥𝜌(𝑢) suffices; no
additional short-interval estimate is needed. Indeed, for either 𝑥 =𝑋 +𝑡 −1 or 𝑥 =2𝑋 +𝑡 −1, log𝑦𝑋/log𝑥 →1/2. For every fixed
0 <𝜖 <1, eventually
𝑥1/(2+𝜖)≤𝑦𝑋≤𝑥1/(2−𝜖).
Monotonicity in 𝑦 bounds Ψ(𝑥,𝑦𝑋)/𝑥 between quantities tending
to 𝜌(2 +𝜖) and 𝜌(2 −𝜖). Letting 𝜖 →0 and using continuity gives
the limit 𝜌(2). Subtracting the
two endpoint asymptotics yields (𝜌(2) +𝑜(1))𝑋. Since 𝜌(2) =1 −log2 <8/25, the claimed
bound follows. ◻
The Lean proof uses no smooth-number asymptotic. For large 𝑋, 𝑦2𝑋 >2𝑋 +𝑡 −1, so an integer in (𝑋 +𝑡 −1,2𝑋 +𝑡 −1] that is not 𝑦𝑋-smooth has exactly one prime factor
above 𝑦𝑋, and
Ψ(2𝑋+𝑡−1,𝑦𝑋)−Ψ(𝑋+𝑡−1,𝑦𝑋)=𝑋−∑𝑦𝑋<𝑝≤2𝑋+𝑡−1(⌊2𝑋+𝑡−1𝑝⌋−⌊𝑋+𝑡−1𝑝⌋).
Mertens’ theorems, proved in Lean with explicit constants, then give
(1 −log2)𝑋 +𝑂(𝑋/log𝑋). The written
proof above cites instead the fixed-𝑢 asymptotic [20] and the value 𝜌(𝑢) =1 −log𝑢 on [1,2] [20]. No effective crossover scale or
exact density for the unassigned indices is asserted. The estimate uses
the minimal admissible depth; it does not supply either weighted phase
bound at that depth.
Proposition 12.7 (The excluded-cofactor estimate).
Fix ℎ,𝑠 and use the minimal
admissible depth 𝐿, as in
Proposition 12.6;
thus 𝑡 =𝐿 −𝑠 +1 =𝑂ℎ,𝑠(log𝑋). For
𝜂 ∈(0,1) let 𝐵(𝜂) ={𝑚 ≥1 :𝜑(𝑚) <𝜂𝑚},
with natural density 𝐷(𝜂); by
Schoenberg’s theorem 𝐷 exists, is
continuous, and 𝐷(0 +) =0 [21], in the framework
of [22]. Then
#{𝑁∈A:𝑚𝑁∈𝐵(𝜂)}≤(𝐷(𝜂)+𝑜(1))𝑋,
so a single choice of
𝜂 with 𝐷(𝜂) <1/200 meets the 1100𝑋 bound for all large 𝑋. This choice fixes 𝜂 before 𝑋0, as required. It supplies only the
excluded-cofactor bound: the mean and mean-subtracted estimates must
still hold for this same 𝜂, and
do not follow from making 𝜂
smaller.
Proof. For a fixed cofactor 𝑚 ≤√𝑋/2, each assigned index gives
a prime 𝑝 with 𝑋 +𝑡 ≤𝑚𝑝 <2𝑋 +𝑡. Dropping the other
assignment restrictions bounds the number of indices by the number of
primes in this interval. The prime number theorem, uniformly for 𝑋/𝑚 ≥2√𝑋, and 𝑡 =𝑂ℎ,𝑠(log𝑋) give the upper bound
(2+𝑜(1))𝑋𝑚log𝑋.
The
possible endpoint contribution is 𝑂(1) for each 𝑚, hence 𝑜(𝑋) after summing over 𝑚 ≤√𝑋/2. Natural density and
partial summation give
∑𝑚≤√𝑋/2𝑚∈𝐵(𝜂)1𝑚=(𝐷(𝜂)2+𝑜(1))log𝑋.
Multiplying
the two estimates proves the stated bound. If 𝐷(𝜂) <1/200, its right side is less
than 𝑋/100 for all sufficiently
large 𝑋. ◻
The existence of a usable cutoff can also be made explicit by an
elementary estimate. For 𝑥 ≥1,
1𝑥∑𝑛≤𝑥𝑛𝜑(𝑛)≤∑𝑑≥1𝜇(𝑑)2𝑑𝜑(𝑑)=∏𝑝(1+1𝑝(𝑝−1))≤exp(∑𝑛≥21𝑛(𝑛−1))=exp(1)<3.
The first step uses 𝑛/𝜑(𝑛) =∑𝑑∣𝑛𝜇(𝑑)2/𝜑(𝑑) and ⌊𝑥/𝑑⌋ ≤𝑥/𝑑; the Euler product has nonnegative terms and
converges by the displayed majorant. Markov’s inequality gives #(𝐵(𝜂) ∩[1,𝑥]) <3𝜂𝑥, hence
𝐷(𝜂) ≤3𝜂. In particular,
𝜂 =1/1000 gives 𝐷(𝜂) ≤3/1000 <1/200, an explicit
sufficient choice for the excluded-cofactor bound. This does not
establish either weighted phase estimate for that choice, and it is not
claimed to be an optimal cutoff. Lean checks the estimate #(𝐵(𝜂) ∩[1,𝑥]) <3𝜂𝑥 with no
further input (Lean
proof) and the excluded-cofactor bound at 𝜂 =1/1000 with no input at all (Lean
proof). For that bound Chebyshev’s bound replaces the prime number
theorem in the proof above: the primes 𝑝 with 𝑎 +1 <𝑝 ≤2𝑎 +1 divide (2𝑎+1𝑎) ≤4𝑎, so #{𝑝 prime :𝑎 <𝑝 ≤2𝑎 +1}log𝑎 ≤𝑎log4 +log𝑎, the fibre bound becomes (2log4 +𝑜(1))𝑋/(𝑚log𝑋), and the count
is at most (3log4/1000 +𝑜(1))𝑋 with
3log4/1000 <0.0042. The proof
uses 𝜂 =1/1000 only through 3𝜂log4 <1/100, so Lean checks the
bound with no input for every 𝜂
with 0 <𝜂 <1/(300log4) (Lean
proof).
The first element of 𝐵(1/5) is
30030 =2 ⋅3 ⋅5 ⋅7 ⋅11 ⋅13,
and 𝜑(30030)/30030 =5760/30030 ≈0.191808.
Enumeration through 3 ⋅105
gives 38 elements of 𝐵(1/5) and
1log(3⋅105)∑𝑚≤3⋅105𝑚∈𝐵(1/5)1𝑚≈2.82⋅10−5.
This finite weighted proportion is not
the limiting density 𝐷(1/5). Using
𝜂 =1/5 in the asymptotic bound
would require a rigorous bound for 𝐷(1/5), including the integers beyond the
enumeration; the finite count does not supply one.