More minor simplifications for Sum.lean

Changes

1 changed files (+6/-7)

• Sum.lean
  • @@ -7,10 +7,10 @@ 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)) := 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] + rw [this, geom_sum_Ico (by grind) hn] field_simp have : b ^ n ≠ 0 := by positivity - grind [one_div, inv_pow, mul_pow_sub_one] + grind [inv_pow, 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 calc
  • @@ -31,7 +31,7 @@ lemma telescope_sum (n : ℕ) (h : 2 ≤ n) : ∑ a ∈ Ico 2 n, ∑ b ∈ Ico 2
    lemma exp_larger (n : ℕ) (h : 2 ≤ n) : (n - 2) * 2 ≤ 2 ^ (n - 1) := by by_cases h : 2 < n · induction h - · trivial + · decide · grind [mul_pow_sub_one] · grind
  • @@ -40,7 +40,7 @@ lemma exp_larger' (n : ℕ) (h : 2 ≤ n) : (n - 2) * (n * (n - 1)) < (2 * n - 3
    by_cases h : 4 < n · have : n * (n - 1) * (n - 2) < 2 ^ (n + 1) := by induction h - · trivial + · decide · rename_i m _ _ suffices (m + 1) * (m * (m - 1)) ≤ 2 * (m - 2) * (m * (m - 1)) by grind apply Nat.mul_le_mul_right (m * (m - 1))
  • @@ -49,7 +49,7 @@ lemma exp_larger' (n : ℕ) (h : 2 ≤ n) : (n - 2) * (n * (n - 1)) < (2 * n - 3
    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] grind - · interval_cases n <;> trivial + · interval_cases n <;> decide 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)]
  • @@ -101,6 +101,5 @@ theorem double_sum : Tendsto (fun n : ℕ ↦ ∑ a ∈ Ico 2 n, ∑ b ∈ Ico 2
    rw [one_div_nonneg] have : 1 < (b : ℝ) := Nat.one_lt_cast.mpr (List.left_le_of_mem_range' bico) exact mul_nonneg (pow_nonneg (by linarith) (n - 1)) (by linarith) - have := sum_nonneg h₂ have : 0 < (1 : ℝ) / (n - 1) := by simp [Nat.one_lt_cast.mpr h₁] - grind + grind [sum_nonneg h₂]