An integrated bound for the transformed Hooley moment series #
The derivative majorant is integrable on every compact interval to the right of one. The resulting bound is unconditional and keeps the prime-series estimates separate from the analytic differential argument.
noncomputable def
NairTenenbaum.hooleyReducedMomentMajorant
(Q : Polynomial ℤ)
(t : ℝ)
(q : ℕ)
(s : ℝ)
:
A majorant for the reduced Hooley moment used in differential integration.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
NairTenenbaum.intervalIntegrable_hooleyReducedMomentMajorant
{Q : Polynomial ℤ}
(hQ : NoFixedPrimeDivisor Q)
{t a b : ℝ}
{q : ℕ}
(hq : 0 < q)
(htq : t ≤ ↑q)
(ha : 1 < a)
(hab : a ≤ b)
:
theorem
NairTenenbaum.hooleyReducedMoment_le_endpoint_add_integral
{Q : Polynomial ℤ}
(hQ : NoFixedPrimeDivisor Q)
{t a b : ℝ}
(ht : 0 ≤ t)
{q : ℕ}
(hq : 2 < q)
(htq : t ≤ ↑q)
(ha : 1 < a)
(hab : a ≤ b)
:
hooleyReducedMoment Q t q a ≤ hooleyReducedMoment Q t q b + ∫ (s : ℝ) in a..b, hooleyReducedMomentMajorant Q t q s