Subpolynomial bounds for products over distinct prime factors

theorem NairTenenbaum.exists_primeFactorPower_le_rpow {K η : ℝ} (hK : 1 ≤ K) (hη : 0 < η) : ∃ (C : ℝ), 1 ≤ C ∧ ∀ (n : ℕ), n ≠ 0 → K ^ n.primeFactors.card ≤ C * ↑n ^ η

A fixed exponential in the number of distinct prime factors is smaller than every positive power of the integer, up to a uniform constant.

theorem NairTenenbaum.primeFactorPower_lcm_le {K : ℝ} (hK : 1 ≤ K) {a b : ℕ} (ha : a ≠ 0) (hb : b ≠ 0) : K ^ (a.lcm b).primeFactors.card ≤ K ^ a.primeFactors.card * K ^ b.primeFactors.card