Reciprocal two-power weight estimate #
The W1 lemma C estimate is
Σ_{d≤Q} μ²(d)·2^{ω(d)}/d ≤ C·(log(Q+2))².
Its proof parallels panMainTotientWeightedSum_le_polylog
(W3, PanMainTerm.lean §4).
For squarefree d, d = ∏_{p|d} p and
2^{ω(d)} = ∏_{p|d} 2, so
μ²(d)·2^{ω(d)}/d = ∏_{p|d} 2/p.
Apply the subset bound
Σ_{q≤Q, squarefree} ∏_{p|q} c p ≤ ∏_{p≤Q} (1+c p)
with c p = 2/p, then Real.prod_one_add_le_exp_sum.
Since Σ_{p≤Q} 2/p = 2·Σ_{p≤Q} 1/p, Mertens' second theorem
(mertensSecond_nat) gives
Σ_{p≤Q} 1/p ≤ log log Q + O(1).
Thus
rexp(2·(log log Q + K)) = e^{2K}·(log Q)² ≤ C·(log(Q+2))².
The finite range Q ≤ 2, where the sum is at most 2, is absorbed
into the constant.
Two-power weight sum Σ_{d≤Q} μ²(d)·2^{ω(d)}/d,
the left side of W1 lemma C.
Equations
- AnalyticNumberTheory.Sieve.sumTwoPowWeighted Q = ∑ d ∈ Finset.range (Q + 1), ↑(ArithmeticFunction.moebius d) ^ 2 * 2 ^ d.primeFactors.card / ↑d
Instances For
For squarefree d, μ²(d)=1, 2^{ω(d)}=∏_{p|d}2,
and d=∏_{p|d}p, so the summand equals ∏_{p|d}2/p.
The weight vanishes for nonsquarefree d, since μ(d)=0.
The two-power weight sum is at most ∏_{p≤Q} (1+2/p),
by subset expansion with c p = 2/p.
The two-power weight sum is monotone in Q, by nonnegative weights.
W1 lemma C:
Σ_{d≤Q} μ²(d)·2^{ω(d)}/d ≤ C·(log(Q+2))².
Use subset expansion, ∏(1+u) ≤ exp(Σu),
Σ_{p≤Q}2/p = 2·Σ_{p≤Q}1/p, and Mertens' second theorem.
Absorb the initial range Q ≤ 2 into the constant.