refactor(algebra/geom_sum): remove definition (#14120)

There's no need to have a separate definition `geom_sum := ∑ i in range n, x ^ i`. Instead it's better to just write the lemmas about the sum itself: that way `simp` lemmas fire "in the wild", without needing to rewrite expression in terms of `geom_sum` manually.




Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

archive/100-theorems-list/70_perfect_numbers.lean

@@ -34,8 +34,7 @@ open arithmetic_function finset
 open_locale arithmetic_function
 
 lemma sigma_two_pow_eq_mersenne_succ (k : ℕ) : σ 1 (2 ^ k) = mersenne (k + 1) :=
-by simpa [mersenne, prime_two, ← geom_sum_mul_add 1 (k+1)]
-
+by simp [mersenne, prime_two, ← geom_sum_mul_add 1 (k+1)]
 
 /-- Euclid's theorem that Mersenne primes induce perfect numbers -/
 theorem perfect_two_pow_mul_mersenne_of_prime (k : ℕ) (pr : (mersenne (k + 1)).prime) :

docs/100.yaml

@@ -228,7 +228,7 @@
 66:
   title  : Sum of a Geometric Series
   decls  :
-    - geom_sum
+    - geom_sum_Ico
     - nnreal.has_sum_geometric
   author : Sander R. Dahmen (finite) and Johannes Hölzl (infinite)
 67:

src/analysis/normed_space/units.lean

@@ -120,14 +120,14 @@ begin
   simp only [inverse_one_sub t ht, set.mem_set_of_eq],
   have h : 1 = ((range n).sum (λ i, t ^ i)) * (units.one_sub t ht) + t ^ n,
   { simp only [units.coe_one_sub],
-    rw [← geom_sum, geom_sum_mul_neg],
+    rw [geom_sum_mul_neg],
     simp },
   rw [← one_mul ↑(units.one_sub t ht)⁻¹, h, add_mul],
   congr,
   { rw [mul_assoc, (units.one_sub t ht).mul_inv],
     simp },
   { simp only [units.coe_one_sub],
-    rw [← add_mul, ← geom_sum, geom_sum_mul_neg],
+    rw [← add_mul, geom_sum_mul_neg],
     simp }
 end
 

src/analysis/special_functions/log/deriv.lean

@@ -207,7 +207,7 @@ begin
     have : (∑ i in range n, (↑i + 1) * y ^ i / (↑i + 1)) = (∑ i in range n, y ^ i),
     { congr' with i,
       exact mul_div_cancel_left _ (nat.cast_add_one_pos i).ne' },
-    field_simp [F, this, ← geom_sum_def, geom_sum_eq (ne_of_lt hy.2),
+    field_simp [F, this, geom_sum_eq (ne_of_lt hy.2),
                 sub_ne_zero_of_ne (ne_of_gt hy.2), sub_ne_zero_of_ne (ne_of_lt hy.2)],
     ring },
   -- second step: show that the derivative of `F` is small

src/analysis/specific_limits/basic.lean

@@ -138,7 +138,6 @@ lemma has_sum_geometric_of_lt_1 {r : ℝ} (h₁ : 0 ≤ r) (h₂ : r < 1) :
 have r ≠ 1, from ne_of_lt h₂,
 have tendsto (λn, (r ^ n - 1) * (r - 1)⁻¹) at_top (𝓝 ((0 - 1) * (r - 1)⁻¹)),
   from ((tendsto_pow_at_top_nhds_0_of_lt_1 h₁ h₂).sub tendsto_const_nhds).mul tendsto_const_nhds,
-have (λ n, (∑ i in range n, r ^ i)) = (λ n, geom_sum r n) := rfl,
 (has_sum_iff_tendsto_nat_of_nonneg (pow_nonneg h₁) _).mpr $
   by simp [neg_inv, geom_sum_eq, div_eq_mul_inv, *] at *
 

src/analysis/specific_limits/normed.lean

@@ -262,8 +262,7 @@ begin
   have xi_ne_one : ξ ≠ 1, by { contrapose! h, simp [h] },
   have A : tendsto (λn, (ξ ^ n - 1) * (ξ - 1)⁻¹) at_top (𝓝 ((0 - 1) * (ξ - 1)⁻¹)),
     from ((tendsto_pow_at_top_nhds_0_of_norm_lt_1 h).sub tendsto_const_nhds).mul tendsto_const_nhds,
-  have B : (λ n, (∑ i in range n, ξ ^ i)) = (λ n, geom_sum ξ n) := rfl,
-  rw [has_sum_iff_tendsto_nat_of_summable_norm, B],
+  rw [has_sum_iff_tendsto_nat_of_summable_norm],
   { simpa [geom_sum_eq, xi_ne_one, neg_inv, div_eq_mul_inv] using A },
   { simp [norm_pow, summable_geometric_of_lt_1 (norm_nonneg _) h] }
 end
@@ -453,7 +452,7 @@ begin
   { simpa using tendsto_const_nhds.sub (tendsto_pow_at_top_nhds_0_of_norm_lt_1 h) },
   convert ← this,
   ext n,
-  rw [←geom_sum_mul_neg, geom_sum_def, finset.sum_mul],
+  rw [←geom_sum_mul_neg, finset.sum_mul],
 end
 
 lemma mul_neg_geom_series (x : R) (h : ∥x∥ < 1) :
@@ -466,7 +465,7 @@ begin
       (tendsto_pow_at_top_nhds_0_of_norm_lt_1 h) },
   convert ← this,
   ext n,
-  rw [←mul_neg_geom_sum, geom_sum_def, finset.mul_sum]
+  rw [←mul_neg_geom_sum, finset.mul_sum]
 end
 
 end normed_ring_geometric
@@ -581,7 +580,7 @@ begin
 end
 
 lemma norm_sum_neg_one_pow_le (n : ℕ) : ∥∑ i in range n, (-1 : ℝ) ^ i∥ ≤ 1 :=
-by { rw [←geom_sum_def, neg_one_geom_sum], split_ifs; norm_num }
+by { rw [neg_one_geom_sum], split_ifs; norm_num }
 
 /-- The **alternating series test** for monotone sequences.
 See also `tendsto_alternating_series_of_monotone_tendsto_zero`. -/

src/combinatorics/colex.lean

@@ -94,7 +94,7 @@ lemma nat.sum_two_pow_lt {k : ℕ} {A : finset ℕ} (h₁ : ∀ {x}, x ∈ A →
 begin
   apply lt_of_le_of_lt (sum_le_sum_of_subset (λ t, mem_range.2 ∘ h₁)),
   have z := geom_sum_mul_add 1 k,
-  rw [geom_sum, mul_one, one_add_one_eq_two] at z,
+  rw [mul_one, one_add_one_eq_two] at z,
   rw ← z,
   apply nat.lt_succ_self,
 end

src/data/complex/exponential.lean

@@ -117,10 +117,7 @@ lemma is_cau_geo_series {β : Type*} [ring β] [nontrivial β] {abv : β → α}
 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] {eta := ff},
-  have : (λ (m : ℕ), ∑ n in range m, (abv x) ^ n) =
-   λ m, geom_sum (abv x) m := rfl,
-  simp only [this, geom_sum_eq hx1'] {eta := ff},
+  simp only [abv_pow abv, geom_sum_eq hx1'],
   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,
@@ -1238,7 +1235,7 @@ calc ∑ m in filter (λ k, n ≤ k) (range j), (1 / m! : α)
     from mul_ne_zero (nat.cast_ne_zero.2 (pos_iff_ne_zero.1 (nat.factorial_pos _)))
     (nat.cast_ne_zero.2 (pos_iff_ne_zero.1 hn)),
   have h₄ : (n.succ - 1 : α) = n, by simp,
-  by rw [← geom_sum_def, geom_sum_inv h₁ h₂, eq_div_iff_mul_eq h₃,
+  by rw [geom_sum_inv h₁ h₂, eq_div_iff_mul_eq h₃,
       mul_comm _ (n! * n : α), ← mul_assoc (n!⁻¹ : α), ← mul_inv_rev, h₄,
       ← mul_assoc (n! * n : α), mul_comm (n : α) n!, mul_inv_cancel h₃];
     simp [mul_add, add_mul, mul_assoc, mul_comm]
@@ -1309,7 +1306,7 @@ begin
   { rw [←mul_sum],
     apply mul_le_mul_of_nonneg_left,
     { simp_rw [←div_pow],
-      rw [←geom_sum_def, geom_sum_eq, div_le_iff_of_neg],
+      rw [geom_sum_eq, div_le_iff_of_neg],
       { transitivity (-1 : ℝ),
         { linarith },
         { simp only [neg_le_sub_iff_le_add, div_pow, nat.cast_succ, le_add_iff_nonneg_left],

src/data/polynomial/eval.lean

@@ -830,8 +830,9 @@ lemma eval_eq_zero_of_dvd_of_eval_eq_zero : p ∣ q → eval x p = 0 → eval x
 eval₂_eq_zero_of_dvd_of_eval₂_eq_zero _ _
 
 @[simp]
-lemma eval_geom_sum {R} [comm_semiring R] {n : ℕ} {x : R} : eval x (geom_sum X n) = geom_sum x n :=
-by simp [geom_sum_def, eval_finset_sum]
+lemma eval_geom_sum {R} [comm_semiring R] {n : ℕ} {x : R} :
+  eval x (∑ i in range n, X ^ i) = ∑ i in range n, x ^ i :=
+by simp [eval_finset_sum]
 
 end
 

src/data/real/pi/leibniz.lean

@@ -92,7 +92,7 @@ begin
     convert (has_deriv_at_arctan x).sub (has_deriv_at.sum has_deriv_at_b),
     have g_sum :=
       @geom_sum_eq _ _ (-x^2) ((neg_nonpos.mpr (sq_nonneg x)).trans_lt zero_lt_one).ne k,
-    simp only [geom_sum, f'] at g_sum ⊢,
+    simp only [f'] at g_sum ⊢,
     rw [g_sum, ← neg_add' (x^2) 1, add_comm (x^2) 1, sub_eq_add_neg, neg_div', neg_div_neg_eq],
     ring },
   have hderiv1 : ∀ x ∈ Icc (U:ℝ) 1, has_deriv_within_at f (f' x) (Icc (U:ℝ) 1) x :=

src/linear_algebra/adic_completion.lean

@@ -211,17 +211,18 @@ h.1.subsingleton
 @[priority 100] instance of_subsingleton [subsingleton M] : is_adic_complete I M := {}
 
 open_locale big_operators
+open finset
 
 lemma le_jacobson_bot [is_adic_complete I R] : I ≤ (⊥ : ideal R).jacobson :=
 begin
   intros x hx,
   rw [← ideal.neg_mem_iff, ideal.mem_jacobson_bot],
   intros y,
   rw add_comm,
-  let f : ℕ → R := geom_sum (x * y),
+  let f : ℕ → R := λ n, ∑ i in range n, (x * y) ^ i,
   have hf : ∀ m n, m ≤ n → f m ≡ f n [SMOD I ^ m • (⊤ : submodule R R)],
   { intros m n h,
-    simp only [f, geom_sum_def, algebra.id.smul_eq_mul, ideal.mul_top, smodeq.sub_mem],
+    simp only [f, algebra.id.smul_eq_mul, ideal.mul_top, smodeq.sub_mem],
     rw [← add_tsub_cancel_of_le h, finset.sum_range_add, ← sub_sub, sub_self, zero_sub,
       neg_mem_iff],
     apply submodule.sum_mem,

src/number_theory/bernoulli.lean

@@ -307,7 +307,7 @@ begin
     { have h_const : C ℚ (constant_coeff ℚ (exp ℚ ^ n)) = 1 := by simp,
       rw [← h_const, sub_const_eq_X_mul_shift] },
     -- key step: a chain of equalities of power series
-    rw [← mul_right_inj' hexp, mul_comm, ← exp_pow_sum, ← geom_sum_def, geom_sum_mul, h_r,
+    rw [← mul_right_inj' hexp, mul_comm, ← exp_pow_sum, geom_sum_mul, h_r,
         ← bernoulli_power_series_mul_exp_sub_one, bernoulli_power_series, mul_right_comm],
     simp [h_cauchy, mul_comm] },
   -- massage `hps` into our goal

src/ring_theory/integral_domain.lean

@@ -193,7 +193,7 @@ begin
       (λ b hb, let ⟨n, hn⟩ := hx b in ⟨n % order_of x, mem_range.2 (nat.mod_lt _ (order_of_pos _)),
         by rw [← pow_eq_mod_order_of, hn]⟩)
   ... = 0 : _,
-  rw [← mul_left_inj' hx1, zero_mul, ← geom_sum, geom_sum_mul, coe_coe],
+  rw [← mul_left_inj' hx1, zero_mul, geom_sum_mul, coe_coe],
   norm_cast,
   simp [pow_order_of_eq_one],
 end

src/ring_theory/polynomial/basic.lean

@@ -27,6 +27,7 @@ import ring_theory.unique_factorization_domain
 
 noncomputable theory
 open_locale classical big_operators polynomial
+open finset
 
 universes u v w
 variables {R : Type u} {S : Type*}
@@ -158,7 +159,7 @@ begin
 end
 
 lemma geom_sum_X_comp_X_add_one_eq_sum (n : ℕ) :
-  (geom_sum (X : R[X]) n).comp (X + 1) =
+  (∑ i in range n, (X : R[X]) ^ i).comp (X + 1) =
   (finset.range n).sum (λ (i : ℕ), (n.choose (i + 1) : R[X]) * X ^ i) :=
 begin
   ext i,
@@ -175,11 +176,11 @@ begin
 end
 
 lemma monic.geom_sum {P : R[X]}
-  (hP : P.monic) (hdeg : 0 < P.nat_degree) {n : ℕ} (hn : n ≠ 0) : (geom_sum P n).monic :=
+  (hP : P.monic) (hdeg : 0 < P.nat_degree) {n : ℕ} (hn : n ≠ 0) : (∑ i in range n, P ^ i).monic :=
 begin
   nontriviality R,
   cases n, { exact (hn rfl).elim },
-  rw [geom_sum_succ', geom_sum_def],
+  rw [geom_sum_succ'],
   refine (hP.pow _).add_of_left _,
   refine lt_of_le_of_lt (degree_sum_le _ _) _,
   rw [finset.sup_lt_iff],
@@ -191,11 +192,11 @@ begin
 end
 
 lemma monic.geom_sum' {P : R[X]}
-  (hP : P.monic) (hdeg : 0 < P.degree) {n : ℕ} (hn : n ≠ 0) : (geom_sum P n).monic :=
+  (hP : P.monic) (hdeg : 0 < P.degree) {n : ℕ} (hn : n ≠ 0) : (∑ i in range n, P ^ i).monic :=
 hP.geom_sum (nat_degree_pos_iff_degree_pos.2 hdeg) hn
 
 lemma monic_geom_sum_X {n : ℕ} (hn : n ≠ 0) :
-  (geom_sum (X : R[X]) n).monic :=
+  (∑ i in range n, (X : R[X]) ^ i).monic :=
 begin
   nontriviality R,
   apply monic_X.geom_sum _ hn,

src/ring_theory/polynomial/cyclotomic/basic.lean

@@ -419,8 +419,11 @@ begin
   exact nat.proper_divisors.not_self_mem
 end
 
+open_locale big_operators
+open finset
+
 lemma prod_cyclotomic_eq_geom_sum {n : ℕ} (h : 0 < n) (R) [comm_ring R] [is_domain R] :
-  ∏ i in n.divisors \ {1}, cyclotomic i R = geom_sum X n :=
+  ∏ i in n.divisors \ {1}, cyclotomic i R = ∑ i in range n, X ^ i :=
 begin
   apply_fun (* cyclotomic 1 R) using mul_left_injective₀ (cyclotomic_ne_zero 1 R),
   have : ∏ i in {1}, cyclotomic i R = cyclotomic 1 R := finset.prod_singleton,
@@ -429,9 +432,10 @@ begin
 end
 
 lemma cyclotomic_dvd_geom_sum_of_dvd (R) [comm_ring R] {d n : ℕ} (hdn : d ∣ n)
-  (hd : d ≠ 1) : cyclotomic d R ∣ geom_sum X n :=
+  (hd : d ≠ 1) : cyclotomic d R ∣ ∑ i in range n, X ^ i :=
 begin
-  suffices : (cyclotomic d ℤ).map (int.cast_ring_hom R) ∣ (geom_sum X n).map (int.cast_ring_hom R),
+  suffices : (cyclotomic d ℤ).map (int.cast_ring_hom R) ∣
+    (∑ i in range n, X ^ i).map (int.cast_ring_hom R),
   { have key := (map_ring_hom (int.cast_ring_hom R)).map_geom_sum X n,
     simp only [coe_map_ring_hom, map_X] at key,
     rwa [map_cyclotomic, key] at this },
@@ -701,9 +705,9 @@ begin
     exact monic.ne_zero prod_monic (degree_eq_bot.1 h) },
 end
 
-/-- If `p` is prime, then `cyclotomic p R = geom_sum X p`. -/
+/-- If `p` is prime, then `cyclotomic p R = ∑ i in range p, X ^ i`. -/
 lemma cyclotomic_eq_geom_sum {R : Type*} [comm_ring R] {p : ℕ}
-  (hp : nat.prime p) : cyclotomic p R = geom_sum X p :=
+  (hp : nat.prime p) : cyclotomic p R = ∑ i in range p, X ^ i :=
 begin
   refine ((eq_cyclotomic_iff hp.pos _).mpr _).symm,
   simp only [nat.prime.proper_divisors hp, geom_sum_mul, finset.prod_singleton, cyclotomic_one],
@@ -713,12 +717,13 @@ lemma cyclotomic_prime_mul_X_sub_one (R : Type*) [comm_ring R] (p : ℕ) [hn : f
   (cyclotomic p R) * (X - 1) = X ^ p - 1 :=
 by rw [cyclotomic_eq_geom_sum hn.out, geom_sum_mul]
 
-/-- If `p ^ k` is a prime power, then `cyclotomic (p ^ (n + 1)) R = geom_sum (X ^ p ^ n) p`. -/
+/-- If `p ^ k` is a prime power, then
+`cyclotomic (p ^ (n + 1)) R = ∑ i in range p, (X ^ (p ^ n)) ^ i`. -/
 lemma cyclotomic_prime_pow_eq_geom_sum {R : Type*} [comm_ring R] {p n : ℕ} (hp : nat.prime p) :
-  cyclotomic (p ^ (n + 1)) R = geom_sum (X ^ p ^ n) p :=
+  cyclotomic (p ^ (n + 1)) R = ∑ i in range p, (X ^ (p ^ n)) ^ i :=
 begin
-  have : ∀ m, cyclotomic (p ^ (m + 1)) R = geom_sum (X ^ (p ^ m)) p ↔
-    geom_sum (X ^ p ^ m) p * ∏ (x : ℕ) in finset.range (m + 1),
+  have : ∀ m, cyclotomic (p ^ (m + 1)) R = ∑ i in range p, (X ^ (p ^ m)) ^ i ↔
+    (∑ i in range p, (X ^ (p ^ m)) ^ i) * ∏ (x : ℕ) in finset.range (m + 1),
       cyclotomic (p ^ x) R = X ^ p ^ (m + 1) - 1,
   { intro m,
     have := eq_cyclotomic_iff (pow_pos hp.pos (m + 1)) _,
@@ -729,7 +734,7 @@ begin
   rw ((eq_cyclotomic_iff (pow_pos hp.pos (n_n.succ + 1)) _).mpr _).symm,
   rw [nat.prod_proper_divisors_prime_pow hp, finset.prod_range_succ, n_ih],
   rw this at n_ih,
-  rw [mul_comm _ (geom_sum _ _), n_ih, geom_sum_mul, sub_left_inj, ← pow_mul, pow_add, pow_one],
+  rw [mul_comm _ (∑ i in _, _), n_ih, geom_sum_mul, sub_left_inj, ← pow_mul, pow_add, pow_one],
 end
 
 lemma cyclotomic_prime_pow_mul_X_pow_sub_one (R : Type*) [comm_ring R] (p k : ℕ)

src/ring_theory/polynomial/cyclotomic/eval.lean

@@ -26,7 +26,7 @@ open_locale big_operators
 
 @[simp] lemma eval_one_cyclotomic_prime {R : Type*} [comm_ring R] {p : ℕ} [hn : fact p.prime] :
   eval 1 (cyclotomic p R) = p :=
-by simp only [cyclotomic_eq_geom_sum hn.out, geom_sum_def, eval_X, one_pow, sum_const, eval_pow,
+by simp only [cyclotomic_eq_geom_sum hn.out, eval_X, one_pow, sum_const, eval_pow,
               eval_finset_sum, card_range, smul_one_eq_coe]
 
 @[simp] lemma eval₂_one_cyclotomic_prime {R S : Type*} [comm_ring R] [semiring S] (f : R →+* S)
@@ -35,7 +35,7 @@ by simp
 
 @[simp] lemma eval_one_cyclotomic_prime_pow {R : Type*} [comm_ring R] {p : ℕ} (k : ℕ)
   [hn : fact p.prime] : eval 1 (cyclotomic (p ^ (k + 1)) R) = p :=
-by simp only [cyclotomic_prime_pow_eq_geom_sum hn.out, geom_sum_def, eval_X, one_pow, sum_const,
+by simp only [cyclotomic_prime_pow_eq_geom_sum hn.out, eval_X, one_pow, sum_const,
               eval_pow, eval_finset_sum, card_range, smul_one_eq_coe]
 
 @[simp] lemma eval₂_one_cyclotomic_prime_pow {R S : Type*} [comm_ring R] [semiring S] (f : R →+* S)
@@ -77,7 +77,7 @@ begin
   { simp only [lt_self_iff_false, mem_sdiff, not_false_iff, mem_proper_divisors, and_false,
       false_and]},
   { simpa only [mem_singleton] using hn''.ne' },
-  rcases lt_trichotomy 0 (geom_sum x n) with h | h | h,
+  rcases lt_trichotomy 0 (∑ i in range n, x ^ i) with h | h | h,
   { apply pos_of_mul_pos_right,
     { rwa this },
     rw eval_prod,

src/ring_theory/polynomial/eisenstein.lean

@@ -277,7 +277,7 @@ begin
         simpa [map_comp] using hn },
       { exact ⟨p ^ n, by rw [pow_succ]⟩ } } },
   { rw [coeff_zero_eq_eval_zero, eval_comp, cyclotomic_prime_pow_eq_geom_sum hp.out, eval_add,
-      eval_X, eval_one, zero_add, geom_sum_def, eval_finset_sum],
+      eval_X, eval_one, zero_add, eval_finset_sum],
     simp only [eval_pow, eval_X, one_pow, sum_const, card_range, nat.smul_one_eq_coe,
       int.nat_cast_eq_coe_nat, submodule_span_eq, ideal.submodule_span_eq,
       ideal.span_singleton_pow, ideal.mem_span_singleton],