A fixed exponential in the number of distinct prime factors is subpower. The proof splits the prime divisors at a fixed cutoff; above the cutoff, each logarithmic cost is absorbed by the prime itself.

theorem CCDN.two_pow_primeFactors_subpower (a : ℕ) {ε : ℝ} (hε : 0 < ε) : ∃ (C : ℝ), 0 < C ∧ ∀ (D : ℕ), 1 ≤ D → 2 ^ (a * D.primeFactors.card) ≤ C * ↑D ^ ε

For every a and ε > 0 there is C > 0 with 2 ^ (a * ω(D)) ≤ C * D ^ ε for all D ≥ 1, where ω(D) is the number of distinct prime factors of D.