internlm/Lean-Github huggingface dataset:
Theorem: centralBinomialLower_monotone
Proof state before:
case d0
n : ℕ
⊢ 0 < centralBinom n
Tactic:
exact centralBinom_pos _
Proof state after:
no goals
Theorem: centralBinomialLower_monotone
Proof state before:
n : ℕ
⊢ 0 < 4
Tactic:
positivity
Proof state after:
no goals
Theorem: centralBinomialUpper_monotone
Proof state before:
⊢ Antitone centralBinomialUpper
Tactic:
refine' antitone_nat_of_succ_le _
Proof state after:
⊢ ∀ (n : ℕ), centralBinomialUpper (n + 1) ≤ centralBinomialUpper n
Theorem: centralBinomialUpper_monotone
Proof state before:
⊢ ∀ (n : ℕ), centralBinomialUpper (n + 1) ≤ centralBinomialUpper n
Tactic:
intro n
Proof state after:
n : ℕ
⊢ centralBinomialUpper (n + 1) ≤ centralBinomialUpper n
Theorem: centralBinomialUpper_monotone
Proof state before:
n : ℕ
⊢ centralBinomialUpper (n + 1) ≤ centralBinomialUpper n
Tactic:
rw [centralBinomialUpper, centralBinomialUpper, _root_.pow_succ, ← div_div]
Proof state after:
n : ℕ
⊢ ↑(centralBinom (n + 1)) * Real.sqrt (↑(n + 1) + 1 / 3) / 4 / 4 ^ n ≤
    ↑(centralBinom n) * Real.sqrt (↑n + 1 / 3) / 4 ^ n
Theorem: centralBinomialUpper_monotone
Proof state before:
n : ℕ
⊢ ↑(centralBinom (n + 1)) * Real.sqrt (↑(n + 1) + 1 / 3) / 4 / 4 ^ n ≤
    ↑(centralBinom n) * Real.sqrt (↑n + 1 / 3) / 4 ^ n
Tactic:
refine' div_le_div_of_le (by positivity) _
Proof state after:
n : ℕ
⊢ ↑(centralBinom (n + 1)) * Real.sqrt (↑(n + 1) + 1 / 3) / 4 ≤ ↑(centralBinom n) * Real.sqrt (↑n + 1 / 3)
Theorem: centralBinomialUpper_monotone
Proof state before:
n : ℕ
⊢ ↑(centralBinom (n + 1)) * Real.sqrt (↑(n + 1) + 1 / 3) / 4 ≤ ↑(centralBinom n) * Real.sqrt (↑n + 1 / 3)
Tactic:
rw [div_le_iff, mul_assoc, mul_comm _ (_ * _), ← div_le_div_iff, mul_comm, mul_div_assoc,
  centralBinom_ratio, Nat.cast_add_one]
Proof state after:
n : ℕ
⊢ 4 * ((↑n + 1 / 2) / (↑n + 1)) ≤ 4 * (Real.sqrt (↑n + 1 / 3) / Real.sqrt (↑n + 1 + 1 / 3))

case b0
n : ℕ
⊢ 0 < ↑(centralBinom n)

case d0
n : ℕ
⊢ 0 < Real.sqrt (↑(n + 1) + 1 / 3)

n : ℕ
⊢ 0 < 4
Theorem: centralBinomialUpper_monotone
Proof state before:
n : ℕ
⊢ 4 * ((↑n + 1 / 2) / (↑n + 1)) ≤ 4 * (Real.sqrt (↑n + 1 / 3) / Real.sqrt (↑n + 1 + 1 / 3))

case b0
n : ℕ
⊢ 0 < ↑(centralBinom n)

case d0
n : ℕ
⊢ 0 < Real.sqrt (↑(n + 1) + 1 / 3)

n : ℕ
⊢ 0 < 4
Tactic:
refine' mul_le_mul_of_nonneg_left (upper_monotone_aux _) (by positivity)
Proof state after:
case b0
n : ℕ
⊢ 0 < ↑(centralBinom n)

