Greatest prime factors and divisor hits

This is the finite counting step of Theorem 2. The arithmetic estimate for how much logarithmic mass survives in the rough cofactors is separate.

theorem NairTenenbaum.prime_le_maxPrimeFac_prod {ι : Type u_1} (S : Finset ι) (n : ι → ℕ) (hn : ∀ i ∈ S, n i ≠ 0) {p : ℕ} {j : ι} (hj : j ∈ S) (hp : Nat.Prime p) (hd : p ∣ n j) : p ≤ (∏ j ∈ S, n j).maxPrimeFac

theorem NairTenenbaum.rough_logMass_le_maxPrimeFac_prod {ι : Type u_1} (S H : Finset ι) (hH : H ⊆ S) (n b : ι → ℕ) (hn : ∀ i ∈ S, n i ≠ 0) (hb : ∀ i ∈ S, b i ≠ 0) (hd : ∀ i ∈ S, b i ∣ n i) {k : ℕ} (hk : 2 ≤ k) (hΩ : ∀ i ∈ S, bigOmega (b i) ≤ k - 1) (hΩH : ∀ i ∈ H, bigOmega (b i) ≤ k - 2) : ∑ i ∈ S, Real.log ↑(b i) ≤ ((↑k - 1) * ↑S.card - ↑H.card) * Real.log ↑(∏ i ∈ S, n i).maxPrimeFac

theorem NairTenenbaum.rough_logMass_le_divisorHits {ι : Type u_1} (S : Finset ι) (n a b : ι → ℕ) (ha : ∀ i ∈ S, a i ≠ 0) (hb : ∀ i ∈ S, b i ≠ 0) (hsplit : ∀ i ∈ S, a i * b i = n i) {k : ℕ} (hk : 2 ≤ k) {A C y : ℝ} (hy : 1 ≤ y) (hC : 1 ≤ C) (hA : A < C ^ k) (hA' : 2 * A < C ^ (k - 1)) (hsize : ∀ i ∈ S, ↑(n i) ≤ A * y ^ k) (hrough : ∀ i ∈ S, ∀ p ∈ (b i).primeFactors, C * y < ↑p) : ∑ i ∈ S, Real.log ↑(b i) ≤ ((↑k - 1) * ↑S.card - ↑{i ∈ S | 0 < dyadicDivisorCount (n i) y}.card) * Real.log ↑(∏ i ∈ S, n i).maxPrimeFac