[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]