case d0
n : ℕ
⊢ 0 < Real.sqrt (↑(n + 1) + 1 / 3)

n : ℕ
⊢ 0 < 4
Theorem: centralBinomialUpper_monotone
Proof state before:
n : ℕ
⊢ 0 ≤ 4 ^ n
Tactic:
positivity
Proof state after:
no goals
Theorem: centralBinomialUpper_monotone
Proof state before:
n : ℕ
⊢ 0 ≤ 4
Tactic:
positivity
Proof state after:
no goals
Theorem: centralBinomialUpper_monotone
Proof state before:
case b0
n : ℕ
⊢ 0 < ↑(centralBinom n)
Tactic:
rw [Nat.cast_pos]
Proof state after:
case b0
n : ℕ
⊢ 0 < centralBinom n
Theorem: centralBinomialUpper_monotone
Proof state before:
case b0
n : ℕ
⊢ 0 < centralBinom n
Tactic:
exact centralBinom_pos _
Proof state after:
no goals
Theorem: centralBinomialUpper_monotone
Proof state before:
case d0
n : ℕ
⊢ 0 < Real.sqrt (↑(n + 1) + 1 / 3)
Tactic:
positivity
Proof state after:
no goals
Theorem: centralBinomialUpper_monotone
Proof state before:
n : ℕ
⊢ 0 < 4
Tactic:
positivity
Proof state after:
no goals
Theorem: centralBinom_limit
Proof state before:
⊢ Tendsto (fun n => ↑(centralBinom n) * Real.sqrt ↑n / 4 ^ n) atTop (𝓝 (Real.sqrt π)⁻¹)
Tactic:
have := Real.pi_pos
Proof state after:
this : 0 < π
⊢ Tendsto (fun n => ↑(centralBinom n) * Real.sqrt ↑n / 4 ^ n) atTop (𝓝 (Real.sqrt π)⁻¹)
Theorem: centralBinom_limit
Proof 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
Proof 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 π)⁻¹)
Theorem: centralBinom_limit
Proof 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]
Proof 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))
Theorem: centralBinom_limit
Proof 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
Proof 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))
Theorem: centralBinom_limit
Proof 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' _
Proof 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
Theorem: centralBinom_limit
Proof 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
Proof 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
Theorem: centralBinom_limit
Proof 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
Proof 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
Theorem: centralBinom_limit
Proof 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]
Proof 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
Theorem: centralBinom_limit
Proof 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
Proof 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)
Theorem: centralBinom_limit
Proof 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
Proof 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)
Theorem: centralBinom_limit
Proof 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 : ℝ)]
Proof 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
Theorem: centralBinom_limit
Proof 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
Proof 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
Theorem: centralBinom_limit
Proof 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
Proof state after:
no goals
Theorem: centralBinom_limit
Proof state before:
this : 0 < π
⊢ (Real.sqrt π)⁻¹ = Real.sqrt π / Real.sqrt π ^ 2
Tactic:
rw [inv_eq_one_div, sq, ← div_div, div_self]
Proof state after:
this : 0 < π
⊢ Real.sqrt π ≠ 0
Theorem: centralBinom_limit
Proof state before:
this : 0 < π
⊢ Real.sqrt π ≠ 0
Tactic:
positivity
Proof state after:
no goals
Theorem: centralBinom_limit
Proof 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 _
Proof state after:
this✝ : 0 < π
this : (Real.sqrt π)⁻¹ = Real.sqrt π / Real.sqrt π ^ 2
⊢ Tendsto (fun n => 2 * n) atTop atTop
Theorem: centralBinom_limit
Proof 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
Proof state after:
no goals
Theorem: centralBinom_limit
Proof 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
Proof state after:
no goals
Theorem: centralBinomialUpper_limit
Proof state before:
⊢ Tendsto centralBinomialUpper atTop (𝓝 (Real.sqrt π)⁻¹)
Tactic:
have : (sqrt π)⁻¹ = (sqrt π)⁻¹ / Real.sqrt 1 := by rw [Real.sqrt_one, div_one]
Proof state after:
this : (Real.sqrt π)⁻¹ = (Real.sqrt π)⁻¹ / Real.sqrt 1
⊢ Tendsto centralBinomialUpper atTop (𝓝 (Real.sqrt π)⁻¹)
Theorem: centralBinomialUpper_limit
Proof state before:
this : (Real.sqrt π)⁻¹ = (Real.sqrt π)⁻¹ / Real.sqrt 1
⊢ Tendsto centralBinomialUpper atTop (𝓝 (Real.sqrt π)⁻¹)
Tactic:
have h : Real.sqrt 1 ≠ 0 := sqrt_ne_zero'.2 zero_lt_one
Proof state after:
this : (Real.sqrt π)⁻¹ = (Real.sqrt π)⁻¹ / Real.sqrt 1
h : Real.sqrt 1 ≠ 0
⊢ Tendsto centralBinomialUpper atTop (𝓝 (Real.sqrt π)⁻¹)
Theorem: centralBinomialUpper_limit
Proof state before:
this : (Real.sqrt π)⁻¹ = (Real.sqrt π)⁻¹ / Real.sqrt 1
h : Real.sqrt 1 ≠ 0
⊢ Tendsto centralBinomialUpper atTop (𝓝 (Real.sqrt π)⁻¹)
Tactic:
rw [this]
Proof state after:
this : (Real.sqrt π)⁻¹ = (Real.sqrt π)⁻¹ / Real.sqrt 1
h : Real.sqrt 1 ≠ 0
⊢ Tendsto centralBinomialUpper atTop (𝓝 ((Real.sqrt π)⁻¹ / Real.sqrt 1))
Theorem: centralBinomialUpper_limit
Proof state before:
this : (Real.sqrt π)⁻¹ = (Real.sqrt π)⁻¹ / Real.sqrt 1
h : Real.sqrt 1 ≠ 0
⊢ Tendsto centralBinomialUpper atTop (𝓝 ((Real.sqrt π)⁻¹ / Real.sqrt 1))
Tactic:
refine' (centralBinom_limit.div (tendsto_coe_nat_div_add_atTop (1 / 3 : ℝ)).sqrt h).congr' _
Proof state after:
this : (Real.sqrt π)⁻¹ = (Real.sqrt π)⁻¹ / Real.sqrt 1
h : Real.sqrt 1 ≠ 0
⊢ ((fun n => ↑(centralBinom n) * Real.sqrt ↑n / 4 ^ n) / fun x => Real.sqrt (↑x / (↑x + 1 / 3))) =ᶠ[atTop]
    centralBinomialUpper
