Decay after paying the arithmetic and Euler-product costs

theorem NairTenenbaum.primeBand_decay_of_margin {A c κ τ α x v : ℝ} {g : ℕ} (hA : 0 < A) (hα : 0 < α) (hx : 1 < x) (hκ : c * Real.log A + 4 * ↑g * Real.log 4 + v ≤ κ * τ / 2) : A ^ (c / α) * Real.exp (4 * ↑g * Real.log 4 / α) * Real.exp (-κ * Real.log (x ^ τ) / Real.log (x ^ (2 * α))) ≤ Real.exp (-v / α)

A margin v in the smooth-tail moment leaves decay exp(-v / α) after paying for the rough remainder and restoring the Euler product.

theorem NairTenenbaum.primeBand_decay {A c κ τ α x : ℝ} {g : ℕ} (hA : 0 < A) (hα : 0 < α) (hx : 1 < x) (hκ : c * Real.log A + 4 * ↑g * Real.log 4 + 1 ≤ κ * τ / 2) : A ^ (c / α) * Real.exp (4 * ↑g * Real.log 4 / α) * Real.exp (-κ * Real.log (x ^ τ) / Real.log (x ^ (2 * α))) ≤ Real.exp (-1 / α)

For a band with upper cutoff x^(2α), the smooth-tail moment can pay both the rough remainder and the restoration of the Euler product.

theorem NairTenenbaum.dyadic_primeBand_decay {a : ℝ} (ha : 0 < a) (ha₁ : a ≤ 1) (j : ℕ) : Real.exp (-1 / (a / 2 ^ (j + 1))) ≤ Real.exp (-1) ^ j

The dyadic logarithmic bands have a summable decay, uniformly in their number. This deliberately uses the weaker geometric decay exp(-j).

theorem NairTenenbaum.sum_dyadic_primeBand_decay_le {a : ℝ} (ha : 0 < a) (ha₁ : a ≤ 1) (J : Finset ℕ) : ∑ j ∈ J, Real.exp (-1 / (a / 2 ^ (j + 1))) ≤ (1 - Real.exp (-1))⁻¹

Any finite collection of dyadic bands has a uniformly bounded total cost.

theorem NairTenenbaum.dyadic_primeBand_exponent_le {a : ℝ} (ha : 0 ≤ a) (j : ℕ) : 2 * (a / 2 ^ (j + 1)) ≤ a

The doubled lower exponent of a dyadic band never exceeds its initial upper exponent.

theorem NairTenenbaum.exists_dyadic_exponent_band {a b : ℝ} (hb : 0 < b) (hba : b ≤ a) : ∃ (j : ℕ), a / 2 ^ (j + 1) < b ∧ b ≤ 2 * (a / 2 ^ (j + 1))

Dyadic logarithmic intervals cover every positive exponent below the initial cutoff, with a strict lower endpoint and a closed upper endpoint.

theorem NairTenenbaum.exists_dyadic_primeBand {a x p : ℝ} (hx : 1 < x) (hp : 1 < p) (hpa : p ≤ x ^ a) : ∃ (j : ℕ), x ^ (a / 2 ^ (j + 1)) < p ∧ p ≤ x ^ (2 * (a / 2 ^ (j + 1)))

Every prime cutoff between 1 and x^a belongs to a logarithmic band. This is a statement for all real cutoffs, so it also covers ties at powers.

theorem NairTenenbaum.sum_le_dyadic_primeBand_bound {u C : ℝ} (hu : 0 < u) (hu₁ : u ≤ 1) (J : Finset ℕ) (hC : 0 ≤ C) (f : ℕ → ℝ) (hf : ∀ j ∈ J, f j ≤ C * Real.exp (-1 / (u / 2 ^ (j + 1)))) : ∑ j ∈ J, f j ≤ C * (1 - Real.exp (-1))⁻¹

Sum any nonnegative multiple of the common dyadic band decay.