-- Mathlib/Analysis/SpecialFunctions/Stirling.lean
theorem log_stirlingSeq_diff_hasSum (m : ℕ) :
    HasSum (fun k : ℕ => (1 : ℝ) / (2 * ↑(k + 1) + 1) * ((1 / (2 * ↑(m + 1) + 1)) ^ 2) ^ ↑(k + 1))
      (log (stirlingSeq (m + 1)) - log (stirlingSeq (m + 2)))

Proof state:
case h.e'_5
m : ℕ
f : ℕ → ℝ := fun k => 1 / (2 * ↑k + 1) * ((1 / (2 * ↑(m + 1) + 1)) ^ 2) ^ k
⊢ f = fun i => (↑(m + 1) + 1 / 2) * (2 * (1 / (2 * ↑i + 1)) * (1 / (2 * (↑m + 1) + 1)) ^ (2 * i + 1))

Tactic:
ext k

Result:
case h.e'_5.h
m : ℕ
f : ℕ → ℝ := fun k => 1 / (2 * ↑k + 1) * ((1 / (2 * ↑(m + 1) + 1)) ^ 2) ^ k
k : ℕ
⊢ f k = (↑(m + 1) + 1 / 2) * (2 * (1 / (2 * ↑k + 1)) * (1 / (2 * (↑m + 1) + 1)) ^ (2 * k + 1))

Proof state:
case h.e'_5.h
m : ℕ
f : ℕ → ℝ := fun k => 1 / (2 * ↑k + 1) * ((1 / (2 * ↑(m + 1) + 1)) ^ 2) ^ k
k : ℕ
⊢ 1 / (2 * ↑k + 1) * (1 / (2 * (↑m + 1) + 1)) ^ (2 * k) =
    (↑m + 1 + 1 / 2) * (2 * (1 / (2 * ↑k + 1)) * ((1 / (2 * (↑m + 1) + 1)) ^ (2 * k) * (1 / (2 * (↑m + 1) + 1)) ^ 1))

Tactic:
field_simp

Result:
case h.e'_5.h
m : ℕ
f : ℕ → ℝ := fun k => 1 / (2 * ↑k + 1) * ((1 / (2 * ↑(m + 1) + 1)) ^ 2) ^ k
k : ℕ
⊢ (2 * ↑k + 1) * ((2 * (↑m + 1) + 1) ^ (2 * k) * (2 * (↑m + 1) + 1)) =
    ((↑m + 1) * 2 + 1) * ((2 * ↑k + 1) * (2 * (↑m + 1) + 1) ^ (2 * k))

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

Tactic:
let f (k : ℕ) := (1 : ℝ) / (2 * k + 1) * ((1 / (2 * ↑(m + 1) + 1)) ^ 2) ^ k

Result:
m : ℕ
f : ℕ → ℝ := fun k => 1 / (2 * ↑k + 1) * ((1 / (2 * ↑(m + 1) + 1)) ^ 2) ^ k
⊢ HasSum (fun k => 1 / (2 * ↑(k + 1) + 1) * ((1 / (2 * ↑(m + 1) + 1)) ^ 2) ^ (k + 1))
    (Real.log (stirlingSeq (m + 1)) - Real.log (stirlingSeq (m + 2)))

Proof state:
m : ℕ
f : ℕ → ℝ := fun k => 1 / (2 * ↑k + 1) * ((1 / (2 * ↑(m + 1) + 1)) ^ 2) ^ k
⊢ HasSum (fun k => f (k + 1)) (Real.log (stirlingSeq (m + 1)) - Real.log (stirlingSeq (m + 2)))

Tactic:
rw [hasSum_nat_add_iff]

Result:
m : ℕ
f : ℕ → ℝ := fun k => 1 / (2 * ↑k + 1) * ((1 / (2 * ↑(m + 1) + 1)) ^ 2) ^ k
⊢ HasSum f (Real.log (stirlingSeq (m + 1)) - Real.log (stirlingSeq (m + 2)) + ∑ i ∈ range 1, f i)

Proof state:
m : ℕ
f : ℕ → ℝ := fun k => 1 / (2 * ↑k + 1) * ((1 / (2 * ↑(m + 1) + 1)) ^ 2) ^ k
⊢ HasSum (fun k => 1 / (2 * ↑(k + 1) + 1) * ((1 / (2 * ↑(m + 1) + 1)) ^ 2) ^ (k + 1))
    (Real.log (stirlingSeq (m + 1)) - Real.log (stirlingSeq (m + 2)))

Tactic:
change HasSum (fun k => f (k + 1)) _

Result:
m : ℕ
f : ℕ → ℝ := fun k => 1 / (2 * ↑k + 1) * ((1 / (2 * ↑(m + 1) + 1)) ^ 2) ^ k
⊢ HasSum (fun k => f (k + 1)) (Real.log (stirlingSeq (m + 1)) - Real.log (stirlingSeq (m + 2)))