Theorem: centralBinomialUpper_limit
Proof state before:
this : (Real.sqrt π)⁻¹ = (Real.sqrt π)⁻¹ / Real.sqrt 1
h : Real.sqrt 1 ≠ 0
⊢ ((fun n => ↑(centralBinom n) * Real.sqrt ↑n / 4 ^ n) / fun x => Real.sqrt (↑x / (↑x + 1 / 3))) =ᶠ[atTop]
    centralBinomialUpper
Tactic:
filter_upwards [eventually_gt_atTop 0] with n hn
Proof state after:
case h
this : (Real.sqrt π)⁻¹ = (Real.sqrt π)⁻¹ / Real.sqrt 1
h : Real.sqrt 1 ≠ 0
n : ℕ
hn : 0 < n
⊢ ((fun n => ↑(centralBinom n) * Real.sqrt ↑n / 4 ^ n) / fun x => Real.sqrt (↑x / (↑x + 1 / 3))) n =
    centralBinomialUpper n
Theorem: centralBinomialUpper_limit
Proof state before:
case h
this : (Real.sqrt π)⁻¹ = (Real.sqrt π)⁻¹ / Real.sqrt 1
h : Real.sqrt 1 ≠ 0
n : ℕ
hn : 0 < n
⊢ ((fun n => ↑(centralBinom n) * Real.sqrt ↑n / 4 ^ n) / fun x => Real.sqrt (↑x / (↑x + 1 / 3))) n =
    centralBinomialUpper n
