refactor(topology/algebra/infinite_sum): Cauchy condition for infinite sums generalized to complete topological groups

Author: johoelzl

src/analysis/normed_space/basic.lean

@@ -114,6 +114,9 @@ abs_norm_sub_norm_le g h
 lemma norm_sub_rev (g h : α) : ∥g - h∥ = ∥h - g∥ :=
 by rw ←norm_neg; simp
 
+lemma ball_0_eq (ε : ℝ) : ball (0:α) ε = {x | ∥x∥ < ε} :=
+set.ext $ assume a, by simp
+
 section nnnorm
 
 def nnnorm (a : α) : nnreal := ⟨norm a, norm_nonneg a⟩
@@ -178,26 +181,18 @@ end
 lemma continuous_nnnorm : continuous (nnnorm : α → nnreal) :=
 continuous_subtype_mk _ continuous_norm
 
-instance normed_top_monoid : topological_add_monoid α :=
-⟨continuous_iff_continuous_at.2 $ λ ⟨x₁, x₂⟩,
-  tendsto_iff_norm_tendsto_zero.2
-  begin
-    refine squeeze_zero (by simp) _
-      (by simpa using tendsto_add (lim_norm (x₁, x₂)) (lim_norm (x₁, x₂))),
-    exact λ ⟨e₁, e₂⟩, calc
-      ∥(e₁ + e₂) - (x₁ + x₂)∥ = ∥(e₁ - x₁) + (e₂ - x₂)∥ : by simp
-      ... ≤ ∥e₁ - x₁∥ + ∥e₂ - x₂∥ : norm_triangle _ _
-      ... ≤ max (∥e₁ - x₁∥) (∥e₂ - x₂∥) + max (∥e₁ - x₁∥) (∥e₂ - x₂∥) :
-        add_le_add (le_max_left _ _) (le_max_right _ _)
-  end⟩
-
-instance normed_top_group : topological_add_group α :=
-⟨continuous_iff_continuous_at.2 $ λ x,
-tendsto_iff_norm_tendsto_zero.2 begin
-  have : ∀ (e : α), ∥-e - -x∥ = ∥e - x∥,
-  { intro, simpa using norm_neg (e - x) },
-  rw funext this, exact lim_norm x,
-end⟩
+instance normed_uniform_group : uniform_add_group α :=
+begin
+  refine ⟨metric.uniform_continuous_iff.2 $ assume ε hε, ⟨ε / 2, half_pos hε, assume a b h, _⟩⟩,
+  rw [prod.dist_eq, max_lt_iff, dist_eq_norm, dist_eq_norm] at h,
+  calc dist (a.1 - a.2) (b.1 - b.2) = ∥(a.1 - b.1) - (a.2 - b.2)∥  : by simp [dist_eq_norm]
+    ... ≤ ∥a.1 - b.1∥ + ∥a.2 - b.2∥ : norm_triangle_sub
+    ... < ε / 2 + ε / 2 : add_lt_add h.1 h.2
+    ... = ε : add_halves _
+end
+
+instance normed_top_monoid : topological_add_monoid α := by apply_instance
+instance normed_top_group : topological_add_group α := by apply_instance
 
 end normed_group
 
@@ -416,3 +411,43 @@ noncomputable def normed_space.of_core (α : Type*) (β : Type*)
 }
 
 end normed_space
