Minor tweaks to Sum.lean

Changes

1 changed files (+3/-3)

• Sum.lean
  • @@ -16,8 +16,8 @@ lemma telescope_sum (n : ℕ) (h : 2 ≤ n) : ∑ a ∈ Ico 2 n, ∑ b ∈ Ico 2
    calc ∑ a ∈ Ico 2 n, ∑ b ∈ Ico 2 n, (1 : ℝ) / (b ^ a) = ∑ b ∈ Ico 2 n, ∑ a ∈ Ico 2 n, (1 : ℝ) / (b ^ a) := sum_comm _ = ∑ b ∈ Ico 2 n, ((1 : ℝ) / (b - 1) - (1 : ℝ) / b - (1 : ℝ) / (b ^ (n - 1) * (b - 1))) := by - apply Finset.sum_congr rfl - exact fun b bico ↦ geom_sum n b h <| Nat.ofNat_le_cast.mpr (List.left_le_of_mem_range' bico) + apply sum_congr rfl + exact fun b bico ↦ geom_sum n b h <| Nat.ofNat_le_cast.mpr <| List.left_le_of_mem_range' bico _ = ∑ 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 suffices ∑ b ∈ Ico 2 n, ((1 : ℝ) / (b - 1) - (1 : ℝ) / b) = 1 - (1 : ℝ) / (n - 1) by rw [this]
  • @@ -43,7 +43,7 @@ lemma exp_larger' (n : ℕ) (h : 2 ≤ n) : (n - 2) * (n * (n - 1)) < (2 * n - 3
    grind suffices 2 ^ (n + 1) ≤ (2 * n - 3) * 2 ^ (n - 1) by lia have : 2 ^ (n + 1) = 4 * 2 ^ (n - 1) := by grind [mul_pow_sub_one] - simp only [this, Nat.ofNat_pos, pow_pos, mul_le_mul_iff_left₀, ge_iff_le] + rw [this, mul_le_mul_iff_left₀ (by positivity)] grind · interval_cases n <;> decide