Only 3 sorry's remaining

Changes

1 changed files (+8/-1)

• sum.lean
  • @@ -181,7 +181,14 @@ theorem double_sum : converges_to (fun N : ℕ => ∑ a ∈ Ico 2 N, ∑ b ∈ I
    have h₁₀ : 3 ≤ n := by omega exact exp_larger n h₁₀ - sorry + rw [mul_comm, ←one_mul (2 ^ (n - 1))] at h₈ + have h₉ : 0 < (2 : ℝ) ^ (n - 1) := by + norm_num + have h₁₀ : 0 < (2 : ℝ) := by + norm_num + have h₁₁ : ((n : ℝ) - 2) * 2 ≤ 1 * 2 ^ (n - 1) := by + norm_cast + exact (div_le_div_iff₀ h₉ h₁₀).mpr h₁₁ linarith else simp at hε