More cleanup for Sum.lean

Changes

1 changed files (+42/-55)

• Sum.lean
  • @@ -58,10 +58,9 @@ lemma exp_larger (n : ℕ) (h : 3 ≤ n) : 2 * (n - 2) ≤ 2 ^ (n - 1) := by
    rename_i m simp simp at a - have h₁ : 2 * 2 ^ (m - 1) = 2 ^ m := by - apply mul_pow_sub_one - linarith + rw [←mul_pow_sub_one] grind + omega -- Another similar lemma lemma exp_larger' (n : ℕ) (h : 5 ≤ n) : n * (n - 1) * (n - 2) < (2 * n - 3) * 2 ^ (n - 1) := by
  • @@ -81,11 +80,11 @@ lemma exp_larger' (n : ℕ) (h : 5 ≤ n) : n * (n - 1) * (n - 2) < (2 * n - 3)
    omega grind have h₂ : 2 ^ (n + 1) ≤ (2 * n - 3) * 2 ^ (n - 1) := by - have h₃ : 2 * (2 * 2 ^ (n - 1)) = 2 ^ (n + 1) := by + have h₃ : 2 ^ (n + 1) = 2 * (2 * 2 ^ (n - 1)) := by rw [mul_pow_sub_one] omega omega - rw [←h₃, ←mul_assoc] + rw [h₃, ←mul_assoc] apply Nat.mul_le_mul_right (2 ^ (n - 1)) omega linarith
  • @@ -105,25 +104,24 @@ theorem double_sum : converges_to (fun N : ℕ => ∑ a ∈ Ico 2 N, ∑ b ∈ I
    have h₂ : ∑ b ∈ Ico 2 n, (1 : ℝ) / (b ^ (n - 1) * (b - 1)) ≤ (n - 2) / 2 ^ (n - 1) := by have h₃ : ∀ b ∈ Ico 2 n, (1 : ℝ) / (b ^ (n - 1) * (b - 1)) ≤ 1 / 2 ^ (n - 1) := by intro b bico - have h₄ : 2 ≤ b := List.left_le_of_mem_range' bico - have h₅ : 2 ≤ (b : ℝ) := by + have h₄ : 2 ≤ (b : ℝ) := by norm_num - exact h₄ - have h₆ : 1 / ((b : ℝ) - 1) ≤ 1 := by + exact (List.left_le_of_mem_range' bico) + have h₅ : 1 / ((b : ℝ) - 1) ≤ 1 := by refine (div_le_one₀ ?_).mpr (by linarith) linarith - have h₇ : 1 / (b : ℝ) ^ (n - 1) ≤ 1 / 2 ^ (n - 1) := by + have h₆ : 1 / (b : ℝ) ^ (n - 1) ≤ 1 / 2 ^ (n - 1) := by rw [←one_div_pow, ←one_div_pow] apply pow_le_pow_left₀ norm_num simp - apply inv_anti₀ at h₅ - exact h₅ + apply inv_anti₀ at h₄ + exact h₄ norm_num rw [←one_div_mul_one_div, mul_comm] nth_rw 5 [←one_mul 1] rw [mul_div_assoc] - exact mul_le_mul h₆ h₇ (by norm_num) (by norm_num) + exact mul_le_mul h₅ h₆ (by norm_num) (by norm_num) have h₄ : ∑ b ∈ Ico 2 n, (1 : ℝ) / (b ^ (n - 1) * (b - 1)) ≤ ∑ b ∈ Ico 2 n, 1 / 2 ^ (n - 1) := sum_le_sum h₃ field_simp at h₄ field_simp
  • @@ -134,9 +132,7 @@ theorem double_sum : converges_to (fun N : ℕ => ∑ a ∈ Ico 2 N, ∑ b ∈ I
    if hε : 3 / 2 < ε then have h₅ : 2 ≤ (n : ℝ) := Nat.ofNat_le_cast.mpr h₁ have h₆ : 1 / ((n : ℝ) - 1) ≤ 1 := by - have h₇ : 1 ≤ (n : ℝ) - 1 := by - linarith - refine (div_le_one₀ ?_).mpr h₇ + 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
  • @@ -149,56 +145,47 @@ theorem double_sum : converges_to (fun N : ℕ => ∑ a ∈ Ico 2 N, ∑ b ∈ I
    linarith else simp at hε - have h₃ : Nat.ceil (3 / ε) ≤ n := le_of_max_le_left nlarge - have h₄ : 3 / n ≤ ε := by - have h₅ : 3 / ε ≤ n := Nat.ceil_le.mp h₃ - refine (div_le_comm₀ ?_ εpos).mpr 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 - linarith - 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 + 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 = 3 then + else if h₈ : n = 4 then simp [h₈] - else if h₉ : n = 4 then - simp [h₉] else - have h₁₀ : 5 ≤ n := by - omega - exact exp_larger' n h₁₀ + 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 + have h₆ : 3 / (n : ℝ) - 1 / (n - 1) = (2 * n - 3) / (n * (n - 1)) := by + have h₇ : (n : ℝ) ≠ 0 := by rw [Nat.cast_ne_zero] - linarith - have h₉ : (n : ℝ) - 1 ≠ 0 := by + 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 - have h₁₀ : 0 < n := by - linarith - rw [Nat.cast_sub h₁₀] + 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 - have h₁₁ : 2 < 2 * n := by - linarith - rw [Nat.cast_sub h₁₁] + have h₉ : ↑(2 * n - 3) = 2 * (n : ℝ) - 3 := by + rw [Nat.cast_sub (by linarith)] simp - have h₁₁ : ↑(n - 2) = (n : ℝ) - 2 := by + have h₁₀ : ↑(n - 2) = (n : ℝ) - 2 := by norm_cast - rw [h₉, h₁₀, h₁₁] at h₆ - exact h₆ - have h₉ : 0 < (2 : ℝ) ^ (n - 1) := by + 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₈ + exact (div_lt_div_iff₀ h₈ (by nlinarith)).mpr h₇ linarith linarith ring_nf at h₃
  • @@ -210,7 +197,7 @@ theorem double_sum : converges_to (fun N : ℕ => ∑ a ∈ Ico 2 N, ∑ b ∈ I
    field_simp have h₂ : 0 < (1 : ℝ) / (-1 + n) := by field_simp - linarith + omega have h₃ : ∀ b ∈ Ico 2 n, 0 < (1 : ℝ) / (b ^ (n - 1) * (b - 1)) := by intro b bico field_simp
  • @@ -218,7 +205,7 @@ theorem double_sum : converges_to (fun N : ℕ => ∑ a ∈ Ico 2 N, ∑ b ∈ I
    have h₅ : 1 < (b : ℝ) := Nat.one_lt_cast.mpr h₄ have h₆ : 0 < (b : ℝ) ^ (n - 1) := by apply pow_pos (by linarith) - apply mul_pos h₆ (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₅