[GOAL]
x y : ℝ
⊢ MonotoneOn (fun x => log x * x) {x | 1 ≤ x}
[PROOFSTEP]
simp only [MonotoneOn, mem_setOf_eq]
[GOAL]
x y : ℝ
⊢ ∀ ⦃a : ℝ⦄, 1 ≤ a → ∀ ⦃b : ℝ⦄, 1 ≤ b → a ≤ b → log a * a ≤ log b * b
[PROOFSTEP]
intro x hex y hey hxy
[GOAL]
x✝ y✝ x : ℝ
hex : 1 ≤ x
y : ℝ
hey : 1 ≤ y
hxy : x ≤ y
⊢ log x * x ≤ log y * y
[PROOFSTEP]
have x_pos : 0 < x := lt_of_lt_of_le zero_lt_one hex
[GOAL]
x✝ y✝ x : ℝ
hex : 1 ≤ x
y : ℝ
hey : 1 ≤ y
hxy : x ≤ y
x_pos : 0 < x
⊢ log x * x ≤ log y * y
[PROOFSTEP]
have y_pos : 0 < y := lt_of_lt_of_le zero_lt_one hey
[GOAL]
x✝ y✝ x : ℝ
hex : 1 ≤ x
y : ℝ
hey : 1 ≤ y
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
⊢ log x * x ≤ log y * y
[PROOFSTEP]
refine' mul_le_mul ((log_le_log x_pos y_pos).mpr hxy) hxy (le_of_lt x_pos) _
[GOAL]
x✝ y✝ x : ℝ
hex : 1 ≤ x
y : ℝ
hey : 1 ≤ y
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
⊢ 0 ≤ log y
[PROOFSTEP]
rwa [le_log_iff_exp_le y_pos, Real.exp_zero]
[GOAL]
x y : ℝ
⊢ AntitoneOn (fun x => log x / x) {x | exp 1 ≤ x}
[PROOFSTEP]
simp only [AntitoneOn, mem_setOf_eq]
[GOAL]
x y : ℝ
⊢ ∀ ⦃a : ℝ⦄, exp 1 ≤ a → ∀ ⦃b : ℝ⦄, exp 1 ≤ b → a ≤ b → log b / b ≤ log a / a
[PROOFSTEP]
intro x hex y hey hxy
[GOAL]
x✝ y✝ x : ℝ
hex : exp 1 ≤ x
y : ℝ
hey : exp 1 ≤ y
hxy : x ≤ y
⊢ log y / y ≤ log x / x
[PROOFSTEP]
have x_pos : 0 < x := (exp_pos 1).trans_le hex
[GOAL]
x✝ y✝ x : ℝ
hex : exp 1 ≤ x
y : ℝ
hey : exp 1 ≤ y
hxy : x ≤ y
x_pos : 0 < x
⊢ log y / y ≤ log x / x
[PROOFSTEP]
have y_pos : 0 < y := (exp_pos 1).trans_le hey
[GOAL]
x✝ y✝ x : ℝ
hex : exp 1 ≤ x
y : ℝ
hey : exp 1 ≤ y
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
⊢ log y / y ≤ log x / x
[PROOFSTEP]
have hlogx : 1 ≤ log x := by rwa [le_log_iff_exp_le x_pos]
[GOAL]
x✝ y✝ x : ℝ
hex : exp 1 ≤ x
y : ℝ
hey : exp 1 ≤ y
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
⊢ 1 ≤ log x
[PROOFSTEP]
rwa [le_log_iff_exp_le x_pos]
[GOAL]
x✝ y✝ x : ℝ
hex : exp 1 ≤ x
y : ℝ
hey : exp 1 ≤ y
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
hlogx : 1 ≤ log x
⊢ log y / y ≤ log x / x
[PROOFSTEP]
have hyx : 0 ≤ y / x - 1 := by rwa [le_sub_iff_add_le, le_div_iff x_pos, zero_add, one_mul]
[GOAL]
x✝ y✝ x : ℝ
hex : exp 1 ≤ x
y : ℝ
hey : exp 1 ≤ y
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
hlogx : 1 ≤ log x
⊢ 0 ≤ y / x - 1
[PROOFSTEP]
rwa [le_sub_iff_add_le, le_div_iff x_pos, zero_add, one_mul]
[GOAL]
x✝ y✝ x : ℝ
hex : exp 1 ≤ x
y : ℝ
hey : exp 1 ≤ y
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
hlogx : 1 ≤ log x
hyx : 0 ≤ y / x - 1
⊢ log y / y ≤ log x / x
[PROOFSTEP]
rw [div_le_iff y_pos, ← sub_le_sub_iff_right (log x)]
[GOAL]
x✝ y✝ x : ℝ
hex : exp 1 ≤ x
y : ℝ
hey : exp 1 ≤ y
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
hlogx : 1 ≤ log x
hyx : 0 ≤ y / x - 1
⊢ log y - log x ≤ log x / x * y - log x
[PROOFSTEP]
calc
  log y - log x = log (y / x) := by rw [log_div y_pos.ne' x_pos.ne']
  _ ≤ y / x - 1 := (log_le_sub_one_of_pos (div_pos y_pos x_pos))
  _ ≤ log x * (y / x - 1) := (le_mul_of_one_le_left hyx hlogx)
  _ = log x / x * y - log x := by ring
[GOAL]
x✝ y✝ x : ℝ
hex : exp 1 ≤ x
y : ℝ
hey : exp 1 ≤ y
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
hlogx : 1 ≤ log x
hyx : 0 ≤ y / x - 1
⊢ log y - log x = log (y / x)
[PROOFSTEP]
rw [log_div y_pos.ne' x_pos.ne']
[GOAL]
x✝ y✝ x : ℝ
hex : exp 1 ≤ x
y : ℝ
hey : exp 1 ≤ y
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
hlogx : 1 ≤ log x
hyx : 0 ≤ y / x - 1
⊢ log x * (y / x - 1) = log x / x * y - log x
[PROOFSTEP]
ring
[GOAL]
x y a : ℝ
ha : 0 < a
⊢ AntitoneOn (fun x => log x / x ^ a) {x | exp (1 / a) ≤ x}
[PROOFSTEP]
simp only [AntitoneOn, mem_setOf_eq]
[GOAL]
x y a : ℝ
ha : 0 < a
⊢ ∀ ⦃a_1 : ℝ⦄, exp (1 / a) ≤ a_1 → ∀ ⦃b : ℝ⦄, exp (1 / a) ≤ b → a_1 ≤ b → log b / b ^ a ≤ log a_1 / a_1 ^ a
[PROOFSTEP]
intro x hex y _ hxy
[GOAL]
x✝¹ y✝ a : ℝ
ha : 0 < a
x : ℝ
hex : exp (1 / a) ≤ x
y : ℝ
x✝ : exp (1 / a) ≤ y
hxy : x ≤ y
⊢ log y / y ^ a ≤ log x / x ^ a
[PROOFSTEP]
have x_pos : 0 < x := lt_of_lt_of_le (exp_pos (1 / a)) hex
[GOAL]
x✝¹ y✝ a : ℝ
ha : 0 < a
x : ℝ
hex : exp (1 / a) ≤ x
y : ℝ
x✝ : exp (1 / a) ≤ y
hxy : x ≤ y
x_pos : 0 < x
⊢ log y / y ^ a ≤ log x / x ^ a
[PROOFSTEP]
have y_pos : 0 < y := by linarith
[GOAL]
x✝¹ y✝ a : ℝ
ha : 0 < a
x : ℝ
hex : exp (1 / a) ≤ x
y : ℝ
x✝ : exp (1 / a) ≤ y
hxy : x ≤ y
x_pos : 0 < x
⊢ 0 < y
[PROOFSTEP]
linarith
[GOAL]
x✝¹ y✝ a : ℝ
ha : 0 < a
x : ℝ
hex : exp (1 / a) ≤ x
y : ℝ
x✝ : exp (1 / a) ≤ y
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
⊢ log y / y ^ a ≤ log x / x ^ a
[PROOFSTEP]
have x_nonneg : 0 ≤ x := le_trans (le_of_lt (exp_pos (1 / a))) hex
[GOAL]
x✝¹ y✝ a : ℝ
ha : 0 < a
x : ℝ
hex : exp (1 / a) ≤ x
y : ℝ
x✝ : exp (1 / a) ≤ y
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
x_nonneg : 0 ≤ x
⊢ log y / y ^ a ≤ log x / x ^ a
[PROOFSTEP]
have y_nonneg : 0 ≤ y := by linarith
[GOAL]
x✝¹ y✝ a : ℝ
ha : 0 < a
x : ℝ
hex : exp (1 / a) ≤ x
y : ℝ
x✝ : exp (1 / a) ≤ y
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
x_nonneg : 0 ≤ x
⊢ 0 ≤ y
[PROOFSTEP]
linarith
[GOAL]
x✝¹ y✝ a : ℝ
ha : 0 < a
x : ℝ
hex : exp (1 / a) ≤ x
y : ℝ
x✝ : exp (1 / a) ≤ y
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
x_nonneg : 0 ≤ x
y_nonneg : 0 ≤ y
⊢ log y / y ^ a ≤ log x / x ^ a
[PROOFSTEP]
nth_rw 1 [← rpow_one y]
[GOAL]
x✝¹ y✝ a : ℝ
ha : 0 < a
x : ℝ
hex : exp (1 / a) ≤ x
y : ℝ
x✝ : exp (1 / a) ≤ y
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
x_nonneg : 0 ≤ x
y_nonneg : 0 ≤ y
⊢ log (y ^ 1) / y ^ a ≤ log x / x ^ a
[PROOFSTEP]
nth_rw 1 [← rpow_one x]
[GOAL]
x✝¹ y✝ a : ℝ
ha : 0 < a
x : ℝ
hex : exp (1 / a) ≤ x
y : ℝ
x✝ : exp (1 / a) ≤ y
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
x_nonneg : 0 ≤ x
y_nonneg : 0 ≤ y
⊢ log (y ^ 1) / y ^ a ≤ log (x ^ 1) / x ^ a
[PROOFSTEP]
rw [← div_self (ne_of_lt ha).symm, div_eq_mul_one_div a a, rpow_mul y_nonneg, rpow_mul x_nonneg,
  log_rpow (rpow_pos_of_pos y_pos a), log_rpow (rpow_pos_of_pos x_pos a), mul_div_assoc, mul_div_assoc,
  mul_le_mul_left (one_div_pos.mpr ha)]
