The exponent margin in Theorem 2

theorem NairTenenbaum.eventually_log_rpow_lt_gain {α η c : ℝ} (hα : α < 1 - η) (hc : 0 < c) : ∀ᶠ (x : ℝ) in Filter.atTop, Real.log x ^ α < c * Real.log x ^ (1 - η)

theorem NairTenenbaum.eventually_greatestPrimeFactor_gain {α η c : ℝ} (hα : α < 1 - η) (hc : 0 < c) : ∀ᶠ (x : ℝ) in Filter.atTop, ∀ (y P : ℝ), 0 < y → y * Real.exp (c * Real.log x ^ (1 - η)) ≤ P → y * Real.exp (Real.log x ^ α) < P

The final strict inequality follows from any fixed positive coefficient in the stronger logarithmic exponent.