Proof state:
case h.e'_5.h
m : ℕ
f : ℕ → ℝ := fun k => 1 / (2 * ↑k + 1) * ((1 / (2 * ↑(m + 1) + 1)) ^ 2) ^ k
k : ℕ
⊢ f k = (↑(m + 1) + 1 / 2) * (2 * (1 / (2 * ↑k + 1)) * (1 / (2 * (↑m + 1) + 1)) ^ (2 * k + 1))

Tactic:
dsimp only [f]

Result:
case h.e'_5.h
m : ℕ
f : ℕ → ℝ := fun k => 1 / (2 * ↑k + 1) * ((1 / (2 * ↑(m + 1) + 1)) ^ 2) ^ k
k : ℕ
⊢ 1 / (2 * ↑k + 1) * ((1 / (2 * ↑(m + 1) + 1)) ^ 2) ^ k =
    (↑(m + 1) + 1 / 2) * (2 * (1 / (2 * ↑k + 1)) * (1 / (2 * (↑m + 1) + 1)) ^ (2 * k + 1))

Proof state:
m : ℕ
f : ℕ → ℝ := fun k => 1 / (2 * ↑k + 1) * ((1 / (2 * ↑(m + 1) + 1)) ^ 2) ^ k
⊢ HasSum f (Real.log (stirlingSeq (m + 1)) - Real.log (stirlingSeq (m + 2)) + ∑ i ∈ range 1, f i)

Tactic:
convert (hasSum_log_one_add_inv m.cast_add_one_pos).mul_left ((↑(m + 1) : ℝ) + 1 / 2) using 1

Result:
case h.e'_5
m : ℕ
f : ℕ → ℝ := fun k => 1 / (2 * ↑k + 1) * ((1 / (2 * ↑(m + 1) + 1)) ^ 2) ^ k
⊢ f = fun i => (↑(m + 1) + 1 / 2) * (2 * (1 / (2 * ↑i + 1)) * (1 / (2 * (↑m + 1) + 1)) ^ (2 * i + 1))

case h.e'_6
m : ℕ
f : ℕ → ℝ := fun k => 1 / (2 * ↑k + 1) * ((1 / (2 * ↑(m + 1) + 1)) ^ 2) ^ k
⊢ Real.log (stirlingSeq (m + 1)) - Real.log (stirlingSeq (m + 2)) + ∑ i ∈ range 1, f i =
    (↑(m + 1) + 1 / 2) * Real.log (1 + (↑m + 1)⁻¹)

Proof state:
case h.e'_6
m : ℕ
f : ℕ → ℝ := fun k => 1 / (2 * ↑k + 1) * ((1 / (2 * ↑(m + 1) + 1)) ^ 2) ^ k
h : ∀ (x : ℝ), x ≠ 0 → 1 + x⁻¹ = (x + 1) / x
⊢ Real.log (stirlingSeq (m + 1)) - Real.log (stirlingSeq (m + 2)) + ∑ i ∈ range 1, f i =
    (↑(m + 1) + 1 / 2) * Real.log (1 + (↑m + 1)⁻¹)

Tactic:
simp (disch := positivity) only [log_stirlingSeq_formula, log_div, log_mul, log_exp,
  factorial_succ, cast_mul, cast_succ, cast_zero, range_one, sum_singleton, h]

Result:
case h.e'_6
m : ℕ
f : ℕ → ℝ := fun k => 1 / (2 * ↑k + 1) * ((1 / (2 * ↑(m + 1) + 1)) ^ 2) ^ k
h : ∀ (x : ℝ), x ≠ 0 → 1 + x⁻¹ = (x + 1) / x
⊢ Real.log (↑m + 1) + Real.log ↑m ! - 1 / 2 * (Real.log 2 + Real.log (↑m + 1)) - (↑m + 1) * (Real.log (↑m + 1) - 1) -
        (Real.log (↑m + 1 + 1) + (Real.log (↑m + 1) + Real.log ↑m !) - 1 / 2 * (Real.log 2 + Real.log (↑m + 1 + 1)) -
          (↑m + 1 + 1) * (Real.log (↑m + 1 + 1) - 1)) +
      f 0 =
    (↑m + 1 + 1 / 2) * (Real.log (↑m + 1 + 1) - Real.log (↑m + 1))

Proof state:
case h.e'_5.h
m : ℕ
f : ℕ → ℝ := fun k => 1 / (2 * ↑k + 1) * ((1 / (2 * ↑(m + 1) + 1)) ^ 2) ^ k
k : ℕ
⊢ 1 / (2 * ↑k + 1) * (1 / (2 * ↑(m + 1) + 1)) ^ (2 * k) =
    (↑(m + 1) + 1 / 2) * (2 * (1 / (2 * ↑k + 1)) * ((1 / (2 * (↑m + 1) + 1)) ^ (2 * k) * (1 / (2 * (↑m + 1) + 1)) ^ 1))

Tactic:
push_cast

