Recovering the original moment Dirichlet series

Undoing the exact integrating factor gives the exponent 2^t−t+t/q.

theorem NairTenenbaum.hooleyDirichlet_eq_reducedMoment (Q : Polynomial ℤ) (t σ : ℝ) {q : ℕ} (hq : 1 < q) : hooleyDirichlet Q t q σ = Real.exp (2 ^ (t / ↑q) * rootPrimePowerSum Q σ) * hooleyReducedMoment Q t q σ ^ (↑q - 1)

theorem NairTenenbaum.hooleyMomentExponentGap_identity (t : ℝ) {q : ℕ} (hq : 1 < q) : 2 ^ (t / ↑q) + hooleyMomentExponentGap t q * (↑q - 1) = 2 ^ t - t + t / ↑q

theorem NairTenenbaum.hooleyDirichlet_le_of_reducedMoment_bound (Q : Polynomial ℤ) {t σ C K : ℝ} {q : ℕ} (hq : 1 < q) (hσ : 1 < σ) (hK : 0 ≤ K) (hR : rootPrimePowerSum Q σ ≤ C - Real.log (σ - 1)) (hU : hooleyReducedMoment Q t q σ ≤ K * (σ - 1) ^ (-hooleyMomentExponentGap t q)) : hooleyDirichlet Q t q σ ≤ Real.exp (2 ^ (t / ↑q) * C) * K ^ (↑q - 1) * (σ - 1) ^ (-(2 ^ t - t + t / ↑q))