n : ℕ
h_nonneg : 0 ≤ (1 / (2 * ↑(succ n) + 1)) ^ 2
⊢ Real.log (stirlingSeq (succ n)) - Real.log (stirlingSeq (succ (succ n))) ≤
    (1 / (2 * ↑(succ n) + 1)) ^ 2 / (1 - (1 / (2 * ↑(succ n) + 1)) ^ 2)
n : ℕ
⊢ Real.log (stirlingSeq (succ n)) - Real.log (stirlingSeq (succ (succ n))) ≤
    (1 / (2 * ↑(succ n) + 1)) ^ 2 / (1 - (1 / (2 * ↑(succ n) + 1)) ^ 2)
have h_nonneg : ↑0 ≤ ((1:ℝ) / (2 * n.succ + 1)) ^ 2 := sq_nonneg _
n : ℕ
h_nonneg : 0 ≤ (1 / (2 * ↑(succ n) + 1)) ^ 2
g :
  HasSum (fun k => ((1 / (2 * ↑(succ n) + 1)) ^ 2) ^ succ k)
    ((1 / (2 * ↑(succ n) + 1)) ^ 2 / (1 - (1 / (2 * ↑(succ n) + 1)) ^ 2))
hab :
  ∀ (k : ℕ),
    1 / (2 * ↑(succ k) + 1) * ((1 / (2 * ↑(succ n) + 1)) ^ 2) ^ succ k ≤ ((1 / (2 * ↑(succ n) + 1)) ^ 2) ^ succ k
⊢ Real.log (stirlingSeq (succ n)) - Real.log (stirlingSeq (succ (succ n))) ≤
    (1 / (2 * ↑(succ n) + 1)) ^ 2 / (1 - (1 / (2 * ↑(succ n) + 1)) ^ 2)
n : ℕ
h_nonneg : 0 ≤ (1 / (2 * ↑(succ n) + 1)) ^ 2
g :
  HasSum (fun k => ((1 / (2 * ↑(succ n) + 1)) ^ 2) ^ succ k)
    ((1 / (2 * ↑(succ n) + 1)) ^ 2 / (1 - (1 / (2 * ↑(succ n) + 1)) ^ 2))
⊢ Real.log (stirlingSeq (succ n)) - Real.log (stirlingSeq (succ (succ n))) ≤
    (1 / (2 * ↑(succ n) + 1)) ^ 2 / (1 - (1 / (2 * ↑(succ n) + 1)) ^ 2)
have hab : ∀ k : ℕ, (1:ℝ) / (↑2 * k.succ + ↑1) * (((1:ℝ) / (2 * n.succ + 1)) ^ 2) ^ k.succ ≤
    (((1:ℝ) / (2 * n.succ + 1)) ^ 2) ^ k.succ := by
  refine' fun k => mul_le_of_le_one_left (pow_nonneg h_nonneg k.succ) _
  rw [one_div]
  exact inv_le_one (le_add_of_nonneg_left <| by positivity)
no goals
n : ℕ
h_nonneg : 0 ≤ (1 / (2 * ↑(succ n) + 1)) ^ 2
g :
  HasSum (fun k => ((1 / (2 * ↑(succ n) + 1)) ^ 2) ^ succ k)
    ((1 / (2 * ↑(succ n) + 1)) ^ 2 / (1 - (1 / (2 * ↑(succ n) + 1)) ^ 2))
hab :
  ∀ (k : ℕ),
    1 / (2 * ↑(succ k) + 1) * ((1 / (2 * ↑(succ n) + 1)) ^ 2) ^ succ k ≤ ((1 / (2 * ↑(succ n) + 1)) ^ 2) ^ succ k
⊢ Real.log (stirlingSeq (succ n)) - Real.log (stirlingSeq (succ (succ n))) ≤
    (1 / (2 * ↑(succ n) + 1)) ^ 2 / (1 - (1 / (2 * ↑(succ n) + 1)) ^ 2)
