Splitting at the first prime beyond a mass threshold

This constructs the ordered prime-power decomposition underlying (28). All powers of a prime are retained together, so the existing cross-coprime splitting lemmas apply. The case where the whole mass is already small is kept explicitly rather than assuming that a crossing prime exists.

theorem NairTenenbaum.primePart_eq_one_of_not_mem {r : ℕ} (n : Tuple r) {p : ℕ} (hp : p ∉ (mass n).primeFactors) : primePart n p = 1

theorem NairTenenbaum.primeSelect_range_succ {r : ℕ} (n : Tuple r) (q : ℕ) : primeSelect n (Finset.range (q + 1)) = primeSelect n (Finset.range q) * primePart n q

Increasing the prime cutoff by one adds precisely that whole prime part.

theorem NairTenenbaum.primeSelect_range_zero {r : ℕ} (n : Tuple r) : primeSelect n (Finset.range 0) = 1

theorem NairTenenbaum.primeSelect_range_full {r : ℕ} (n : Tuple r) : primeSelect n (Finset.range (mass n + 1)) = n

theorem NairTenenbaum.primeSelect_range_prime_lt {r : ℕ} (n : Tuple r) (q : ℕ) (i : Fin r) {p : ℕ} (hp : p ∈ (↑(primeSelect n (Finset.range q) i)).primeFactors) : p < q

The prime powers in the selected part are strictly below the cutoff.

theorem NairTenenbaum.primeReject_range_prime_ge {r : ℕ} (n : Tuple r) (q : ℕ) (i : Fin r) {p : ℕ} (hp : p ∈ (↑(primeReject n (Finset.range q) i)).primeFactors) : q ≤ p

The complementary part contains no smaller prime.

theorem NairTenenbaum.prime_mem_reject_range {r : ℕ} (n : Tuple r) {q : ℕ} (hq : q ∈ (mass n).primeFactors) : q ∈ (mass (primeReject n (Finset.range q))).primeFactors

A supported cutoff prime survives in the complementary mass.

theorem NairTenenbaum.exists_prime_threshold {k r : ℕ} (γ : Fin k → Fin r → ℕ) (n : Tuple r) {T : ℝ} (hT : 1 ≤ T) (hn : T < ↑(weightedMass γ n)) : ∃ (q : ℕ), Nat.Prime q ∧ q ∈ (mass n).primeFactors ∧ ↑(weightedMass γ (primeSelect n (Finset.range q))) ≤ T ∧ T < ↑(weightedMass γ (primeSelect n (Finset.range q))) * ↑q ^ ∑ i : Fin r, totalExponent γ i * (↑(n i)).factorization q ∧ q ∈ (mass (primeReject n (Finset.range q))).primeFactors ∧ (∀ (i : Fin r), ∀ p ∈ (↑(primeSelect n (Finset.range q) i)).primeFactors, p < q) ∧ ∀ (i : Fin r), ∀ p ∈ (↑(primeReject n (Finset.range q) i)).primeFactors, q ≤ p

Equation (28) for arbitrary positive tuples and a real mass threshold. The selected prime is the least prime dividing the complementary mass.

theorem NairTenenbaum.small_mass_or_prime_threshold {k r : ℕ} (γ : Fin k → Fin r → ℕ) (n : Tuple r) {T : ℝ} (hT : 1 ≤ T) : ↑(weightedMass γ n) ≤ T ∨ ∃ (q : ℕ), Nat.Prime q ∧ ↑(weightedMass γ (primeSelect n (Finset.range q))) ≤ T ∧ T < ↑(weightedMass γ (primeSelect n (Finset.range (q + 1))))

An exhaustive threshold dichotomy, including the small-total-mass case.