Changes
1 changed files (+79/-88)
-
-
@@ -38,16 +38,15 @@ lemma telescope_sum (N : ℕ) (h : 2 ≤ N): ∑ a ∈ Ico 2 N, ∑ b ∈ Ico 2_ = ∑ b ∈ Ico 2 N, ((1 : ℝ) / (b - 1) - (1 : ℝ) / b) - ∑ b ∈ Ico 2 N, (1 : ℝ) / (b ^ (N - 1) * (b - 1)) := by apply sum_sub_distrib _ = 1 - (1 : ℝ) / (N - 1) - ∑ b ∈ Ico 2 N, (1 : ℝ) / (b ^ (N - 1) * (b - 1)) := by have h₁ : ∑ b ∈ Ico 2 N, ((1 : ℝ) / (b - 1) - (1 : ℝ) / b) = 1 - (1 : ℝ) / (N - 1) := by induction h with | refl => field_simp linarith | step h ih => rw [sum_Ico_succ_top, ih] field_simp exact h rw [h₁] suffices ∑ b ∈ Ico 2 N, ((1 : ℝ) / (b - 1) - (1 : ℝ) / b) = 1 - (1 : ℝ) / (N - 1) by rw [this] induction h with | refl => field_simp linarith | step h ih => rw [sum_Ico_succ_top, ih] field_simp exact h -- Exponentials grow quickly lemma exp_larger (n : ℕ) (h : 3 ≤ n) : 2 * (n - 2) ≤ 2 ^ (n - 1) := by
-
@@ -72,22 +71,20 @@ lemma exp_larger' (n : ℕ) (h : 5 ≤ n) : n * (n - 1) * (n - 2) < (2 * n - 3)rename_i m simp simp at a have h₂ : (m + 1) * m * (m - 1) ≤ 2 * (m * (m - 1) * (m - 2)) := by rw [←mul_assoc, mul_assoc] nth_rw 3 [mul_comm] nth_rw 2 [←mul_assoc] apply Nat.mul_le_mul_right (m * (m - 1)) omega grind have h₂ : 2 ^ (n + 1) ≤ (2 * n - 3) * 2 ^ (n - 1) := by have h₃ : 2 ^ (n + 1) = 2 * (2 * 2 ^ (n - 1)) := by rw [mul_pow_sub_one] suffices (m + 1) * m * (m - 1) ≤ 2 * (m * (m - 1) * (m - 2)) by grind rw [←mul_assoc, mul_assoc] nth_rw 3 [mul_comm] nth_rw 2 [←mul_assoc] apply Nat.mul_le_mul_right (m * (m - 1)) omega omega rw [h₃, ←mul_assoc] apply Nat.mul_le_mul_right (2 ^ (n - 1)) suffices 2 ^ (n + 1) ≤ (2 * n - 3) * 2 ^ (n - 1) by linarith have h₂ : 2 ^ (n + 1) = 2 * (2 * 2 ^ (n - 1)) := by rw [mul_pow_sub_one] omega linarith omega rw [h₂, ←mul_assoc] apply Nat.mul_le_mul_right (2 ^ (n - 1)) omega theorem double_sum : converges_to (fun N : ℕ => ∑ a ∈ Ico 2 N, ∑ b ∈ Ico 2 N, 1 / (b ^ a)) 1 := by intro ε εpos
-
@@ -128,66 +125,63 @@ theorem double_sum : converges_to (fun N : ℕ => ∑ a ∈ Ico 2 N, ∑ b ∈ Iexact h₄ ring_nf at h₂ have h₃ : 1 < 1 + ε - 1 / (n - 1) - (n - 2) / 2 ^ (n - 1) := by have h₄ : 1 / (n - 1) + (n - 2) / 2 ^ (n - 1) < ε := by if hε : 3 / 2 < ε then have h₅ : 2 ≤ (n : ℝ) := Nat.ofNat_le_cast.mpr h₁ have h₆ : 1 / ((n : ℝ) - 1) ≤ 1 := by refine (div_le_one₀ ?_).mpr (by linarith) linarith have h₇ : ((n : ℝ) - 2) / 2 ^ (n - 1) ≤ 1 / 2 := by have h₈ : 2 * (n - 2) ≤ 2 ^ (n - 1) := by if h₉ : n = 2 then simp [h₉] else exact exp_larger n (by omega) rw [mul_comm, ←one_mul (2 ^ (n - 1))] at h₈ exact (div_le_div_iff₀ (by norm_num) (by norm_num)).mpr (by norm_cast) suffices 1 / (n - 1) + (n - 2) / 2 ^ (n - 1) < ε by linarith if hε : 3 / 2 < ε then have h₄ : 2 ≤ (n : ℝ) := Nat.ofNat_le_cast.mpr h₁ have h₅ : 1 / ((n : ℝ) - 1) ≤ 1 := by refine (div_le_one₀ ?_).mpr (by linarith) linarith else simp at hε have h₃ : 3 / n ≤ ε := by have h₄ : 3 / ε ≤ n := Nat.ceil_le.mp (le_of_max_le_left nlarge) refine (div_le_comm₀ ?_ εpos).mpr h₄ norm_num suffices ((n : ℝ) - 2) / 2 ^ (n - 1) ≤ 1 / 2 by linarith have h₆ : 2 * (n - 2) ≤ 2 ^ (n - 1) := by if h₇ : n = 2 then simp [h₇] else exact exp_larger n (by omega) rw [mul_comm, ←one_mul (2 ^ (n - 1))] at h₆ exact (div_le_div_iff₀ (by norm_num) (by norm_num)).mpr (by norm_cast) else simp at hε have h₃ : 3 / n ≤ ε := by have h₄ : 3 / ε ≤ n := Nat.ceil_le.mp (le_of_max_le_left nlarge) refine (div_le_comm₀ ?_ εpos).mpr h₄ norm_num omega suffices 1 / ((n : ℝ) - 1) + ((n : ℝ) - 2) / 2 ^ (n - 1) < 3 / n by linarith have h₄ : n * (n - 1) * (n - 2) < (2 * n - 3) * 2 ^ (n - 1) := by if h₅ : n = 2 then simp [h₅] else if h₆ : n = 3 then simp [h₆] else if h₇ : n = 4 then simp [h₇] else exact exp_larger' n (by omega) apply lt_sub_iff_add_lt'.mp have h₅ : 3 / (n : ℝ) - 1 / (n - 1) = (2 * n - 3) / (n * (n - 1)) := by have h₆ : (n : ℝ) ≠ 0 := by rw [Nat.cast_ne_zero] omega have h₄ : 1 / ((n : ℝ) - 1) + ((n : ℝ) - 2) / 2 ^ (n - 1) < 3 / n := by have h₅ : n * (n - 1) * (n - 2) < (2 * n - 3) * 2 ^ (n - 1) := by if h₆ : n = 2 then simp [h₆] else if h₇ : n = 3 then simp [h₇] else if h₈ : n = 4 then simp [h₈] else exact exp_larger' n (by omega) apply lt_sub_iff_add_lt'.mp have h₆ : 3 / (n : ℝ) - 1 / (n - 1) = (2 * n - 3) / (n * (n - 1)) := by have h₇ : (n : ℝ) ≠ 0 := by rw [Nat.cast_ne_zero] omega have h₈ : (n : ℝ) - 1 ≠ 0 := by grind field_simp ring 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 rw [Nat.cast_sub (by linarith)] simp have h₉ : ↑(2 * n - 3) = 2 * (n : ℝ) - 3 := by rw [Nat.cast_sub (by linarith)] 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 exact (div_lt_div_iff₀ h₈ (by nlinarith)).mpr h₇ linarith linarith have h₇ : (n : ℝ) - 1 ≠ 0 := by grind field_simp ring 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 rw [Nat.cast_sub (by linarith)] simp have h₈ : ↑(2 * n - 3) = 2 * (n : ℝ) - 3 := by rw [Nat.cast_sub (by linarith)] 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 exact (div_lt_div_iff₀ h₇ (by nlinarith)).mpr h₆ ring_nf at h₃ linarith -- Less than 1
-
@@ -206,12 +200,9 @@ theorem double_sum : converges_to (fun N : ℕ => ∑ a ∈ Ico 2 N, ∑ b ∈ Ihave h₆ : 0 < (b : ℝ) ^ (n - 1) := by apply pow_pos (by linarith) exact mul_pos h₆ (by linarith) have h₄ : 0 ≤ ∑ b ∈ Ico 2 n, (1 : ℝ) / (b ^ (n - 1) * (b - 1)) := by have h₅ : ∀ b ∈ Ico 2 n, 0 ≤ (1 : ℝ) / (b ^ (n - 1) * (b - 1)) := fun b a => le_of_lt (h₃ b a) exact sum_nonneg h₅ have h₄ : 0 ≤ ∑ b ∈ Ico 2 n, (1 : ℝ) / (b ^ (n - 1) * (b - 1)) := sum_nonneg (fun b a => le_of_lt (h₃ b a)) ring_nf at h₄ field_simp at h₄ have h₅ : -(1 : ℝ) / (-1 + n) < 0 := by nth_rw 1 [← mul_neg_one, mul_comm, mul_div_assoc] linarith suffices -(1 : ℝ) / (-1 + n) < 0 by linarith nth_rw 1 [← mul_neg_one, mul_comm, mul_div_assoc] linarith
-