Absorbing a fixed factor in Hooley's function

The upper multiplication bound holds without a coprimality hypothesis; divisor products can overlap, so the corresponding window formula is an inequality.

theorem NairTenenbaum.divisorWindow_mul_le (m n : ℕ) (u : ℝ) : divisorWindow (m * n) u ≤ ∑ a ∈ m.divisors, divisorWindow n (u - Real.log ↑a)

theorem NairTenenbaum.hooleyDelta_mul_le_without_coprime (m n : ℕ) : hooleyDelta (m * n) ≤ m.divisors.card * hooleyDelta n