Be positive

Changes

1 changed files (+1/-3)

• Sum.lean
  • @@ -9,9 +9,7 @@ lemma geom_sum (n : ℕ) (b : ℝ) (hn : 2 ≤ n) (hb : 2 ≤ b) : ∑ a ∈ Ico
    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 - have : b ^ n ≠ 0 := by - have : 0 < b ^ n := pow_pos (by linarith) n - linarith + have : b ^ n ≠ 0 := by positivity grind [one_div, 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