Skip to content

Instantly share code, notes, and snippets.

@FaffyWaffles

FaffyWaffles/RobinsStirlingBound.lean

Created October 30, 2025 14:11
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save FaffyWaffles/e1703b6146d8b743a257ec364a86bde4 to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save FaffyWaffles/e1703b6146d8b743a257ec364a86bde4 to your computer and use it in GitHub Desktop.
Download ZIP
This file proves the sharp Robbins bound for successive differences in the logarithm of the Stirling sequence: |log(stirlingSeq(k+1)) - log(stirlingSeq(k))| ≤ 1/(12*k*(k+1))
Raw
RobinsStirlingBound.lean
import Mathlib
open scoped BigOperators
open Filter
open scoped Nat
namespace Real
/-
============================================================
Robbins' Sharp Stepwise Bound for Stirling Sequence
============================================================
This file proves the sharp Robbins bound for successive differences in the
logarithm of the Stirling sequence:
|log(stirlingSeq(k+1)) - log(stirlingSeq(k))| ≤ 1/(12*k*(k+1))
This improves upon Mathlib's bound of 1/(4*k^2) and represents work that
Mathlib documentation notes as "not yet formalised."
https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/SpecialFunctions/Stirling.html
Reference: Stirling.log_stirlingSeq_sub_log_stirlingSeq_succ provides the
weaker bound 1/(4*k^2).
This file was written by Ashton Jenson, edited by Aristotle, and refactored by Claude
-/
/-
============================================================
A. Basic inequalities and positivity
============================================================
-/
/-- A1. Basic coefficient bound: 1/(2j+3) ≤ 1/3 for all j ≥ 0 -/
lemma coeff_le_third (j : ℕ) :
(1 : ℝ) / (2 * (j + 1) + 1) ≤ 1 / 3 := by
-- Since $j$ is a natural number, $j + 1 \geq 1$, thus $2 * (j + 1) + 1 \geq 3$.
have h_denom : 2 * (j + 1) + 1 ≥ 3 := by
linarith [ Nat.zero_le j ];
gcongr ; norm_cast
/-- A2. For k ≥ 1, we have 2k+1 > 1 -/
lemma two_k_plus_one_pos {k : ℕ} (hk : 1 ≤ k) :
1 < 2 * (k : ℝ) + 1 := by
norm_cast ; linarith
/-- A3. For k ≥ 1, we have 2k+1 ≠ 0 -/
lemma two_k_plus_one_ne_zero {k : ℕ} (hk : 1 ≤ k) :
2 * (k : ℝ) + 1 ≠ 0 := by
positivity
/-- A4. For k ≥ 1, we have (2k+1)^2 ≠ 0 -/
lemma two_k_plus_one_sq_ne_zero {k : ℕ} (hk : 1 ≤ k) :
(2 * (k : ℝ) + 1) ^ 2 ≠ 0 := by
positivity
/-- A5. For k ≥ 1, we have 0 < (1/(2k+1))^2 -/
lemma ratio_sq_pos {k : ℕ} (hk : 1 ≤ k) :
0 < ((1 : ℝ) / (2 * k + 1)) ^ 2 := by
positivity
/-- A6. For k ≥ 1, we have (1/(2k+1))^2 < 1 -/
lemma ratio_sq_lt_one {k : ℕ} (hk : 1 ≤ k) :
((1 : ℝ) / (2 * k + 1)) ^ 2 < 1 := by
have h_pos : 0 < 2 * (k : ℝ) + 1 := by positivity
rw [div_pow, one_pow, div_lt_one (pow_pos h_pos 2)]
have : (3 : ℝ) ≤ 2 * (k : ℝ) + 1 := by
have : 3 ≤ 2 * k + 1 := by omega
norm_cast
nlinarith [sq_nonneg (2 * (k : ℝ) + 1 - 3)]
/-
============================================================
B. Geometric series lemmas
============================================================
-/
/-- B1. Geometric series: ∑_{j=0}^∞ r^(j+1) = r/(1-r) for 0 < r < 1 -/
lemma tsum_geom_shift {r : ℝ} (hr_pos : 0 < r) (hr_lt_one : r < 1) :
(∑' j : ℕ, r ^ (j + 1)) = r / (1 - r) := by
-- Apply the geometric series sum formula to the series starting from j=0.
have h_geo_series : ∑' j : ℕ, r ^ j = 1 / (1 - r) := by
rw [ tsum_geometric_of_lt_one hr_pos.le hr_lt_one, one_div ];
-- Factor out $r$ from the series starting at $j=1$.
have h_factor : ∑' j : ℕ, r ^ (j + 1) = r * ∑' j : ℕ, r ^ j := by
rw [ ← tsum_mul_left ] ; exact tsum_congr fun _ => by ring;
rw [ h_factor, h_geo_series, mul_one_div ]
/-- B2. Factor constant: ∑ c*r^(j+1) = c * ∑ r^(j+1) -/
lemma tsum_const_mul {r : ℝ} (c : ℝ) :
(∑' j : ℕ, c * r ^ (j + 1)) = c * (∑' j : ℕ, r ^ (j + 1)) := by
rw [ ← tsum_mul_left ]
/-- B3. Geometric series with constant: ∑ c*r^(j+1) = c*r/(1-r) for 0 < r < 1 -/
lemma tsum_geom_const_mul {r : ℝ} (c : ℝ) (hr_pos : 0 < r) (hr_lt_one : r < 1) :
(∑' j : ℕ, c * r ^ (j + 1)) = c * (r / (1 - r)) := by
-- Factor out the constant $c$ and the common ratio $r$ from the series.
have h_factor : ∑' j : ℕ, c * r ^ (j + 1) = c * r * ∑' j : ℕ, r ^ j := by
rw [ ← tsum_mul_left ] ; exact tsum_congr fun j => by ring;
rw [ h_factor, tsum_geometric_of_lt_one hr_pos.le hr_lt_one, mul_assoc, div_eq_mul_inv ]
/-
============================================================
C. Summability results
============================================================
-/
/-- C1. Geometric series r^(j+1) is summable for 0 < r < 1 -/
lemma summable_geom_shift {r : ℝ} (hr_pos : 0 < r) (hr_lt_one : r < 1) :
Summable (fun j : ℕ => r ^ (j + 1)) := by
-- The series $\sum_{j=0}^{\infty} r^{j+1}$ is a geometric series with common ratio $r$ and first term $r$, which converges since $|r| < 1$.
have h_geo_series : Summable (fun j : ℕ => r ^ j) := by
exact summable_geometric_of_lt_one hr_pos.le hr_lt_one;
convert h_geo_series.mul_left r using 2 ; ring
/-- C2. Constant times geometric series is summable -/
lemma summable_const_mul_geom {r : ℝ} (c : ℝ) (hr_pos : 0 < r) (hr_lt_one : r < 1) :
Summable (fun j : ℕ => c * r ^ (j + 1)) := by
-- Since the geometric series ∑' j : ℕ, r ^ (j + 1) is summable, multiplying it by a constant c preserves summability.
have h_geo_series : Summable (fun j : ℕ => r ^ (j + 1)) := by
exact summable_geom_shift hr_pos hr_lt_one;
exact h_geo_series.mul_left c
/-- C3. The Stirling series ∑ [1/(2j+3)] * r^(j+1) is summable for r < 1 -/
lemma stirling_series_summable {k : ℕ} (hk : 1 ≤ k) :
Summable (fun j : ℕ =>
(1 : ℝ) / (2 * (j + 1) + 1) * ((1 / (2 * k + 1)) ^ 2) ^ (j + 1)) := by
-- Let $r = \frac{1}{(2k+1)^2}$. We need to show that $\sum_{j=0}^{\infty} \frac{1}{2j+3} r^{j+1}$ converges.
set r : ℝ := (1 / (2 * k + 1)) ^ 2
have h_summable : Summable (fun j : ℕ => r ^ (j + 1) / (2 * j + 3)) := by
exact Summable.of_nonneg_of_le ( fun j => div_nonneg ( pow_nonneg ( by positivity ) _ ) ( by positivity ) ) ( fun j => div_le_self ( by positivity ) ( by linarith ) ) <| Summable.comp_injective ( summable_geometric_of_lt_one ( by positivity ) <| show ( 1 / ( 2 * k + 1 : ℝ ) ) ^ 2 < 1 by exact pow_lt_one₀ ( by positivity ) ( by rw [ div_lt_iff₀ <| by positivity ] ; norm_cast ; linarith ) ( by positivity ) ) <| by intros a b; aesop;
convert h_summable using 2 ; ring
/-
============================================================
D. Termwise bounds
============================================================
-/
/-- D1. Each term in the series is bounded by the geometric comparison -/
lemma series_term_bound {k : ℕ} (hk : 1 ≤ k) (j : ℕ) :
(1 : ℝ) / (2 * (j + 1) + 1) * ((1 / (2 * k + 1)) ^ 2) ^ (j + 1)
≤ (1 / 3) * ((1 / (2 * k + 1)) ^ 2) ^ (j + 1) := by
apply mul_le_mul_of_nonneg_right
· exact coeff_le_third j
· positivity
/-- D2. Bound is multiplicative: if a ≤ b and 0 ≤ c, then a*c ≤ b*c -/
lemma mul_bound_helper {a b c : ℝ} (hab : a ≤ b) (hc : 0 ≤ c) :
a * c ≤ b * c := by
exact mul_le_mul_of_nonneg_right hab hc
/-
============================================================
E. Series comparison
============================================================
-/
/-- E0a. The geometric comparison series is summable -/
lemma geom_comparison_summable {k : ℕ} (hk : 1 ≤ k) :
Summable (fun j : ℕ => (1 / 3 : ℝ) * ((1 / (2 * k + 1)) ^ 2) ^ (j + 1)) := by
exact summable_const_mul_geom (1 / 3) (ratio_sq_pos hk) (ratio_sq_lt_one hk)
/-- E0b. Term-by-term inequality holds for all j -/
lemma term_by_term_bound {k : ℕ} (hk : 1 ≤ k) :
∀ j : ℕ, (1 : ℝ) / (2 * (j + 1) + 1) * ((1 / (2 * k + 1)) ^ 2) ^ (j + 1)
≤ (1 / 3 : ℝ) * ((1 / (2 * k + 1)) ^ 2) ^ (j + 1) := by
intro j
exact series_term_bound hk j
/-- E0c. Both terms are nonnegative -/
lemma stirling_term_nonneg {k : ℕ} (hk : 1 ≤ k) (j : ℕ) :
0 ≤ (1 : ℝ) / (2 * (j + 1) + 1) * ((1 / (2 * k + 1)) ^ 2) ^ (j + 1) := by
positivity
/-- E0d. Comparison term is nonnegative -/
lemma geom_term_nonneg {k : ℕ} (hk : 1 ≤ k) (j : ℕ) :
0 ≤ (1 / 3 : ℝ) * ((1 / (2 * k + 1)) ^ 2) ^ (j + 1) := by
positivity
/-- E1. The Stirling series is bounded by the geometric series -/
lemma stirling_series_le_geom {k : ℕ} (hk : 1 ≤ k) :
(∑' j : ℕ, (1 : ℝ) / (2 * (j + 1) + 1) * ((1 / (2 * k + 1)) ^ 2) ^ (j + 1))
≤ (∑' j : ℕ, (1 / 3 : ℝ) * ((1 / (2 * k + 1)) ^ 2) ^ (j + 1)) := by
apply Summable.tsum_le_tsum (term_by_term_bound hk) (stirling_series_summable hk) (geom_comparison_summable hk)
/-
============================================================
F. Algebraic identity
============================================================
-/
/-- F0a. Expand (2k+1)² -/
lemma two_k_plus_one_sq {k : ℕ} :
(2 * (k : ℝ) + 1) ^ 2 = 4 * k^2 + 4 * k + 1 := by
ring
/-- F0b. Factor 4k² + 4k = 4k(k+1) -/
lemma four_k_sq_plus_four_k {k : ℕ} :
4 * (k : ℝ)^2 + 4 * k = 4 * k * (k + 1) := by
ring
/-- F0c. (2k+1)² - 1 = 4k(k+1) -/
lemma two_k_plus_one_sq_sub_one {k : ℕ} :
(2 * (k : ℝ) + 1) ^ 2 - 1 = 4 * k * (k + 1) := by
rw [two_k_plus_one_sq, four_k_sq_plus_four_k]
ring
/-- F1a. For k ≥ 1, we have 4k(k+1) > 0 -/
lemma four_k_times_k_plus_one_pos {k : ℕ} (hk : 1 ≤ k) :
0 < 4 * (k : ℝ) * (k + 1) := by
positivity
/-- F1b. For k ≥ 1, we have 4k(k+1) ≠ 0 -/
lemma four_k_times_k_plus_one_ne_zero {k : ℕ} (hk : 1 ≤ k) :
4 * (k : ℝ) * (k + 1) ≠ 0 := by
positivity
/-- F2. Compute 1 - r where r = 1/(2k+1)² -/
lemma one_sub_ratio_sq {k : ℕ} (hk : 1 ≤ k) :
1 - ((1 : ℝ) / (2 * k + 1)) ^ 2
= (4 * k * (k + 1)) / ((2 * k + 1) ^ 2) := by
have h1 : (2 * (k : ℝ) + 1) ^ 2 ≠ 0 := two_k_plus_one_sq_ne_zero hk
field_simp
ring
/-- F3. For k ≥ 1, we have 1 - r > 0 where r = 1/(2k+1)² -/
lemma one_sub_ratio_sq_pos {k : ℕ} (hk : 1 ≤ k) :
0 < 1 - ((1 : ℝ) / (2 * k + 1)) ^ 2 := by
rw [one_sub_ratio_sq hk]
positivity
/-- F4. For k ≥ 1, we have 1 - r ≠ 0 where r = 1/(2k+1)² -/
lemma one_sub_ratio_sq_ne_zero {k : ℕ} (hk : 1 ≤ k) :
1 - ((1 : ℝ) / (2 * k + 1)) ^ 2 ≠ 0 := by
linarith [one_sub_ratio_sq_pos hk]
/-- F5. Compute r / (1 - r) where r = 1/(2k+1)² -/
lemma ratio_sq_div_one_sub {k : ℕ} (hk : 1 ≤ k) :
((1 : ℝ) / (2 * k + 1)) ^ 2 / (1 - ((1 / (2 * k + 1)) ^ 2))
= 1 / (4 * k * (k + 1)) := by
rw [one_sub_ratio_sq hk]
have h1 : (2 * (k : ℝ) + 1) ^ 2 ≠ 0 := two_k_plus_one_sq_ne_zero hk
have h2 : 4 * (k : ℝ) * (k + 1) ≠ 0 := four_k_times_k_plus_one_ne_zero hk
field_simp
/-- F6. For k ≥ 1, we have 12k(k+1) ≠ 0 -/
lemma twelve_k_times_k_plus_one_ne_zero {k : ℕ} (hk : 1 ≤ k) :
12 * (k : ℝ) * (k + 1) ≠ 0 := by
positivity
/-- F7. (1/3) × [1/(4k(k+1))] = 1/(12k(k+1)) -/
lemma one_third_times_quarter {k : ℕ} (hk : 1 ≤ k) :
(1 / 3 : ℝ) * (1 / (4 * k * (k + 1))) = 1 / (12 * k * (k + 1)) := by
have h : 4 * (k : ℝ) * (k + 1) ≠ 0 := four_k_times_k_plus_one_ne_zero hk
have h' : 12 * (k : ℝ) * (k + 1) ≠ 0 := twelve_k_times_k_plus_one_ne_zero hk
field_simp
ring
/-- F1. Algebraic identity: (1/3) × [r/(1-r)] = 1/(12k(k+1)) where r = 1/(2k+1)² -/
lemma robbins_algebraic_identity {k : ℕ} (hk : 1 ≤ k) :
(1 / 3 : ℝ) * (((1 / (2 * k + 1)) ^ 2) / (1 - (1 / (2 * k + 1)) ^ 2))
= 1 / (12 * k * (k + 1)) := by
rw [ratio_sq_div_one_sub hk, one_third_times_quarter hk]
/-
============================================================
G. Monotonicity of log ∘ stirlingSeq (ATOMIZED)
============================================================
-/
/-- G0a. stirlingSeq(n+1) is always positive -/
lemma stirlingSeq_pos (n : ℕ) :
0 < Stirling.stirlingSeq (n + 1) := by
exact Stirling.stirlingSeq'_pos n
/-- G0b. stirlingSeq is positive for n ≥ 1 -/
lemma stirlingSeq_pos_succ (n : ℕ) :
0 < Stirling.stirlingSeq (n + 1) := by
exact stirlingSeq_pos n -- stirlingSeq_pos n gives 0 < stirlingSeq (n + 1)
/-- G0c. The ratio stirlingSeq(n+1)/stirlingSeq(n) -/
noncomputable def stirlingSeq_ratio (n : ℕ) : ℝ :=
Stirling.stirlingSeq (n + 1) / Stirling.stirlingSeq n
/-- G0d. For n ≥ 1, the ratio is well-defined (denominator nonzero) -/
lemma stirlingSeq_ratio_welldef {n : ℕ} (hn : 1 ≤ n) :
Stirling.stirlingSeq n ≠ 0 := by
-- Since n ≥ 1, we have n = (n - 1) + 1
have : n = (n - 1) + 1 := by omega
rw [this]
linarith [stirlingSeq_pos (n - 1)]
/-- G0e. stirlingSeq(n+1) ≤ stirlingSeq(n) for n ≥ 1 -/
lemma stirlingSeq_antitone {n : ℕ} (hn : 1 ≤ n) :
Stirling.stirlingSeq (n + 1) ≤ Stirling.stirlingSeq n := by
have h := Stirling.stirlingSeq'_antitone
-- stirlingSeq'_antitone says: Antitone (stirlingSeq ∘ succ)
-- which means for m ≤ n, stirlingSeq(m+1) ≥ stirlingSeq(n+1)
-- We need: stirlingSeq(n+1) ≤ stirlingSeq(n)
-- Set m = n-1, then m+1 = n, and we need m+1 ≤ n which is n ≤ n (true)
cases n with
| zero => omega
| succ n =>
-- Need stirlingSeq(n+2) ≤ stirlingSeq(n+1)
-- Antitone means: m ≤ n → f(m+1) ≥ f(n+1)
-- So n ≤ n+1 → stirlingSeq(n+1) ≥ stirlingSeq(n+2)
have : Stirling.stirlingSeq (n + 1 + 1) ≤ Stirling.stirlingSeq (n + 1) :=
h (Nat.le_succ n)
exact this
/-- G0f. The ratio stirlingSeq(n+1)/stirlingSeq(n) ≤ 1 -/
lemma stirlingSeq_ratio_le_one {n : ℕ} (hn : 1 ≤ n) :
stirlingSeq_ratio n ≤ 1 := by
unfold stirlingSeq_ratio
have pos_n : 0 < Stirling.stirlingSeq n := by
have : n = (n - 1) + 1 := by omega
rw [this]
exact stirlingSeq_pos (n - 1)
rw [div_le_one pos_n]
exact stirlingSeq_antitone hn
/-- G0g. log is monotone on positive reals -/
lemma log_mono_on_pos {x y : ℝ} (hx : 0 < x) (hy : 0 < y) (hxy : x ≤ y) :
Real.log x ≤ Real.log y := by
exact Real.log_le_log hx hxy
/-- G0h. For 0 < x ≤ y, we have log(x) ≤ log(y) -/
lemma log_antitone_of_antitone {n : ℕ} (hn : 1 ≤ n)
(h_anti : Stirling.stirlingSeq (n + 1) ≤ Stirling.stirlingSeq n) :
Real.log (Stirling.stirlingSeq (n + 1)) ≤ Real.log (Stirling.stirlingSeq n) := by
apply log_mono_on_pos
· exact stirlingSeq_pos n -- gives 0 < stirlingSeq (n + 1)
· -- Need 0 < stirlingSeq n, and n ≥ 1
have : n = (n - 1) + 1 := by omega
rw [this]
exact stirlingSeq_pos (n - 1)
· exact h_anti
/-- G1. The sequence log(stirlingSeq(n)) is decreasing -/
lemma log_stirlingSeq_antitone :
Antitone ((Real.log ∘ Stirling.stirlingSeq ∘ Nat.succ) : ℕ → ℝ) := by
intro m n hmn
-- Need to show log(stirlingSeq(m+1)) ≥ log(stirlingSeq(n+1)) when m ≤ n
-- stirlingSeq ∘ succ is antitone, so stirlingSeq(m+1) ≥ stirlingSeq(n+1)
have h_seq : Stirling.stirlingSeq (n + 1) ≤ Stirling.stirlingSeq (m + 1) :=
Stirling.stirlingSeq'_antitone hmn
-- log is monotone, so log(stirlingSeq(n+1)) ≤ log(stirlingSeq(m+1))
apply log_mono_on_pos
· exact stirlingSeq_pos n
· exact stirlingSeq_pos m
· exact h_seq
/-- G2. For k ≥ 1, we have log(stirlingSeq(k+1)) ≤ log(stirlingSeq(k)) -/
lemma log_stirlingSeq_succ_le {k : ℕ} (hk : 1 ≤ k) :
Real.log (Stirling.stirlingSeq (k + 1)) ≤ Real.log (Stirling.stirlingSeq k) := by
apply log_antitone_of_antitone hk
exact stirlingSeq_antitone hk
/-- G3. The difference log(stirlingSeq(k+1)) - log(stirlingSeq(k)) ≤ 0 -/
lemma log_stirlingSeq_diff_nonpos {k : ℕ} (hk : 1 ≤ k) :
Real.log (Stirling.stirlingSeq (k + 1)) - Real.log (Stirling.stirlingSeq k) ≤ 0 := by
linarith [log_stirlingSeq_succ_le hk]
/-
============================================================
H. Series expansion connection
============================================================
-/
/-- H0a. Mathlib has a series expansion for log stirlingSeq differences -/
lemma mathlib_stirling_series_exists {m : ℕ} :
HasSum (fun k : ℕ => (1 : ℝ) / (2 * ↑(k + 1) + 1) * ((1 / (2 * ↑(m + 1) + 1)) ^ 2) ^ (k + 1))
(Real.log (Stirling.stirlingSeq (m + 1)) - Real.log (Stirling.stirlingSeq (m + 2))) := by
exact Stirling.log_stirlingSeq_diff_hasSum m
/-- H0b. Index shift: j in new series corresponds to j+1 in old -/
lemma series_reindex_shift (r : ℝ) :
(fun j : ℕ => (1 : ℝ) / (2 * (j + 1) + 1) * (r ^ 2) ^ (j + 1))
= (fun i : ℕ => (1 / (2 * i + 1)) * (r ^ 2) ^ i) ∘ Nat.succ := by
ext j
simp [Function.comp]
/-- H0c. Index shift: coefficients match up correctly -/
lemma series_coeff_eq (j : ℕ) :
(1 : ℝ) / (2 * (j + 1) + 1) = 1 / (2 * j + 3) := by
norm_num
ring
/-- H0d. For k ≥ 1, there exists m such that k = m + 1 -/
lemma exists_pred_of_ge_one {k : ℕ} (hk : 1 ≤ k) :
∃ m : ℕ, k = m + 1 := by
use k - 1
omega
/-- H0e. If k = m + 1, then 2k + 1 = 2m + 3 -/
lemma two_k_plus_one_eq {k m : ℕ} (h : k = m + 1) :
2 * k + 1 = 2 * m + 3 := by
omega
/-- H0f. If k = m + 1, then k + 1 = m + 2 -/
lemma k_plus_one_eq {k m : ℕ} (h : k = m + 1) :
k + 1 = m + 2 := by
omega
/-- H0i. HasSum is unique -/
lemma hasSum_unique {α : Type*} [AddCommMonoid α] [TopologicalSpace α] [T2Space α]
{f : ℕ → α} {a b : α} (ha : HasSum f a) (hb : HasSum f b) :
a = b := by
exact HasSum.unique ha hb
/-- H1. Reindex: m+1 = k and m+2 = k+1 -/
lemma reindex_helper {k : ℕ} (hk : 1 ≤ k) :
∃ m : ℕ, m + 1 = k ∧ m + 2 = k + 1 := by
use k - 1
omega
/-- H2. The series expansion from Mathlib applies to our indices -/
lemma stirling_series_expansion {k : ℕ} (hk : 1 ≤ k) :
HasSum (fun j : ℕ => (1 : ℝ) / (2 * (j + 1) + 1) *
((1 / (2 * k + 1)) ^ 2) ^ (j + 1))
(Real.log (Stirling.stirlingSeq k) - Real.log (Stirling.stirlingSeq (k + 1))) := by
obtain ⟨m, hm⟩ := exists_pred_of_ge_one hk
subst hm
convert mathlib_stirling_series_exists using 1
ext j
simp only [Nat.cast_add, Nat.cast_one]
/-
============================================================
R. Main Result (Robbins' Sharp Bound)
============================================================
-/
/-- R1. Robbins' sharp stepwise bound for the Stirling sequence -/
theorem log_stirlingSeq_step_bound {k : ℕ} (hk : 1 ≤ k) :
|Real.log (Stirling.stirlingSeq (k+1)) - Real.log (Stirling.stirlingSeq k)|
≤ (1 : ℝ) / (12 * k * (k+1)) := by
-- The difference is non-positive by G3, so |a - b| = -(a - b) = b - a
rw [abs_of_nonpos (log_stirlingSeq_diff_nonpos hk)]
-- Get the series expansion from H2
have h_series := stirling_series_expansion hk
-- Convert the negation
have h_neg : -(Real.log (Stirling.stirlingSeq (k + 1)) - Real.log (Stirling.stirlingSeq k))
= Real.log (Stirling.stirlingSeq k) - Real.log (Stirling.stirlingSeq (k + 1)) := by ring
rw [h_neg]
-- The series sum equals the logarithm difference
rw [← h_series.tsum_eq]
-- Apply the series bound from E1
calc (∑' j : ℕ, (1 : ℝ) / (2 * (j + 1) + 1) * ((1 / (2 * k + 1)) ^ 2) ^ (j + 1))
≤ (∑' j : ℕ, (1 / 3 : ℝ) * ((1 / (2 * k + 1)) ^ 2) ^ (j + 1)) :=
stirling_series_le_geom hk
_ = (1 / 3) * (((1 / (2 * k + 1)) ^ 2) / (1 - (1 / (2 * k + 1)) ^ 2)) :=
tsum_geom_const_mul (1 / 3) (ratio_sq_pos hk) (ratio_sq_lt_one hk)
_ = (1 : ℝ) / (12 * k * (k + 1)) :=
robbins_algebraic_identity hk
end Real
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment