Only 1 sorry remains!!

Changes

1 changed files (+51/-15)

• sum.lean
  • @@ -90,8 +90,8 @@ lemma exp_larger (n : ℕ) (h : n ≥ 3) : 2 * (n - 2) ≤ 2 ^ (n - 1) := by
    linarith -- Another similar lemma - lemma exp_larger' (n : ℕ) (h : n ≥ 3) : n * (n - 1) < (3 * n - 4) * 2 ^ (n - 1) := by - have h₁ : n * (n - 1) < 2 ^ n := by + lemma exp_larger' (n : ℕ) (h : n ≥ 5) : n * (n - 1) * (n - 2) < (2 * n - 3) * 2 ^ (n - 1) := by + have h₁ : n * (n - 1) * (n - 2) < 2 ^ (n + 1) := by induction h with | refl => trivial
  • @@ -99,18 +99,21 @@ lemma exp_larger' (n : ℕ) (h : n ≥ 3) : n * (n - 1) < (3 * n - 4) * 2 ^ (n -
    rename_i m simp simp at a - have h₂ : (m + 1) * m ≤ 2 * (m * (m - 1)) := by - nth_rw 3 [mul_comm] + have h₂ : (m + 1) * m * (m - 1) ≤ 2 * (m * (m - 1) * (m - 2)) := by rw [←mul_assoc] - apply Nat.mul_le_mul_right m + rw [mul_assoc] + nth_rw 3 [mul_comm] + nth_rw 2 [←mul_assoc] + apply Nat.mul_le_mul_right (m * (m - 1)) omega - have h₃ : 2 ^ (m + 1) = 2 * 2 ^ m := Nat.pow_succ' - linarith - have h₂ : 2 ^ n ≤ (3 * n - 4) * 2 ^ (n - 1) := by - have h₃ : 2 * 2 ^ (n - 1) = 2 ^ n := by - apply mul_pow_sub_one + have h₃ : 2 ^ (m + 2) = 2 * 2 ^ (m + 1) := Nat.pow_succ' linarith - rw [←h₃] + have h₂ : 2 ^ (n + 1) ≤ (2 * n - 3) * 2 ^ (n - 1) := by + have h₃ : 2 * (2 * 2 ^ (n - 1)) = 2 ^ (n + 1) := by + rw [mul_pow_sub_one] + omega + omega + rw [←h₃, ←mul_assoc] apply Nat.mul_le_mul_right (2 ^ (n - 1)) omega linarith
  • @@ -201,15 +204,48 @@ theorem double_sum : converges_to (fun N : ℕ => ∑ a ∈ Ico 2 N, ∑ b ∈ I
    norm_num linarith have h₅ : 1 / ((n : ℝ) - 1) + ((n : ℝ) - 2) / 2 ^ (n - 1) < 3 / n := by - have h₆ : n * (n - 1) < (3 * n - 4) * 2 ^ (n - 1) := by + have h₆ : n * (n - 1) * (n - 2) < (2 * n - 3) * 2 ^ (n - 1) := by if h₇ : n = 2 then rw [h₇] norm_num + else if h₈ : n = 3 then + rw [h₈] + norm_num + else if h₉ : n = 4 then + rw [h₉] + norm_num else - have h₈ : 3 ≤ n := by + have h₁₀ : 5 ≤ n := by omega - exact exp_larger' n h₈ - sorry + 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 + rw [h₇] + have h₈ : ((n : ℝ) - 2) * (n * (n - 1)) < (2 * n - 3) * 2 ^ (n - 1) := by + nth_rw 1 [mul_comm] at h₆ + rify at h₆ + have h₉ : ↑(n - 1) = (n : ℝ) - 1 := by + have h₁₀ : 0 < n := by + linarith + rw [Nat.cast_sub h₁₀] + simp + have h₁₀ : ↑(2 * n - 3) = 2 * (n : ℝ) - 3 := by + have h₁₁ : 2 < 2 * n := by + linarith + rw [Nat.cast_sub h₁₁] + simp + have h₁₁ : ↑(n - 2) = (n : ℝ) - 2 := by + norm_cast + rw [h₉, h₁₀, h₁₁] at h₆ + exact h₆ + have h₉ : 0 < (2 : ℝ) ^ (n - 1) := by + norm_num + have h₁₀ : 0 < (n : ℝ) * (n - 1) := by + nlinarith + exact (div_lt_div_iff₀ h₉ h₁₀).mpr h₈ linarith linarith ring_nf at h₃