[GOAL]
k : ℕ
⊢ 0 < W k
[PROOFSTEP]
induction' k with k hk
[GOAL]
case zero
⊢ 0 < W Nat.zero
[PROOFSTEP]
unfold W
[GOAL]
case zero
⊢ 0 < ∏ i in range Nat.zero, (2 * ↑i + 2) / (2 * ↑i + 1) * ((2 * ↑i + 2) / (2 * ↑i + 3))
[PROOFSTEP]
simp
[GOAL]
case succ
k : ℕ
hk : 0 < W k
⊢ 0 < W (Nat.succ k)
[PROOFSTEP]
rw [W_succ]
[GOAL]
case succ
k : ℕ
hk : 0 < W k
⊢ 0 < W k * ((2 * ↑k + 2) / (2 * ↑k + 1) * ((2 * ↑k + 2) / (2 * ↑k + 3)))
[PROOFSTEP]
refine' mul_pos hk (mul_pos (div_pos _ _) (div_pos _ _))
[GOAL]
case succ.refine'_1
k : ℕ
hk : 0 < W k
⊢ 0 < 2 * ↑k + 2
[PROOFSTEP]
positivity
[GOAL]
case succ.refine'_2
k : ℕ
hk : 0 < W k
⊢ 0 < 2 * ↑k + 1
[PROOFSTEP]
positivity
[GOAL]
case succ.refine'_3
k : ℕ
hk : 0 < W k
⊢ 0 < 2 * ↑k + 2
[PROOFSTEP]
positivity
[GOAL]
case succ.refine'_4
k : ℕ
hk : 0 < W k
⊢ 0 < 2 * ↑k + 3
[PROOFSTEP]
positivity
[GOAL]
n : ℕ
⊢ W n = ↑(2 ^ (4 * n)) * ↑(n ! ^ 4) / (↑((2 * n)! ^ 2) * (2 * ↑n + 1))
[PROOFSTEP]
induction' n with n IH
[GOAL]
case zero
⊢ W Nat.zero = ↑(2 ^ (4 * Nat.zero)) * ↑(Nat.zero ! ^ 4) / (↑((2 * Nat.zero)! ^ 2) * (2 * ↑Nat.zero + 1))
[PROOFSTEP]
simp only [W, prod_range_zero, Nat.factorial_zero, mul_zero, pow_zero, algebraMap.coe_one, one_pow, mul_one,
  algebraMap.coe_zero, zero_add, div_self, Ne.def, one_ne_zero, not_false_iff]
[GOAL]
case zero
⊢ 1 = ↑(2 ^ (4 * Nat.zero)) * ↑1 / (↑((2 * Nat.zero)! ^ 2) * (2 * ↑Nat.zero + 1))
[PROOFSTEP]
norm_num
[GOAL]
case succ
n : ℕ
IH : W n = ↑(2 ^ (4 * n)) * ↑(n ! ^ 4) / (↑((2 * n)! ^ 2) * (2 * ↑n + 1))
⊢ W (Nat.succ n) = ↑(2 ^ (4 * Nat.succ n)) * ↑((Nat.succ n)! ^ 4) / (↑((2 * Nat.succ n)! ^ 2) * (2 * ↑(Nat.succ n) + 1))
[PROOFSTEP]
unfold W at IH ⊢
[GOAL]
case succ
n : ℕ
IH :
  ∏ i in range n, (2 * ↑i + 2) / (2 * ↑i + 1) * ((2 * ↑i + 2) / (2 * ↑i + 3)) =
    ↑(2 ^ (4 * n)) * ↑(n ! ^ 4) / (↑((2 * n)! ^ 2) * (2 * ↑n + 1))
⊢ ∏ i in range (Nat.succ n), (2 * ↑i + 2) / (2 * ↑i + 1) * ((2 * ↑i + 2) / (2 * ↑i + 3)) =
    ↑(2 ^ (4 * Nat.succ n)) * ↑((Nat.succ n)! ^ 4) / (↑((2 * Nat.succ n)! ^ 2) * (2 * ↑(Nat.succ n) + 1))