exact hasSum_le hab (log_stirlingSeq_diff_hasSum n) g
case refine_2
n : ℕ
h_nonneg : 0 ≤ (1 / (2 * ↑(succ n) + 1)) ^ 2
this :
  HasSum (fun i => (1 / (2 * ↑(succ n) + 1)) ^ 2 * ((1 / (2 * ↑(succ n) + 1)) ^ 2) ^ i)
    ((1 / (2 * ↑(succ n) + 1)) ^ 2 * (1 - (1 / (2 * ↑(succ n) + 1)) ^ 2)⁻¹)
⊢ HasSum (fun k => ((1 / (2 * ↑(succ n) + 1)) ^ 2) ^ succ k)
    ((1 / (2 * ↑(succ n) + 1)) ^ 2 / (1 - (1 / (2 * ↑(succ n) + 1)) ^ 2))

case refine_1
n : ℕ
h_nonneg : 0 ≤ (1 / (2 * ↑(succ n) + 1)) ^ 2
⊢ (1 / (2 * ↑(succ n) + 1)) ^ 2 < 1
n : ℕ
h_nonneg : 0 ≤ (1 / (2 * ↑(succ n) + 1)) ^ 2
⊢ HasSum (fun k => ((1 / (2 * ↑(succ n) + 1)) ^ 2) ^ succ k)
    ((1 / (2 * ↑(succ n) + 1)) ^ 2 / (1 - (1 / (2 * ↑(succ n) + 1)) ^ 2))
have := (hasSum_geometric_of_lt_1 h_nonneg ?_).mul_left (((1:ℝ) / (2 * n.succ + 1)) ^ 2)
case refine_1
n : ℕ
h_nonneg : 0 ≤ (1 / (2 * ↑(succ n) + 1)) ^ 2
⊢ ((2 * ↑(succ n) + 1) ^ 2)⁻¹ < 1
case refine_1
n : ℕ
h_nonneg : 0 ≤ (1 / (2 * ↑(succ n) + 1)) ^ 2
⊢ (1 / (2 * ↑(succ n) + 1)) ^ 2 < 1
rw [one_div, inv_pow]
no goals
case refine_1
n : ℕ
h_nonneg : 0 ≤ (1 / (2 * ↑(succ n) + 1)) ^ 2
⊢ ((2 * ↑(succ n) + 1) ^ 2)⁻¹ < 1
exact inv_lt_one (one_lt_pow ((lt_add_iff_pos_left 1).mpr <| by positivity) two_ne_zero)
case refine_2
n : ℕ
h_nonneg : 0 ≤ (1 / (2 * ↑(succ n) + 1)) ^ 2
this :
  HasSum (fun i => ((1 / (2 * ↑(succ n) + 1)) ^ 2) ^ (i + 1))
    ((1 / (2 * ↑(succ n) + 1)) ^ 2 * (1 - (1 / (2 * ↑(succ n) + 1)) ^ 2)⁻¹)
⊢ HasSum (fun k => ((1 / (2 * ↑(succ n) + 1)) ^ 2) ^ succ k)
    ((1 / (2 * ↑(succ n) + 1)) ^ 2 / (1 - (1 / (2 * ↑(succ n) + 1)) ^ 2))
case refine_2
n : ℕ
h_nonneg : 0 ≤ (1 / (2 * ↑(succ n) + 1)) ^ 2
this :
  HasSum (fun i => (1 / (2 * ↑(succ n) + 1)) ^ 2 * ((1 / (2 * ↑(succ n) + 1)) ^ 2) ^ i)
    ((1 / (2 * ↑(succ n) + 1)) ^ 2 * (1 - (1 / (2 * ↑(succ n) + 1)) ^ 2)⁻¹)
⊢ HasSum (fun k => ((1 / (2 * ↑(succ n) + 1)) ^ 2) ^ succ k)
    ((1 / (2 * ↑(succ n) + 1)) ^ 2 / (1 - (1 / (2 * ↑(succ n) + 1)) ^ 2))
simp_rw [← _root_.pow_succ] at this
no goals
case refine_2
n : ℕ
h_nonneg : 0 ≤ (1 / (2 * ↑(succ n) + 1)) ^ 2
this :
  HasSum (fun i => ((1 / (2 * ↑(succ n) + 1)) ^ 2) ^ (i + 1))
    ((1 / (2 * ↑(succ n) + 1)) ^ 2 * (1 - (1 / (2 * ↑(succ n) + 1)) ^ 2)⁻¹)
