m : ℕ
⊢ HasSum ((fun b => 1 / (2 * ↑b + 1) * ((1 / (2 * ↑(succ m) + 1)) ^ 2) ^ b) ∘ succ)
    (Real.log (stirlingSeq (succ m)) - Real.log (stirlingSeq (succ (succ m))))
m : ℕ
⊢ HasSum (fun k => 1 / (2 * ↑(succ k) + 1) * ((1 / (2 * ↑(succ m) + 1)) ^ 2) ^ succ k)
    (Real.log (stirlingSeq (succ m)) - Real.log (stirlingSeq (succ (succ m))))
change HasSum
  ((fun b : ℕ => (1:ℝ) / ((2:ℝ) * b + (1:ℝ)) * (((1:ℝ) / (2 * m.succ + 1)) ^ 2) ^ b) ∘ succ) _
m : ℕ
⊢ HasSum (fun b => 1 / (2 * ↑b + 1) * ((1 / (2 * ↑(succ m) + 1)) ^ 2) ^ b)
    (Real.log (stirlingSeq (succ m)) - Real.log (stirlingSeq (succ (succ m))) +
      ∑ i in range 1, 1 / (2 * ↑i + 1) * ((1 / (2 * ↑(succ m) + 1)) ^ 2) ^ i)
m : ℕ
⊢ HasSum ((fun b => 1 / (2 * ↑b + 1) * ((1 / (2 * ↑(succ m) + 1)) ^ 2) ^ b) ∘ succ)
    (Real.log (stirlingSeq (succ m)) - Real.log (stirlingSeq (succ (succ m))))
refine' (hasSum_nat_add_iff (a := _ - _) (f := (fun b : ℕ => ↑1 / (↑2 * b + ↑1) * (((1:ℝ) / (2 * m.succ + 1)) ^ 2) ^ b)) 1).mpr _
case h.e'_5
m : ℕ
⊢ (fun b => 1 / (2 * ↑b + 1) * ((1 / (2 * ↑(succ m) + 1)) ^ 2) ^ b) = fun i =>
    (↑(succ m) + 1 / 2) * (2 * (1 / (2 * ↑i + 1)) * (1 / (2 * ↑(succ m) + 1)) ^ (2 * i + 1))

case h.e'_6
m : ℕ
⊢ Real.log (stirlingSeq (succ m)) - Real.log (stirlingSeq (succ (succ m))) +
      ∑ i in range 1, 1 / (2 * ↑i + 1) * ((1 / (2 * ↑(succ m) + 1)) ^ 2) ^ i =
    (↑(succ m) + 1 / 2) * Real.log (1 + (↑(succ m))⁻¹)
m : ℕ
⊢ HasSum (fun b => 1 / (2 * ↑b + 1) * ((1 / (2 * ↑(succ m) + 1)) ^ 2) ^ b)
    (Real.log (stirlingSeq (succ m)) - Real.log (stirlingSeq (succ (succ m))) +
      ∑ i in range 1, 1 / (2 * ↑i + 1) * ((1 / (2 * ↑(succ m) + 1)) ^ 2) ^ i)
convert (hasSum_log_one_add_inv <|
  cast_pos.mpr (succ_pos m)).mul_left ((m.succ : ℝ) + 1 / 2) using 1
case h.e'_5.h
m k : ℕ
⊢ 1 / (2 * ↑k + 1) * ((1 / (2 * ↑(succ m) + 1)) ^ 2) ^ k =
    (↑(succ m) + 1 / 2) * (2 * (1 / (2 * ↑k + 1)) * (1 / (2 * ↑(succ m) + 1)) ^ (2 * k + 1))
case h.e'_5
m : ℕ
⊢ (fun b => 1 / (2 * ↑b + 1) * ((1 / (2 * ↑(succ m) + 1)) ^ 2) ^ b) = fun i =>
    (↑(succ m) + 1 / 2) * (2 * (1 / (2 * ↑i + 1)) * (1 / (2 * ↑(succ m) + 1)) ^ (2 * i + 1))
ext k
case h.e'_5.h
m k : ℕ
⊢ 1 / (2 * ↑k + 1) * (1 / (2 * ↑(succ m) + 1)) ^ (2 * k) =
    (↑(succ m) + 1 / 2) *
      (2 * (1 / (2 * ↑k + 1)) * ((1 / (2 * ↑(succ m) + 1)) ^ (2 * k) * (1 / (2 * ↑(succ m) + 1)) ^ 1))
case h.e'_5.h
m k : ℕ
⊢ 1 / (2 * ↑k + 1) * ((1 / (2 * ↑(succ m) + 1)) ^ 2) ^ k =
    (↑(succ m) + 1 / 2) * (2 * (1 / (2 * ↑k + 1)) * (1 / (2 * ↑(succ m) + 1)) ^ (2 * k + 1))
rw [← pow_mul, pow_add]
case h.e'_5.h
m 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))
case h.e'_5.h
m k : ℕ
⊢ 1 / (2 * ↑k + 1) * (1 / (2 * ↑(succ m) + 1)) ^ (2 * k) =
    (↑(succ m) + 1 / 2) *
      (2 * (1 / (2 * ↑k + 1)) * ((1 / (2 * ↑(succ m) + 1)) ^ (2 * k) * (1 / (2 * ↑(succ m) + 1)) ^ 1))