[PROOFSTEP]
rw [prod_range_succ, IH, _root_.div_mul_div_comm, _root_.div_mul_div_comm]
[GOAL]
case succ
n : ℕ
IH :
  ∏ i in range n, (2 * ↑i + 2) / (2 * ↑i + 1) * ((2 * ↑i + 2) / (2 * ↑i + 3)) =
    ↑(2 ^ (4 * n)) * ↑(n ! ^ 4) / (↑((2 * n)! ^ 2) * (2 * ↑n + 1))
⊢ ↑(2 ^ (4 * n)) * ↑(n ! ^ 4) * ((2 * ↑n + 2) * (2 * ↑n + 2)) /
      (↑((2 * n)! ^ 2) * (2 * ↑n + 1) * ((2 * ↑n + 1) * (2 * ↑n + 3))) =
    ↑(2 ^ (4 * Nat.succ n)) * ↑((Nat.succ n)! ^ 4) / (↑((2 * Nat.succ n)! ^ 2) * (2 * ↑(Nat.succ n) + 1))
[PROOFSTEP]
refine' (div_eq_div_iff _ _).mpr _
[GOAL]
case succ.refine'_1
n : ℕ
IH :
  ∏ i in range n, (2 * ↑i + 2) / (2 * ↑i + 1) * ((2 * ↑i + 2) / (2 * ↑i + 3)) =
    ↑(2 ^ (4 * n)) * ↑(n ! ^ 4) / (↑((2 * n)! ^ 2) * (2 * ↑n + 1))
⊢ ↑((2 * n)! ^ 2) * (2 * ↑n + 1) * ((2 * ↑n + 1) * (2 * ↑n + 3)) ≠ 0
case succ.refine'_2
n : ℕ
IH :
  ∏ i in range n, (2 * ↑i + 2) / (2 * ↑i + 1) * ((2 * ↑i + 2) / (2 * ↑i + 3)) =
    ↑(2 ^ (4 * n)) * ↑(n ! ^ 4) / (↑((2 * n)! ^ 2) * (2 * ↑n + 1))
⊢ ↑((2 * Nat.succ n)! ^ 2) * (2 * ↑(Nat.succ n) + 1) ≠ 0
case succ.refine'_3
n : ℕ
IH :
  ∏ i in range n, (2 * ↑i + 2) / (2 * ↑i + 1) * ((2 * ↑i + 2) / (2 * ↑i + 3)) =
    ↑(2 ^ (4 * n)) * ↑(n ! ^ 4) / (↑((2 * n)! ^ 2) * (2 * ↑n + 1))
⊢ ↑(2 ^ (4 * n)) * ↑(n ! ^ 4) * ((2 * ↑n + 2) * (2 * ↑n + 2)) * (↑((2 * Nat.succ n)! ^ 2) * (2 * ↑(Nat.succ n) + 1)) =
    ↑(2 ^ (4 * Nat.succ n)) * ↑((Nat.succ n)! ^ 4) * (↑((2 * n)! ^ 2) * (2 * ↑n + 1) * ((2 * ↑n + 1) * (2 * ↑n + 3)))
[PROOFSTEP]
any_goals exact ne_of_gt (by positivity)
[GOAL]
case succ.refine'_1
n : ℕ
IH :
  ∏ i in range n, (2 * ↑i + 2) / (2 * ↑i + 1) * ((2 * ↑i + 2) / (2 * ↑i + 3)) =
    ↑(2 ^ (4 * n)) * ↑(n ! ^ 4) / (↑((2 * n)! ^ 2) * (2 * ↑n + 1))
⊢ ↑((2 * n)! ^ 2) * (2 * ↑n + 1) * ((2 * ↑n + 1) * (2 * ↑n + 3)) ≠ 0
[PROOFSTEP]
exact ne_of_gt (by positivity)
[GOAL]
n : ℕ
IH :
  ∏ i in range n, (2 * ↑i + 2) / (2 * ↑i + 1) * ((2 * ↑i + 2) / (2 * ↑i + 3)) =
    ↑(2 ^ (4 * n)) * ↑(n ! ^ 4) / (↑((2 * n)! ^ 2) * (2 * ↑n + 1))
