Theorem: centralBinom_limit (ExponentialRamsey/Prereq/Mathlib/Analysis/SpecialFunctions/ExplicitStirling.lean)

State before:
⊢ Tendsto (fun n => ↑(centralBinom n) * Real.sqrt ↑n / 4 ^ n) atTop (𝓝 (Real.sqrt π)⁻¹)
Tactic:
have := Real.pi_pos
State after:
this : 0 < π
⊢ Tendsto (fun n => ↑(centralBinom n) * Real.sqrt ↑n / 4 ^ n) atTop (𝓝 (Real.sqrt π)⁻¹)

State before:
this : 0 < π
⊢ Tendsto (fun n => ↑(centralBinom n) * Real.sqrt ↑n / 4 ^ n) atTop (𝓝 (Real.sqrt π)⁻¹)
Tactic:
have : (sqrt π)⁻¹ = sqrt π / sqrt π ^ 2 := by
  rw [inv_eq_one_div, sq, ← div_div, div_self]
  positivity
State after:
this✝ : 0 < π
this : (Real.sqrt π)⁻¹ = Real.sqrt π / Real.sqrt π ^ 2
⊢ Tendsto (fun n => ↑(centralBinom n) * Real.sqrt ↑n / 4 ^ n) atTop (𝓝 (Real.sqrt π)⁻¹)

State before:
this✝ : 0 < π
this : (Real.sqrt π)⁻¹ = Real.sqrt π / Real.sqrt π ^ 2
⊢ Tendsto (fun n => ↑(centralBinom n) * Real.sqrt ↑n / 4 ^ n) atTop (𝓝 (Real.sqrt π)⁻¹)
Tactic:
rw [this]
State after:
this✝ : 0 < π
this : (Real.sqrt π)⁻¹ = Real.sqrt π / Real.sqrt π ^ 2
⊢ Tendsto (fun n => ↑(centralBinom n) * Real.sqrt ↑n / 4 ^ n) atTop (𝓝 (Real.sqrt π / Real.sqrt π ^ 2))

State before:
this✝ : 0 < π
this : (Real.sqrt π)⁻¹ = Real.sqrt π / Real.sqrt π ^ 2
⊢ Tendsto (fun n => ↑(centralBinom n) * Real.sqrt ↑n / 4 ^ n) atTop (𝓝 (Real.sqrt π / Real.sqrt π ^ 2))
Tactic:
have : Tendsto (fun n => Stirling.stirlingSeq (2 * n)) atTop (𝓝 (sqrt π)) := by
  refine' Tendsto.comp Stirling.tendsto_stirlingSeq_sqrt_pi _
  exact tendsto_id.const_mul_atTop' two_pos
State after:
this✝¹ : 0 < π
this✝ : (Real.sqrt π)⁻¹ = Real.sqrt π / Real.sqrt π ^ 2
this : Tendsto (fun n => Stirling.stirlingSeq (2 * n)) atTop (𝓝 (Real.sqrt π))
⊢ Tendsto (fun n => ↑(centralBinom n) * Real.sqrt ↑n / 4 ^ n) atTop (𝓝 (Real.sqrt π / Real.sqrt π ^ 2))

State before:
this✝¹ : 0 < π
this✝ : (Real.sqrt π)⁻¹ = Real.sqrt π / Real.sqrt π ^ 2
this : Tendsto (fun n => Stirling.stirlingSeq (2 * n)) atTop (𝓝 (Real.sqrt π))
⊢ Tendsto (fun n => ↑(centralBinom n) * Real.sqrt ↑n / 4 ^ n) atTop (𝓝 (Real.sqrt π / Real.sqrt π ^ 2))
Tactic:
refine' (this.div (Stirling.tendsto_stirlingSeq_sqrt_pi.pow 2) (by positivity)).congr' _
State after:
this✝¹ : 0 < π
this✝ : (Real.sqrt π)⁻¹ = Real.sqrt π / Real.sqrt π ^ 2
this : Tendsto (fun n => Stirling.stirlingSeq (2 * n)) atTop (𝓝 (Real.sqrt π))
⊢ ((fun n => Stirling.stirlingSeq (2 * n)) / fun x => Stirling.stirlingSeq x ^ 2) =ᶠ[atTop] fun n =>
    ↑(centralBinom n) * Real.sqrt ↑n / 4 ^ n

