Integrating the explicit moment power bound

The singular power is integrated with its full dependence on the exponent gap. For t≥1 and q≥2t, positivity of the gap is already proved.

theorem NairTenenbaum.intervalIntegrable_sub_one_rpow {a b r : ℝ} (ha : 1 < a) (hab : a ≤ b) : IntervalIntegrable (fun (s : ℝ) => (s - 1) ^ r) MeasureTheory.volume a b

theorem NairTenenbaum.integral_sub_one_rpow_le {a b e : ℝ} (ha : 1 < a) (hab : a ≤ b) (he : 0 < e) : ∫ (s : ℝ) in a..b, (s - 1) ^ (-1 - e) ≤ (a - 1) ^ (-e) / e

theorem NairTenenbaum.hooleyReducedMoment_le_endpoint_add_power {Q : Polynomial ℤ} (hQ : NoFixedPrimeDivisor Q) {t a b C : ℝ} (ht : 0 ≤ t) {q : ℕ} (hq : 2 < q) (htq : t ≤ ↑q) (ha : 1 < a) (hab : a ≤ b) (hgap : 0 < hooleyMomentExponentGap t q) (hbound : ∀ s ∈ Set.Icc a b, hooleyReducedMomentMajorant Q t q s ≤ hooleyPoleCoefficient Q t q C * (s - 1) ^ (-1 - hooleyMomentExponentGap t q)) : hooleyReducedMoment Q t q a ≤ hooleyReducedMoment Q t q b + hooleyPoleCoefficient Q t q C / hooleyMomentExponentGap t q * (a - 1) ^ (-hooleyMomentExponentGap t q)