W1 lemma B: decomposing 3^{ω(q)} for squarefree q

For squarefree q with prime factors {p₁, ..., p_k},

3^{ω(q)} = 3^k = ∏_{p|q} (1+2) = Σ_{S⊆primeFactors q} 2^{|S|} = Σ_{d|q, Squarefree d} 2^{ω(d)}.

Each subset S corresponds to the squarefree divisor d = ∏_{p∈S} p. WeightedPan.lean already supplies the natural-number version threeOmega_eq_sum_twoOmega_divisors. This module gives the real-valued version with a squarefree filter needed for W1, separating the combinatorial identity 3^k = Σ_{S⊆[k]} 2^{|S|} from the subset-divisor bijection.

theorem AnalyticNumberTheory.Sieve.sum_powerset_two_pow_eq_three_pow {α : Type u_1} [DecidableEq α] (t : Finset α) : ∑ u ∈ t.powerset, 2 ^ u.card = 3 ^ t.card

Combinatorial identity: Σ_{u∈t.powerset} 2^{|u|} = 3^{|t|}. Expand (1+2)^{|t|} over subsets: each element is independently included with weight 2 or excluded with weight 1.

theorem AnalyticNumberTheory.Sieve.divisors_squarefree_filter_eq_self {q : ℕ} (hq : Squarefree q) : Finset.filter Squarefree q.divisors = q.divisors

Every divisor of squarefree q is squarefree, so divisors.filter Squarefree removes no terms.

theorem AnalyticNumberTheory.Sieve.sum_squarefree_divisors_eq_sum_powerset {q : ℕ} (hq : Squarefree q) : ∑ S ∈ q.primeFactors.powerset, 2 ^ S.card = ∑ d ∈ q.divisors with Squarefree d, 2 ^ d.primeFactors.card

Subset-divisor bijection: for squarefree q, Σ_{S⊆primeFactors q} 2^{|S|} = Σ_{d|q, Squarefree d} 2^{ω(d)}. The bijection is S ↦ ∏_{p∈S} p, with inverse d ↦ d.primeFactors.

theorem AnalyticNumberTheory.Sieve.three_pow_omega_eq_sum_two_pow {q : ℕ} (hq : Squarefree q) : 3 ^ q.primeFactors.card = ∑ d ∈ q.divisors with Squarefree d, 2 ^ d.primeFactors.card

W1 lemma B: for squarefree q, 3^{ω(q)} = Σ_{d|q, Squarefree d} 2^{ω(d)}. Each prime factor contributes 3 = 1+2, according to whether it is excluded from or included in d; every squarefree divisor corresponds to exactly one subset of the prime-factor set.