Tactic:
dsimp
Proof state after:
case h
this : (Real.sqrt π)⁻¹ = (Real.sqrt π)⁻¹ / Real.sqrt 1
h : Real.sqrt 1 ≠ 0
n : ℕ
hn : 0 < n
⊢ ↑(centralBinom n) * Real.sqrt ↑n / 4 ^ n / Real.sqrt (↑n / (↑n + 1 / 3)) = centralBinomialUpper n
Theorem: centralBinomialUpper_limit
Proof state before:
case h
this : (Real.sqrt π)⁻¹ = (Real.sqrt π)⁻¹ / Real.sqrt 1
h : Real.sqrt 1 ≠ 0
n : ℕ
hn : 0 < n
⊢ ↑(centralBinom n) * Real.sqrt ↑n / 4 ^ n / Real.sqrt (↑n / (↑n + 1 / 3)) = centralBinomialUpper n
Tactic:
rw [sqrt_div (Nat.cast_nonneg _), centralBinomialUpper, div_div, mul_div_assoc',
  div_div_eq_mul_div, mul_right_comm, mul_div_mul_right]
Proof state after:
case h.hc
this : (Real.sqrt π)⁻¹ = (Real.sqrt π)⁻¹ / Real.sqrt 1
h : Real.sqrt 1 ≠ 0
n : ℕ
hn : 0 < n
⊢ Real.sqrt ↑n ≠ 0
Theorem: centralBinomialUpper_limit
Proof state before:
⊢ (Real.sqrt π)⁻¹ = (Real.sqrt π)⁻¹ / Real.sqrt 1
Tactic:
rw [Real.sqrt_one, div_one]
Proof state after:
no goals
Theorem: centralBinomialUpper_limit
Proof state before:
case h.hc
this : (Real.sqrt π)⁻¹ = (Real.sqrt π)⁻¹ / Real.sqrt 1
h : Real.sqrt 1 ≠ 0
n : ℕ
hn : 0 < n
⊢ Real.sqrt ↑n ≠ 0
Tactic:
positivity
Proof state after:
no goals
Theorem: centralBinomialLower_limit
Proof state before:
⊢ Tendsto centralBinomialLower atTop (𝓝 (Real.sqrt π)⁻¹)
Tactic:
have : (sqrt π)⁻¹ = (sqrt π)⁻¹ / Real.sqrt 1 := by rw [Real.sqrt_one, div_one]
Proof state after:
this : (Real.sqrt π)⁻¹ = (Real.sqrt π)⁻¹ / Real.sqrt 1
⊢ Tendsto centralBinomialLower atTop (𝓝 (Real.sqrt π)⁻¹)
Theorem: centralBinomialLower_limit
Proof state before:
this : (Real.sqrt π)⁻¹ = (Real.sqrt π)⁻¹ / Real.sqrt 1
⊢ Tendsto centralBinomialLower atTop (𝓝 (Real.sqrt π)⁻¹)
Tactic:
have h : Real.sqrt 1 ≠ 0 := sqrt_ne_zero'.2 zero_lt_one
Proof state after:
this : (Real.sqrt π)⁻¹ = (Real.sqrt π)⁻¹ / Real.sqrt 1
h : Real.sqrt 1 ≠ 0
⊢ Tendsto centralBinomialLower atTop (𝓝 (Real.sqrt π)⁻¹)
Theorem: centralBinomialLower_limit
Proof state before:
this : (Real.sqrt π)⁻¹ = (Real.sqrt π)⁻¹ / Real.sqrt 1
h : Real.sqrt 1 ≠ 0
⊢ Tendsto centralBinomialLower atTop (𝓝 (Real.sqrt π)⁻¹)
Tactic:
rw [this]
Proof state after:
this : (Real.sqrt π)⁻¹ = (Real.sqrt π)⁻¹ / Real.sqrt 1
h : Real.sqrt 1 ≠ 0
⊢ Tendsto centralBinomialLower atTop (𝓝 ((Real.sqrt π)⁻¹ / Real.sqrt 1))
Theorem: centralBinomialLower_limit
Proof state before:
this : (Real.sqrt π)⁻¹ = (Real.sqrt π)⁻¹ / Real.sqrt 1
h : Real.sqrt 1 ≠ 0
⊢ Tendsto centralBinomialLower atTop (𝓝 ((Real.sqrt π)⁻¹ / Real.sqrt 1))
Tactic:
refine' (centralBinom_limit.div (tendsto_coe_nat_div_add_atTop (1 / 4 : ℝ)).sqrt h).congr' _
Proof state after:
this : (Real.sqrt π)⁻¹ = (Real.sqrt π)⁻¹ / Real.sqrt 1
h : Real.sqrt 1 ≠ 0
⊢ ((fun n => ↑(centralBinom n) * Real.sqrt ↑n / 4 ^ n) / fun x => Real.sqrt (↑x / (↑x + 1 / 4))) =ᶠ[atTop]
    centralBinomialLower
