-- Mathlib/Analysis/SpecialFunctions/Stirling.lean
theorem log_stirlingSeq_bounded_aux :
    ∃ c : ℝ, ∀ n : ℕ, log (stirlingSeq 1) - log (stirlingSeq (n + 1)) ≤ c

Proof state:
⊢ ∃ c, ∀ (n : ℕ), Real.log (stirlingSeq 1) - Real.log (stirlingSeq (n + 1)) ≤ c

Tactic:
let d : ℝ := ∑' k : ℕ, (1 : ℝ) / (↑(k + 1) : ℝ) ^ 2

Result:
d : ℝ := ∑' (k : ℕ), 1 / ↑(k + 1) ^ 2
⊢ ∃ c, ∀ (n : ℕ), Real.log (stirlingSeq 1) - Real.log (stirlingSeq (n + 1)) ≤ c

Proof state:
d : ℝ := ∑' (k : ℕ), 1 / ↑(k + 1) ^ 2
log_stirlingSeq' : ℕ → ℝ := fun k => Real.log (stirlingSeq (k + 1))
n k : ℕ
⊢ log_stirlingSeq' k - log_stirlingSeq' (k + 1) ≤ 1 / 4 * (1 / ↑(k + 1) ^ 2)

Tactic:
convert log_stirlingSeq_sub_log_stirlingSeq_succ k using 1

Result:
case h.e'_4
d : ℝ := ∑' (k : ℕ), 1 / ↑(k + 1) ^ 2
log_stirlingSeq' : ℕ → ℝ := fun k => Real.log (stirlingSeq (k + 1))
n k : ℕ
⊢ 1 / 4 * (1 / ↑(k + 1) ^ 2) = 1 / (4 * ↑(k + 1) ^ 2)

Proof state:
d : ℝ := ∑' (k : ℕ), 1 / ↑(k + 1) ^ 2
log_stirlingSeq' : ℕ → ℝ := fun k => Real.log (stirlingSeq (k + 1))
n : ℕ
h₁ : ∀ (k : ℕ), log_stirlingSeq' k - log_stirlingSeq' (k + 1) ≤ 1 / 4 * (1 / ↑(k + 1) ^ 2)
this : Summable fun n => 1 / ↑(n + 1) ^ 2
k : ℕ
x✝ : k ∉ range n
⊢ 0 ≤ 1 / ↑(k + 1) ^ 2

Tactic:
positivity

Result:
no goals

Proof state:
d : ℝ := ∑' (k : ℕ), 1 / ↑(k + 1) ^ 2
log_stirlingSeq' : ℕ → ℝ := fun k => Real.log (stirlingSeq (k + 1))
n : ℕ
h₁ : ∀ (k : ℕ), log_stirlingSeq' k - log_stirlingSeq' (k + 1) ≤ 1 / 4 * (1 / ↑(k + 1) ^ 2)
h₂ : ∑ k ∈ range n, 1 / ↑(k + 1) ^ 2 ≤ d
⊢ ∑ k ∈ range n, 1 / 4 * (1 / ↑(k + 1) ^ 2) = 1 / 4 * ∑ k ∈ range n, 1 / ↑(k + 1) ^ 2

Tactic:
rw [mul_sum]

Result:
no goals

Proof state:
case h
d : ℝ := ∑' (k : ℕ), 1 / ↑(k + 1) ^ 2
log_stirlingSeq' : ℕ → ℝ := fun k => Real.log (stirlingSeq (k + 1))
n : ℕ
h₁ : ∀ (k : ℕ), log_stirlingSeq' k - log_stirlingSeq' (k + 1) ≤ 1 / 4 * (1 / ↑(k + 1) ^ 2)
⊢ Real.log (stirlingSeq 1) - Real.log (stirlingSeq (n + 1)) ≤ 1 / 4 * d

Tactic:
have h₂ : (∑ k ∈ range n, 1 / (↑(k + 1) : ℝ) ^ 2) ≤ d := by
  have := (summable_nat_add_iff 1).mpr <| Real.summable_one_div_nat_pow.mpr one_lt_two
  exact sum_le_tsum (range n) (fun k _ => by positivity) this

Result:
case h
d : ℝ := ∑' (k : ℕ), 1 / ↑(k + 1) ^ 2
log_stirlingSeq' : ℕ → ℝ := fun k => Real.log (stirlingSeq (k + 1))
n : ℕ
h₁ : ∀ (k : ℕ), log_stirlingSeq' k - log_stirlingSeq' (k + 1) ≤ 1 / 4 * (1 / ↑(k + 1) ^ 2)
h₂ : ∑ k ∈ range n, 1 / ↑(k + 1) ^ 2 ≤ d
⊢ Real.log (stirlingSeq 1) - Real.log (stirlingSeq (n + 1)) ≤ 1 / 4 * d

