Logarithmic mass of the canonical rough parts

theorem NairTenenbaum.sum_log_roughPart {ι : Type u_1} (S : Finset ι) (n : ι → ℕ+) (z : ℝ) : ∑ i ∈ S, Real.log ↑↑(roughPart (n i) z) = ∑ i ∈ S, Real.log ↑↑(n i) - ∑ i ∈ S, Real.log ↑↑(smoothPart (n i) z)

theorem NairTenenbaum.roughPart_logMass_le_divisorHits {ι : Type u_1} (S : Finset ι) (n : ι → ℕ+) {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) : ∑ i ∈ S, Real.log ↑↑(roughPart (n i) (C * y)) ≤ ((↑k - 1) * ↑S.card - ↑{i ∈ S | 0 < dyadicDivisorCount (↑(n i)) y}.card) * Real.log ↑(∏ i ∈ S, ↑(n i)).maxPrimeFac

theorem NairTenenbaum.maxPrimeFac_prod_ge_exp_divisorHits {ι : Type u_1} (S : Finset ι) (hS : S.Nonempty) (n : ι → ℕ+) {k : ℕ} (hk : 2 ≤ k) {A C y E : ℝ} (hy : 1 ≤ y) (hC : 1 ≤ C) (hA : A < C ^ k) (hA' : 2 * A < C ^ (k - 1)) (hsize : ∀ i ∈ S, ↑↑(n i) ≤ A * y ^ k) (hlower : (↑k - 1) * ↑S.card * Real.log y - E ≤ ∑ i ∈ S, Real.log ↑↑(roughPart (n i) (C * y))) (herror : E ≤ ↑{i ∈ S | 0 < dyadicDivisorCount (↑(n i)) y}.card * Real.log y / 2) : y * Real.exp (↑{i ∈ S | 0 < dyadicDivisorCount (↑(n i)) y}.card * Real.log y / (2 * ((↑k - 1) * ↑S.card))) ≤ ↑(∏ i ∈ S, ↑(n i)).maxPrimeFac

A quantitative lower bound for the rough mass yields the required type of exponential gain. The lower bound and its error remain explicit inputs.