The intermediate-prefix bound in the original real short interval

def NairTenenbaum.PolynomialSystem.HasIntermediatePrefixReal {k r : ℕ} (P : PolynomialSystem k r) (T X w₀ x u : ℝ) (t : ℤ) : Prop

A bounded prefix above the mass threshold with primes in the intermediate range.

Equations

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

theorem NairTenenbaum.PolynomialSystem.hasIntermediatePrefixReal_iff {k r : ℕ} (P : PolynomialSystem k r) {T : ℝ} (hT : 1 ≤ T) (X w₀ x u : ℝ) (t : ℤ) : P.HasIntermediatePrefixReal T X w₀ x u t ↔ P.HasIntermediatePrefix ⌊T⌋₊.toPNat' X w₀ x u t