State before:
this✝¹ : 0 < π
this✝ : (Real.sqrt π)⁻¹ = Real.sqrt π / Real.sqrt π ^ 2
this : Tendsto (fun n => Stirling.stirlingSeq (2 * n)) atTop (𝓝 (Real.sqrt π))
⊢ ((fun n => Stirling.stirlingSeq (2 * n)) / fun x => Stirling.stirlingSeq x ^ 2) =ᶠ[atTop] fun n =>
    ↑(centralBinom n) * Real.sqrt ↑n / 4 ^ n
Tactic:
filter_upwards [eventually_gt_atTop (0 : ℕ)] with n hn
State after:
case h
this✝¹ : 0 < π
this✝ : (Real.sqrt π)⁻¹ = Real.sqrt π / Real.sqrt π ^ 2
this : Tendsto (fun n => Stirling.stirlingSeq (2 * n)) atTop (𝓝 (Real.sqrt π))
n : ℕ
hn : 0 < n
⊢ ((fun n => Stirling.stirlingSeq (2 * n)) / fun x => Stirling.stirlingSeq x ^ 2) n =
    ↑(centralBinom n) * Real.sqrt ↑n / 4 ^ n

State before:
case h
this✝¹ : 0 < π
this✝ : (Real.sqrt π)⁻¹ = Real.sqrt π / Real.sqrt π ^ 2
this : Tendsto (fun n => Stirling.stirlingSeq (2 * n)) atTop (𝓝 (Real.sqrt π))
n : ℕ
hn : 0 < n
⊢ ((fun n => Stirling.stirlingSeq (2 * n)) / fun x => Stirling.stirlingSeq x ^ 2) n =
    ↑(centralBinom n) * Real.sqrt ↑n / 4 ^ n
Tactic:
dsimp
State after:
case h
this✝¹ : 0 < π
this✝ : (Real.sqrt π)⁻¹ = Real.sqrt π / Real.sqrt π ^ 2
this : Tendsto (fun n => Stirling.stirlingSeq (2 * n)) atTop (𝓝 (Real.sqrt π))
n : ℕ
hn : 0 < n
⊢ Stirling.stirlingSeq (2 * n) / Stirling.stirlingSeq n ^ 2 = ↑(centralBinom n) * Real.sqrt ↑n / 4 ^ n

State before:
case h
this✝¹ : 0 < π
this✝ : (Real.sqrt π)⁻¹ = Real.sqrt π / Real.sqrt π ^ 2
this : Tendsto (fun n => Stirling.stirlingSeq (2 * n)) atTop (𝓝 (Real.sqrt π))
n : ℕ
hn : 0 < n
⊢ Stirling.stirlingSeq (2 * n) / Stirling.stirlingSeq n ^ 2 = ↑(centralBinom n) * Real.sqrt ↑n / 4 ^ n
Tactic:
rw [Stirling.stirlingSeq, Stirling.stirlingSeq, centralBinom, two_mul n, cast_add_choose,
  ←two_mul]
State after:
case h
this✝¹ : 0 < π
this✝ : (Real.sqrt π)⁻¹ = Real.sqrt π / Real.sqrt π ^ 2
this : Tendsto (fun n => Stirling.stirlingSeq (2 * n)) atTop (𝓝 (Real.sqrt π))
n : ℕ
hn : 0 < n
⊢ ↑(2 * n)! / (Real.sqrt (2 * ↑(2 * n)) * (↑(2 * n) / rexp 1) ^ (2 * n)) /
      (↑n ! / (Real.sqrt (2 * ↑n) * (↑n / rexp 1) ^ n)) ^ 2 =
    ↑(2 * n)! / (↑n ! * ↑n !) * Real.sqrt ↑n / 4 ^ n

State before:
case h
this✝¹ : 0 < π
this✝ : (Real.sqrt π)⁻¹ = Real.sqrt π / Real.sqrt π ^ 2
this : Tendsto (fun n => Stirling.stirlingSeq (2 * n)) atTop (𝓝 (Real.sqrt π))
n : ℕ
hn : 0 < n
⊢ ↑(2 * n)! / (Real.sqrt (2 * ↑(2 * n)) * (↑(2 * n) / rexp 1) ^ (2 * n)) /
      (↑n ! / (Real.sqrt (2 * ↑n) * (↑n / rexp 1) ^ n)) ^ 2 =
    ↑(2 * n)! / (↑n ! * ↑n !) * Real.sqrt ↑n / 4 ^ n
