Even more cleanup for Sum.lean

Changes

1 changed files (+4/-4)

• Sum.lean
  • @@ -35,7 +35,7 @@ lemma telescope_sum (n : ℕ) (h : 2 ≤ n): ∑ a ∈ Ico 2 n, ∑ b ∈ Ico 2
    exact h -- Exponentials grow quickly - lemma exp_larger (n : ℕ) (h : 2 ≤ n) : 2 * (n - 2) ≤ 2 ^ (n - 1) := by + lemma exp_larger (n : ℕ) (h : 2 ≤ n) : (n - 2) * 2 ≤ 2 ^ (n - 1) := by by_cases h : 2 < n · induction h · trivial
  • @@ -64,7 +64,7 @@ theorem double_sum : Tendsto (fun n : ℕ => ∑ a ∈ Ico 2 n, ∑ b ∈ Ico 2
    simp use max (Nat.ceil (3 / ε)) 2 intro n nlarge - have h₁ : 2 ≤ n := le_of_max_le_right nlarge + have h₁ := le_of_max_le_right nlarge constructor <;> field_simp <;> rw [telescope_sum n h₁] · -- Greater than 1 - ε suffices (∑ b ∈ Ico 2 n, (1 : ℝ) / (b ^ (n - 1) * (b - 1)) ≤ (n - 2) / 2 ^ (n - 1)) ∧ 1 / (n - 1) + (n - 2) / 2 ^ (n - 1) < ε by linarith
  • @@ -88,9 +88,9 @@ theorem double_sum : Tendsto (fun n : ℕ => ∑ a ∈ Ico 2 n, ∑ b ∈ Ico 2
    have : 1 / ((n : ℝ) - 1) ≤ 1 := div_le_one₀ (by linarith) |>.mpr (by linarith) suffices ((n : ℝ) - 2) / 2 ^ (n - 1) ≤ 1 / 2 by linarith have := exp_larger n h₁ - rw [mul_comm, ← one_mul (2 ^ (n - 1))] at this + rw [← one_mul (2 ^ (n - 1))] at this exact div_le_div_iff₀ (by norm_num) (by norm_num) |>.mpr (by norm_cast) - · have : 3 / n ≤ ε := (div_le_comm₀ (by positivity) εpos).mpr <| Nat.ceil_le.mp (le_of_max_le_left nlarge) + · have := (div_le_comm₀ (by positivity) εpos).mpr <| Nat.ceil_le.mp (le_of_max_le_left nlarge) grw [← this] have : 3 / (n : ℝ) - 1 / (n - 1) = (2 * n - 3) / (n * (n - 1)) := by field_simp