More Sum.lean golf

Changes

1 changed files (+3/-6)

• Sum.lean
  • @@ -17,15 +17,12 @@ lemma telescope_sum (n : ℕ) (h : 2 ≤ n) : ∑ a ∈ Ico 2 n, ∑ b ∈ Ico 2
    ∑ 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 - intro b bico - exact geom_sum n b h <| Nat.ofNat_le_cast.mpr (List.left_le_of_mem_range' bico) + 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] induction h with - | refl => - simp - norm_num + | refl => norm_num | step h ih => rw [sum_Ico_succ_top h, ih] simp
  • @@ -69,7 +66,7 @@ theorem double_sum : Tendsto (fun n : ℕ ↦ ∑ a ∈ Ico 2 n, ∑ b ∈ Ico 2
    · have h₂ b (bico : b ∈ Ico 2 n) : (1 : ℝ) / (b ^ (n - 1) * (b - 1)) ≤ 1 / 2 ^ (n - 1) := by rw [← one_div_mul_one_div] have h₃ : 2 ≤ (b : ℝ) := by - norm_num + norm_cast exact (List.left_le_of_mem_range' bico) 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