Theorem: centralBinomialLower_limit
Proof state before:
this : (Real.sqrt π)⁻¹ = (Real.sqrt π)⁻¹ / Real.sqrt 1
h : Real.sqrt 1 ≠ 0
⊢ ((fun n => ↑(centralBinom n) * Real.sqrt ↑n / 4 ^ n) / fun x => Real.sqrt (↑x / (↑x + 1 / 4))) =ᶠ[atTop]
    centralBinomialLower
Tactic:
filter_upwards [eventually_gt_atTop 0] with n hn
Proof state after:
case h
this : (Real.sqrt π)⁻¹ = (Real.sqrt π)⁻¹ / Real.sqrt 1
h : Real.sqrt 1 ≠ 0
n : ℕ
hn : 0 < n
⊢ ((fun n => ↑(centralBinom n) * Real.sqrt ↑n / 4 ^ n) / fun x => Real.sqrt (↑x / (↑x + 1 / 4))) n =
    centralBinomialLower n
Theorem: centralBinomialLower_limit
Proof state before:
case h
this : (Real.sqrt π)⁻¹ = (Real.sqrt π)⁻¹ / Real.sqrt 1
h : Real.sqrt 1 ≠ 0
n : ℕ
hn : 0 < n
⊢ ((fun n => ↑(centralBinom n) * Real.sqrt ↑n / 4 ^ n) / fun x => Real.sqrt (↑x / (↑x + 1 / 4))) n =
    centralBinomialLower n
Tactic:
dsimp
Proof state after:
case h
this : (Real.sqrt π)⁻¹ = (Real.sqrt π)⁻¹ / Real.sqrt 1
h : Real.sqrt 1 ≠ 0
n : ℕ
hn : 0 < n
⊢ ↑(centralBinom n) * Real.sqrt ↑n / 4 ^ n / Real.sqrt (↑n / (↑n + 1 / 4)) = centralBinomialLower n
Theorem: centralBinomialLower_limit
Proof state before:
case h
this : (Real.sqrt π)⁻¹ = (Real.sqrt π)⁻¹ / Real.sqrt 1
h : Real.sqrt 1 ≠ 0
n : ℕ
hn : 0 < n
⊢ ↑(centralBinom n) * Real.sqrt ↑n / 4 ^ n / Real.sqrt (↑n / (↑n + 1 / 4)) = centralBinomialLower n
Tactic:
rw [sqrt_div (Nat.cast_nonneg _), centralBinomialLower, div_div, mul_div_assoc',
  div_div_eq_mul_div, mul_right_comm, mul_div_mul_right]
