W1 weight estimate

This module assembles Σ_{q≤Q} μ²(q)·3^{ω(q)}·φ(q)/q ≤ C·Q·(log(Q+2))² from the following estimates:

Σ_{q≤Q} μ²·3^ω·φ/q
  ≤ Σ_{q≤Q} μ²·3^ω                              (lemma A: φ/q ≤ 1)
  = Σ_{q≤Q, squarefree} 3^ω(q)                   (μ² is the squarefree indicator)
  = Σ_{q≤Q, squarefree} Σ_{d|q, squarefree} 2^ω(d) (lemma B)
  ≤ Σ_{d≤Q, squarefree} 2^ω(d)·(Q/d)             (exchange sums and count multiples)
  = Q·Σ_{d≤Q, squarefree} 2^ω(d)/d
  = Q·Σ_{d≤Q} μ²(d)·2^ω(d)/d
  = Q·sumTwoPowWeighted Q
  ≤ C·Q·(log(Q+2))²                              (lemma C).

The count of positive multiples is at most ⌊Q/d⌋ ≤ Q/d. The shift in log(Q+2) is essential, as in lemma C and panMainTotientWeightedSum_le_polylog: using log Q would give right side 0 but left side 1 at Q = 1.

1. Lemma A: φ(q)/q ≤ 1

theorem AnalyticNumberTheory.Sieve.totient_div_self_le_one (q : ℕ) : ↑q.totient / ↑q ≤ 1

Lemma A: (φ(q):ℝ)/q ≤ 1 for every natural q, by Nat.totient_le. At q = 0, totalized division gives a left side of 0, so the inequality is trivial.

2. The weighted expression panTypeIWeight3 and lemma A

noncomputable def AnalyticNumberTheory.Sieve.panTypeIWeight3 (Q : ℕ) : ℝ

W1 weighted expression: panTypeIWeight3 Q = Σ_{q≤Q} μ²(q)·3^{ω(q)}·φ(q)/q. The q = 0 term has zero weight.

Equations

• AnalyticNumberTheory.Sieve.panTypeIWeight3 Q = ∑ q ∈ Finset.range (Q + 1), ↑(ArithmeticFunction.moebius q) ^ 2 * 3 ^ q.primeFactors.card * ↑q.totient / ↑q

theorem AnalyticNumberTheory.Sieve.panTypeIWeight3_le_sqfree_three_pow (Q : ℕ) : panTypeIWeight3 Q ≤ ∑ q ∈ Finset.range (Q + 1) with Squarefree q, 3 ^ q.primeFactors.card

panTypeIWeight3 Q ≤ Σ_{q≤Q, squarefree} 3^{ω(q)}: apply lemma A termwise, then use the squarefree indicator μ².

3. Exchanging sums and counting multiples

theorem AnalyticNumberTheory.Sieve.panTypeIWeight3_le_Q_mul_sumTwoPowWeighted (Q : ℕ) : panTypeIWeight3 Q ≤ ↑Q * sumTwoPowWeighted Q

W1 assembly: panTypeIWeight3 Q ≤ Q·sumTwoPowWeighted Q for every Q, by lemma A, the termwise expansion in lemma B, exchange of sums, counting multiples, and restoration of μ².

4. W1 theorem

theorem AnalyticNumberTheory.Sieve.panTypeIWeight3_le_polylog : ∃ (C : ℝ), 0 < C ∧ ∀ (Q : ℕ), panTypeIWeight3 Q ≤ C * ↑Q * Real.log (↑Q + 2) ^ 2

W1 theorem: Σ_{q≤Q} μ²(q)·3^{ω(q)}·φ(q)/q ≤ C·Q·(log(Q+2))² for all Q : ℕ. Apply lemma A (φ/q ≤ 1), restrict to squarefree integers, expand by lemma B, exchange sums and count positive multiples by Q/d, restore μ², and apply lemma C (sumTwoPowWeighted_le_polylog). The shift Q+2 matches lemma C; replacing it by Q would make the bound false at Q = 1.