Growth of arithmetic weights on rough remaining factors

theorem NairTenenbaum.rough_pow_bigOmega_le {n : ℕ} (hn : n ≠ 0) {z : ℝ} (hz : 0 ≤ z) (hrough : ∀ p ∈ n.primeFactors, z ≤ ↑p) : z ^ bigOmega n ≤ ↑n

A rough integer has at most log n / log z prime factors, counted with multiplicity. The power form also covers n=1.

theorem NairTenenbaum.rough_bigOmega_le {n : ℕ} (hn : n ≠ 0) {z : ℝ} (hz : 1 < z) (hrough : ∀ p ∈ n.primeFactors, z ≤ ↑p) : ↑(bigOmega n) ≤ Real.log ↑n / Real.log z

theorem NairTenenbaum.rough_bigOmega_le_of_power {n : ℕ} (hn : n ≠ 0) {x α c : ℝ} (hx : 1 < x) (hα : 0 < α) (hnx : ↑n ≤ x ^ c) (hrough : ∀ p ∈ n.primeFactors, x ^ α ≤ ↑p) : ↑(bigOmega n) ≤ c / α

With a power cutoff and a power bound on the integer, the number of remaining prime factors is uniformly bounded.

theorem NairTenenbaum.prime_dvd_weightedMass_iff {k r : ℕ} (γ : Fin k → Fin r → ℕ) (hγ : ∀ (i : Fin r), 0 < totalExponent γ i) (n : Tuple r) {p : ℕ} (hp : Nat.Prime p) : p ∣ weightedMass γ n ↔ p ∣ mass n

theorem NairTenenbaum.primeReject_weightedMass_rough {k r : ℕ} (γ : Fin k → Fin r → ℕ) (hγ : ∀ (i : Fin r), 0 < totalExponent γ i) (n : Tuple r) (q p : ℕ) : p ∈ (weightedMass γ (primeReject n (Finset.range q))).primeFactors → q ≤ p

Selecting all primes below q leaves a rough weighted mass.

theorem NairTenenbaum.Admissible.pullback_primeSplit_le_of_rough {k r : ℕ} {A B σ : ℝ} {F : ArithmeticMap k} (hF : Admissible A B σ F) (hA : 1 ≤ A) (hB : 0 ≤ B) (γ : Fin k → Fin r → ℕ) (hγ : ∀ (i : Fin r), 0 < totalExponent γ i) (n : Tuple r) (q : ℕ) {x α c : ℝ} (hx : 1 < x) (hα : 0 < α) (hq : x ^ α ≤ ↑q) (hnx : ↑(weightedMass γ n) ≤ x ^ c) : pullback γ F n ≤ A ^ (c / α) * pullback γ F (primeSelect n (Finset.range q))

Equation (29) with the remaining rough factor bounded by a constant.