⊢ 0 < ↑((2 * n)! ^ 2) * (2 * ↑n + 1) * ((2 * ↑n + 1) * (2 * ↑n + 3))
[PROOFSTEP]
positivity
[GOAL]
case succ.refine'_2
n : ℕ
IH :
  ∏ i in range n, (2 * ↑i + 2) / (2 * ↑i + 1) * ((2 * ↑i + 2) / (2 * ↑i + 3)) =
    ↑(2 ^ (4 * n)) * ↑(n ! ^ 4) / (↑((2 * n)! ^ 2) * (2 * ↑n + 1))
⊢ ↑((2 * Nat.succ n)! ^ 2) * (2 * ↑(Nat.succ n) + 1) ≠ 0
[PROOFSTEP]
exact ne_of_gt (by positivity)
[GOAL]
n : ℕ
IH :
  ∏ i in range n, (2 * ↑i + 2) / (2 * ↑i + 1) * ((2 * ↑i + 2) / (2 * ↑i + 3)) =
    ↑(2 ^ (4 * n)) * ↑(n ! ^ 4) / (↑((2 * n)! ^ 2) * (2 * ↑n + 1))
⊢ 0 < ↑((2 * Nat.succ n)! ^ 2) * (2 * ↑(Nat.succ n) + 1)
[PROOFSTEP]
positivity
[GOAL]
case succ.refine'_3
n : ℕ
IH :
  ∏ i in range n, (2 * ↑i + 2) / (2 * ↑i + 1) * ((2 * ↑i + 2) / (2 * ↑i + 3)) =
    ↑(2 ^ (4 * n)) * ↑(n ! ^ 4) / (↑((2 * n)! ^ 2) * (2 * ↑n + 1))
⊢ ↑(2 ^ (4 * n)) * ↑(n ! ^ 4) * ((2 * ↑n + 2) * (2 * ↑n + 2)) * (↑((2 * Nat.succ n)! ^ 2) * (2 * ↑(Nat.succ n) + 1)) =
    ↑(2 ^ (4 * Nat.succ n)) * ↑((Nat.succ n)! ^ 4) * (↑((2 * n)! ^ 2) * (2 * ↑n + 1) * ((2 * ↑n + 1) * (2 * ↑n + 3)))
[PROOFSTEP]
exact ne_of_gt (by positivity)
[GOAL]
n : ℕ
IH :
  ∏ i in range n, (2 * ↑i + 2) / (2 * ↑i + 1) * ((2 * ↑i + 2) / (2 * ↑i + 3)) =
    ↑(2 ^ (4 * n)) * ↑(n ! ^ 4) / (↑((2 * n)! ^ 2) * (2 * ↑n + 1))
⊢ ?m.19110 < ?m.19109
[PROOFSTEP]
positivity
[GOAL]
case succ.refine'_3
n : ℕ
IH :
  ∏ i in range n, (2 * ↑i + 2) / (2 * ↑i + 1) * ((2 * ↑i + 2) / (2 * ↑i + 3)) =
    ↑(2 ^ (4 * n)) * ↑(n ! ^ 4) / (↑((2 * n)! ^ 2) * (2 * ↑n + 1))
⊢ ↑(2 ^ (4 * n)) * ↑(n ! ^ 4) * ((2 * ↑n + 2) * (2 * ↑n + 2)) * (↑((2 * Nat.succ n)! ^ 2) * (2 * ↑(Nat.succ n) + 1)) =
    ↑(2 ^ (4 * Nat.succ n)) * ↑((Nat.succ n)! ^ 4) * (↑((2 * n)! ^ 2) * (2 * ↑n + 1) * ((2 * ↑n + 1) * (2 * ↑n + 3)))
