Absorbing the linear mass error and retaining an exponential gain

theorem NairTenenbaum.exists_divisorHit_exponent_margin_lt_one {α : ℝ} (hα : α < 2 - Real.log 4) : ∃ (η : ℝ), Real.log 4 - 1 < η ∧ η < 1 ∧ α < 1 - η

theorem NairTenenbaum.eventually_divisorHit_log_gain {β c η B D : ℝ} (hβ : 0 < β) (hc : 0 < c) (hη : η < 1) (hD : 0 < D) : ∀ᶠ (x : ℝ) in Filter.atTop, ∀ (H N : ℝ), c * x ^ β / Real.log x ^ η ≤ H → 0 < N → N ≤ 2 * x ^ β → B * x ^ β ≤ H * Real.log (x ^ β) / 2 ∧ c * β / (4 * D) * Real.log x ^ (1 - η) ≤ H * Real.log (x ^ β) / (2 * (D * N))