Proof state after:
case h.hc
this : (Real.sqrt π)⁻¹ = (Real.sqrt π)⁻¹ / Real.sqrt 1
h : Real.sqrt 1 ≠ 0
n : ℕ
hn : 0 < n
⊢ Real.sqrt ↑n ≠ 0
Theorem: centralBinomialLower_limit
Proof state before:
⊢ (Real.sqrt π)⁻¹ = (Real.sqrt π)⁻¹ / Real.sqrt 1
Tactic:
rw [Real.sqrt_one, div_one]
Proof state after:
no goals
Theorem: centralBinomialLower_limit
Proof state before:
case h.hc
this : (Real.sqrt π)⁻¹ = (Real.sqrt π)⁻¹ / Real.sqrt 1
h : Real.sqrt 1 ≠ 0
n : ℕ
hn : 0 < n
⊢ Real.sqrt ↑n ≠ 0
Tactic:
positivity
Proof state after:
no goals
Theorem: centralBinomialUpper_bound
Proof state before:
n : ℕ
⊢ ↑(centralBinom n) ≤ 4 ^ n / Real.sqrt (π * (↑n + 1 / 4))
Tactic:
have := pi_pos
Proof state after:
n : ℕ
this : 0 < π
⊢ ↑(centralBinom n) ≤ 4 ^ n / Real.sqrt (π * (↑n + 1 / 4))
Theorem: centralBinomialUpper_bound
Proof state before:
n : ℕ
this : 0 < π
⊢ ↑(centralBinom n) ≤ 4 ^ n / Real.sqrt (π * (↑n + 1 / 4))
Tactic:
have := centralBinomialLower_monotone.ge_of_tendsto centralBinomialLower_limit n
Proof state after:
n : ℕ
this✝ : 0 < π
this : centralBinomialLower n ≤ (Real.sqrt π)⁻¹
⊢ ↑(centralBinom n) ≤ 4 ^ n / Real.sqrt (π * (↑n + 1 / 4))
Theorem: centralBinomialUpper_bound
Proof state before:
n : ℕ
this✝ : 0 < π
this : centralBinomialLower n ≤ (Real.sqrt π)⁻¹
⊢ ↑(centralBinom n) ≤ 4 ^ n / Real.sqrt (π * (↑n + 1 / 4))
Tactic:
rwa [sqrt_mul, ← div_div, le_div_iff, div_eq_mul_one_div ((4 : ℝ) ^ n : ℝ), ← div_le_iff',
  one_div (sqrt π)]
Proof state after:
n : ℕ
this✝ : 0 < π
this : centralBinomialLower n ≤ (Real.sqrt π)⁻¹
⊢ 0 < 4 ^ n

n : ℕ
this✝ : 0 < π
this : centralBinomialLower n ≤ (Real.sqrt π)⁻¹
⊢ 0 < Real.sqrt (↑n + 1 / 4)

case hx
n : ℕ
this✝ : 0 < π
this : centralBinomialLower n ≤ (Real.sqrt π)⁻¹
⊢ 0 ≤ π
Theorem: centralBinomialUpper_bound
Proof state before:
n : ℕ
this✝ : 0 < π
this : centralBinomialLower n ≤ (Real.sqrt π)⁻¹
⊢ 0 < 4 ^ n

n : ℕ
this✝ : 0 < π
this : centralBinomialLower n ≤ (Real.sqrt π)⁻¹
⊢ 0 < Real.sqrt (↑n + 1 / 4)