+
+section has_sum
+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 ∥ < ε) :=
+begin
+  simp only [has_sum_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,
+    rcases h ε hε with ⟨t, ht⟩,
+    refine ⟨t, assume u hu, hs _⟩,
+    rw [ball_0_eq],
+    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
+  ⟨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 norm_tsum_le_tsum_norm {f : ι → α} (hf : has_sum (λ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 _),
+have h₂ : tendsto (λs:finset ι, s.sum (λi, ∥f i∥)) at_top (nhds (∑ i, ∥f i∥)) :=
+  is_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

src/analysis/specific_limits.lean

@@ -15,43 +15,6 @@ open classical function lattice filter finset metric
 
 variables {α : Type*} {β : Type*} {ι : Type*}
 
-lemma has_sum_iff_cauchy [normed_group α] [complete_space α] {f : ι → α} :
-  has_sum f ↔ ∀ε>0, (∃s:finset ι, ∀t, disjoint t s → ∥ t.sum f ∥ < ε) :=
-begin
-  refine iff.trans (cauchy_map_iff_exists_tendsto at_top_ne_bot).symm _,
-  simp only [cauchy_map_iff, and_iff_right at_top_ne_bot, prod_at_top_at_top_eq, uniformity_dist,
-    tendsto_infi, tendsto_at_top_principal, set.mem_set_of_eq],
-  split,
-  { assume h ε hε,
-    rcases h ε hε with ⟨⟨s₁, s₂⟩, h⟩,
-    use [s₁ ∪ s₂],
-    assume t ht,
-    have : (s₁ ∪ s₂) ∩ t = ∅ := finset.disjoint_iff_inter_eq_empty.1 ht.symm,
-    specialize h (s₁ ∪ s₂, (s₁ ∪ s₂) ∪ t) ⟨le_sup_left, le_sup_left_of_le le_sup_right⟩,
-    simpa only [finset.sum_union this, dist_eq_norm,
-      sub_add_eq_sub_sub, sub_self, zero_sub, norm_neg] using h },
-  { assume h' ε hε,
-    rcases h' (ε / 2) (half_pos hε) with ⟨s, h⟩,
-    use [(s, s)],
-    rintros ⟨t₁, t₂⟩ ⟨ht₁, ht₂⟩,
-    dsimp at ht₁ ht₂,
-    calc dist (t₁.sum f) (t₂.sum f) = ∥sum (t₁ \ s) f - sum (t₂ \ s) f∥ :
-        by simp only [(finset.sum_sdiff ht₁).symm, (finset.sum_sdiff ht₂).symm,
-          dist_eq_norm, add_sub_add_right_eq_sub]
-      ... ≤ ∥sum (t₁ \ s) f∥ + ∥ sum (t₂ \ s) f∥ : norm_triangle_sub
-      ... < ε / 2 + ε / 2 : add_lt_add (h _ finset.disjoint_sdiff) (h _ finset.disjoint_sdiff)
-      ... = ε : add_halves _ }
-end
-
-lemma has_sum_of_has_sum_norm [normed_group α] [complete_space α] {f : ι → α}
-  (hf : has_sum (λa, norm (f a))) : has_sum f :=
-has_sum_iff_cauchy.2 $ assume ε hε,
-  let ⟨s, hs⟩ := has_sum_iff_cauchy.1 hf ε hε in
-  ⟨s, assume t ht,
-    have ∥t.sum (λa, ∥f a∥)∥ < ε := hs t ht,
-    have nn : 0 ≤ t.sum (λa, ∥f a∥) := finset.zero_le_sum (assume a _, norm_nonneg _),
-    lt_of_le_of_lt (norm_triangle_sum t f) $ by rwa [real.norm_eq_abs, abs_of_nonneg nn] at this⟩
-
 lemma has_sum_of_absolute_convergence_real {f : ℕ → ℝ} (hf : ∀n, 0 ≤ f n) :
   (∃r, tendsto (λn, (range n).sum (λi, abs (f i))) at_top (nhds r)) → has_sum f
 | ⟨r, hr⟩ :=
@@ -142,28 +105,11 @@ begin
   have hf : is_sum f ε := is_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 _, _⟩,
-  let g : ℕ → ℝ := λ n, option.cases_on (encodable.decode2 ι n) 0 (f ∘ encodable.encode),
-  have : ∀ n, g n = 0 ∨ g n = f n,
-  { intro n, dsimp [g], cases e : encodable.decode2 ι n with a,
-    { exact or.inl rfl },
-    { simp [encodable.mem_decode2.1 e] } },
-  cases has_sum_of_has_sum_of_sub ⟨_, hf⟩ this with c hg,
-  have cε : c ≤ ε,
-  { refine is_sum_le (λ n, _) hg hf,
-    cases this n; rw h, exact le_of_lt (f0 _) },
-  have hs : ∀ n, g n ≠ 0 → (encodable.decode2 ι n).is_some,
-  { intros n h, dsimp [g] at h,
-    cases encodable.decode2 ι n,
-    exact (h rfl).elim, exact rfl },
-  refine ⟨c, _, cε⟩,
-  refine is_sum_of_is_sum_ne_zero
-    (λ n h, option.get (hs n h)) (λ n _, ne_of_gt (f0 _))
-    (λ i _, encodable.encode i) (λ n h, ne_of_gt _)
-    (λ n h, _) (λ i _, _) (λ i _, _) hg,
-  { dsimp [g], rw encodable.encodek2, exact f0 _ },
-  { exact encodable.mem_decode2.1 (option.get_mem _) },
-  { exact option.get_of_mem _ (encodable.encodek2 _) },
-  { dsimp [g], rw encodable.encodek2 }
+  rcases has_sum_comp_of_has_sum_of_injective f (has_sum_spec hf) (@encodable.encode_injective ι _)
+    with ⟨c, hg⟩,
+  refine ⟨c, hg, is_sum_le_inj _ (@encodable.encode_injective ι _) _ _ hg hf⟩,
+  { assume i _, exact le_of_lt (f0 _) },
+  { assume n, exact le_refl _ }
 end
 
 namespace nnreal

src/measure_theory/probability_mass_function.lean

@@ -28,14 +28,14 @@ lemma has_sum_coe (p : pmf α) : has_sum p := has_sum_spec p.is_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 _ _⟩
+def pure (a : α) : pmf α := ⟨λa', if a' = a then 1 else 0, is_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 a (p a)) p.2
+is_sum_le (by intro b; split_ifs; simp [h]; exact le_refl _) (is_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) :=
 begin

src/order/filter/basic.lean

@@ -652,6 +652,7 @@ section map
 variables {f f₁ f₂ : filter α} {g g₁ g₂ : filter β} {m : α → β} {m' : β → γ} {s : set α} {t : set β}
 
 @[simp] theorem mem_comap_sets : s ∈ (comap m g).sets ↔ ∃t∈g.sets, m ⁻¹' t ⊆ s := iff.rfl
+
 theorem preimage_mem_comap (ht : t ∈ g.sets) : m ⁻¹' t ∈ (comap m g).sets :=
 ⟨t, ht, subset.refl _⟩
 
@@ -1386,10 +1387,14 @@ calc map f (⨅a, principal {a' | a ≤ a'}) = (⨅a, map f $ principal {a' | a
       (by apply_instance)
   ... = (⨅a, principal $ f '' {a' | a ≤ a'}) : by simp only [map_principal, eq_self_iff_true]
 
-lemma tendsto_at_top {α β} [preorder β] (m : α → β) (f : filter α) :
+lemma tendsto_at_top [preorder β] (m : α → β) (f : filter α) :
   tendsto m f at_top ↔ (∀b, {a | b ≤ m a} ∈ f.sets) :=
 by simp only [at_top, tendsto_infi, tendsto_principal]; refl
 
+lemma tendsto_at_top' [nonempty α] [semilattice_sup α] (f : α → β) (l : filter β) :
+  tendsto f at_top l ↔ (∀s∈l.sets, ∃a, ∀b≥a, f b ∈ s) :=
+by simp only [tendsto_def, mem_at_top_sets]; refl
+
 theorem tendsto_at_top_principal [nonempty β] [semilattice_sup β] {f : β → α} {s : set α} :
   tendsto f at_top (principal s) ↔ ∃N, ∀n≥N, f n ∈ s :=
 by rw [tendsto_iff_comap, comap_principal, le_principal_iff, mem_at_top_sets]; refl