rename has_sum and is_sum to summable and has_sum

src/analysis/normed_space/basic.lean

@@ -502,15 +502,15 @@ noncomputable def normed_space.of_core (α : Type*) (β : Type*)
 
 end normed_space
 
-section has_sum
+section summable
 local attribute [instance] classical.prop_decidable
 open finset filter
 variables [normed_group α] [complete_space α]
 
-lemma has_sum_iff_vanishing_norm {f : ι → α} :
-  has_sum f ↔ ∀ε>0, (∃s:finset ι, ∀t, disjoint t s → ∥ t.sum f ∥ < ε) :=
+lemma summable_iff_vanishing_norm {f : ι → α} :
+  summable f ↔ ∀ε>0, (∃s:finset ι, ∀t, disjoint t s → ∥ t.sum f ∥ < ε) :=
 begin
-  simp only [has_sum_iff_vanishing, metric.mem_nhds_iff, exists_imp_distrib],
+  simp only [summable_iff_vanishing, metric.mem_nhds_iff, exists_imp_distrib],
   split,
   { assume h ε hε, refine h {x | ∥x∥ < ε} ε hε _, rw [ball_0_eq ε] },
   { assume h s ε hε hs,
@@ -520,27 +520,27 @@ begin
     exact ht u hu }
 end
 
-lemma has_sum_of_norm_bounded {f : ι → α} (g : ι → ℝ) (hf : has_sum g) (h : ∀i, ∥f i∥ ≤ g i) :
-  has_sum f :=
-has_sum_iff_vanishing_norm.2 $ assume ε hε,
-  let ⟨s, hs⟩ := has_sum_iff_vanishing_norm.1 hf ε hε in
+lemma summable_of_norm_bounded {f : ι → α} (g : ι → ℝ) (hf : summable g) (h : ∀i, ∥f i∥ ≤ g i) :
+  summable f :=
+summable_iff_vanishing_norm.2 $ assume ε hε,
+  let ⟨s, hs⟩ := summable_iff_vanishing_norm.1 hf ε hε in
   ⟨s, assume t ht,
     have ∥t.sum g∥ < ε := hs t ht,
     have nn : 0 ≤ t.sum g := finset.zero_le_sum (assume a _, le_trans (norm_nonneg _) (h a)),
     lt_of_le_of_lt (norm_triangle_sum t f) $ lt_of_le_of_lt (finset.sum_le_sum $ assume i _, h i) $
       by rwa [real.norm_eq_abs, abs_of_nonneg nn] at this⟩
 
-lemma has_sum_of_has_sum_norm {f : ι → α} (hf : has_sum (λa, ∥f a∥)) : has_sum f :=
-has_sum_of_norm_bounded _ hf (assume i, le_refl _)
+lemma summable_of_summable_norm {f : ι → α} (hf : summable (λa, ∥f a∥)) : summable f :=
+summable_of_norm_bounded _ hf (assume i, le_refl _)
 
-lemma norm_tsum_le_tsum_norm {f : ι → α} (hf : has_sum (λi, ∥f i∥)) : ∥(∑i, f i)∥ ≤ (∑ i, ∥f i∥) :=
+lemma norm_tsum_le_tsum_norm {f : ι → α} (hf : summable (λi, ∥f i∥)) : ∥(∑i, f i)∥ ≤ (∑ i, ∥f i∥) :=
 have h₁ : tendsto (λs:finset ι, ∥s.sum f∥) at_top (nhds ∥(∑ i, f i)∥) :=
-  (is_sum_tsum $ has_sum_of_has_sum_norm hf).comp (continuous_norm.tendsto _),
+  (has_sum_tsum $ summable_of_summable_norm hf).comp (continuous_norm.tendsto _),
 have h₂ : tendsto (λs:finset ι, s.sum (λi, ∥f i∥)) at_top (nhds (∑ i, ∥f i∥)) :=
-  is_sum_tsum hf,
+  has_sum_tsum hf,
 le_of_tendsto_of_tendsto at_top_ne_bot h₁ h₂ $ univ_mem_sets' $ assume s, norm_triangle_sum _ _
 
-end has_sum
+end summable
 
 namespace complex
 

src/analysis/specific_limits.lean

