-- Mathlib/Analysis/SpecialFunctions/Stirling.lean
theorem log_stirlingSeq_diff_le_geo_sum (n : ℕ) :
    log (stirlingSeq (n + 1)) - log (stirlingSeq (n + 2)) ≤
      ((1 : ℝ) / (2 * ↑(n + 1) + 1)) ^ 2 / (1 - ((1 : ℝ) / (2 * ↑(n + 1) + 1)) ^ 2)

Proof state:
n : ℕ
h_nonneg : 0 ≤ (1 / (2 * ↑(n + 1) + 1)) ^ 2
g :
  HasSum (fun k => ((1 / (2 * ↑(n + 1) + 1)) ^ 2) ^ (k + 1))
    ((1 / (2 * ↑(n + 1) + 1)) ^ 2 / (1 - (1 / (2 * ↑(n + 1) + 1)) ^ 2))
k : ℕ
⊢ 0 ≤ 2 * ↑(k + 1)

Tactic:
positivity

Result:
no goals

Proof state:
n : ℕ
h_nonneg : 0 ≤ (1 / (2 * ↑(n + 1) + 1)) ^ 2
g :
  HasSum (fun k => ((1 / (2 * ↑(n + 1) + 1)) ^ 2) ^ (k + 1))
    ((1 / (2 * ↑(n + 1) + 1)) ^ 2 / (1 - (1 / (2 * ↑(n + 1) + 1)) ^ 2))
k : ℕ
⊢ 1 / (2 * ↑(k + 1) + 1) ≤ 1

Tactic:
rw [one_div]

Result:
n : ℕ
h_nonneg : 0 ≤ (1 / (2 * ↑(n + 1) + 1)) ^ 2
g :
  HasSum (fun k => ((1 / (2 * ↑(n + 1) + 1)) ^ 2) ^ (k + 1))
    ((1 / (2 * ↑(n + 1) + 1)) ^ 2 / (1 - (1 / (2 * ↑(n + 1) + 1)) ^ 2))
k : ℕ
⊢ (2 * ↑(k + 1) + 1)⁻¹ ≤ 1

Proof state:
case refine_2
n : ℕ
h_nonneg : 0 ≤ (1 / (2 * ↑(n + 1) + 1)) ^ 2
this :
  HasSum (fun i => (1 / (2 * ↑(n + 1) + 1)) ^ 2 * ((1 / (2 * ↑(n + 1) + 1)) ^ 2) ^ i)
    ((1 / (2 * ↑(n + 1) + 1)) ^ 2 * (1 - (1 / (2 * ↑(n + 1) + 1)) ^ 2)⁻¹)
⊢ HasSum (fun k => ((1 / (2 * ↑(n + 1) + 1)) ^ 2) ^ (k + 1))
    ((1 / (2 * ↑(n + 1) + 1)) ^ 2 / (1 - (1 / (2 * ↑(n + 1) + 1)) ^ 2))