[PROOFSTEP]
simp_rw [Nat.mul_succ, Nat.factorial_succ, pow_succ]
[GOAL]
case succ.refine'_3
n : ℕ
IH :
  ∏ i in range n, (2 * ↑i + 2) / (2 * ↑i + 1) * ((2 * ↑i + 2) / (2 * ↑i + 3)) =
    ↑(2 ^ (4 * n)) * ↑(n ! ^ 4) / (↑((2 * n)! ^ 2) * (2 * ↑n + 1))
⊢ ↑(2 ^ (4 * n)) * ↑(n ! * (n ! * (n ! * (n ! * n ! ^ 0)))) * ((2 * ↑n + 2) * (2 * ↑n + 2)) *
      (↑((2 * n + 1 + 1) * ((2 * n + 1) * (2 * n)!) *
            ((2 * n + 1 + 1) * ((2 * n + 1) * (2 * n)!) * ((2 * n + 1 + 1) * ((2 * n + 1) * (2 * n)!)) ^ 0)) *
        (2 * ↑(Nat.succ n) + 1)) =
    ↑(2 * (2 * (2 * (2 * 2 ^ (4 * n))))) *
        ↑((n + 1) * n ! * ((n + 1) * n ! * ((n + 1) * n ! * ((n + 1) * n ! * ((n + 1) * n !) ^ 0)))) *
      (↑((2 * n)! * ((2 * n)! * (2 * n)! ^ 0)) * (2 * ↑n + 1) * ((2 * ↑n + 1) * (2 * ↑n + 3)))
[PROOFSTEP]
push_cast
[GOAL]
case succ.refine'_3
n : ℕ
IH :
  ∏ i in range n, (2 * ↑i + 2) / (2 * ↑i + 1) * ((2 * ↑i + 2) / (2 * ↑i + 3)) =
    ↑(2 ^ (4 * n)) * ↑(n ! ^ 4) / (↑((2 * n)! ^ 2) * (2 * ↑n + 1))
⊢ 2 ^ (4 * n) * (↑n ! * (↑n ! * (↑n ! * (↑n ! * ↑n ! ^ 0)))) * ((2 * ↑n + 2) * (2 * ↑n + 2)) *
      ((2 * ↑n + 1 + 1) * ((2 * ↑n + 1) * ↑(2 * n)!) *
          ((2 * ↑n + 1 + 1) * ((2 * ↑n + 1) * ↑(2 * n)!) * ((2 * ↑n + 1 + 1) * ((2 * ↑n + 1) * ↑(2 * n)!)) ^ 0) *
        (2 * (↑n + 1) + 1)) =
    2 * (2 * (2 * (2 * 2 ^ (4 * n)))) *
        ((↑n + 1) * ↑n ! * ((↑n + 1) * ↑n ! * ((↑n + 1) * ↑n ! * ((↑n + 1) * ↑n ! * ((↑n + 1) * ↑n !) ^ 0)))) *
      (↑(2 * n)! * (↑(2 * n)! * ↑(2 * n)! ^ 0) * (2 * ↑n + 1) * ((2 * ↑n + 1) * (2 * ↑n + 3)))