[GOAL]
x✝¹ y✝ a : ℝ
ha : 0 < a
x : ℝ
hex : exp (1 / a) ≤ x
y : ℝ
x✝ : exp (1 / a) ≤ y
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
x_nonneg : 0 ≤ x
y_nonneg : 0 ≤ y
⊢ log (y ^ a) / y ^ a ≤ log (x ^ a) / x ^ a
[PROOFSTEP]
refine' log_div_self_antitoneOn _ _ _
[GOAL]
case refine'_1
x✝¹ y✝ a : ℝ
ha : 0 < a
x : ℝ
hex : exp (1 / a) ≤ x
y : ℝ
x✝ : exp (1 / a) ≤ y
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
x_nonneg : 0 ≤ x
y_nonneg : 0 ≤ y
⊢ x ^ a ∈ {x | exp 1 ≤ x}
[PROOFSTEP]
simp only [Set.mem_setOf_eq]
[GOAL]
case refine'_1
x✝¹ y✝ a : ℝ
ha : 0 < a
x : ℝ
hex : exp (1 / a) ≤ x
y : ℝ
x✝ : exp (1 / a) ≤ y
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
x_nonneg : 0 ≤ x
y_nonneg : 0 ≤ y
⊢ exp 1 ≤ x ^ a
[PROOFSTEP]
convert rpow_le_rpow _ hex (le_of_lt ha) using 1
[GOAL]
case h.e'_3
x✝¹ y✝ a : ℝ
ha : 0 < a
x : ℝ
hex : exp (1 / a) ≤ x
y : ℝ
x✝ : exp (1 / a) ≤ y
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
x_nonneg : 0 ≤ x
y_nonneg : 0 ≤ y
⊢ exp 1 = exp (1 / a) ^ a
case refine'_1
x✝¹ y✝ a : ℝ
ha : 0 < a
x : ℝ
hex : exp (1 / a) ≤ x
y : ℝ
x✝ : exp (1 / a) ≤ y
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
x_nonneg : 0 ≤ x
y_nonneg : 0 ≤ y
⊢ 0 ≤ exp (1 / a)
[PROOFSTEP]
rw [← exp_mul]
[GOAL]
case h.e'_3
x✝¹ y✝ a : ℝ
ha : 0 < a
x : ℝ
hex : exp (1 / a) ≤ x
y : ℝ
x✝ : exp (1 / a) ≤ y
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
x_nonneg : 0 ≤ x
y_nonneg : 0 ≤ y
⊢ exp 1 = exp (1 / a * a)
case refine'_1
x✝¹ y✝ a : ℝ
ha : 0 < a
x : ℝ
hex : exp (1 / a) ≤ x
y : ℝ
x✝ : exp (1 / a) ≤ y
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
x_nonneg : 0 ≤ x
y_nonneg : 0 ≤ y
⊢ 0 ≤ exp (1 / a)
[PROOFSTEP]
simp only [Real.exp_eq_exp]
[GOAL]
case h.e'_3
x✝¹ y✝ a : ℝ
ha : 0 < a
x : ℝ
hex : exp (1 / a) ≤ x
y : ℝ
x✝ : exp (1 / a) ≤ y
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
x_nonneg : 0 ≤ x
y_nonneg : 0 ≤ y
⊢ 1 = 1 / a * a
case refine'_1
x✝¹ y✝ a : ℝ
ha : 0 < a
x : ℝ
hex : exp (1 / a) ≤ x
y : ℝ
x✝ : exp (1 / a) ≤ y
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
x_nonneg : 0 ≤ x
y_nonneg : 0 ≤ y
⊢ 0 ≤ exp (1 / a)
[PROOFSTEP]
field_simp [(ne_of_lt ha).symm]
[GOAL]
case refine'_1
x✝¹ y✝ a : ℝ
ha : 0 < a
x : ℝ
hex : exp (1 / a) ≤ x
y : ℝ
x✝ : exp (1 / a) ≤ y
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
x_nonneg : 0 ≤ x
y_nonneg : 0 ≤ y
⊢ 0 ≤ exp (1 / a)
[PROOFSTEP]
exact le_of_lt (exp_pos (1 / a))
[GOAL]
case refine'_2
x✝¹ y✝ a : ℝ
ha : 0 < a
x : ℝ
hex : exp (1 / a) ≤ x
y : ℝ
x✝ : exp (1 / a) ≤ y
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
x_nonneg : 0 ≤ x
y_nonneg : 0 ≤ y
⊢ y ^ a ∈ {x | exp 1 ≤ x}
[PROOFSTEP]
simp only [Set.mem_setOf_eq]
[GOAL]
case refine'_2
x✝¹ y✝ a : ℝ
ha : 0 < a
x : ℝ
hex : exp (1 / a) ≤ x
y : ℝ
x✝ : exp (1 / a) ≤ y
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
x_nonneg : 0 ≤ x
y_nonneg : 0 ≤ y
⊢ exp 1 ≤ y ^ a
[PROOFSTEP]
convert rpow_le_rpow _ (_root_.trans hex hxy) (le_of_lt ha) using 1
[GOAL]
case h.e'_3
x✝¹ y✝ a : ℝ
ha : 0 < a
x : ℝ
hex : exp (1 / a) ≤ x
y : ℝ
x✝ : exp (1 / a) ≤ y
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
x_nonneg : 0 ≤ x
y_nonneg : 0 ≤ y
⊢ exp 1 = exp (1 / a) ^ a
case refine'_2
x✝¹ y✝ a : ℝ
ha : 0 < a
x : ℝ
hex : exp (1 / a) ≤ x
y : ℝ
x✝ : exp (1 / a) ≤ y
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
x_nonneg : 0 ≤ x
y_nonneg : 0 ≤ y
⊢ 0 ≤ exp (1 / a)
[PROOFSTEP]
rw [← exp_mul]
[GOAL]
case h.e'_3
x✝¹ y✝ a : ℝ
ha : 0 < a
x : ℝ
hex : exp (1 / a) ≤ x
y : ℝ
x✝ : exp (1 / a) ≤ y
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
x_nonneg : 0 ≤ x
y_nonneg : 0 ≤ y
⊢ exp 1 = exp (1 / a * a)
case refine'_2
x✝¹ y✝ a : ℝ
ha : 0 < a
x : ℝ
hex : exp (1 / a) ≤ x
y : ℝ
x✝ : exp (1 / a) ≤ y
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
x_nonneg : 0 ≤ x
y_nonneg : 0 ≤ y
⊢ 0 ≤ exp (1 / a)
[PROOFSTEP]
simp only [Real.exp_eq_exp]
[GOAL]
case h.e'_3
x✝¹ y✝ a : ℝ
ha : 0 < a
x : ℝ
hex : exp (1 / a) ≤ x
y : ℝ
x✝ : exp (1 / a) ≤ y
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
x_nonneg : 0 ≤ x
y_nonneg : 0 ≤ y
⊢ 1 = 1 / a * a
case refine'_2
x✝¹ y✝ a : ℝ
ha : 0 < a
x : ℝ
hex : exp (1 / a) ≤ x
y : ℝ
x✝ : exp (1 / a) ≤ y
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
x_nonneg : 0 ≤ x
y_nonneg : 0 ≤ y
⊢ 0 ≤ exp (1 / a)
[PROOFSTEP]
field_simp [(ne_of_lt ha).symm]
[GOAL]
case refine'_2
x✝¹ y✝ a : ℝ
ha : 0 < a
x : ℝ
hex : exp (1 / a) ≤ x
y : ℝ
x✝ : exp (1 / a) ≤ y
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
x_nonneg : 0 ≤ x
y_nonneg : 0 ≤ y
⊢ 0 ≤ exp (1 / a)
[PROOFSTEP]
exact le_of_lt (exp_pos (1 / a))
[GOAL]
case refine'_3
x✝¹ y✝ a : ℝ
ha : 0 < a
x : ℝ
hex : exp (1 / a) ≤ x
y : ℝ
x✝ : exp (1 / a) ≤ y
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
x_nonneg : 0 ≤ x
y_nonneg : 0 ≤ y
⊢ x ^ a ≤ y ^ a
[PROOFSTEP]
exact rpow_le_rpow x_nonneg hxy (le_of_lt ha)
[GOAL]
x y : ℝ
⊢ AntitoneOn (fun x => log x / sqrt x) {x | exp 2 ≤ x}
[PROOFSTEP]
simp_rw [sqrt_eq_rpow]
[GOAL]
x y : ℝ
⊢ AntitoneOn (fun x => log x / x ^ (1 / 2)) {x | exp 2 ≤ x}
[PROOFSTEP]
convert @log_div_self_rpow_antitoneOn (1 / 2) (by norm_num)
[GOAL]
x y : ℝ
⊢ 0 < 1 / 2
[PROOFSTEP]
norm_num
[GOAL]
case h.e'_6.h.e'_2.h.h.e'_3.h.e'_1
x y x✝ : ℝ
⊢ 2 = 1 / (1 / 2)
[PROOFSTEP]
norm_num