Tactic:
field_simp
State after:
case h
this✝¹ : 0 < π
this✝ : (Real.sqrt π)⁻¹ = Real.sqrt π / Real.sqrt π ^ 2
this : Tendsto (fun n => Stirling.stirlingSeq (2 * n)) atTop (𝓝 (Real.sqrt π))
n : ℕ
hn : 0 < n
⊢ ↑(2 * n)! * rexp 1 ^ (2 * n) * (Real.sqrt 2 * Real.sqrt ↑n * ↑n ^ n) ^ 2 * (↑n ! * ↑n ! * 4 ^ n) =
    ↑(2 * n)! * Real.sqrt ↑n *
      (Real.sqrt 2 * (Real.sqrt 2 * Real.sqrt ↑n) * (2 * ↑n) ^ (2 * n) * (↑n ! * rexp 1 ^ n) ^ 2)

State before:
case h
this✝¹ : 0 < π
this✝ : (Real.sqrt π)⁻¹ = Real.sqrt π / Real.sqrt π ^ 2
this : Tendsto (fun n => Stirling.stirlingSeq (2 * n)) atTop (𝓝 (Real.sqrt π))
n : ℕ
hn : 0 < n
⊢ ↑(2 * n)! * rexp 1 ^ (2 * n) * (Real.sqrt 2 * Real.sqrt ↑n * ↑n ^ n) ^ 2 * (↑n ! * ↑n ! * 4 ^ n) =
    ↑(2 * n)! * Real.sqrt ↑n *
      (Real.sqrt 2 * (Real.sqrt 2 * Real.sqrt ↑n) * (2 * ↑n) ^ (2 * n) * (↑n ! * rexp 1 ^ n) ^ 2)
Tactic:
ring_nf
State after:
case h
this✝¹ : 0 < π
this✝ : (Real.sqrt π)⁻¹ = Real.sqrt π / Real.sqrt π ^ 2
this : Tendsto (fun n => Stirling.stirlingSeq (2 * n)) atTop (𝓝 (Real.sqrt π))
n : ℕ
hn : 0 < n
⊢ ↑(n * 2)! * rexp 1 ^ (n * 2) * Real.sqrt 2 ^ 2 * Real.sqrt ↑n ^ 2 * ↑n ^ (n * 2) * ↑n ! ^ 2 * 4 ^ n =
    ↑(n * 2)! * rexp 1 ^ (n * 2) * Real.sqrt 2 ^ 2 * Real.sqrt ↑n ^ 2 * ↑n ^ (n * 2) * ↑n ! ^ 2 * 2 ^ (n * 2)

State before:
case h
this✝¹ : 0 < π
this✝ : (Real.sqrt π)⁻¹ = Real.sqrt π / Real.sqrt π ^ 2
this : Tendsto (fun n => Stirling.stirlingSeq (2 * n)) atTop (𝓝 (Real.sqrt π))
n : ℕ
hn : 0 < n
⊢ ↑(n * 2)! * rexp 1 ^ (n * 2) * Real.sqrt 2 ^ 2 * Real.sqrt ↑n ^ 2 * ↑n ^ (n * 2) * ↑n ! ^ 2 * 4 ^ n =
    ↑(n * 2)! * rexp 1 ^ (n * 2) * Real.sqrt 2 ^ 2 * Real.sqrt ↑n ^ 2 * ↑n ^ (n * 2) * ↑n ! ^ 2 * 2 ^ (n * 2)
Tactic:
rw [mul_comm n 2, pow_mul (2 : ℝ)]
State after:
case h
this✝¹ : 0 < π
this✝ : (Real.sqrt π)⁻¹ = Real.sqrt π / Real.sqrt π ^ 2
this : Tendsto (fun n => Stirling.stirlingSeq (2 * n)) atTop (𝓝 (Real.sqrt π))
n : ℕ
hn : 0 < n
⊢ ↑(2 * n)! * rexp 1 ^ (2 * n) * Real.sqrt 2 ^ 2 * Real.sqrt ↑n ^ 2 * ↑n ^ (2 * n) * ↑n ! ^ 2 * 4 ^ n =
    ↑(2 * n)! * rexp 1 ^ (2 * n) * Real.sqrt 2 ^ 2 * Real.sqrt ↑n ^ 2 * ↑n ^ (2 * n) * ↑n ! ^ 2 * (2 ^ 2) ^ n

