The first-contribution bound in the real short interval

def NairTenenbaum.PolynomialSystem.HasSmallRoughPrefixReal {k r : ℕ} (P : PolynomialSystem k r) (T z : ℝ) (t : ℤ) : Prop

A whole-prime-power prefix with bounded real mass and a large next-prime cutoff.

Equations

• One or more equations did not get rendered due to their size.

theorem NairTenenbaum.PolynomialSystem.hasSmallRoughPrefixReal_iff {k r : ℕ} (P : PolynomialSystem k r) {T : ℝ} (hT : 1 ≤ T) (z : ℝ) (t : ℤ) : P.HasSmallRoughPrefixReal T z t ↔ P.HasSmallRoughPrefix ⌊T⌋₊.toPNat' z t