[PROOFSTEP]
ring_nf
[GOAL]
k : ℕ
⊢ (π / 2)⁻¹ * W k = (∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k + 1)) / ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k)
[PROOFSTEP]
rw [integral_sin_pow_even, integral_sin_pow_odd, mul_div_mul_comm, ← prod_div_distrib, inv_div]
[GOAL]
k : ℕ
⊢ 2 / π * W k = 2 / π * ∏ x in range k, (2 * ↑x + 2) / (2 * ↑x + 3) / ((2 * ↑x + 1) / (2 * ↑x + 2))
[PROOFSTEP]
simp_rw [div_div_div_comm, div_div_eq_mul_div, mul_div_assoc]
[GOAL]
k : ℕ
⊢ 2 / π * W k = 2 / π * ∏ x in range k, (2 * ↑x + 2) / (2 * ↑x + 1) * ((2 * ↑x + 2) / (2 * ↑x + 3))
[PROOFSTEP]
rfl
[GOAL]
k : ℕ
⊢ W k ≤ π / 2
[PROOFSTEP]
rw [← div_le_one pi_div_two_pos, div_eq_inv_mul]
[GOAL]
k : ℕ
⊢ (π / 2)⁻¹ * W k ≤ 1
[PROOFSTEP]
rw [W_eq_integral_sin_pow_div_integral_sin_pow, div_le_one (integral_sin_pow_pos _)]
[GOAL]
k : ℕ
⊢ ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k + 1) ≤ ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k)
[PROOFSTEP]
apply integral_sin_pow_succ_le
[GOAL]
k : ℕ
⊢ (2 * ↑k + 1) / (2 * ↑k + 2) * (π / 2) ≤ W k
[PROOFSTEP]
rw [← le_div_iff pi_div_two_pos, div_eq_inv_mul (W k) _]
[GOAL]
k : ℕ
⊢ (2 * ↑k + 1) / (2 * ↑k + 2) ≤ (π / 2)⁻¹ * W k
[PROOFSTEP]
rw [W_eq_integral_sin_pow_div_integral_sin_pow, le_div_iff (integral_sin_pow_pos _)]
[GOAL]
k : ℕ
⊢ (2 * ↑k + 1) / (2 * ↑k + 2) * ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k) ≤ ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k + 1)
[PROOFSTEP]
convert integral_sin_pow_succ_le (2 * k + 1)
[GOAL]
case h.e'_3
k : ℕ
⊢ (2 * ↑k + 1) / (2 * ↑k + 2) * ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k) = ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k + 1 + 1)
[PROOFSTEP]
rw [integral_sin_pow (2 * k)]
[GOAL]
case h.e'_3
k : ℕ
⊢ (2 * ↑k + 1) / (2 * ↑k + 2) * ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k) =
    (sin 0 ^ (2 * k + 1) * cos 0 - sin π ^ (2 * k + 1) * cos π) / (↑(2 * k) + 2) +
      (↑(2 * k) + 1) / (↑(2 * k) + 2) * ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k)
[PROOFSTEP]
simp only [sin_zero, zero_pow', Ne.def, Nat.succ_ne_zero, zero_mul, sin_pi, tsub_zero, zero_div, zero_add]
[GOAL]
case h.e'_3
k : ℕ
⊢ (2 * ↑k + 1) / (2 * ↑k + 2) * ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k) =
    (↑(2 * k) + 1) / (↑(2 * k) + 2) * ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k)
[PROOFSTEP]
norm_cast
[GOAL]
⊢ Tendsto W atTop (𝓝 (π / 2))
[PROOFSTEP]
refine' tendsto_of_tendsto_of_tendsto_of_le_of_le _ tendsto_const_nhds le_W W_le
[GOAL]
⊢ Tendsto (fun i => (2 * ↑i + 1) / (2 * ↑i + 2) * (π / 2)) atTop (𝓝 (π / 2))
[PROOFSTEP]
have : 𝓝 (π / 2) = 𝓝 ((1 - 0) * (π / 2)) := by rw [sub_zero, one_mul]
[GOAL]
⊢ 𝓝 (π / 2) = 𝓝 ((1 - 0) * (π / 2))
[PROOFSTEP]
rw [sub_zero, one_mul]
[GOAL]
this : 𝓝 (π / 2) = 𝓝 ((1 - 0) * (π / 2))
⊢ Tendsto (fun i => (2 * ↑i + 1) / (2 * ↑i + 2) * (π / 2)) atTop (𝓝 (π / 2))
[PROOFSTEP]
rw [this]
[GOAL]
this : 𝓝 (π / 2) = 𝓝 ((1 - 0) * (π / 2))
⊢ Tendsto (fun i => (2 * ↑i + 1) / (2 * ↑i + 2) * (π / 2)) atTop (𝓝 ((1 - 0) * (π / 2)))
[PROOFSTEP]
refine' Tendsto.mul _ tendsto_const_nhds
[GOAL]
this : 𝓝 (π / 2) = 𝓝 ((1 - 0) * (π / 2))
⊢ Tendsto (fun i => (2 * ↑i + 1) / (2 * ↑i + 2)) atTop (𝓝 (1 - 0))
[PROOFSTEP]
have h : ∀ n : ℕ, ((2 : ℝ) * n + 1) / (2 * n + 2) = 1 - 1 / (2 * n + 2) :=
  by
  intro n
  rw [sub_div' _ _ _
      (ne_of_gt (add_pos_of_nonneg_of_pos (mul_nonneg (two_pos : 0 < (2 : ℝ)).le (Nat.cast_nonneg _)) two_pos)),
    one_mul]
  congr 1; ring
