The small-crossing-prime contribution in the original interval

def NairTenenbaum.PolynomialSystem.HasSmallCrossingPrime {k r : ℕ} (P : PolynomialSystem k r) (ε x : ℝ) (t : ℤ) : Prop

A small prime causes the prefix mass to cross the larger threshold.

Equations

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

theorem NairTenenbaum.primePower_scale_identity (g : ℕ) (ε : ℝ) {x : ℝ} (hx : 0 ≤ x) : ((x ^ (↑g * ε / 2)) ^ 3) ^ g = x ^ (3 * ↑g ^ 2 * ε / 2)

theorem NairTenenbaum.secondContribution_sieve_level {g : ℕ} (hg : 0 < g) {ε x y : ℝ} (hε : 0 < ε) (hx : 1 ≤ x) (hz : 2 ≤ x ^ (↑g * ε / 2)) (hy : x ^ (4 * ↑g ^ 2 * ε) ≤ y) : (x ^ (↑g * ε / 2)) ^ 4 ≤ y / 2

At the paper's scales the modulus of every selected prime power fits in the rounded interval once the prime cutoff reaches two.