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