@@ -15,11 +15,11 @@ open classical function lattice filter finset metric
 
 variables {α : Type*} {β : Type*} {ι : Type*}
 
-lemma has_sum_of_absolute_convergence_real {f : ℕ → ℝ} :
-  (∃r, tendsto (λn, (range n).sum (λi, abs (f i))) at_top (nhds r)) → has_sum f
+lemma summable_of_absolute_convergence_real {f : ℕ → ℝ} :
+  (∃r, tendsto (λn, (range n).sum (λi, abs (f i))) at_top (nhds r)) → summable f
 | ⟨r, hr⟩ :=
   begin
-    refine has_sum_of_has_sum_norm ⟨r, (is_sum_iff_tendsto_nat_of_nonneg _ _).2 _⟩,
+    refine summable_of_summable_norm ⟨r, (has_sum_iff_tendsto_nat_of_nonneg _ _).2 _⟩,
     exact assume i, norm_nonneg _,
     simpa only using hr
   end
@@ -78,46 +78,46 @@ lemma tendsto_one_div_add_at_top_nhds_0_nat :
 suffices tendsto (λ n : ℕ, 1 / (↑(n + 1) : ℝ)) at_top (nhds 0), by simpa,
 (tendsto_add_at_top_iff_nat 1).2 tendsto_one_div_at_top_nhds_0_nat
 
-lemma is_sum_geometric {r : ℝ} (h₁ : 0 ≤ r) (h₂ : r < 1) :
-  is_sum (λn:ℕ, r ^ n) (1 / (1 - r)) :=
+lemma has_sum_geometric {r : ℝ} (h₁ : 0 ≤ r) (h₂ : r < 1) :
+  has_sum (λn:ℕ, r ^ n) (1 / (1 - r)) :=
 have r ≠ 1, from ne_of_lt h₂,
 have r + -1 ≠ 0,
   by rw [←sub_eq_add_neg, ne, sub_eq_iff_eq_add]; simp; assumption,
 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 $
+(has_sum_iff_tendsto_nat_of_nonneg (pow_nonneg h₁) _).mpr $
   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 :=
+lemma has_sum_geometric_two (a : ℝ) : has_sum (λn:ℕ, (a / 2) / 2 ^ n) a :=
 begin
-  convert is_sum_mul_left (a / 2) (is_sum_geometric
+  convert has_sum_mul_left (a / 2) (has_sum_geometric
     (le_of_lt one_half_pos) one_half_lt_one),
   { funext n, simp,
     rw ← pow_inv; [refl, exact two_ne_zero] },
   { norm_num, rw div_mul_cancel _ two_ne_zero }
 end
 
 def pos_sum_of_encodable {ε : ℝ} (hε : 0 < ε)
-  (ι) [encodable ι] : {ε' : ι → ℝ // (∀ i, 0 < ε' i) ∧ ∃ c, is_sum ε' c ∧ c ≤ ε} :=
+  (ι) [encodable ι] : {ε' : ι → ℝ // (∀ i, 0 < ε' i) ∧ ∃ c, has_sum ε' c ∧ c ≤ ε} :=
 begin
   let f := λ n, (ε / 2) / 2 ^ n,
-  have hf : is_sum f ε := is_sum_geometric_two _,
+  have hf : has_sum f ε := has_sum_geometric_two _,
   have f0 : ∀ n, 0 < f n := λ n, div_pos (half_pos hε) (pow_pos two_pos _),
   refine ⟨f ∘ encodable.encode, λ i, f0 _, _⟩,
-  rcases has_sum_comp_of_has_sum_of_injective f (has_sum_spec hf) (@encodable.encode_injective ι _)
+  rcases summable_comp_of_summable_of_injective f (summable_spec hf) (@encodable.encode_injective ι _)
     with ⟨c, hg⟩,
-  refine ⟨c, hg, is_sum_le_inj _ (@encodable.encode_injective ι _) _ _ hg hf⟩,
+  refine ⟨c, hg, has_sum_le_inj _ (@encodable.encode_injective ι _) _ _ hg hf⟩,
   { assume i _, exact le_of_lt (f0 _) },
   { assume n, exact le_refl _ }
 end
 
 lemma cauchy_seq_of_le_geometric [metric_space α] (r C : ℝ) (hr : r < 1) {f : ℕ → α}
   (hu : ∀n, dist (f n) (f (n+1)) ≤ C * r^n) : cauchy_seq f :=
 begin
-  refine cauchy_seq_of_has_sum_dist (has_sum_of_norm_bounded (λn, C * r^n) _ _),
+  refine cauchy_seq_of_summable_dist (summable_of_norm_bounded (λn, C * r^n) _ _),
   { by_cases h : C = 0,
-    { simp [h, has_sum_zero] },
+    { simp [h, summable_zero] },
     { have Cpos : C > 0,
       { have := le_trans dist_nonneg (hu 0),
         simp only [mul_one, pow_zero] at this,
@@ -126,20 +126,20 @@ begin
       { have := le_trans dist_nonneg (hu 1),
         simp only [pow_one] at this,
         exact nonneg_of_mul_nonneg_left this Cpos },
-      refine has_sum_mul_left C _,
-      exact has_sum_spec (@is_sum_geometric r rnonneg hr) }},
+      refine summable_mul_left C _,
+      exact summable_spec (@has_sum_geometric r rnonneg hr) }},
   show ∀n, abs (dist (f n) (f (n+1))) ≤ C * r^n,
   { assume n, rw abs_of_nonneg (dist_nonneg), exact hu n }
 end
 
 namespace nnreal
 
 theorem exists_pos_sum_of_encodable {ε : nnreal} (hε : 0 < ε) (ι) [encodable ι] :
