YAYAYAYAYAYYAYYY

Changes

1 changed files (+14/-3)

• sum.lean
  • @@ -220,9 +220,20 @@ theorem double_sum : converges_to (fun N : ℕ => ∑ a ∈ Ico 2 N, ∑ b ∈ I
    exact exp_larger' n h₁₀ apply lt_sub_iff_add_lt'.mp have h₇ : 3 / (n : ℝ) - 1 / (n - 1) = (2 * n - 3) / (n * (n - 1)) := by - field_simp - ring_nf - sorry + have h₈ : (n : ℝ) ≠ 0 := by + rw [Nat.cast_ne_zero] + linarith + have h₉ : (n : ℝ) - 1 ≠ 0 := by + have h₁₀ : 0 < n := by + linarith + have h₁₁ : ↑(n - 1) = (n : ℝ) - 1 := by + rw [Nat.cast_sub h₁₀] + simp + rw [←h₁₁] + norm_cast + omega + field_simp [h₈, h₉] + ring rw [h₇] have h₈ : ((n : ℝ) - 2) * (n * (n - 1)) < (2 * n - 3) * 2 ^ (n - 1) := by nth_rw 1 [mul_comm] at h₆