Tactic:
simp_rw [← _root_.pow_succ'] at this

Result:
case refine_2
n : ℕ
h_nonneg : 0 ≤ (1 / (2 * ↑(n + 1) + 1)) ^ 2
this :
  HasSum (fun i => ((1 / (2 * ↑(n + 1) + 1)) ^ 2) ^ (i + 1))
    ((1 / (2 * ↑(n + 1) + 1)) ^ 2 * (1 - (1 / (2 * ↑(n + 1) + 1)) ^ 2)⁻¹)
⊢ HasSum (fun k => ((1 / (2 * ↑(n + 1) + 1)) ^ 2) ^ (k + 1))
    ((1 / (2 * ↑(n + 1) + 1)) ^ 2 / (1 - (1 / (2 * ↑(n + 1) + 1)) ^ 2))

Proof state:
n : ℕ
h_nonneg : 0 ≤ (1 / (2 * ↑(n + 1) + 1)) ^ 2
g :
  HasSum (fun k => ((1 / (2 * ↑(n + 1) + 1)) ^ 2) ^ (k + 1))
    ((1 / (2 * ↑(n + 1) + 1)) ^ 2 / (1 - (1 / (2 * ↑(n + 1) + 1)) ^ 2))
k : ℕ
⊢ (2 * ↑(k + 1) + 1)⁻¹ ≤ 1

Tactic:
exact inv_le_one_of_one_le₀ (le_add_of_nonneg_left <| by positivity)

Result:
no goals

Proof state:
n : ℕ
h_nonneg : 0 ≤ (1 / (2 * ↑(n + 1) + 1)) ^ 2
g :
  HasSum (fun k => ((1 / (2 * ↑(n + 1) + 1)) ^ 2) ^ (k + 1))
    ((1 / (2 * ↑(n + 1) + 1)) ^ 2 / (1 - (1 / (2 * ↑(n + 1) + 1)) ^ 2))
hab :
  ∀ (k : ℕ),
    1 / (2 * ↑(k + 1) + 1) * ((1 / (2 * ↑(n + 1) + 1)) ^ 2) ^ (k + 1) ≤ ((1 / (2 * ↑(n + 1) + 1)) ^ 2) ^ (k + 1)
⊢ Real.log (stirlingSeq (n + 1)) - Real.log (stirlingSeq (n + 2)) ≤
    (1 / (2 * ↑(n + 1) + 1)) ^ 2 / (1 - (1 / (2 * ↑(n + 1) + 1)) ^ 2)

Tactic:
exact hasSum_le hab (log_stirlingSeq_diff_hasSum n) g

Result:
no goals

Proof state:
case refine_2
n : ℕ
h_nonneg : 0 ≤ (1 / (2 * ↑(n + 1) + 1)) ^ 2
this :
  HasSum (fun i => ((1 / (2 * ↑(n + 1) + 1)) ^ 2) ^ (i + 1))
    ((1 / (2 * ↑(n + 1) + 1)) ^ 2 * (1 - (1 / (2 * ↑(n + 1) + 1)) ^ 2)⁻¹)
⊢ HasSum (fun k => ((1 / (2 * ↑(n + 1) + 1)) ^ 2) ^ (k + 1))
    ((1 / (2 * ↑(n + 1) + 1)) ^ 2 / (1 - (1 / (2 * ↑(n + 1) + 1)) ^ 2))

Tactic:
exact this

Result:
no goals

Proof state:
n : ℕ
h_nonneg : 0 ≤ (1 / (2 * ↑(n + 1) + 1)) ^ 2
g :
  HasSum (fun k => ((1 / (2 * ↑(n + 1) + 1)) ^ 2) ^ (k + 1))
    ((1 / (2 * ↑(n + 1) + 1)) ^ 2 / (1 - (1 / (2 * ↑(n + 1) + 1)) ^ 2))
⊢ Real.log (stirlingSeq (n + 1)) - Real.log (stirlingSeq (n + 2)) ≤
    (1 / (2 * ↑(n + 1) + 1)) ^ 2 / (1 - (1 / (2 * ↑(n + 1) + 1)) ^ 2)

Tactic:
have hab (k : ℕ) : (1 : ℝ) / (2 * ↑(k + 1) + 1) * ((1 / (2 * ↑(n + 1) + 1)) ^ 2) ^ ↑(k + 1) ≤
    (((1 : ℝ) / (2 * ↑(n + 1) + 1)) ^ 2) ^ ↑(k + 1) := by
  refine mul_le_of_le_one_left (pow_nonneg h_nonneg ↑(k + 1)) ?_
  rw [one_div]
  exact inv_le_one_of_one_le₀ (le_add_of_nonneg_left <| by positivity)

Result:
n : ℕ
h_nonneg : 0 ≤ (1 / (2 * ↑(n + 1) + 1)) ^ 2
g :
  HasSum (fun k => ((1 / (2 * ↑(n + 1) + 1)) ^ 2) ^ (k + 1))
    ((1 / (2 * ↑(n + 1) + 1)) ^ 2 / (1 - (1 / (2 * ↑(n + 1) + 1)) ^ 2))
hab :
  ∀ (k : ℕ),
    1 / (2 * ↑(k + 1) + 1) * ((1 / (2 * ↑(n + 1) + 1)) ^ 2) ^ (k + 1) ≤ ((1 / (2 * ↑(n + 1) + 1)) ^ 2) ^ (k + 1)
⊢ Real.log (stirlingSeq (n + 1)) - Real.log (stirlingSeq (n + 2)) ≤
    (1 / (2 * ↑(n + 1) + 1)) ^ 2 / (1 - (1 / (2 * ↑(n + 1) + 1)) ^ 2)

Proof state:
case refine_1
n : ℕ
h_nonneg : 0 ≤ (1 / (2 * ↑(n + 1) + 1)) ^ 2
⊢ (1 / (2 * ↑(n + 1) + 1)) ^ 2 < 1

Tactic:
rw [one_div, inv_pow]

Result:
case refine_1
n : ℕ
h_nonneg : 0 ≤ (1 / (2 * ↑(n + 1) + 1)) ^ 2
⊢ ((2 * ↑(n + 1) + 1) ^ 2)⁻¹ < 1

Proof state:
n : ℕ
⊢ Real.log (stirlingSeq (n + 1)) - Real.log (stirlingSeq (n + 2)) ≤
    (1 / (2 * ↑(n + 1) + 1)) ^ 2 / (1 - (1 / (2 * ↑(n + 1) + 1)) ^ 2)

Tactic:
have h_nonneg : (0 : ℝ) ≤ ((1 : ℝ) / (2 * ↑(n + 1) + 1)) ^ 2 := sq_nonneg _

Result:
n : ℕ
h_nonneg : 0 ≤ (1 / (2 * ↑(n + 1) + 1)) ^ 2
⊢ Real.log (stirlingSeq (n + 1)) - Real.log (stirlingSeq (n + 2)) ≤
    (1 / (2 * ↑(n + 1) + 1)) ^ 2 / (1 - (1 / (2 * ↑(n + 1) + 1)) ^ 2)

Proof state:
n : ℕ
h_nonneg : 0 ≤ (1 / (2 * ↑(n + 1) + 1)) ^ 2
⊢ HasSum (fun k => ((1 / (2 * ↑(n + 1) + 1)) ^ 2) ^ (k + 1))
    ((1 / (2 * ↑(n + 1) + 1)) ^ 2 / (1 - (1 / (2 * ↑(n + 1) + 1)) ^ 2))

Tactic:
have := (hasSum_geometric_of_lt_one h_nonneg ?_).mul_left (((1 : ℝ) / (2 * ↑(n + 1) + 1)) ^ 2)

Result:
case refine_2
n : ℕ
h_nonneg : 0 ≤ (1 / (2 * ↑(n + 1) + 1)) ^ 2
this :
  HasSum (fun i => (1 / (2 * ↑(n + 1) + 1)) ^ 2 * ((1 / (2 * ↑(n + 1) + 1)) ^ 2) ^ i)
    ((1 / (2 * ↑(n + 1) + 1)) ^ 2 * (1 - (1 / (2 * ↑(n + 1) + 1)) ^ 2)⁻¹)
⊢ HasSum (fun k => ((1 / (2 * ↑(n + 1) + 1)) ^ 2) ^ (k + 1))
    ((1 / (2 * ↑(n + 1) + 1)) ^ 2 / (1 - (1 / (2 * ↑(n + 1) + 1)) ^ 2))

case refine_1
n : ℕ
h_nonneg : 0 ≤ (1 / (2 * ↑(n + 1) + 1)) ^ 2
⊢ (1 / (2 * ↑(n + 1) + 1)) ^ 2 < 1

Proof state:
n : ℕ
h_nonneg : 0 ≤ (1 / (2 * ↑(n + 1) + 1)) ^ 2
⊢ 0 < 2 * ↑(n + 1)

Tactic:
positivity

Result:
no goals

Proof state:
case refine_1
n : ℕ
h_nonneg : 0 ≤ (1 / (2 * ↑(n + 1) + 1)) ^ 2
⊢ ((2 * ↑(n + 1) + 1) ^ 2)⁻¹ < 1

Tactic:
exact inv_lt_one_of_one_lt₀ (one_lt_pow₀ (lt_add_of_pos_left _ <| by positivity) two_ne_zero)

Result:
no goals

Proof state:
n : ℕ
h_nonneg : 0 ≤ (1 / (2 * ↑(n + 1) + 1)) ^ 2
g :
  HasSum (fun k => ((1 / (2 * ↑(n + 1) + 1)) ^ 2) ^ (k + 1))
    ((1 / (2 * ↑(n + 1) + 1)) ^ 2 / (1 - (1 / (2 * ↑(n + 1) + 1)) ^ 2))
k : ℕ
⊢ 1 / (2 * ↑(k + 1) + 1) * ((1 / (2 * ↑(n + 1) + 1)) ^ 2) ^ (k + 1) ≤ ((1 / (2 * ↑(n + 1) + 1)) ^ 2) ^ (k + 1)

Tactic:
refine mul_le_of_le_one_left (pow_nonneg h_nonneg ↑(k + 1)) ?_

Result:
n : ℕ
h_nonneg : 0 ≤ (1 / (2 * ↑(n + 1) + 1)) ^ 2
g :
  HasSum (fun k => ((1 / (2 * ↑(n + 1) + 1)) ^ 2) ^ (k + 1))
    ((1 / (2 * ↑(n + 1) + 1)) ^ 2 / (1 - (1 / (2 * ↑(n + 1) + 1)) ^ 2))
k : ℕ
⊢ 1 / (2 * ↑(k + 1) + 1) ≤ 1