Proof state:
case h
d : ℝ := ∑' (k : ℕ), 1 / ↑(k + 1) ^ 2
⊢ ∀ (n : ℕ), Real.log (stirlingSeq 1) - Real.log (stirlingSeq (n + 1)) ≤ 1 / 4 * d

Tactic:
let log_stirlingSeq' : ℕ → ℝ := fun k => log (stirlingSeq (k + 1))

Result:
case h
d : ℝ := ∑' (k : ℕ), 1 / ↑(k + 1) ^ 2
log_stirlingSeq' : ℕ → ℝ := fun k => Real.log (stirlingSeq (k + 1))
⊢ ∀ (n : ℕ), Real.log (stirlingSeq 1) - Real.log (stirlingSeq (n + 1)) ≤ 1 / 4 * d

Proof state:
d : ℝ := ∑' (k : ℕ), 1 / ↑(k + 1) ^ 2
log_stirlingSeq' : ℕ → ℝ := fun k => Real.log (stirlingSeq (k + 1))
n : ℕ
h₁ : ∀ (k : ℕ), log_stirlingSeq' k - log_stirlingSeq' (k + 1) ≤ 1 / 4 * (1 / ↑(k + 1) ^ 2)
h₂ : ∑ k ∈ range n, 1 / ↑(k + 1) ^ 2 ≤ d
⊢ 1 / 4 * ∑ k ∈ range n, 1 / ↑(k + 1) ^ 2 ≤ 1 / 4 * d

Tactic:
gcongr

Result:
no goals

Proof state:
d : ℝ := ∑' (k : ℕ), 1 / ↑(k + 1) ^ 2
log_stirlingSeq' : ℕ → ℝ := fun k => Real.log (stirlingSeq (k + 1))
n : ℕ
h₁ : ∀ (k : ℕ), log_stirlingSeq' k - log_stirlingSeq' (k + 1) ≤ 1 / 4 * (1 / ↑(k + 1) ^ 2)
⊢ ∑ k ∈ range n, 1 / ↑(k + 1) ^ 2 ≤ d

Tactic:
have := (summable_nat_add_iff 1).mpr <| Real.summable_one_div_nat_pow.mpr one_lt_two

Result:
d : ℝ := ∑' (k : ℕ), 1 / ↑(k + 1) ^ 2
log_stirlingSeq' : ℕ → ℝ := fun k => Real.log (stirlingSeq (k + 1))
n : ℕ
h₁ : ∀ (k : ℕ), log_stirlingSeq' k - log_stirlingSeq' (k + 1) ≤ 1 / 4 * (1 / ↑(k + 1) ^ 2)
this : Summable fun n => 1 / ↑(n + 1) ^ 2
⊢ ∑ k ∈ range n, 1 / ↑(k + 1) ^ 2 ≤ d

Proof state:
case h
d : ℝ := ∑' (k : ℕ), 1 / ↑(k + 1) ^ 2
log_stirlingSeq' : ℕ → ℝ := fun k => Real.log (stirlingSeq (k + 1))
n : ℕ
⊢ Real.log (stirlingSeq 1) - Real.log (stirlingSeq (n + 1)) ≤ 1 / 4 * d

Tactic:
have h₁ k : log_stirlingSeq' k - log_stirlingSeq' (k + 1) ≤ 1 / 4 * (1 / (↑(k + 1) : ℝ) ^ 2) := by
  convert log_stirlingSeq_sub_log_stirlingSeq_succ k using 1; field_simp

Result:
case h
d : ℝ := ∑' (k : ℕ), 1 / ↑(k + 1) ^ 2
log_stirlingSeq' : ℕ → ℝ := fun k => Real.log (stirlingSeq (k + 1))
n : ℕ
h₁ : ∀ (k : ℕ), log_stirlingSeq' k - log_stirlingSeq' (k + 1) ≤ 1 / 4 * (1 / ↑(k + 1) ^ 2)
⊢ Real.log (stirlingSeq 1) - Real.log (stirlingSeq (n + 1)) ≤ 1 / 4 * d

