Divisor estimates in the middle-game range

Choose eventual thresholds where divisor counts satisfy the real-power bounds required by the middle-game argument.

theorem BGS.Markoff.eventually_const_mul_rpow_lt_rpow {C a b : ℝ} (hab : a < b) : ∀ᶠ (n : ℕ) in Filter.atTop, C * ↑n ^ a < ↑n ^ b

theorem BGS.Markoff.exists_threshold_middleGameDivisorCount_le_two_mul_rpow {ε : ℝ} (hε : 0 < ε) : ∃ (threshold : ℕ), ∀ (p : ℕ), threshold ≤ p → ↑((p - 1).divisors.card + (p + 1).divisors.card) ≤ 2 * ↑(p + 1) ^ ε

theorem BGS.Markoff.eventually_corvajaZannierDivisorCount_le_rpow {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (p : ℕ) in Filter.atTop, ↑corvajaZannierCorollaryTwoSafeCoefficient * (↑(p - 1).divisors.card + ↑(p + 1).divisors.card) ≤ ↑(2 * corvajaZannierCorollaryTwoSafeCoefficient) * 2 ^ ε * ↑p ^ ε

theorem BGS.Markoff.eventually_middleGame_corvajaZannier_sizeBounds {δ : ℝ} (hδ : 0 < δ) : ∀ᶠ (p : ℕ) in Filter.atTop, ∀ (currentOrder : ℕ), ↑p ^ δ < ↑currentOrder → ↑currentOrder < ↑p ^ (1 - δ) → (corvajaZannierCorollaryTwoSafeCoefficient * ((p - 1).divisors.card + (p + 1).divisors.card)) ^ 3 < currentOrder ∧ corvajaZannierCorollaryTwoSafeCoefficient * ((p - 1).divisors.card + (p + 1).divisors.card) * currentOrder < p

Throughout the genuine middle range, the two finite inequalities needed by the Corvaja--Zannier escape theorem eventually hold uniformly in the current order.