-  ∃ ε' : ι → nnreal, (∀ i, 0 < ε' i) ∧ ∃c, is_sum ε' c ∧ c < ε :=
+  ∃ ε' : ι → nnreal, (∀ i, 0 < ε' i) ∧ ∃c, has_sum ε' c ∧ c < ε :=
 let ⟨a, a0, aε⟩ := dense hε in
 let ⟨ε', hε', c, hc, hcε⟩ := pos_sum_of_encodable a0 ι in
 ⟨ λi, ⟨ε' i, le_of_lt $ hε' i⟩, assume i, nnreal.coe_lt.2 $ hε' i,
-  ⟨c, is_sum_le (assume i, le_of_lt $ hε' i) is_sum_zero hc ⟩, nnreal.is_sum_coe.1 hc,
+  ⟨c, has_sum_le (assume i, le_of_lt $ hε' i) has_sum_zero hc ⟩, nnreal.has_sum_coe.1 hc,
    lt_of_le_of_lt (nnreal.coe_le.1 hcε) aε ⟩
 
 end nnreal

src/measure_theory/probability_mass_function.lean

@@ -11,7 +11,7 @@ variables {α : Type*} {β : Type*} {γ : Type*}
 local attribute [instance] classical.prop_decidable
 
 /-- Probability mass functions, i.e. discrete probability measures -/
-def {u} pmf (α : Type u) : Type u := { f : α → nnreal // is_sum f 1 }
+def {u} pmf (α : Type u) : Type u := { f : α → nnreal // has_sum f 1 }
 
 namespace pmf
 
@@ -20,44 +20,44 @@ instance : has_coe_to_fun (pmf α) := ⟨λp, α → nnreal, λp a, p.1 a⟩
 @[extensionality] protected lemma ext : ∀{p q : pmf α}, (∀a, p a = q a) → p = q
 | ⟨f, hf⟩ ⟨g, hg⟩ eq :=  subtype.eq $ funext eq
 
-lemma is_sum_coe_one (p : pmf α) : is_sum p 1 := p.2
+lemma has_sum_coe_one (p : pmf α) : has_sum p 1 := p.2
 
-lemma has_sum_coe (p : pmf α) : has_sum p := has_sum_spec p.is_sum_coe_one
+lemma summable_coe (p : pmf α) : summable p := summable_spec p.has_sum_coe_one
 
-@[simp] lemma tsum_coe (p : pmf α) : (∑a, p a) = 1 := tsum_eq_is_sum p.is_sum_coe_one
+@[simp] lemma tsum_coe (p : pmf α) : (∑a, p a) = 1 := tsum_eq_has_sum p.has_sum_coe_one
 
 def support (p : pmf α) : set α := {a | p.1 a ≠ 0}
 
-def pure (a : α) : pmf α := ⟨λa', if a' = a then 1 else 0, is_sum_ite_eq _ _⟩
+def pure (a : α) : pmf α := ⟨λa', if a' = a then 1 else 0, has_sum_ite_eq _ _⟩
 
 @[simp] lemma pure_apply (a a' : α) : pure a a' = (if a' = a then 1 else 0) := rfl
 
 instance [inhabited α] : inhabited (pmf α) := ⟨pure (default α)⟩
 
 lemma coe_le_one (p : pmf α) (a : α) : p a ≤ 1 :=
-is_sum_le (by intro b; split_ifs; simp [h]; exact le_refl _) (is_sum_ite_eq a (p a)) p.2
+has_sum_le (by intro b; split_ifs; simp [h]; exact le_refl _) (has_sum_ite_eq a (p a)) p.2
 
-protected lemma bind.has_sum (p : pmf α) (f : α → pmf β) (b : β) : has_sum (λa:α, p a * f a b) :=
+protected lemma bind.summable (p : pmf α) (f : α → pmf β) (b : β) : summable (λa:α, p a * f a b) :=
 begin
-  refine nnreal.has_sum_of_le (assume a, _) p.has_sum_coe,
+  refine nnreal.summable_of_le (assume a, _) p.summable_coe,
   suffices : p a * f a b ≤ p a * 1, { simpa },
   exact mul_le_mul_of_nonneg_left ((f a).coe_le_one _) (p a).2
 end
 
 def bind (p : pmf α) (f : α → pmf β) : pmf β :=
 ⟨λb, (∑a, p a * f a b),
   begin
-    simp [ennreal.is_sum_coe.symm, (ennreal.tsum_coe (bind.has_sum p f _)).symm],
-    rw [is_sum_iff_of_has_sum ennreal.has_sum, ennreal.tsum_comm],
-    simp [ennreal.mul_tsum, (ennreal.tsum_coe (f _).has_sum_coe),
-      ennreal.tsum_coe p.has_sum_coe]
+    simp [ennreal.has_sum_coe.symm, (ennreal.tsum_coe (bind.summable p f _)).symm],
+    rw [has_sum_iff_of_summable ennreal.summable, ennreal.tsum_comm],
+    simp [ennreal.mul_tsum, (ennreal.tsum_coe (f _).summable_coe),
+      ennreal.tsum_coe p.summable_coe]
   end⟩
 
 @[simp] lemma bind_apply (p : pmf α) (f : α → pmf β) (b : β) : p.bind f b = (∑a, p a * f a b) := rfl
 
 lemma coe_bind_apply (p : pmf α) (f : α → pmf β) (b : β) :
   (p.bind f b : ennreal) = (∑a, p a * f a b) :=
-eq.trans (ennreal.tsum_coe $ bind.has_sum p f b).symm $ by simp
+eq.trans (ennreal.tsum_coe $ bind.summable p f b).symm $ by simp
 
 @[simp] lemma pure_bind (a : α) (f : α → pmf β) : (pure a).bind f = f a :=
 have ∀b a', ite (a' = a) 1 0 * f a' b = ite (a' = a) (f a b) 0, from
@@ -109,12 +109,12 @@ def of_multiset (s : multiset α) (hs : s ≠ 0) : pmf α :=
     by rw [← nnreal.eq_iff, nnreal.coe_one, ← this, nnreal.sum_coe]; simp,
   begin
     rw ← this,
-    apply is_sum_sum_of_ne_finset_zero,
+    apply has_sum_sum_of_ne_finset_zero,
     simp {contextual := tt},
   end⟩
 
 def of_fintype [fintype α] (f : α → nnreal) (h : finset.univ.sum f = 1) : pmf α :=
-⟨f, h ▸ is_sum_sum_of_ne_finset_zero (by simp)⟩
+⟨f, h ▸ has_sum_sum_of_ne_finset_zero (by simp)⟩
 
 def bernoulli (p : nnreal) (h : p ≤ 1) : pmf bool :=
 of_fintype (λb, cond b p (1 - p)) (nnreal.eq $ by simp [h])