refactor(geo_sum): remove duplicate proofs about geometric sums (#706)

* feat(data/finset): add range_add_one

* feat(algebra/big_operators): geometric sum for semiring, ring and division ring

* refactor(geo_sum): remove duplicate proofs about geometric sums

Author: ChrisHughes24

src/algebra/big_operators.lean

@@ -549,11 +549,24 @@ theorem geom_sum_mul [ring α] (x : α) (n : ℕ) :
 have _ := geom_sum_mul_add (x-1) n,
 by rw [sub_add_cancel] at this; rw [← this, add_sub_cancel]
 
-theorem geom_sum [division_ring α] (x : α) (h : x ≠ 1) (n : ℕ) :
+theorem geom_sum [division_ring α] {x : α} (h : x ≠ 1) (n : ℕ) :
   (range n).sum (λ i, x^i) = (x^n-1)/(x-1) :=
 have x - 1 ≠ 0, by simp [*, -sub_eq_add_neg, sub_eq_iff_eq_add] at *,
 by rw [← geom_sum_mul, mul_div_cancel _ this]
 
+lemma geom_sum_inv [division_ring α] {x : α} (hx1 : x ≠ 1) (hx0 : x ≠ 0) (n : ℕ) :
+  (range n).sum (λ m, x⁻¹ ^ m) = (x - 1)⁻¹ * (x - x⁻¹ ^ n * x) :=
+have h₁ : x⁻¹ ≠ 1, by rwa [inv_eq_one_div, ne.def, div_eq_iff_mul_eq hx0, one_mul],
+have h₂ : x⁻¹ - 1 ≠ 0, from mt sub_eq_zero.1 h₁,
+have h₃ : x - 1 ≠ 0, from mt sub_eq_zero.1 hx1,
+have h₄ : x * x⁻¹ ^ n = x⁻¹ ^ n * x,
+  from nat.cases_on n (by simp)
+  (λ _, by conv { to_rhs, rw [pow_succ', mul_assoc, inv_mul_cancel hx0, mul_one] };
+    rw [pow_succ, ← mul_assoc, mul_inv_cancel hx0, one_mul]),
+by rw [geom_sum h₁, div_eq_iff_mul_eq h₂, ← domain.mul_left_inj h₃,
+    ← mul_assoc, ← mul_assoc, mul_inv_cancel h₃];
+  simp [mul_add, add_mul, mul_inv_cancel hx0, mul_assoc, h₄]
+
 end geom_sum
 
 section group

src/analysis/specific_limits.lean

@@ -154,21 +154,6 @@ lemma tendsto_one_div_add_at_top_nhds_0_nat : tendsto (λ n : ℕ, 1 / ((n : ℝ
 suffices tendsto (λ n : ℕ, 1 / (↑(n + 1) : ℝ)) at_top (nhds 0), by simpa,
 tendsto_comp_succ_at_top_iff.2 tendsto_one_div_at_top_nhds_0_nat
 
-lemma sum_geometric' {r : ℝ} (h : r ≠ 0) :
-  ∀{n}, (finset.range n).sum (λi, (r + 1) ^ i) = ((r + 1) ^ n - 1) / r
-| 0     := by simp [zero_div]
-| (n+1) :=
-  by simp [@sum_geometric' n, h, pow_succ, range_succ, add_div_eq_mul_add_div, add_mul, mul_comm, mul_assoc]
-
-lemma sum_geometric {r : ℝ} {n : ℕ} (h : r ≠ 1) :
-  (range n).sum (λi, r ^ i) = (r ^ n - 1) / (r - 1) :=
-calc (range n).sum (λi, r ^ i) = (range n).sum (λi, ((r - 1) + 1) ^ i) :
-    by simp
-  ... = (((r - 1) + 1) ^ n - 1) / (r - 1) :
-    sum_geometric' $ by simp [sub_eq_iff_eq_add, -sub_eq_add_neg, h]
-  ... = (r ^ n - 1) / (r - 1) :
-    by simp
-
 lemma is_sum_geometric {r : ℝ} (h₁ : 0 ≤ r) (h₂ : r < 1) :
   is_sum (λn:ℕ, r ^ n) (1 / (1 - r)) :=
 have r ≠ 1, from ne_of_lt h₂,
@@ -178,7 +163,7 @@ have tendsto (λn, (r ^ n - 1) * (r - 1)⁻¹) at_top (nhds ((0 - 1) * (r - 1)
   from tendsto_mul
     (tendsto_sub (tendsto_pow_at_top_nhds_0_of_lt_1 h₁ h₂) tendsto_const_nhds) tendsto_const_nhds,
 (is_sum_iff_tendsto_nat_of_nonneg $ pow_nonneg h₁).mpr $
-  by simp [neg_inv, sum_geometric, div_eq_mul_inv, *] at *
+  by simp [neg_inv, geom_sum, div_eq_mul_inv, *] at *
 
 lemma is_sum_geometric_two (a : ℝ) : is_sum (λn:ℕ, (a / 2) / 2 ^ n) a :=
 begin

src/data/complex/basic.lean

@@ -218,19 +218,19 @@ ext_iff.2 $ begin
   rw [← div_div_eq_div_mul, div_self h, one_div_eq_inv]
 end
 
-lemma inv_zero : (0⁻¹ : ℂ) = 0 :=
+protected lemma inv_zero : (0⁻¹ : ℂ) = 0 :=
 by rw [← of_real_zero, ← of_real_inv, inv_zero]
 
-theorem mul_inv_cancel {z : ℂ} (h : z ≠ 0) : z * z⁻¹ = 1 :=
+protected theorem mul_inv_cancel {z : ℂ} (h : z ≠ 0) : z * z⁻¹ = 1 :=
 by rw [inv_def, ← mul_assoc, mul_conj, ← of_real_mul,
   mul_inv_cancel (mt norm_sq_eq_zero.1 h), of_real_one]
 
 noncomputable instance : discrete_field ℂ :=
 { inv := has_inv.inv,
   zero_ne_one := mt (congr_arg re) zero_ne_one,
-  mul_inv_cancel := @mul_inv_cancel,
-  inv_mul_cancel := λ z h, by rw [mul_comm, mul_inv_cancel h],
-  inv_zero := inv_zero,
+  mul_inv_cancel := @complex.mul_inv_cancel,
+  inv_mul_cancel := λ z h, by rw [mul_comm, complex.mul_inv_cancel h],
+  inv_zero := complex.inv_zero,
   has_decidable_eq := classical.dec_eq _,
   ..complex.comm_ring }
 

src/data/complex/exponential.lean

@@ -14,22 +14,6 @@ open is_absolute_value
 section
 open real is_absolute_value finset
 
-lemma geo_sum_eq {α : Type*} [field α] {x : α} : ∀ (n : ℕ) (hx1 : x ≠ 1),
-  (range n).sum (λ m, x ^ m) = (1 - x ^ n) / (1 - x)
-| 0     hx1 := by simp
-| (n+1) hx1 := have 1 - x ≠ 0 := mt sub_eq_zero_iff_eq.1 hx1.symm,
-by rw [sum_range_succ, ← mul_div_cancel (x ^ n) this, geo_sum_eq n hx1, ← add_div, _root_.pow_succ];
-    simp [mul_add, add_mul, mul_comm]
-
-lemma geo_sum_inv_eq {α : Type*} [discrete_field α] {x : α} (n : ℕ) (hx1 : x ≠ 1) (hx0 : x ≠ 0) :
-  (range n).sum (λ m, x⁻¹ ^ m) = (x - x * x⁻¹ ^ n) / (x - 1) :=
-have hx1' : x⁻¹ ≠ 1, from λ h, by rw [← @inv_inv' _ _ x, h] at hx1; simpa using hx1,
-have h1x' : 1 - x⁻¹ ≠ 0, from sub_ne_zero.2 hx1'.symm,
-have h1x : x - 1 ≠ 0, from sub_ne_zero.2 hx1,
-by rw [geo_sum_eq _ hx1', div_eq_div_iff h1x' h1x];
-  simp [mul_add, add_mul, mul_inv_cancel hx0, mul_comm x, mul_left_comm x,
-    mul_assoc, inv_mul_cancel hx0]
-
 lemma forall_ge_le_of_forall_le_succ {α : Type*} [preorder α] (f : ℕ → α) {m : ℕ}
   (h : ∀ n ≥ m, f n.succ ≤ f n) : ∀ {l}, ∀ k ≥ m, k ≤ l → f l ≤ f k :=
 begin
@@ -122,10 +106,11 @@ lemma is_cau_geo_series {β : Type*} [field β] {abv : β → α} [is_absolute_v
 have hx1' : abv x ≠ 1 := λ h, by simpa [h, lt_irrefl] using hx1,
 is_cau_series_of_abv_cau
 begin
-  simp only [abv_pow abv, geo_sum_eq _ hx1'] {eta := ff},
+  simp only [abv_pow abv, geom_sum hx1'] {eta := ff},
+  conv in (_ / _) { rw [← neg_div_neg_eq, neg_sub, neg_sub] },
   refine @is_cau_of_mono_bounded _ _ _ _ ((1 : α) / (1 - abv x)) 0 _ _,
   { assume n hn,
-    rw abs_of_nonneg ,
+    rw abs_of_nonneg,
     refine div_le_div_of_le_of_pos (sub_le_self _ (abv_pow abv x n ▸ abv_nonneg _ _))
       (sub_pos.2 hx1),
     refine div_nonneg (sub_nonneg.2 _) (sub_pos.2 hx1),
@@ -877,12 +862,11 @@ calc (filter (λ k, n ≤ k) (range j)).sum (λ m : ℕ, (1 / m.fact : α))
   have h₂ : (n.succ : α) ≠ 0, from nat.cast_ne_zero.2 (nat.succ_ne_zero _),
   have h₃ : (n.fact * n : α) ≠ 0, from mul_ne_zero (nat.cast_ne_zero.2 (nat.pos_iff_ne_zero.1 (nat.fact_pos _)))
     (nat.cast_ne_zero.2 (nat.pos_iff_ne_zero.1 hn)),
-  have h₄ : (n.succ - 1 : α) * (n.fact : ℕ) ≠ 0,
-    from mul_ne_zero (sub_ne_zero.2 h₁)
-      (nat.cast_ne_zero.2 (nat.pos_iff_ne_zero.1 (nat.fact_pos _))),
-  by rw [geo_sum_inv_eq _ h₁ h₂, mul_comm, ← div_eq_mul_inv, div_div_eq_div_mul,
-      div_eq_div_iff h₄ h₃];
-    simp [mul_add, add_mul, mul_comm, mul_assoc, mul_left_comm]
+  have h₄ : (n.succ - 1 : α) = n, by simp,
+  by rw [geom_sum_inv h₁ h₂, eq_div_iff_mul_eq _ _ h₃, mul_comm _ (n.fact * n : α),
+      ← mul_assoc (n.fact⁻¹ : α), ← mul_inv', h₄, ← mul_assoc (n.fact * n : α),
+      mul_comm (n : α) n.fact, mul_inv_cancel h₃];
+    simp [mul_add, add_mul, mul_assoc, mul_comm]
 ... ≤ n.succ / (n.fact * n) :
   begin
     refine (div_le_div_right (mul_pos _ _)).2 _,