case hx
n : ℕ
this✝ : 0 < π
this : centralBinomialLower n ≤ (Real.sqrt π)⁻¹
⊢ 0 ≤ π
Tactic:
all_goals positivity
Proof state after:
no goals
Theorem: centralBinomialUpper_bound
Proof state before:
case hx
n : ℕ
this✝ : 0 < π
this : centralBinomialLower n ≤ (Real.sqrt π)⁻¹
⊢ 0 ≤ π
Tactic:
positivity
Proof state after:
no goals
Theorem: centralBinomialLower_bound
Proof state before:
n : ℕ
⊢ 4 ^ n / Real.sqrt (π * (↑n + 1 / 3)) ≤ ↑(centralBinom n)
Tactic:
have := pi_pos
Proof state after:
n : ℕ
this : 0 < π
⊢ 4 ^ n / Real.sqrt (π * (↑n + 1 / 3)) ≤ ↑(centralBinom n)
Theorem: centralBinomialLower_bound
Proof state before:
n : ℕ
this : 0 < π
⊢ 4 ^ n / Real.sqrt (π * (↑n + 1 / 3)) ≤ ↑(centralBinom n)
Tactic:
have := centralBinomialUpper_monotone.le_of_tendsto centralBinomialUpper_limit n
Proof state after:
n : ℕ
this✝ : 0 < π
this : (Real.sqrt π)⁻¹ ≤ centralBinomialUpper n
⊢ 4 ^ n / Real.sqrt (π * (↑n + 1 / 3)) ≤ ↑(centralBinom n)
Theorem: centralBinomialLower_bound
Proof state before:
n : ℕ
this✝ : 0 < π
this : (Real.sqrt π)⁻¹ ≤ centralBinomialUpper n
⊢ 4 ^ n / Real.sqrt (π * (↑n + 1 / 3)) ≤ ↑(centralBinom n)
Tactic:
rwa [sqrt_mul, ← div_div, div_le_iff, div_eq_mul_one_div, ← le_div_iff', one_div (sqrt π)]
Proof state after:
n : ℕ
this✝ : 0 < π
this : (Real.sqrt π)⁻¹ ≤ centralBinomialUpper n
⊢ 0 < 4 ^ n

n : ℕ
this✝ : 0 < π
this : (Real.sqrt π)⁻¹ ≤ centralBinomialUpper n
⊢ 0 < Real.sqrt (↑n + 1 / 3)

case hx
n : ℕ
this✝ : 0 < π
this : (Real.sqrt π)⁻¹ ≤ centralBinomialUpper n
⊢ 0 ≤ π
Theorem: centralBinomialLower_bound
Proof state before:
n : ℕ
this✝ : 0 < π
this : (Real.sqrt π)⁻¹ ≤ centralBinomialUpper n
⊢ 0 < 4 ^ n

n : ℕ
this✝ : 0 < π
this : (Real.sqrt π)⁻¹ ≤ centralBinomialUpper n
⊢ 0 < Real.sqrt (↑n + 1 / 3)

case hx
n : ℕ
this✝ : 0 < π
this : (Real.sqrt π)⁻¹ ≤ centralBinomialUpper n
⊢ 0 ≤ π
Tactic:
all_goals positivity
Proof state after:
no goals
Theorem: centralBinomialLower_bound
Proof state before:
case hx
n : ℕ
this✝ : 0 < π
this : (Real.sqrt π)⁻¹ ≤ centralBinomialUpper n
⊢ 0 ≤ π
Tactic:
positivity
Proof state after:
no goals
Theorem: cexp_eq_tsum
Proof state before:
x : ℂ
⊢ Complex.exp x = ∑' (i : ℕ), x ^ i / ↑i !
Tactic:
rw [Complex.exp_eq_exp_ℂ, exp_eq_tsum_div]
Proof state after:
no goals
Theorem: rexp_eq_tsum
Proof state before:
x : ℝ
⊢ rexp x = ∑' (i : ℕ), x ^ i / ↑i !
Tactic:
rw [exp_eq_exp_ℝ, exp_eq_tsum_div]
Proof state after:
no goals