Proof state:
case h
d : ℝ := ∑' (k : ℕ), 1 / ↑(k + 1) ^ 2
log_stirlingSeq' : ℕ → ℝ := fun k => Real.log (stirlingSeq (k + 1))
n : ℕ
h₁ : ∀ (k : ℕ), log_stirlingSeq' k - log_stirlingSeq' (k + 1) ≤ 1 / 4 * (1 / ↑(k + 1) ^ 2)
h₂ : ∑ k ∈ range n, 1 / ↑(k + 1) ^ 2 ≤ d
⊢ Real.log (stirlingSeq 1) - Real.log (stirlingSeq (n + 1)) ≤ 1 / 4 * d

Tactic:
calc
  log (stirlingSeq 1) - log (stirlingSeq (n + 1)) = log_stirlingSeq' 0 - log_stirlingSeq' n :=
    rfl
  _ = ∑ k ∈ range n, (log_stirlingSeq' k - log_stirlingSeq' (k + 1)) := by
    rw [← sum_range_sub' log_stirlingSeq' n]
  _ ≤ ∑ k ∈ range n, 1 / 4 * (1 / ↑((k + 1)) ^ 2) := sum_le_sum fun k _ => h₁ k
  _ = 1 / 4 * ∑ k ∈ range n, 1 / ↑((k + 1)) ^ 2 := by rw [mul_sum]
  _ ≤ 1 / 4 * d := by gcongr

Result:
no goals

Proof state:
case h.e'_4
d : ℝ := ∑' (k : ℕ), 1 / ↑(k + 1) ^ 2
log_stirlingSeq' : ℕ → ℝ := fun k => Real.log (stirlingSeq (k + 1))
n k : ℕ
⊢ 1 / 4 * (1 / ↑(k + 1) ^ 2) = 1 / (4 * ↑(k + 1) ^ 2)

Tactic:
field_simp

Result:
no goals

Proof state:
d : ℝ := ∑' (k : ℕ), 1 / ↑(k + 1) ^ 2
log_stirlingSeq' : ℕ → ℝ := fun k => Real.log (stirlingSeq (k + 1))
n : ℕ
h₁ : ∀ (k : ℕ), log_stirlingSeq' k - log_stirlingSeq' (k + 1) ≤ 1 / 4 * (1 / ↑(k + 1) ^ 2)
h₂ : ∑ k ∈ range n, 1 / ↑(k + 1) ^ 2 ≤ d
⊢ log_stirlingSeq' 0 - log_stirlingSeq' n = ∑ k ∈ range n, (log_stirlingSeq' k - log_stirlingSeq' (k + 1))

Tactic:
rw [← sum_range_sub' log_stirlingSeq' n]

Result:
no goals

Proof state:
d : ℝ := ∑' (k : ℕ), 1 / ↑(k + 1) ^ 2
⊢ ∃ c, ∀ (n : ℕ), Real.log (stirlingSeq 1) - Real.log (stirlingSeq (n + 1)) ≤ c

Tactic:
use 1 / 4 * d

Result:
case h
d : ℝ := ∑' (k : ℕ), 1 / ↑(k + 1) ^ 2
⊢ ∀ (n : ℕ), Real.log (stirlingSeq 1) - Real.log (stirlingSeq (n + 1)) ≤ 1 / 4 * d

Proof state:
case h
d : ℝ := ∑' (k : ℕ), 1 / ↑(k + 1) ^ 2
log_stirlingSeq' : ℕ → ℝ := fun k => Real.log (stirlingSeq (k + 1))
⊢ ∀ (n : ℕ), Real.log (stirlingSeq 1) - Real.log (stirlingSeq (n + 1)) ≤ 1 / 4 * d

Tactic:
intro n

Result:
case h
d : ℝ := ∑' (k : ℕ), 1 / ↑(k + 1) ^ 2
log_stirlingSeq' : ℕ → ℝ := fun k => Real.log (stirlingSeq (k + 1))
n : ℕ
⊢ Real.log (stirlingSeq 1) - Real.log (stirlingSeq (n + 1)) ≤ 1 / 4 * d

Proof state:
d : ℝ := ∑' (k : ℕ), 1 / ↑(k + 1) ^ 2
log_stirlingSeq' : ℕ → ℝ := fun k => Real.log (stirlingSeq (k + 1))
n : ℕ
h₁ : ∀ (k : ℕ), log_stirlingSeq' k - log_stirlingSeq' (k + 1) ≤ 1 / 4 * (1 / ↑(k + 1) ^ 2)
this : Summable fun n => 1 / ↑(n + 1) ^ 2
⊢ ∑ k ∈ range n, 1 / ↑(k + 1) ^ 2 ≤ d

Tactic:
exact sum_le_tsum (range n) (fun k _ => by positivity) this

Result:
no goals