[GOAL]
⊢ stirlingSeq 0 = 0
[PROOFSTEP]
rw [stirlingSeq, cast_zero, mul_zero, Real.sqrt_zero, zero_mul, div_zero]
[GOAL]
⊢ stirlingSeq 1 = exp 1 / Real.sqrt 2
[PROOFSTEP]
rw [stirlingSeq, pow_one, factorial_one, cast_one, mul_one, mul_one_div, one_div_div]
[GOAL]
n : ℕ
⊢ Real.log (stirlingSeq (succ n)) =
    Real.log ↑(succ n)! - 1 / 2 * Real.log (2 * ↑(succ n)) - ↑(succ n) * Real.log (↑(succ n) / exp 1)
[PROOFSTEP]
rw [stirlingSeq, log_div, log_mul, sqrt_eq_rpow, log_rpow, Real.log_pow, tsub_tsub]
[GOAL]
case hx
n : ℕ
⊢ 0 < 2 * ↑(succ n)
[PROOFSTEP]
positivity
[GOAL]
case hx
n : ℕ
⊢ Real.sqrt (2 * ↑(succ n)) ≠ 0
[PROOFSTEP]
positivity
[GOAL]
case hy
n : ℕ
⊢ (↑(succ n) / exp 1) ^ succ n ≠ 0
[PROOFSTEP]
positivity
[GOAL]
case hx
n : ℕ
⊢ ↑(succ n)! ≠ 0
[PROOFSTEP]
positivity
[GOAL]
case hy
n : ℕ
⊢ Real.sqrt (2 * ↑(succ n)) * (↑(succ n) / exp 1) ^ succ n ≠ 0
[PROOFSTEP]
positivity
[GOAL]
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))))
[PROOFSTEP]
change HasSum ((fun b : ℕ => (1 : ℝ) / ((2 : ℝ) * b + (1 : ℝ)) * (((1 : ℝ) / (2 * m.succ + 1)) ^ 2) ^ b) ∘ succ) _
[GOAL]
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))))
[PROOFSTEP]
refine'
  (hasSum_nat_add_iff (a := _ - _)
        -- Porting note: must give implicit arguments (f :=
        (fun b : ℕ => ↑1 / (↑2 * b + ↑1) * (((1 : ℝ) / (2 * m.succ + 1)) ^ 2) ^ b)) 1).mpr
    _
[GOAL]
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)
[PROOFSTEP]
convert (hasSum_log_one_add_inv <| cast_pos.mpr (succ_pos m)).mul_left ((m.succ : ℝ) + 1 / 2) using 1
[GOAL]
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))
[PROOFSTEP]
ext k
[GOAL]
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))
[PROOFSTEP]
rw [← pow_mul, pow_add]
[GOAL]
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))
[PROOFSTEP]
push_cast
[GOAL]
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))
[PROOFSTEP]
have : 2 * (k : ℝ) + 1 ≠ 0 := by norm_cast; exact succ_ne_zero (2 * k)
[GOAL]
m k : ℕ
⊢ 2 * ↑k + 1 ≠ 0
[PROOFSTEP]
norm_cast
[GOAL]
m k : ℕ
⊢ ¬2 * k + 1 = 0
[PROOFSTEP]
exact succ_ne_zero (2 * k)
[GOAL]
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))
[PROOFSTEP]
have : 2 * ((m : ℝ) + 1) + 1 ≠ 0 := by norm_cast; exact succ_ne_zero (2 * m.succ)
[GOAL]
m k : ℕ
this : 2 * ↑k + 1 ≠ 0
⊢ 2 * (↑m + 1) + 1 ≠ 0
[PROOFSTEP]
norm_cast
[GOAL]
m k : ℕ
this : 2 * ↑k + 1 ≠ 0
⊢ ¬2 * (m + 1) + 1 = 0
[PROOFSTEP]
exact succ_ne_zero (2 * m.succ)
[GOAL]
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))
[PROOFSTEP]
field_simp
[GOAL]
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))
[PROOFSTEP]
ring
[GOAL]
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))⁻¹)
[PROOFSTEP]
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]
[GOAL]
m : ℕ
⊢ ∀ (x : ℝ), x ≠ 0 → 1 + x⁻¹ = (x + 1) / x
[PROOFSTEP]
intro x hx
[GOAL]
m : ℕ
x : ℝ
hx : x ≠ 0
⊢ 1 + x⁻¹ = (x + 1) / x
[PROOFSTEP]
rw [_root_.add_div, div_self hx, inv_eq_one_div]
[GOAL]
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))⁻¹)
[PROOFSTEP]
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]
[GOAL]
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))
[PROOFSTEP]
ring
[GOAL]
n m : ℕ
⊢ 0 ≤ 1 / (2 * ↑(succ m) + 1) * ((1 / (2 * ↑(succ n) + 1)) ^ 2) ^ succ m
[PROOFSTEP]
positivity
[GOAL]
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)
[PROOFSTEP]
have h_nonneg : ↑0 ≤ ((1 : ℝ) / (2 * n.succ + 1)) ^ 2 := sq_nonneg _
[GOAL]
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)
[PROOFSTEP]
have g :
  HasSum (fun k : ℕ => (((1 : ℝ) / (2 * n.succ + 1)) ^ 2) ^ k.succ)
    (((1 : ℝ) / (2 * n.succ + 1)) ^ 2 / (↑1 - ((1 : ℝ) / (2 * n.succ + 1)) ^ 2)) :=
  by
  have := (hasSum_geometric_of_lt_1 h_nonneg ?_).mul_left (((1 : ℝ) / (2 * n.succ + 1)) ^ 2)
  · simp_rw [← _root_.pow_succ] at this
    exact this
  rw [one_div, inv_pow]
  exact inv_lt_one (one_lt_pow ((lt_add_iff_pos_left 1).mpr <| by positivity) two_ne_zero)
