Sum.lean is now only half as long!

Changes

1 changed files (+42/-68)

• Sum.lean
  • @@ -6,9 +6,7 @@ lemma geom_sum (b : ℝ) (N : ℕ) (h₁ : 2 ≤ N) (h₂ : 2 ≤ b) : ∑ a ∈
    calc ∑ a ∈ Ico 2 N, 1 / (b ^ a) = ∑ a ∈ Ico 2 N, (1 / b) ^ a := by simp _ = ((1 / b) ^ 2 - (1 / b) ^ N) / (1 - (1 / b)) := by - rw [geom_sum_Ico'] - grind - exact h₁ + rw [geom_sum_Ico' (by grind) h₁] _ = 1 / (b - 1) - 1 / b - b / (b ^ N * (b - 1)) := by have : b - 1 ≠ 0 := by linarith field_simp
  • @@ -34,7 +32,7 @@ lemma telescope_sum (N : ℕ) (h : 2 ≤ N): ∑ a ∈ Ico 2 N, ∑ b ∈ Ico 2
    induction h with | refl => field_simp - linarith + norm_num | step h ih => rw [sum_Ico_succ_top, ih] field_simp
  • @@ -46,33 +44,22 @@ lemma exp_larger (n : ℕ) (h : 3 ≤ n) : 2 * (n - 2) ≤ 2 ^ (n - 1) := by
    | refl => trivial | step a a_ih => - rename_i m - simp - simp at a - rw [← mul_pow_sub_one] - grind - omega + grind [mul_pow_sub_one] -- Another similar lemma lemma exp_larger' (n : ℕ) (h : 5 ≤ n) : n * (n - 1) * (n - 2) < (2 * n - 3) * 2 ^ (n - 1) := by - have h₁ : n * (n - 1) * (n - 2) < 2 ^ (n + 1) := by + have : n * (n - 1) * (n - 2) < 2 ^ (n + 1) := by induction h with | refl => trivial | step a a_ih => rename_i m - simp - simp at a - 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] + suffices (m + 1) * (m * (m - 1)) ≤ 2 * (m - 2) * (m * (m - 1)) by grind apply Nat.mul_le_mul_right (m * (m - 1)) - omega + grind suffices 2 ^ (n + 1) ≤ (2 * n - 3) * 2 ^ (n - 1) by linarith - have h₂ : 2 ^ (n + 1) = 2 * (2 * 2 ^ (n - 1)) := by grind [mul_pow_sub_one] - rw [h₂, ← mul_assoc] - apply Nat.mul_le_mul_right (2 ^ (n - 1)) + have : 2 ^ (n + 1) = 4 * 2 ^ (n - 1) := by grind [mul_pow_sub_one] + simp [this] omega theorem double_sum : Tendsto (fun N : ℕ => ∑ a ∈ Ico 2 N, ∑ b ∈ Ico 2 N, (1 : ℝ) / (b ^ a)) atTop (𝓝 (1 : ℝ)) := by
  • @@ -83,19 +70,14 @@ theorem double_sum : Tendsto (fun N : ℕ => ∑ a ∈ Ico 2 N, ∑ b ∈ Ico 2
    use max (Nat.ceil (3 / ε)) 2 intro n nlarge have h₁ : 2 ≤ n := le_of_max_le_right nlarge - constructor + constructor <;> field_simp <;> rw [telescope_sum n h₁] <;> ring_nf · -- Greater than 1 - ε - field_simp - rw [telescope_sum n h₁] 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₃ b (bico : b ∈ Ico 2 n) : (1 : ℝ) / (b ^ (n - 1) * (b - 1)) ≤ 1 / 2 ^ (n - 1) := by have h₄ : 2 ≤ (b : ℝ) := by norm_num 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 : ℝ) - 1) ≤ 1 := (div_le_one₀ (by linarith)).mpr (by linarith) have h₆ : 1 / (b : ℝ) ^ (n - 1) ≤ 1 / 2 ^ (n - 1) := by rw [← one_div_pow, ← one_div_pow] apply pow_le_pow_left₀ (by norm_num)
  • @@ -109,10 +91,11 @@ theorem double_sum : Tendsto (fun N : ℕ => ∑ a ∈ Ico 2 N, ∑ b ∈ Ico 2
    field_simp at h₄ field_simp exact h₄ + ring_nf at h₂ have h₃ : 1 < 1 + ε - 1 / (n - 1) - (n - 2) / 2 ^ (n - 1) := by suffices 1 / (n - 1) + (n - 2) / 2 ^ (n - 1) < ε by linarith - if hε : 3 / 2 < ε then - have : 2 ≤ (n : ℝ) := Nat.ofNat_le_cast.mpr h₁ + by_cases hε : 3 / 2 < ε + · have : 2 ≤ (n : ℝ) := Nat.ofNat_le_cast.mpr h₁ have : 1 / ((n : ℝ) - 1) ≤ 1 := div_le_one₀ (by linarith) |>.mpr (by linarith) suffices ((n : ℝ) - 2) / 2 ^ (n - 1) ≤ 1 / 2 by linarith have h₄ : 2 * (n - 2) ≤ 2 ^ (n - 1) := by
  • @@ -121,56 +104,47 @@ theorem double_sum : Tendsto (fun N : ℕ => ∑ a ∈ Ico 2 N, ∑ b ∈ Ico 2
    · grind 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 + · simp at hε + have : 3 / n ≤ ε := by + have h₃ : 3 / ε ≤ n := Nat.ceil_le.mp (le_of_max_le_left nlarge) + have h₄ : 0 < (n : ℝ) := by + norm_num + omega + exact (div_le_comm₀ h₄ εpos).mpr h₃ 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 - by_cases h₅ : n > 4 - · exact exp_larger' n h₅ - · interval_cases n <;> simp rw [← lt_sub_iff_add_lt'] - have h₅ : 3 / (n : ℝ) - 1 / (n - 1) = (2 * n - 3) / (n * (n - 1)) := by + have h₃ : 3 / (n : ℝ) - 1 / (n - 1) = (2 * n - 3) / (n * (n - 1)) := by have : (n : ℝ) ≠ 0 := by grind [Nat.cast_ne_zero] have : (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 [h₃] + have h₄ : ((n : ℝ) - 2) * (n * (n - 1)) < (2 * n - 3) * 2 ^ (n - 1) := by + have h₅ : n * (n - 1) * (n - 2) < (2 * n - 3) * 2 ^ (n - 1) := by + by_cases h₆ : n > 4 + · exact exp_larger' n h₆ + · interval_cases n <;> simp + 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 * n - 3) = 2 * (n : ℝ) - 3 := by rw [Nat.cast_sub (by linarith)] simp - have h₉ : ↑(n - 2) = (n : ℝ) - 2 := by norm_cast - rwa [h₇, h₈, h₉] at h₄ - have h₇ : 0 < (2 : ℝ) ^ (n - 1) := by norm_num - exact (div_lt_div_iff₀ h₇ (by nlinarith)).mpr h₆ - ring_nf - ring_nf at h₂ + have h₈ : ↑(n - 2) = (n : ℝ) - 2 := by norm_cast + rwa [h₆, h₇, h₈] at 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 - field_simp - rw [telescope_sum n h₁] - ring_nf - field_simp - have : 0 < (1 : ℝ) / (-1 + n) := by - field_simp - omega - have h₂ : ∀ b ∈ Ico 2 n, 0 < (1 : ℝ) / (b ^ (n - 1) * (b - 1)) := by - intro b bico + have h₂ b (bico : b ∈ Ico 2 n) : 0 < (1 : ℝ) / (b ^ (n - 1) * (b - 1)) := by field_simp have : 1 < (b : ℝ) := Nat.one_lt_cast.mpr (List.left_le_of_mem_range' bico) - have 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)) := sum_nonneg (fun b a => le_of_lt (h₂ b a)) - field_simp at h₃ + exact mul_pos (pow_pos (by linarith) (n - 1)) (by linarith) + have : 0 ≤ ∑ b ∈ Ico 2 n, (1 : ℝ) / (b ^ (n - 1) * (b - 1)) := sum_nonneg (fun b a => le_of_lt (h₂ b a)) + have : 0 < (1 : ℝ) / (n - 1) := by + field_simp + omega grind