[GOAL]
this : 𝓝 (π / 2) = 𝓝 ((1 - 0) * (π / 2))
⊢ ∀ (n : ℕ), (2 * ↑n + 1) / (2 * ↑n + 2) = 1 - 1 / (2 * ↑n + 2)
[PROOFSTEP]
intro n
[GOAL]
this : 𝓝 (π / 2) = 𝓝 ((1 - 0) * (π / 2))
n : ℕ
⊢ (2 * ↑n + 1) / (2 * ↑n + 2) = 1 - 1 / (2 * ↑n + 2)
[PROOFSTEP]
rw [sub_div' _ _ _
    (ne_of_gt (add_pos_of_nonneg_of_pos (mul_nonneg (two_pos : 0 < (2 : ℝ)).le (Nat.cast_nonneg _)) two_pos)),
  one_mul]
[GOAL]
this : 𝓝 (π / 2) = 𝓝 ((1 - 0) * (π / 2))
n : ℕ
⊢ (2 * ↑n + 1) / (2 * ↑n + 2) = (2 * ↑n + 2 - 1) / (2 * ↑n + 2)
[PROOFSTEP]
congr 1
[GOAL]
case e_a
this : 𝓝 (π / 2) = 𝓝 ((1 - 0) * (π / 2))
n : ℕ
⊢ 2 * ↑n + 1 = 2 * ↑n + 2 - 1
[PROOFSTEP]
ring
[GOAL]
this : 𝓝 (π / 2) = 𝓝 ((1 - 0) * (π / 2))
h : ∀ (n : ℕ), (2 * ↑n + 1) / (2 * ↑n + 2) = 1 - 1 / (2 * ↑n + 2)
⊢ Tendsto (fun i => (2 * ↑i + 1) / (2 * ↑i + 2)) atTop (𝓝 (1 - 0))
[PROOFSTEP]
simp_rw [h]
[GOAL]
this : 𝓝 (π / 2) = 𝓝 ((1 - 0) * (π / 2))
h : ∀ (n : ℕ), (2 * ↑n + 1) / (2 * ↑n + 2) = 1 - 1 / (2 * ↑n + 2)
⊢ Tendsto (fun i => 1 - 1 / (2 * ↑i + 2)) atTop (𝓝 (1 - 0))
[PROOFSTEP]
refine' (tendsto_const_nhds.div_atTop _).const_sub _
[GOAL]
this : 𝓝 (π / 2) = 𝓝 ((1 - 0) * (π / 2))
h : ∀ (n : ℕ), (2 * ↑n + 1) / (2 * ↑n + 2) = 1 - 1 / (2 * ↑n + 2)
⊢ Tendsto (fun i => 2 * ↑i + 2) atTop atTop
[PROOFSTEP]
refine' Tendsto.atTop_add _ tendsto_const_nhds
[GOAL]
this : 𝓝 (π / 2) = 𝓝 ((1 - 0) * (π / 2))
h : ∀ (n : ℕ), (2 * ↑n + 1) / (2 * ↑n + 2) = 1 - 1 / (2 * ↑n + 2)
⊢ Tendsto (fun i => 2 * ↑i) atTop atTop
[PROOFSTEP]
exact tendsto_nat_cast_atTop_atTop.const_mul_atTop two_pos