[GOAL]
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))
[PROOFSTEP]
have := (hasSum_geometric_of_lt_1 h_nonneg ?_).mul_left (((1 : ℝ) / (2 * n.succ + 1)) ^ 2)
[GOAL]
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))
[PROOFSTEP]
simp_rw [← _root_.pow_succ] at this
[GOAL]
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))
[PROOFSTEP]
exact this
[GOAL]
case refine_1
n : ℕ
h_nonneg : 0 ≤ (1 / (2 * ↑(succ n) + 1)) ^ 2
⊢ (1 / (2 * ↑(succ n) + 1)) ^ 2 < 1
[PROOFSTEP]
rw [one_div, inv_pow]
[GOAL]
case refine_1
n : ℕ
h_nonneg : 0 ≤ (1 / (2 * ↑(succ n) + 1)) ^ 2
⊢ ((2 * ↑(succ n) + 1) ^ 2)⁻¹ < 1
[PROOFSTEP]
exact inv_lt_one (one_lt_pow ((lt_add_iff_pos_left 1).mpr <| by positivity) two_ne_zero)
[GOAL]
n : ℕ
h_nonneg : 0 ≤ (1 / (2 * ↑(succ n) + 1)) ^ 2
⊢ 0 < 2 * ↑(succ n)
[PROOFSTEP]
positivity
[GOAL]
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)
[PROOFSTEP]
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)
[GOAL]
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
[PROOFSTEP]
refine' fun k => mul_le_of_le_one_left (pow_nonneg h_nonneg k.succ) _
[GOAL]
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
[PROOFSTEP]
rw [one_div]
[GOAL]
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
[PROOFSTEP]
exact inv_le_one (le_add_of_nonneg_left <| by positivity)
[GOAL]
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)
[PROOFSTEP]
positivity
[GOAL]
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)
[PROOFSTEP]
exact hasSum_le hab (log_stirlingSeq_diff_hasSum n) g
[GOAL]
n : ℕ
⊢ Real.log (stirlingSeq (succ n)) - Real.log (stirlingSeq (succ (succ n))) ≤ 1 / (4 * ↑(succ n) ^ 2)
[PROOFSTEP]
have h₁ : ↑0 < ↑4 * ((n : ℝ) + 1) ^ 2 := by positivity
[GOAL]
n : ℕ
⊢ 0 < 4 * (↑n + 1) ^ 2
[PROOFSTEP]
positivity
[GOAL]
n : ℕ
h₁ : 0 < 4 * (↑n + 1) ^ 2
⊢ Real.log (stirlingSeq (succ n)) - Real.log (stirlingSeq (succ (succ n))) ≤ 1 / (4 * ↑(succ n) ^ 2)
[PROOFSTEP]
have h₃ : ↑0 < (2 * ((n : ℝ) + 1) + 1) ^ 2 := by positivity
[GOAL]
n : ℕ
h₁ : 0 < 4 * (↑n + 1) ^ 2
⊢ 0 < (2 * (↑n + 1) + 1) ^ 2
[PROOFSTEP]
positivity
[GOAL]
n : ℕ
h₁ : 0 < 4 * (↑n + 1) ^ 2
h₃ : 0 < (2 * (↑n + 1) + 1) ^ 2
⊢ Real.log (stirlingSeq (succ n)) - Real.log (stirlingSeq (succ (succ n))) ≤ 1 / (4 * ↑(succ n) ^ 2)
[PROOFSTEP]
have h₂ : ↑0 < ↑1 - (1 / (2 * ((n : ℝ) + 1) + 1)) ^ 2 :=
  by
  rw [← mul_lt_mul_right h₃]
  have H : ↑0 < (2 * ((n : ℝ) + 1) + 1) ^ 2 - 1 := by nlinarith [@cast_nonneg ℝ _ n]
  convert H using 1 <;> field_simp [h₃.ne']
[GOAL]
n : ℕ
h₁ : 0 < 4 * (↑n + 1) ^ 2
h₃ : 0 < (2 * (↑n + 1) + 1) ^ 2
⊢ 0 < 1 - (1 / (2 * (↑n + 1) + 1)) ^ 2
[PROOFSTEP]
rw [← mul_lt_mul_right h₃]
[GOAL]
n : ℕ
h₁ : 0 < 4 * (↑n + 1) ^ 2
h₃ : 0 < (2 * (↑n + 1) + 1) ^ 2
⊢ 0 * (2 * (↑n + 1) + 1) ^ 2 < (1 - (1 / (2 * (↑n + 1) + 1)) ^ 2) * (2 * (↑n + 1) + 1) ^ 2
[PROOFSTEP]
have H : ↑0 < (2 * ((n : ℝ) + 1) + 1) ^ 2 - 1 := by nlinarith [@cast_nonneg ℝ _ n]
[GOAL]
n : ℕ
h₁ : 0 < 4 * (↑n + 1) ^ 2
h₃ : 0 < (2 * (↑n + 1) + 1) ^ 2
⊢ 0 < (2 * (↑n + 1) + 1) ^ 2 - 1
[PROOFSTEP]
nlinarith [@cast_nonneg ℝ _ n]
[GOAL]
n : ℕ
h₁ : 0 < 4 * (↑n + 1) ^ 2
h₃ : 0 < (2 * (↑n + 1) + 1) ^ 2
H : 0 < (2 * (↑n + 1) + 1) ^ 2 - 1
⊢ 0 * (2 * (↑n + 1) + 1) ^ 2 < (1 - (1 / (2 * (↑n + 1) + 1)) ^ 2) * (2 * (↑n + 1) + 1) ^ 2
[PROOFSTEP]
convert H using 1
[GOAL]
case h.e'_3
n : ℕ
h₁ : 0 < 4 * (↑n + 1) ^ 2
h₃ : 0 < (2 * (↑n + 1) + 1) ^ 2
H : 0 < (2 * (↑n + 1) + 1) ^ 2 - 1
⊢ 0 * (2 * (↑n + 1) + 1) ^ 2 = 0
[PROOFSTEP]
field_simp [h₃.ne']
[GOAL]
case h.e'_4
n : ℕ
h₁ : 0 < 4 * (↑n + 1) ^ 2
h₃ : 0 < (2 * (↑n + 1) + 1) ^ 2
H : 0 < (2 * (↑n + 1) + 1) ^ 2 - 1
⊢ (1 - (1 / (2 * (↑n + 1) + 1)) ^ 2) * (2 * (↑n + 1) + 1) ^ 2 = (2 * (↑n + 1) + 1) ^ 2 - 1
[PROOFSTEP]
field_simp [h₃.ne']
[GOAL]
n : ℕ
h₁ : 0 < 4 * (↑n + 1) ^ 2
h₃ : 0 < (2 * (↑n + 1) + 1) ^ 2
h₂ : 0 < 1 - (1 / (2 * (↑n + 1) + 1)) ^ 2
⊢ Real.log (stirlingSeq (succ n)) - Real.log (stirlingSeq (succ (succ n))) ≤ 1 / (4 * ↑(succ n) ^ 2)
[PROOFSTEP]
refine' (log_stirlingSeq_diff_le_geo_sum n).trans _
[GOAL]
n : ℕ
h₁ : 0 < 4 * (↑n + 1) ^ 2
h₃ : 0 < (2 * (↑n + 1) + 1) ^ 2
h₂ : 0 < 1 - (1 / (2 * (↑n + 1) + 1)) ^ 2
⊢ (1 / (2 * ↑(succ n) + 1)) ^ 2 / (1 - (1 / (2 * ↑(succ n) + 1)) ^ 2) ≤ 1 / (4 * ↑(succ n) ^ 2)
[PROOFSTEP]
push_cast
[GOAL]
n : ℕ
h₁ : 0 < 4 * (↑n + 1) ^ 2
h₃ : 0 < (2 * (↑n + 1) + 1) ^ 2
h₂ : 0 < 1 - (1 / (2 * (↑n + 1) + 1)) ^ 2
⊢ (1 / (2 * (↑n + 1) + 1)) ^ 2 / (1 - (1 / (2 * (↑n + 1) + 1)) ^ 2) ≤ 1 / (4 * (↑n + 1) ^ 2)
[PROOFSTEP]
rw [div_le_div_iff h₂ h₁]
[GOAL]
n : ℕ
h₁ : 0 < 4 * (↑n + 1) ^ 2
h₃ : 0 < (2 * (↑n + 1) + 1) ^ 2
h₂ : 0 < 1 - (1 / (2 * (↑n + 1) + 1)) ^ 2
⊢ (1 / (2 * (↑n + 1) + 1)) ^ 2 * (4 * (↑n + 1) ^ 2) ≤ 1 * (1 - (1 / (2 * (↑n + 1) + 1)) ^ 2)
[PROOFSTEP]
field_simp [h₃.ne']
[GOAL]
n : ℕ
h₁ : 0 < 4 * (↑n + 1) ^ 2
h₃ : 0 < (2 * (↑n + 1) + 1) ^ 2
h₂ : 0 < 1 - (1 / (2 * (↑n + 1) + 1)) ^ 2
⊢ 4 * (↑n + 1) ^ 2 / (2 * (↑n + 1) + 1) ^ 2 ≤ ((2 * (↑n + 1) + 1) ^ 2 - 1) / (2 * (↑n + 1) + 1) ^ 2
[PROOFSTEP]
rw [div_le_div_right h₃]
[GOAL]
n : ℕ
h₁ : 0 < 4 * (↑n + 1) ^ 2
h₃ : 0 < (2 * (↑n + 1) + 1) ^ 2
h₂ : 0 < 1 - (1 / (2 * (↑n + 1) + 1)) ^ 2
⊢ 4 * (↑n + 1) ^ 2 ≤ (2 * (↑n + 1) + 1) ^ 2 - 1
[PROOFSTEP]
ring_nf
[GOAL]
n : ℕ
h₁ : 0 < 4 * (↑n + 1) ^ 2
h₃ : 0 < (2 * (↑n + 1) + 1) ^ 2
h₂ : 0 < 1 - (1 / (2 * (↑n + 1) + 1)) ^ 2
⊢ 4 + ↑n * 8 + ↑n ^ 2 * 4 ≤ 8 + ↑n * 12 + ↑n ^ 2 * 4
[PROOFSTEP]
norm_cast
[GOAL]
n : ℕ
h₁ : 0 < 4 * (↑n + 1) ^ 2
h₃ : 0 < (2 * (↑n + 1) + 1) ^ 2
h₂ : 0 < 1 - (1 / (2 * (↑n + 1) + 1)) ^ 2
⊢ 4 + n * 8 + n ^ 2 * 4 ≤ 8 + n * 12 + n ^ 2 * 4
[PROOFSTEP]
linarith
[GOAL]
⊢ ∃ c, ∀ (n : ℕ), Real.log (stirlingSeq 1) - Real.log (stirlingSeq (succ n)) ≤ c
[PROOFSTEP]
let d := ∑' k : ℕ, ↑1 / (k.succ : ℝ) ^ 2
[GOAL]
d : ℝ := ∑' (k : ℕ), 1 / ↑(succ k) ^ 2
⊢ ∃ c, ∀ (n : ℕ), Real.log (stirlingSeq 1) - Real.log (stirlingSeq (succ n)) ≤ c
[PROOFSTEP]
use(1 / 4 * d : ℝ)
[GOAL]
case h
d : ℝ := ∑' (k : ℕ), 1 / ↑(succ k) ^ 2
⊢ ∀ (n : ℕ), Real.log (stirlingSeq 1) - Real.log (stirlingSeq (succ n)) ≤ 1 / 4 * d
[PROOFSTEP]
let log_stirlingSeq' : ℕ → ℝ := fun k => log (stirlingSeq k.succ)
[GOAL]
case h
d : ℝ := ∑' (k : ℕ), 1 / ↑(succ k) ^ 2
log_stirlingSeq' : ℕ → ℝ := fun k => Real.log (stirlingSeq (succ k))
⊢ ∀ (n : ℕ), Real.log (stirlingSeq 1) - Real.log (stirlingSeq (succ n)) ≤ 1 / 4 * d
[PROOFSTEP]
intro n
[GOAL]
case h
d : ℝ := ∑' (k : ℕ), 1 / ↑(succ k) ^ 2
log_stirlingSeq' : ℕ → ℝ := fun k => Real.log (stirlingSeq (succ k))
n : ℕ
⊢ Real.log (stirlingSeq 1) - Real.log (stirlingSeq (succ n)) ≤ 1 / 4 * d
[PROOFSTEP]
have h₁ : ∀ k, log_stirlingSeq' k - log_stirlingSeq' (k + 1) ≤ ↑1 / ↑4 * (↑1 / (k.succ : ℝ) ^ 2) := by intro k;
  convert log_stirlingSeq_sub_log_stirlingSeq_succ k using 1; field_simp
[GOAL]
d : ℝ := ∑' (k : ℕ), 1 / ↑(succ k) ^ 2
log_stirlingSeq' : ℕ → ℝ := fun k => Real.log (stirlingSeq (succ k))
n : ℕ
⊢ ∀ (k : ℕ), log_stirlingSeq' k - log_stirlingSeq' (k + 1) ≤ 1 / 4 * (1 / ↑(succ k) ^ 2)
[PROOFSTEP]
intro k
[GOAL]
d : ℝ := ∑' (k : ℕ), 1 / ↑(succ k) ^ 2
log_stirlingSeq' : ℕ → ℝ := fun k => Real.log (stirlingSeq (succ k))
n k : ℕ
⊢ log_stirlingSeq' k - log_stirlingSeq' (k + 1) ≤ 1 / 4 * (1 / ↑(succ k) ^ 2)
[PROOFSTEP]
convert log_stirlingSeq_sub_log_stirlingSeq_succ k using 1
[GOAL]
case h.e'_4
d : ℝ := ∑' (k : ℕ), 1 / ↑(succ k) ^ 2
log_stirlingSeq' : ℕ → ℝ := fun k => Real.log (stirlingSeq (succ k))
n k : ℕ
⊢ 1 / 4 * (1 / ↑(succ k) ^ 2) = 1 / (4 * ↑(succ k) ^ 2)
[PROOFSTEP]
field_simp
[GOAL]
case h
d : ℝ := ∑' (k : ℕ), 1 / ↑(succ k) ^ 2
log_stirlingSeq' : ℕ → ℝ := fun k => Real.log (stirlingSeq (succ k))
n : ℕ
h₁ : ∀ (k : ℕ), log_stirlingSeq' k - log_stirlingSeq' (k + 1) ≤ 1 / 4 * (1 / ↑(succ k) ^ 2)
⊢ Real.log (stirlingSeq 1) - Real.log (stirlingSeq (succ n)) ≤ 1 / 4 * d
[PROOFSTEP]
have h₂ : (∑ k : ℕ in range n, ↑1 / (k.succ : ℝ) ^ 2) ≤ d :=
  by
  have := (summable_nat_add_iff 1).mpr <| Real.summable_one_div_nat_pow.mpr one_lt_two
  simp only [rpow_nat_cast] at this
  exact sum_le_tsum (range n) (fun k _ => by positivity) this
[GOAL]
d : ℝ := ∑' (k : ℕ), 1 / ↑(succ k) ^ 2
log_stirlingSeq' : ℕ → ℝ := fun k => Real.log (stirlingSeq (succ k))
n : ℕ
h₁ : ∀ (k : ℕ), log_stirlingSeq' k - log_stirlingSeq' (k + 1) ≤ 1 / 4 * (1 / ↑(succ k) ^ 2)
⊢ ∑ k in range n, 1 / ↑(succ k) ^ 2 ≤ d
[PROOFSTEP]
have := (summable_nat_add_iff 1).mpr <| Real.summable_one_div_nat_pow.mpr one_lt_two
[GOAL]
d : ℝ := ∑' (k : ℕ), 1 / ↑(succ k) ^ 2
log_stirlingSeq' : ℕ → ℝ := fun k => Real.log (stirlingSeq (succ k))
n : ℕ
h₁ : ∀ (k : ℕ), log_stirlingSeq' k - log_stirlingSeq' (k + 1) ≤ 1 / 4 * (1 / ↑(succ k) ^ 2)
this : Summable fun n => 1 / ↑(n + 1) ^ 2
⊢ ∑ k in range n, 1 / ↑(succ k) ^ 2 ≤ d
[PROOFSTEP]
simp only [rpow_nat_cast] at this
[GOAL]
d : ℝ := ∑' (k : ℕ), 1 / ↑(succ k) ^ 2
log_stirlingSeq' : ℕ → ℝ := fun k => Real.log (stirlingSeq (succ k))
n : ℕ
h₁ : ∀ (k : ℕ), log_stirlingSeq' k - log_stirlingSeq' (k + 1) ≤ 1 / 4 * (1 / ↑(succ k) ^ 2)
this : Summable fun n => 1 / ↑(n + 1) ^ 2
⊢ ∑ k in range n, 1 / ↑(succ k) ^ 2 ≤ d
[PROOFSTEP]
exact sum_le_tsum (range n) (fun k _ => by positivity) this
[GOAL]
d : ℝ := ∑' (k : ℕ), 1 / ↑(succ k) ^ 2
log_stirlingSeq' : ℕ → ℝ := fun k => Real.log (stirlingSeq (succ k))
n : ℕ
h₁ : ∀ (k : ℕ), log_stirlingSeq' k - log_stirlingSeq' (k + 1) ≤ 1 / 4 * (1 / ↑(succ k) ^ 2)
this : Summable fun n => 1 / ↑(n + 1) ^ 2
k : ℕ
x✝ : ¬k ∈ range n
⊢ 0 ≤ 1 / ↑(succ k) ^ 2
[PROOFSTEP]
positivity
[GOAL]
case h
d : ℝ := ∑' (k : ℕ), 1 / ↑(succ k) ^ 2
log_stirlingSeq' : ℕ → ℝ := fun k => Real.log (stirlingSeq (succ k))
n : ℕ
h₁ : ∀ (k : ℕ), log_stirlingSeq' k - log_stirlingSeq' (k + 1) ≤ 1 / 4 * (1 / ↑(succ k) ^ 2)
h₂ : ∑ k in range n, 1 / ↑(succ k) ^ 2 ≤ d
⊢ Real.log (stirlingSeq 1) - Real.log (stirlingSeq (succ n)) ≤ 1 / 4 * d
[PROOFSTEP]
calc
  log (stirlingSeq 1) - log (stirlingSeq n.succ) = log_stirlingSeq' 0 - log_stirlingSeq' n := rfl
  _ = ∑ k in range n, (log_stirlingSeq' k - log_stirlingSeq' (k + 1)) := by rw [← sum_range_sub' log_stirlingSeq' n]
  _ ≤ ∑ k in range n, ↑1 / ↑4 * (↑1 / ↑(k.succ) ^ 2) := (sum_le_sum fun k _ => h₁ k)
  _ = ↑1 / ↑4 * ∑ k in range n, ↑1 / ↑(k.succ) ^ 2 := by rw [mul_sum]
  _ ≤ 1 / 4 * d := mul_le_mul_of_nonneg_left h₂ <| by positivity
[GOAL]
d : ℝ := ∑' (k : ℕ), 1 / ↑(succ k) ^ 2
log_stirlingSeq' : ℕ → ℝ := fun k => Real.log (stirlingSeq (succ k))
n : ℕ
h₁ : ∀ (k : ℕ), log_stirlingSeq' k - log_stirlingSeq' (k + 1) ≤ 1 / 4 * (1 / ↑(succ k) ^ 2)
h₂ : ∑ k in range n, 1 / ↑(succ k) ^ 2 ≤ d
⊢ log_stirlingSeq' 0 - log_stirlingSeq' n = ∑ k in range n, (log_stirlingSeq' k - log_stirlingSeq' (k + 1))
[PROOFSTEP]
rw [← sum_range_sub' log_stirlingSeq' n]
[GOAL]
d : ℝ := ∑' (k : ℕ), 1 / ↑(succ k) ^ 2
log_stirlingSeq' : ℕ → ℝ := fun k => Real.log (stirlingSeq (succ k))
n : ℕ
h₁ : ∀ (k : ℕ), log_stirlingSeq' k - log_stirlingSeq' (k + 1) ≤ 1 / 4 * (1 / ↑(succ k) ^ 2)
h₂ : ∑ k in range n, 1 / ↑(succ k) ^ 2 ≤ d
⊢ ∑ k in range n, 1 / 4 * (1 / ↑(succ k) ^ 2) = 1 / 4 * ∑ k in range n, 1 / ↑(succ k) ^ 2
[PROOFSTEP]
rw [mul_sum]
[GOAL]
d : ℝ := ∑' (k : ℕ), 1 / ↑(succ k) ^ 2
log_stirlingSeq' : ℕ → ℝ := fun k => Real.log (stirlingSeq (succ k))
n : ℕ
h₁ : ∀ (k : ℕ), log_stirlingSeq' k - log_stirlingSeq' (k + 1) ≤ 1 / 4 * (1 / ↑(succ k) ^ 2)
h₂ : ∑ k in range n, 1 / ↑(succ k) ^ 2 ≤ d
⊢ 0 ≤ 1 / 4
[PROOFSTEP]
positivity
[GOAL]
⊢ ∃ c, ∀ (n : ℕ), c ≤ Real.log (stirlingSeq (succ n))
[PROOFSTEP]
obtain ⟨d, h⟩ := log_stirlingSeq_bounded_aux
[GOAL]
case intro
d : ℝ
h : ∀ (n : ℕ), Real.log (stirlingSeq 1) - Real.log (stirlingSeq (succ n)) ≤ d
⊢ ∃ c, ∀ (n : ℕ), c ≤ Real.log (stirlingSeq (succ n))
[PROOFSTEP]
exact ⟨log (stirlingSeq 1) - d, fun n => sub_le_comm.mp (h n)⟩
[GOAL]
n : ℕ
⊢ 0 < stirlingSeq (succ n)
[PROOFSTEP]
unfold stirlingSeq
[GOAL]
n : ℕ
⊢ 0 < ↑(succ n)! / (Real.sqrt (2 * ↑(succ n)) * (↑(succ n) / exp 1) ^ succ n)
[PROOFSTEP]
positivity
[GOAL]
⊢ ∃ a, 0 < a ∧ ∀ (n : ℕ), a ≤ stirlingSeq (succ n)
[PROOFSTEP]
cases' log_stirlingSeq_bounded_by_constant with c h
[GOAL]
case intro
c : ℝ
h : ∀ (n : ℕ), c ≤ Real.log (stirlingSeq (succ n))
⊢ ∃ a, 0 < a ∧ ∀ (n : ℕ), a ≤ stirlingSeq (succ n)
[PROOFSTEP]
refine' ⟨exp c, exp_pos _, fun n => _⟩
[GOAL]
case intro
c : ℝ
h : ∀ (n : ℕ), c ≤ Real.log (stirlingSeq (succ n))
n : ℕ
⊢ exp c ≤ stirlingSeq (succ n)
[PROOFSTEP]
rw [← le_log_iff_exp_le (stirlingSeq'_pos n)]
[GOAL]
case intro
c : ℝ
h : ∀ (n : ℕ), c ≤ Real.log (stirlingSeq (succ n))
n : ℕ
⊢ c ≤ Real.log (stirlingSeq (succ n))
[PROOFSTEP]
exact h n
[GOAL]
⊢ ∃ a, 0 < a ∧ Tendsto stirlingSeq atTop (𝓝 a)
[PROOFSTEP]
obtain ⟨x, x_pos, hx⟩ := stirlingSeq'_bounded_by_pos_constant
[GOAL]
case intro.intro
x : ℝ
x_pos : 0 < x
hx : ∀ (n : ℕ), x ≤ stirlingSeq (succ n)
⊢ ∃ a, 0 < a ∧ Tendsto stirlingSeq atTop (𝓝 a)
[PROOFSTEP]
have hx' : x ∈ lowerBounds (Set.range (stirlingSeq ∘ succ)) := by simpa [lowerBounds] using hx
[GOAL]
x : ℝ
x_pos : 0 < x
hx : ∀ (n : ℕ), x ≤ stirlingSeq (succ n)
⊢ x ∈ lowerBounds (Set.range (stirlingSeq ∘ succ))
[PROOFSTEP]
simpa [lowerBounds] using hx
[GOAL]
case intro.intro
x : ℝ
x_pos : 0 < x
hx : ∀ (n : ℕ), x ≤ stirlingSeq (succ n)
hx' : x ∈ lowerBounds (Set.range (stirlingSeq ∘ succ))
⊢ ∃ a, 0 < a ∧ Tendsto stirlingSeq atTop (𝓝 a)
[PROOFSTEP]
refine' ⟨_, lt_of_lt_of_le x_pos (le_csInf (Set.range_nonempty _) hx'), _⟩
[GOAL]
case intro.intro
x : ℝ
x_pos : 0 < x
hx : ∀ (n : ℕ), x ≤ stirlingSeq (succ n)
hx' : x ∈ lowerBounds (Set.range (stirlingSeq ∘ succ))
⊢ Tendsto stirlingSeq atTop (𝓝 (sInf (Set.range (stirlingSeq ∘ succ))))
[PROOFSTEP]
rw [← Filter.tendsto_add_atTop_iff_nat 1]
[GOAL]
case intro.intro
x : ℝ
x_pos : 0 < x
hx : ∀ (n : ℕ), x ≤ stirlingSeq (succ n)
hx' : x ∈ lowerBounds (Set.range (stirlingSeq ∘ succ))
⊢ Tendsto (fun n => stirlingSeq (n + 1)) atTop (𝓝 (sInf (Set.range (stirlingSeq ∘ succ))))
[PROOFSTEP]
exact tendsto_atTop_ciInf stirlingSeq'_antitone ⟨x, hx'⟩
[GOAL]
⊢ Tendsto (fun n => ↑n / (2 * ↑n + 1)) atTop (𝓝 (1 / 2))
[PROOFSTEP]
conv =>
  congr
  ·skip
  ·skip
  rw [one_div, ← add_zero (2 : ℝ)]
[GOAL]
| Tendsto (fun n => ↑n / (2 * ↑n + 1)) atTop (𝓝 (1 / 2))
[PROOFSTEP]
  congr
  ·skip
  ·skip
  rw [one_div, ← add_zero (2 : ℝ)]
[GOAL]
| Tendsto (fun n => ↑n / (2 * ↑n + 1)) atTop (𝓝 (1 / 2))
[PROOFSTEP]
  congr
  ·skip
  ·skip
  rw [one_div, ← add_zero (2 : ℝ)]
[GOAL]
| Tendsto (fun n => ↑n / (2 * ↑n + 1)) atTop (𝓝 (1 / 2))
[PROOFSTEP]
congr
[GOAL]
case f
| fun n => ↑n / (2 * ↑n + 1)
case l₁
| atTop
case l₂ | 𝓝 (1 / 2)
[PROOFSTEP]
·skip
[GOAL]
case f
| fun n => ↑n / (2 * ↑n + 1)
[PROOFSTEP]
skip
[GOAL]
case f
| fun n => ↑n / (2 * ↑n + 1)
[PROOFSTEP]
skip
[GOAL]
case f
| fun n => ↑n / (2 * ↑n + 1)
[PROOFSTEP]
skip
[GOAL]
case l₁
| atTop
case l₂ | 𝓝 (1 / 2)
[PROOFSTEP]
·skip
[GOAL]
case l₁
| atTop
[PROOFSTEP]
skip
[GOAL]
case l₁
| atTop
[PROOFSTEP]
skip
[GOAL]
case l₁
| atTop
[PROOFSTEP]
skip
[GOAL]
case l₂
| 𝓝 (1 / 2)
[PROOFSTEP]
rw [one_div, ← add_zero (2 : ℝ)]
[GOAL]
⊢ Tendsto (fun n => ↑n / (2 * ↑n + 1)) atTop (𝓝 (2 + 0)⁻¹)
[PROOFSTEP]
refine'
  (((tendsto_const_div_atTop_nhds_0_nat 1).const_add (2 : ℝ)).inv₀ ((add_zero (2 : ℝ)).symm ▸ two_ne_zero)).congr'
    (eventually_atTop.mpr ⟨1, fun n hn => _⟩)
[GOAL]
n : ℕ
hn : n ≥ 1
⊢ (2 + 1 / ↑n)⁻¹ = (fun n => ↑n / (2 * ↑n + 1)) n
[PROOFSTEP]
rw [add_div' (1 : ℝ) 2 n (cast_ne_zero.mpr (one_le_iff_ne_zero.mp hn)), inv_div]
[GOAL]
n : ℕ
hn : n ≠ 0
⊢ stirlingSeq n ^ 4 / stirlingSeq (2 * n) ^ 2 * (↑n / (2 * ↑n + 1)) = Wallis.W n
[PROOFSTEP]
have : 4 = 2 * 2 := by rfl
[GOAL]
n : ℕ
hn : n ≠ 0
⊢ 4 = 2 * 2
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
hn : n ≠ 0
this : 4 = 2 * 2
⊢ stirlingSeq n ^ 4 / stirlingSeq (2 * n) ^ 2 * (↑n / (2 * ↑n + 1)) = Wallis.W n
[PROOFSTEP]
rw [stirlingSeq, this, pow_mul, stirlingSeq, Wallis.W_eq_factorial_ratio]
[GOAL]
n : ℕ
hn : n ≠ 0
this : 4 = 2 * 2
⊢ ((↑n ! / (Real.sqrt (2 * ↑n) * (↑n / exp 1) ^ n)) ^ 2) ^ 2 /
        (↑(2 * n)! / (Real.sqrt (2 * ↑(2 * n)) * (↑(2 * n) / exp 1) ^ (2 * n))) ^ 2 *
      (↑n / (2 * ↑n + 1)) =
    ↑(2 ^ (4 * n)) * ↑(n ! ^ 4) / (↑((2 * n)! ^ 2) * (2 * ↑n + 1))
[PROOFSTEP]
simp_rw [div_pow, mul_pow]
[GOAL]
n : ℕ
hn : n ≠ 0
this : 4 = 2 * 2
⊢ (↑n ! ^ 2) ^ 2 / ((Real.sqrt (2 * ↑n) ^ 2) ^ 2 * ((↑n ^ n / exp 1 ^ n) ^ 2) ^ 2) /
        (↑(2 * n)! ^ 2 / (Real.sqrt (2 * ↑(2 * n)) ^ 2 * (↑(2 * n) ^ (2 * n) / exp 1 ^ (2 * n)) ^ 2)) *
      (↑n / (2 * ↑n + 1)) =
    ↑(2 ^ (4 * n)) * ↑(n ! ^ 4) / (↑((2 * n)! ^ 2) * (2 * ↑n + 1))
[PROOFSTEP]
rw [sq_sqrt, sq_sqrt]
[GOAL]
n : ℕ
hn : n ≠ 0
this : 4 = 2 * 2
⊢ (↑n ! ^ 2) ^ 2 / ((2 * ↑n) ^ 2 * ((↑n ^ n / exp 1 ^ n) ^ 2) ^ 2) /
        (↑(2 * n)! ^ 2 / (2 * ↑(2 * n) * (↑(2 * n) ^ (2 * n) / exp 1 ^ (2 * n)) ^ 2)) *
      (↑n / (2 * ↑n + 1)) =
    ↑(2 ^ (4 * n)) * ↑(n ! ^ 4) / (↑((2 * n)! ^ 2) * (2 * ↑n + 1))
n : ℕ
hn : n ≠ 0
this : 4 = 2 * 2
⊢ 0 ≤ 2 * ↑(2 * n)
n : ℕ hn : n ≠ 0 this : 4 = 2 * 2 ⊢ 0 ≤ 2 * ↑n
[PROOFSTEP]
any_goals positivity
[GOAL]
n : ℕ
hn : n ≠ 0
this : 4 = 2 * 2
⊢ (↑n ! ^ 2) ^ 2 / ((2 * ↑n) ^ 2 * ((↑n ^ n / exp 1 ^ n) ^ 2) ^ 2) /
        (↑(2 * n)! ^ 2 / (2 * ↑(2 * n) * (↑(2 * n) ^ (2 * n) / exp 1 ^ (2 * n)) ^ 2)) *
      (↑n / (2 * ↑n + 1)) =
    ↑(2 ^ (4 * n)) * ↑(n ! ^ 4) / (↑((2 * n)! ^ 2) * (2 * ↑n + 1))
[PROOFSTEP]
positivity
[GOAL]
n : ℕ
hn : n ≠ 0
this : 4 = 2 * 2
⊢ 0 ≤ 2 * ↑(2 * n)
[PROOFSTEP]
positivity
[GOAL]
n : ℕ
hn : n ≠ 0
this : 4 = 2 * 2
⊢ 0 ≤ 2 * ↑n
[PROOFSTEP]
positivity
[GOAL]
n : ℕ
hn : n ≠ 0
this : 4 = 2 * 2
⊢ (↑n ! ^ 2) ^ 2 / ((2 * ↑n) ^ 2 * ((↑n ^ n / exp 1 ^ n) ^ 2) ^ 2) /
        (↑(2 * n)! ^ 2 / (2 * ↑(2 * n) * (↑(2 * n) ^ (2 * n) / exp 1 ^ (2 * n)) ^ 2)) *
      (↑n / (2 * ↑n + 1)) =
    ↑(2 ^ (4 * n)) * ↑(n ! ^ 4) / (↑((2 * n)! ^ 2) * (2 * ↑n + 1))
[PROOFSTEP]
have : (n : ℝ) ≠ 0 := cast_ne_zero.mpr hn
[GOAL]
n : ℕ
hn : n ≠ 0
this✝ : 4 = 2 * 2
this : ↑n ≠ 0
⊢ (↑n ! ^ 2) ^ 2 / ((2 * ↑n) ^ 2 * ((↑n ^ n / exp 1 ^ n) ^ 2) ^ 2) /
        (↑(2 * n)! ^ 2 / (2 * ↑(2 * n) * (↑(2 * n) ^ (2 * n) / exp 1 ^ (2 * n)) ^ 2)) *
      (↑n / (2 * ↑n + 1)) =
    ↑(2 ^ (4 * n)) * ↑(n ! ^ 4) / (↑((2 * n)! ^ 2) * (2 * ↑n + 1))
[PROOFSTEP]
have : exp 1 ≠ 0 := exp_ne_zero 1
[GOAL]
n : ℕ
hn : n ≠ 0
this✝¹ : 4 = 2 * 2
this✝ : ↑n ≠ 0
this : exp 1 ≠ 0
⊢ (↑n ! ^ 2) ^ 2 / ((2 * ↑n) ^ 2 * ((↑n ^ n / exp 1 ^ n) ^ 2) ^ 2) /
        (↑(2 * n)! ^ 2 / (2 * ↑(2 * n) * (↑(2 * n) ^ (2 * n) / exp 1 ^ (2 * n)) ^ 2)) *
      (↑n / (2 * ↑n + 1)) =
    ↑(2 ^ (4 * n)) * ↑(n ! ^ 4) / (↑((2 * n)! ^ 2) * (2 * ↑n + 1))
[PROOFSTEP]
have : ((2 * n)! : ℝ) ≠ 0 := cast_ne_zero.mpr (factorial_ne_zero (2 * n))
[GOAL]
n : ℕ
hn : n ≠ 0
this✝² : 4 = 2 * 2
this✝¹ : ↑n ≠ 0
this✝ : exp 1 ≠ 0
this : ↑(2 * n)! ≠ 0
⊢ (↑n ! ^ 2) ^ 2 / ((2 * ↑n) ^ 2 * ((↑n ^ n / exp 1 ^ n) ^ 2) ^ 2) /
        (↑(2 * n)! ^ 2 / (2 * ↑(2 * n) * (↑(2 * n) ^ (2 * n) / exp 1 ^ (2 * n)) ^ 2)) *
      (↑n / (2 * ↑n + 1)) =
    ↑(2 ^ (4 * n)) * ↑(n ! ^ 4) / (↑((2 * n)! ^ 2) * (2 * ↑n + 1))
[PROOFSTEP]
have : 2 * (n : ℝ) + 1 ≠ 0 := by norm_cast; exact succ_ne_zero (2 * n)
[GOAL]
n : ℕ
hn : n ≠ 0
this✝² : 4 = 2 * 2
this✝¹ : ↑n ≠ 0
this✝ : exp 1 ≠ 0
this : ↑(2 * n)! ≠ 0
⊢ 2 * ↑n + 1 ≠ 0
[PROOFSTEP]
norm_cast
[GOAL]
n : ℕ
hn : n ≠ 0
this✝² : 4 = 2 * 2
this✝¹ : ↑n ≠ 0
this✝ : exp 1 ≠ 0
this : ↑(2 * n)! ≠ 0
⊢ ¬2 * n + 1 = 0
[PROOFSTEP]
exact succ_ne_zero (2 * n)
[GOAL]
n : ℕ
hn : n ≠ 0
this✝³ : 4 = 2 * 2
this✝² : ↑n ≠ 0
this✝¹ : exp 1 ≠ 0
this✝ : ↑(2 * n)! ≠ 0
this : 2 * ↑n + 1 ≠ 0
⊢ (↑n ! ^ 2) ^ 2 / ((2 * ↑n) ^ 2 * ((↑n ^ n / exp 1 ^ n) ^ 2) ^ 2) /
        (↑(2 * n)! ^ 2 / (2 * ↑(2 * n) * (↑(2 * n) ^ (2 * n) / exp 1 ^ (2 * n)) ^ 2)) *
      (↑n / (2 * ↑n + 1)) =
    ↑(2 ^ (4 * n)) * ↑(n ! ^ 4) / (↑((2 * n)! ^ 2) * (2 * ↑n + 1))
[PROOFSTEP]
field_simp
[GOAL]
n : ℕ
hn : n ≠ 0
this✝³ : 4 = 2 * 2
this✝² : ↑n ≠ 0
this✝¹ : exp 1 ≠ 0
this✝ : ↑(2 * n)! ≠ 0
this : 2 * ↑n + 1 ≠ 0
⊢ (↑n ! ^ 2) ^ 2 * ((exp 1 ^ n) ^ 2) ^ 2 * (2 * (2 * ↑n) * ((2 * ↑n) ^ (2 * n)) ^ 2) * ↑n *
      (↑(2 * n)! ^ 2 * (2 * ↑n + 1)) =
    2 ^ (4 * n) * ↑n ! ^ 4 *
      ((2 * ↑n) ^ 2 * ((↑n ^ n) ^ 2) ^ 2 * (↑(2 * n)! ^ 2 * (exp 1 ^ (2 * n)) ^ 2) * (2 * ↑n + 1))
[PROOFSTEP]
simp only [mul_pow, mul_comm 2 n, mul_comm 4 n, pow_mul]
[GOAL]
n : ℕ
hn : n ≠ 0
this✝³ : 4 = 2 * 2
this✝² : ↑n ≠ 0
this✝¹ : exp 1 ≠ 0
this✝ : ↑(2 * n)! ≠ 0
this : 2 * ↑n + 1 ≠ 0
⊢ (↑n ! ^ 2) ^ 2 * ((exp 1 ^ n) ^ 2) ^ 2 * (2 * (2 * ↑n) * (((2 ^ n) ^ 2) ^ 2 * ((↑n ^ n) ^ 2) ^ 2)) * ↑n *
      (↑(n * 2)! ^ 2 * (2 * ↑n + 1)) =
    (2 ^ n) ^ 4 * ↑n ! ^ 4 *
      (2 ^ 2 * ↑n ^ 2 * ((↑n ^ n) ^ 2) ^ 2 * (↑(n * 2)! ^ 2 * ((exp 1 ^ n) ^ 2) ^ 2) * (2 * ↑n + 1))
[PROOFSTEP]
ring
[GOAL]
a : ℝ
hane : a ≠ 0
ha : Tendsto stirlingSeq atTop (𝓝 a)
⊢ Tendsto Wallis.W atTop (𝓝 (a ^ 2 / 2))
[PROOFSTEP]
refine'
  Tendsto.congr'
    (eventually_atTop.mpr ⟨1, fun n hn => stirlingSeq_pow_four_div_stirlingSeq_pow_two_eq n (one_le_iff_ne_zero.mp hn)⟩)
    _
[GOAL]
a : ℝ
hane : a ≠ 0
ha : Tendsto stirlingSeq atTop (𝓝 a)
⊢ Tendsto (fun n => stirlingSeq n ^ 4 / stirlingSeq (2 * n) ^ 2 * (↑n / (2 * ↑n + 1))) atTop (𝓝 (a ^ 2 / 2))
[PROOFSTEP]
have h : a ^ 2 / ↑2 = a ^ 4 / a ^ 2 * (1 / 2) :=
  by
  rw [mul_one_div, ← mul_one_div (a ^ 4) (a ^ 2), one_div, ← pow_sub_of_lt a]
  norm_num
[GOAL]
a : ℝ
hane : a ≠ 0
ha : Tendsto stirlingSeq atTop (𝓝 a)
⊢ a ^ 2 / 2 = a ^ 4 / a ^ 2 * (1 / 2)
[PROOFSTEP]
rw [mul_one_div, ← mul_one_div (a ^ 4) (a ^ 2), one_div, ← pow_sub_of_lt a]
[GOAL]
a : ℝ
hane : a ≠ 0
ha : Tendsto stirlingSeq atTop (𝓝 a)
⊢ 2 < 4
[PROOFSTEP]
norm_num
[GOAL]
a : ℝ
hane : a ≠ 0
ha : Tendsto stirlingSeq atTop (𝓝 a)
h : a ^ 2 / 2 = a ^ 4 / a ^ 2 * (1 / 2)
⊢ Tendsto (fun n => stirlingSeq n ^ 4 / stirlingSeq (2 * n) ^ 2 * (↑n / (2 * ↑n + 1))) atTop (𝓝 (a ^ 2 / 2))
[PROOFSTEP]
rw [h]
[GOAL]
a : ℝ
hane : a ≠ 0
ha : Tendsto stirlingSeq atTop (𝓝 a)
h : a ^ 2 / 2 = a ^ 4 / a ^ 2 * (1 / 2)
⊢ Tendsto (fun n => stirlingSeq n ^ 4 / stirlingSeq (2 * n) ^ 2 * (↑n / (2 * ↑n + 1))) atTop
    (𝓝 (a ^ 4 / a ^ 2 * (1 / 2)))
[PROOFSTEP]
exact
  ((ha.pow 4).div ((ha.comp (tendsto_id.const_mul_atTop' two_pos)).pow 2) (pow_ne_zero 2 hane)).mul
    tendsto_self_div_two_mul_self_add_one
[GOAL]
⊢ Tendsto (fun n => stirlingSeq n) atTop (𝓝 (Real.sqrt π))
[PROOFSTEP]
obtain ⟨a, hapos, halimit⟩ := stirlingSeq_has_pos_limit_a
[GOAL]
case intro.intro
a : ℝ
hapos : 0 < a
halimit : Tendsto stirlingSeq atTop (𝓝 a)
⊢ Tendsto (fun n => stirlingSeq n) atTop (𝓝 (Real.sqrt π))
[PROOFSTEP]
have hπ : π / 2 = a ^ 2 / 2 :=
  tendsto_nhds_unique Wallis.tendsto_W_nhds_pi_div_two (second_wallis_limit a hapos.ne' halimit)
[GOAL]
case intro.intro
a : ℝ
hapos : 0 < a
halimit : Tendsto stirlingSeq atTop (𝓝 a)
hπ : π / ↑2 = a ^ 2 / 2
⊢ Tendsto (fun n => stirlingSeq n) atTop (𝓝 (Real.sqrt π))
[PROOFSTEP]
rwa [(div_left_inj' (two_ne_zero' ℝ)).mp hπ, sqrt_sq hapos.le]