push_cast
case h.e'_5.h
m k : ℕ
this : 2 * ↑k + 1 ≠ 0
⊢ 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))
case h.e'_5.h
m 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))
have : 2 * (k : ℝ) + 1 ≠ 0 := by norm_cast; exact succ_ne_zero (2 * k)
case h.e'_5.h
m k : ℕ
this✝ : 2 * ↑k + 1 ≠ 0
this : 2 * (↑m + 1) + 1 ≠ 0
⊢ 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))
case h.e'_5.h
m k : ℕ
this : 2 * ↑k + 1 ≠ 0
⊢ 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))
have : 2 * ((m : ℝ) + 1) + 1 ≠ 0 := by norm_cast; exact succ_ne_zero (2 * m.succ)
case h.e'_5.h
m k : ℕ
this✝ : 2 * ↑k + 1 ≠ 0
this : 2 * (↑m + 1) + 1 ≠ 0
⊢ (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))
case h.e'_5.h
m k : ℕ
this✝ : 2 * ↑k + 1 ≠ 0
this : 2 * (↑m + 1) + 1 ≠ 0
⊢ 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))
field_simp
no goals
case h.e'_5.h
m k : ℕ
this✝ : 2 * ↑k + 1 ≠ 0
this : 2 * (↑m + 1) + 1 ≠ 0
⊢ (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))
ring
m k : ℕ
⊢ ¬2 * k + 1 = 0
m k : ℕ
⊢ 2 * ↑k + 1 ≠ 0
norm_cast
no goals
m k : ℕ
⊢ ¬2 * k + 1 = 0
exact succ_ne_zero (2 * k)
m k : ℕ
this : 2 * ↑k + 1 ≠ 0
⊢ ¬2 * (m + 1) + 1 = 0
m k : ℕ
this : 2 * ↑k + 1 ≠ 0
⊢ 2 * (↑m + 1) + 1 ≠ 0
norm_cast
no goals
m k : ℕ
this : 2 * ↑k + 1 ≠ 0
⊢ ¬2 * (m + 1) + 1 = 0
exact succ_ne_zero (2 * m.succ)
case h.e'_6
m : ℕ
h : ∀ (x : ℝ), x ≠ 0 → 1 + x⁻¹ = (x + 1) / x
⊢ Real.log (stirlingSeq (succ m)) - Real.log (stirlingSeq (succ (succ m))) +
      ∑ i in range 1, 1 / (2 * ↑i + 1) * ((1 / (2 * ↑(succ m) + 1)) ^ 2) ^ i =
    (↑(succ m) + 1 / 2) * Real.log (1 + (↑(succ m))⁻¹)
case h.e'_6
m : ℕ
⊢ Real.log (stirlingSeq (succ m)) - Real.log (stirlingSeq (succ (succ m))) +
      ∑ i in range 1, 1 / (2 * ↑i + 1) * ((1 / (2 * ↑(succ m) + 1)) ^ 2) ^ i =
    (↑(succ m) + 1 / 2) * Real.log (1 + (↑(succ m))⁻¹)
have h : ∀ (x : ℝ) (_ : x ≠ 0), 1 + x⁻¹ = (x + 1) / x := by
  intro x hx; rw [_root_.add_div, div_self hx, inv_eq_one_div]
case h.e'_6
m : ℕ
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)) +
      1 / (2 * 0 + 1) * ((1 / (2 * (↑m + 1) + 1)) ^ 2) ^ 0 =
    (↑m + 1 + 1 / 2) * (Real.log (↑m + 1 + 1) - Real.log (↑m + 1))
case h.e'_6
m : ℕ
h : ∀ (x : ℝ), x ≠ 0 → 1 + x⁻¹ = (x + 1) / x
⊢ Real.log (stirlingSeq (succ m)) - Real.log (stirlingSeq (succ (succ m))) +
      ∑ i in range 1, 1 / (2 * ↑i + 1) * ((1 / (2 * ↑(succ m) + 1)) ^ 2) ^ i =
    (↑(succ m) + 1 / 2) * Real.log (1 + (↑(succ m))⁻¹)
simp (disch := norm_cast <;> apply_rules [mul_ne_zero, succ_ne_zero, factorial_ne_zero,
  exp_ne_zero]) only [log_stirlingSeq_formula, log_div, log_mul, log_exp, factorial_succ,
  cast_mul, cast_succ, cast_zero, range_one, sum_singleton, h]
no goals
case h.e'_6
m : ℕ
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)) +
      1 / (2 * 0 + 1) * ((1 / (2 * (↑m + 1) + 1)) ^ 2) ^ 0 =
    (↑m + 1 + 1 / 2) * (Real.log (↑m + 1 + 1) - Real.log (↑m + 1))
ring
m : ℕ
x : ℝ
hx : x ≠ 0
⊢ 1 + x⁻¹ = (x + 1) / x
m : ℕ
⊢ ∀ (x : ℝ), x ≠ 0 → 1 + x⁻¹ = (x + 1) / x
intro x hx
no goals
m : ℕ
x : ℝ
hx : x ≠ 0
⊢ 1 + x⁻¹ = (x + 1) / x
rw [_root_.add_div, div_self hx, inv_eq_one_div]