Result:
case h.e'_5.h
m : ℕ
f : ℕ → ℝ := fun k => 1 / (2 * ↑k + 1) * ((1 / (2 * ↑(m + 1) + 1)) ^ 2) ^ k
k : ℕ
⊢ 1 / (2 * ↑k + 1) * (1 / (2 * (↑m + 1) + 1)) ^ (2 * k) =
    (↑m + 1 + 1 / 2) * (2 * (1 / (2 * ↑k + 1)) * ((1 / (2 * (↑m + 1) + 1)) ^ (2 * k) * (1 / (2 * (↑m + 1) + 1)) ^ 1))

Proof state:
m : ℕ
f : ℕ → ℝ := fun k => 1 / (2 * ↑k + 1) * ((1 / (2 * ↑(m + 1) + 1)) ^ 2) ^ k
x : ℝ
hx : x ≠ 0
⊢ 1 + x⁻¹ = (x + 1) / x

Tactic:
field_simp [hx]

Result:
no goals

Proof state:
case h.e'_5.h
m : ℕ
f : ℕ → ℝ := fun k => 1 / (2 * ↑k + 1) * ((1 / (2 * ↑(m + 1) + 1)) ^ 2) ^ k
k : ℕ
⊢ 1 / (2 * ↑k + 1) * ((1 / (2 * ↑(m + 1) + 1)) ^ 2) ^ k =
    (↑(m + 1) + 1 / 2) * (2 * (1 / (2 * ↑k + 1)) * (1 / (2 * (↑m + 1) + 1)) ^ (2 * k + 1))

Tactic:
rw [← pow_mul, pow_add]

Result:
case h.e'_5.h
m : ℕ
f : ℕ → ℝ := fun k => 1 / (2 * ↑k + 1) * ((1 / (2 * ↑(m + 1) + 1)) ^ 2) ^ k
k : ℕ
⊢ 1 / (2 * ↑k + 1) * (1 / (2 * ↑(m + 1) + 1)) ^ (2 * k) =
    (↑(m + 1) + 1 / 2) * (2 * (1 / (2 * ↑k + 1)) * ((1 / (2 * (↑m + 1) + 1)) ^ (2 * k) * (1 / (2 * (↑m + 1) + 1)) ^ 1))

Proof state:
case h.e'_6
m : ℕ
f : ℕ → ℝ := fun k => 1 / (2 * ↑k + 1) * ((1 / (2 * ↑(m + 1) + 1)) ^ 2) ^ k
h : ∀ (x : ℝ), x ≠ 0 → 1 + x⁻¹ = (x + 1) / x
⊢ Real.log (↑m + 1) + Real.log ↑m ! - 1 / 2 * (Real.log 2 + Real.log (↑m + 1)) - (↑m + 1) * (Real.log (↑m + 1) - 1) -
        (Real.log (↑m + 1 + 1) + (Real.log (↑m + 1) + Real.log ↑m !) - 1 / 2 * (Real.log 2 + Real.log (↑m + 1 + 1)) -
          (↑m + 1 + 1) * (Real.log (↑m + 1 + 1) - 1)) +
      f 0 =
    (↑m + 1 + 1 / 2) * (Real.log (↑m + 1 + 1) - Real.log (↑m + 1))

Tactic:
ring

Result:
no goals

Proof state:
case h.e'_6
m : ℕ
f : ℕ → ℝ := fun k => 1 / (2 * ↑k + 1) * ((1 / (2 * ↑(m + 1) + 1)) ^ 2) ^ k
⊢ Real.log (stirlingSeq (m + 1)) - Real.log (stirlingSeq (m + 2)) + ∑ i ∈ range 1, f i =
    (↑(m + 1) + 1 / 2) * Real.log (1 + (↑m + 1)⁻¹)

Tactic:
have h : ∀ x ≠ (0 : ℝ), 1 + x⁻¹ = (x + 1) / x := fun x hx ↦ by field_simp [hx]

Result:
case h.e'_6
m : ℕ
f : ℕ → ℝ := fun k => 1 / (2 * ↑k + 1) * ((1 / (2 * ↑(m + 1) + 1)) ^ 2) ^ k
h : ∀ (x : ℝ), x ≠ 0 → 1 + x⁻¹ = (x + 1) / x
⊢ Real.log (stirlingSeq (m + 1)) - Real.log (stirlingSeq (m + 2)) + ∑ i ∈ range 1, f i =
    (↑(m + 1) + 1 / 2) * Real.log (1 + (↑m + 1)⁻¹)

Proof state:
case h.e'_5.h
m : ℕ
f : ℕ → ℝ := fun k => 1 / (2 * ↑k + 1) * ((1 / (2 * ↑(m + 1) + 1)) ^ 2) ^ k
k : ℕ
⊢ (2 * ↑k + 1) * ((2 * (↑m + 1) + 1) ^ (2 * k) * (2 * (↑m + 1) + 1)) =
    ((↑m + 1) * 2 + 1) * ((2 * ↑k + 1) * (2 * (↑m + 1) + 1) ^ (2 * k))

Tactic:
ring

Result:
no goals