⊢ HasSum (fun k => ((1 / (2 * ↑(succ n) + 1)) ^ 2) ^ succ k)
    ((1 / (2 * ↑(succ n) + 1)) ^ 2 / (1 - (1 / (2 * ↑(succ n) + 1)) ^ 2))
exact this
no goals
n : ℕ
h_nonneg : 0 ≤ (1 / (2 * ↑(succ n) + 1)) ^ 2
⊢ 0 < 2 * ↑(succ n)
positivity
n : ℕ
h_nonneg : 0 ≤ (1 / (2 * ↑(succ n) + 1)) ^ 2
g :
  HasSum (fun k => ((1 / (2 * ↑(succ n) + 1)) ^ 2) ^ succ k)
    ((1 / (2 * ↑(succ n) + 1)) ^ 2 / (1 - (1 / (2 * ↑(succ n) + 1)) ^ 2))
k : ℕ
⊢ 1 / (2 * ↑(succ k) + 1) ≤ 1
n : ℕ
h_nonneg : 0 ≤ (1 / (2 * ↑(succ n) + 1)) ^ 2
g :
  HasSum (fun k => ((1 / (2 * ↑(succ n) + 1)) ^ 2) ^ succ k)
    ((1 / (2 * ↑(succ n) + 1)) ^ 2 / (1 - (1 / (2 * ↑(succ n) + 1)) ^ 2))
⊢ ∀ (k : ℕ),
    1 / (2 * ↑(succ k) + 1) * ((1 / (2 * ↑(succ n) + 1)) ^ 2) ^ succ k ≤ ((1 / (2 * ↑(succ n) + 1)) ^ 2) ^ succ k
refine' fun k => mul_le_of_le_one_left (pow_nonneg h_nonneg k.succ) _
n : ℕ
h_nonneg : 0 ≤ (1 / (2 * ↑(succ n) + 1)) ^ 2
g :
  HasSum (fun k => ((1 / (2 * ↑(succ n) + 1)) ^ 2) ^ succ k)
    ((1 / (2 * ↑(succ n) + 1)) ^ 2 / (1 - (1 / (2 * ↑(succ n) + 1)) ^ 2))
k : ℕ
⊢ (2 * ↑(succ k) + 1)⁻¹ ≤ 1
n : ℕ
h_nonneg : 0 ≤ (1 / (2 * ↑(succ n) + 1)) ^ 2
g :
  HasSum (fun k => ((1 / (2 * ↑(succ n) + 1)) ^ 2) ^ succ k)
    ((1 / (2 * ↑(succ n) + 1)) ^ 2 / (1 - (1 / (2 * ↑(succ n) + 1)) ^ 2))
k : ℕ
⊢ 1 / (2 * ↑(succ k) + 1) ≤ 1
rw [one_div]
no goals
n : ℕ
h_nonneg : 0 ≤ (1 / (2 * ↑(succ n) + 1)) ^ 2
g :
  HasSum (fun k => ((1 / (2 * ↑(succ n) + 1)) ^ 2) ^ succ k)
    ((1 / (2 * ↑(succ n) + 1)) ^ 2 / (1 - (1 / (2 * ↑(succ n) + 1)) ^ 2))
k : ℕ
⊢ (2 * ↑(succ k) + 1)⁻¹ ≤ 1
exact inv_le_one (le_add_of_nonneg_left <| by positivity)
no goals
n : ℕ
h_nonneg : 0 ≤ (1 / (2 * ↑(succ n) + 1)) ^ 2
g :
  HasSum (fun k => ((1 / (2 * ↑(succ n) + 1)) ^ 2) ^ succ k)
    ((1 / (2 * ↑(succ n) + 1)) ^ 2 / (1 - (1 / (2 * ↑(succ n) + 1)) ^ 2))
k : ℕ
⊢ 0 ≤ 2 * ↑(succ k)
positivity