State before:
case h
this✝¹ : 0 < π
this✝ : (Real.sqrt π)⁻¹ = Real.sqrt π / Real.sqrt π ^ 2
this : Tendsto (fun n => Stirling.stirlingSeq (2 * n)) atTop (𝓝 (Real.sqrt π))
n : ℕ
hn : 0 < n
⊢ ↑(2 * n)! * rexp 1 ^ (2 * n) * Real.sqrt 2 ^ 2 * Real.sqrt ↑n ^ 2 * ↑n ^ (2 * n) * ↑n ! ^ 2 * 4 ^ n =
    ↑(2 * n)! * rexp 1 ^ (2 * n) * Real.sqrt 2 ^ 2 * Real.sqrt ↑n ^ 2 * ↑n ^ (2 * n) * ↑n ! ^ 2 * (2 ^ 2) ^ n
Tactic:
norm_num1
State after:
case h
this✝¹ : 0 < π
this✝ : (Real.sqrt π)⁻¹ = Real.sqrt π / Real.sqrt π ^ 2
this : Tendsto (fun n => Stirling.stirlingSeq (2 * n)) atTop (𝓝 (Real.sqrt π))
n : ℕ
hn : 0 < n
⊢ ↑(2 * n)! * rexp 1 ^ (2 * n) * Real.sqrt 2 ^ 2 * Real.sqrt ↑n ^ 2 * ↑n ^ (2 * n) * ↑n ! ^ 2 * 4 ^ n =
    ↑(2 * n)! * rexp 1 ^ (2 * n) * Real.sqrt 2 ^ 2 * Real.sqrt ↑n ^ 2 * ↑n ^ (2 * n) * ↑n ! ^ 2 * 4 ^ n

State before:
case h
this✝¹ : 0 < π
this✝ : (Real.sqrt π)⁻¹ = Real.sqrt π / Real.sqrt π ^ 2
this : Tendsto (fun n => Stirling.stirlingSeq (2 * n)) atTop (𝓝 (Real.sqrt π))
n : ℕ
hn : 0 < n
⊢ ↑(2 * n)! * rexp 1 ^ (2 * n) * Real.sqrt 2 ^ 2 * Real.sqrt ↑n ^ 2 * ↑n ^ (2 * n) * ↑n ! ^ 2 * 4 ^ n =
    ↑(2 * n)! * rexp 1 ^ (2 * n) * Real.sqrt 2 ^ 2 * Real.sqrt ↑n ^ 2 * ↑n ^ (2 * n) * ↑n ! ^ 2 * 4 ^ n
Tactic:
rfl
State after:
no goals

State before:
this : 0 < π
⊢ (Real.sqrt π)⁻¹ = Real.sqrt π / Real.sqrt π ^ 2
Tactic:
rw [inv_eq_one_div, sq, ← div_div, div_self]
State after:
this : 0 < π
⊢ Real.sqrt π ≠ 0

State before:
this : 0 < π
⊢ Real.sqrt π ≠ 0
Tactic:
positivity
State after:
no goals

State before:
this✝ : 0 < π
this : (Real.sqrt π)⁻¹ = Real.sqrt π / Real.sqrt π ^ 2
⊢ Tendsto (fun n => Stirling.stirlingSeq (2 * n)) atTop (𝓝 (Real.sqrt π))
Tactic:
refine' Tendsto.comp Stirling.tendsto_stirlingSeq_sqrt_pi _
State after:
this✝ : 0 < π
this : (Real.sqrt π)⁻¹ = Real.sqrt π / Real.sqrt π ^ 2
⊢ Tendsto (fun n => 2 * n) atTop atTop

State before:
this✝ : 0 < π
this : (Real.sqrt π)⁻¹ = Real.sqrt π / Real.sqrt π ^ 2
⊢ Tendsto (fun n => 2 * n) atTop atTop
Tactic:
exact tendsto_id.const_mul_atTop' two_pos
State after:
no goals

State before:
this✝¹ : 0 < π
this✝ : (Real.sqrt π)⁻¹ = Real.sqrt π / Real.sqrt π ^ 2
this : Tendsto (fun n => Stirling.stirlingSeq (2 * n)) atTop (𝓝 (Real.sqrt π))
⊢ Real.sqrt π ^ 2 ≠ 0
Tactic:
positivity
State after:
no goals