Simplify geom_sum proof, rename N to n everywhere

Changes

1 changed files (+17/-25)

• Sum.lean
  • @@ -5,34 +5,26 @@ import Mathlib.Tactic.Rify
    open Finset Filter Topology -- Important: b should be in ℝ so that it's real div not nat div - lemma geom_sum (N : ℕ) (b : ℝ) (hN : 2 ≤ N) (hb : 2 ≤ b) : ∑ a ∈ Ico 2 N, 1 / (b ^ a) = 1 / (b - 1) - 1 / b - 1 / (b ^ (N - 1) * (b - 1)) := - 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' (by grind) hN] - _ = 1 / (b - 1) - 1 / b - b / (b ^ N * (b - 1)) := by - have : b - 1 ≠ 0 := by linarith - field_simp - ring_nf - rw [mul_assoc, ← mul_pow, mul_inv_cancel₀ (by linarith)] - simp - _ = 1 / (b - 1) - 1 / b - 1 / (b ^ (N - 1) * (b - 1)) := by - have h₁ : b ≠ 0 := by linarith - have h₂ : b ^ N * (b - 1) = b * (b ^ (N - 1) * (b - 1)) := by - rw [← mul_assoc, ← pow_succ' b (N - 1), Nat.sub_one_add_one] - linarith - simp [h₂, div_mul_cancel_left₀ h₁] + lemma geom_sum (n : ℕ) (b : ℝ) (hn : 2 ≤ n) (hb : 2 ≤ b) : ∑ a ∈ Ico 2 n, 1 / (b ^ a) = 1 / (b - 1) - 1 / b - 1 / (b ^ (n - 1) * (b - 1)) := by + have : ∑ a ∈ Ico 2 n, 1 / (b ^ a) = ∑ a ∈ Ico 2 n, (1 / b) ^ a := by simp + rw [this, geom_sum_Ico' (by grind) hn] + field_simp + simp + have : b ^ n ≠ 0 := by + have : 0 < b ^ n := pow_pos (by linarith) n + linarith + grind [mul_pow_sub_one] - lemma telescope_sum (N : ℕ) (h : 2 ≤ N): ∑ a ∈ Ico 2 N, ∑ b ∈ Ico 2 N, (1 : ℝ) / (b ^ a) = 1 - (1 : ℝ) / (N - 1) - ∑ b ∈ Ico 2 N, (1 : ℝ) / (b ^ (N - 1) * (b - 1)) := by + lemma telescope_sum (n : ℕ) (h : 2 ≤ n): ∑ a ∈ Ico 2 n, ∑ b ∈ Ico 2 n, (1 : ℝ) / (b ^ a) = 1 - (1 : ℝ) / (n - 1) - ∑ b ∈ Ico 2 n, (1 : ℝ) / (b ^ (n - 1) * (b - 1)) := by 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 + ∑ 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) - _ = ∑ 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] + exact 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
  • @@ -66,7 +58,7 @@ lemma exp_larger' (n : ℕ) (h : 2 ≤ n) : (n - 2) * (n * (n - 1)) < (2 * n - 3
    omega · interval_cases n <;> simp - theorem double_sum : Tendsto (fun N : ℕ => ∑ a ∈ Ico 2 N, ∑ b ∈ Ico 2 N, (1 : ℝ) / (b ^ a)) atTop (𝓝 (1 : ℝ)) := by + theorem double_sum : Tendsto (fun n : ℕ => ∑ a ∈ Ico 2 n, ∑ b ∈ Ico 2 n, (1 : ℝ) / (b ^ a)) atTop (𝓝 (1 : ℝ)) := by rw [atTop_basis.tendsto_iff (nhds_basis_Ioo_pos 1)] intro ε εpos simp