chore(analysis): move more code out of analysis.normed_space.basic (#…

…10055)

src/analysis/normed/group/completion.lean

@@ -0,0 +1,49 @@
+/-
+Copyright (c) 2021 Heather Macbeth. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Heather Macbeth
+-/
+import analysis.normed.group.basic
+import topology.algebra.group_completion
+import topology.metric_space.completion
+
+/-!
+# Completion of a normed group
+
+In this file we prove that the completion of a (semi)normed group is a normed group.
+
+## Tags
+
+normed group, completion
+-/
+
+noncomputable theory
+
+namespace uniform_space
+namespace completion
+
+variables (E : Type*)
+
+instance [uniform_space E] [has_norm E] :
+  has_norm (completion E) :=
+{ norm := completion.extension has_norm.norm }
+
+@[simp] lemma norm_coe {E} [semi_normed_group E] (x : E) :
+  ∥(x : completion E)∥ = ∥x∥ :=
+completion.extension_coe uniform_continuous_norm x
+
+instance [semi_normed_group E] : normed_group (completion E) :=
+{ dist_eq :=
+  begin
+    intros x y,
+    apply completion.induction_on₂ x y; clear x y,
+    { refine is_closed_eq (completion.uniform_continuous_extension₂ _).continuous _,
+      exact continuous.comp completion.continuous_extension continuous_sub },
+    { intros x y,
+      rw [← completion.coe_sub, norm_coe, metric.completion.dist_eq, dist_eq_norm] }
+  end,
+  .. uniform_space.completion.add_comm_group,
+  .. metric.completion.metric_space }
+
+end completion
+end uniform_space

src/analysis/normed/group/hom_completion.lean

@@ -5,6 +5,7 @@ Authors: Patrick Massot
 -/
 
 import analysis.normed.group.hom
+import analysis.normed.group.completion
 /-!
 # Completion of normed group homs
 

src/analysis/normed/group/infinite_sum.lean

@@ -0,0 +1,149 @@
+/-
+Copyright (c) 2021 Sébastien Gouëzel. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sébastien Gouëzel, Heather Macbeth, Johannes Hölzl, Yury Kudryashov
+-/
+import analysis.normed.group.basic
+import topology.instances.nnreal
+
+/-!
+# Infinite sums in (semi)normed groups
+
+In a complete (semi)normed group,
+
+- `summable_iff_vanishing_norm`: a series `∑' i, f i` is summable if and only if for any `ε > 0`,
+  there exists a finite set `s` such that the sum `∑ i in t, f i` over any finite set `t` disjoint
+  with `s` has norm less than `ε`;
+
+- `summable_of_norm_bounded`, `summable_of_norm_bounded_eventually`: if `∥f i∥` is bounded above by
+  a summable series `∑' i, g i`, then `∑' i, f i` is summable as well; the same is true if the
+  inequality hold only off some finite set.
+
+- `tsum_of_norm_bounded`, `has_sum.norm_le_of_bounded`: if `∥f i∥ ≤ g i`, where `∑' i, g i` is a
+  summable series, then `∥∑' i, f i∥ ≤ ∑' i, g i`.
+
+## Tags
+
+infinite series, absolute convergence, normed group
+-/
+
+open_locale classical big_operators topological_space nnreal
+open finset filter metric
+
+variables {ι α E F : Type*} [semi_normed_group E] [semi_normed_group F]
+
+lemma cauchy_seq_finset_iff_vanishing_norm {f : ι → E} :
+  cauchy_seq (λ s : finset ι, ∑ i in s, f i) ↔
+    ∀ε > (0 : ℝ), ∃s:finset ι, ∀t, disjoint t s → ∥ ∑ i in t, f i ∥ < ε :=
+begin
+  rw [cauchy_seq_finset_iff_vanishing, nhds_basis_ball.forall_iff],
+  { simp only [ball_zero_eq, set.mem_set_of_eq] },
+  { rintros s t hst ⟨s', hs'⟩,
+    exact ⟨s', λ t' ht', hst $ hs' _ ht'⟩ }
+end
+
+lemma summable_iff_vanishing_norm [complete_space E] {f : ι → E} :
+  summable f ↔ ∀ε > (0 : ℝ), ∃s:finset ι, ∀t, disjoint t s → ∥ ∑ i in t, f i ∥ < ε :=
+by rw [summable_iff_cauchy_seq_finset, cauchy_seq_finset_iff_vanishing_norm]
+
+lemma cauchy_seq_finset_of_norm_bounded {f : ι → E} (g : ι → ℝ) (hg : summable g)
+  (h : ∀i, ∥f i∥ ≤ g i) : cauchy_seq (λ s : finset ι, ∑ i in s, f i) :=
+cauchy_seq_finset_iff_vanishing_norm.2 $ assume ε hε,
+  let ⟨s, hs⟩ := summable_iff_vanishing_norm.1 hg ε hε in
+  ⟨s, assume t ht,
+    have ∥∑ i in t, g i∥ < ε := hs t ht,
+    have nn : 0 ≤ ∑ i in t, g i := finset.sum_nonneg (assume a _, le_trans (norm_nonneg _) (h a)),
+    lt_of_le_of_lt (norm_sum_le_of_le t (λ i _, h i)) $
+      by rwa [real.norm_eq_abs, abs_of_nonneg nn] at this⟩
+
+lemma cauchy_seq_finset_of_summable_norm {f : ι → E} (hf : summable (λa, ∥f a∥)) :
+  cauchy_seq (λ s : finset ι, ∑ a in s, f a) :=
+cauchy_seq_finset_of_norm_bounded _ hf (assume i, le_refl _)
+
+/-- If a function `f` is summable in norm, and along some sequence of finsets exhausting the space
+its sum is converging to a limit `a`, then this holds along all finsets, i.e., `f` is summable
+with sum `a`. -/
+lemma has_sum_of_subseq_of_summable {f : ι → E} (hf : summable (λa, ∥f a∥))
+  {s : α → finset ι} {p : filter α} [ne_bot p]
+  (hs : tendsto s p at_top) {a : E} (ha : tendsto (λ b, ∑ i in s b, f i) p (𝓝 a)) :
+  has_sum f a :=
+tendsto_nhds_of_cauchy_seq_of_subseq (cauchy_seq_finset_of_summable_norm hf) hs ha
+
+lemma has_sum_iff_tendsto_nat_of_summable_norm {f : ℕ → E} {a : E} (hf : summable (λi, ∥f i∥)) :
+  has_sum f a ↔ tendsto (λn:ℕ, ∑ i in range n, f i) at_top (𝓝 a) :=
+⟨λ h, h.tendsto_sum_nat,
+λ h, has_sum_of_subseq_of_summable hf tendsto_finset_range h⟩
+
+/-- The direct comparison test for series:  if the norm of `f` is bounded by a real function `g`
+which is summable, then `f` is summable. -/
+lemma summable_of_norm_bounded
+  [complete_space E] {f : ι → E} (g : ι → ℝ) (hg : summable g) (h : ∀i, ∥f i∥ ≤ g i) :
+  summable f :=
+by { rw summable_iff_cauchy_seq_finset, exact cauchy_seq_finset_of_norm_bounded g hg h }
+
+lemma has_sum.norm_le_of_bounded {f : ι → E} {g : ι → ℝ} {a : E} {b : ℝ}
+  (hf : has_sum f a) (hg : has_sum g b) (h : ∀ i, ∥f i∥ ≤ g i) :
+  ∥a∥ ≤ b :=
+le_of_tendsto_of_tendsto' hf.norm hg $ λ s, norm_sum_le_of_le _ $ λ i hi, h i
+
+/-- Quantitative result associated to the direct comparison test for series:  If `∑' i, g i` is
+summable, and for all `i`, `∥f i∥ ≤ g i`, then `∥∑' i, f i∥ ≤ ∑' i, g i`. Note that we do not
+assume that `∑' i, f i` is summable, and it might not be the case if `α` is not a complete space. -/
+lemma tsum_of_norm_bounded {f : ι → E} {g : ι → ℝ} {a : ℝ} (hg : has_sum g a)
+  (h : ∀ i, ∥f i∥ ≤ g i) :
+  ∥∑' i : ι, f i∥ ≤ a :=
+begin
+  by_cases hf : summable f,
+  { exact hf.has_sum.norm_le_of_bounded hg h },
+  { rw [tsum_eq_zero_of_not_summable hf, norm_zero],
+    exact ge_of_tendsto' hg (λ s, sum_nonneg $ λ i hi, (norm_nonneg _).trans (h i)) }
+end
+
+/-- If `∑' i, ∥f i∥` is summable, then `∥∑' i, f i∥ ≤ (∑' i, ∥f i∥)`. Note that we do not assume
+that `∑' i, f i` is summable, and it might not be the case if `α` is not a complete space. -/
+lemma norm_tsum_le_tsum_norm {f : ι → E} (hf : summable (λi, ∥f i∥)) :
+  ∥∑' i, f i∥ ≤ ∑' i, ∥f i∥ :=
+tsum_of_norm_bounded hf.has_sum $ λ i, le_rfl
+
+/-- Quantitative result associated to the direct comparison test for series: If `∑' i, g i` is
+summable, and for all `i`, `∥f i∥₊ ≤ g i`, then `∥∑' i, f i∥₊ ≤ ∑' i, g i`. Note that we
+do not assume that `∑' i, f i` is summable, and it might not be the case if `α` is not a complete
+space. -/
+lemma tsum_of_nnnorm_bounded {f : ι → E} {g : ι → ℝ≥0} {a : ℝ≥0} (hg : has_sum g a)
+  (h : ∀ i, ∥f i∥₊ ≤ g i) :
+  ∥∑' i : ι, f i∥₊ ≤ a :=
+begin
+  simp only [← nnreal.coe_le_coe, ← nnreal.has_sum_coe, coe_nnnorm] at *,
+  exact tsum_of_norm_bounded hg h
+end
+
+/-- If `∑' i, ∥f i∥₊` is summable, then `∥∑' i, f i∥₊ ≤ ∑' i, ∥f i∥₊`. Note that
+we do not assume that `∑' i, f i` is summable, and it might not be the case if `α` is not a complete
+space. -/
+lemma nnnorm_tsum_le {f : ι → E} (hf : summable (λi, ∥f i∥₊)) :
+  ∥∑' i, f i∥₊ ≤ ∑' i, ∥f i∥₊ :=
+tsum_of_nnnorm_bounded hf.has_sum (λ i, le_rfl)
+
+variable [complete_space E]
+
+/-- Variant of the direct comparison test for series:  if the norm of `f` is eventually bounded by a
+real function `g` which is summable, then `f` is summable. -/
+lemma summable_of_norm_bounded_eventually {f : ι → E} (g : ι → ℝ) (hg : summable g)
+  (h : ∀ᶠ i in cofinite, ∥f i∥ ≤ g i) : summable f :=
+begin
+  replace h := mem_cofinite.1 h,
+  refine h.summable_compl_iff.mp _,
+  refine summable_of_norm_bounded _ (h.summable_compl_iff.mpr hg) _,
+  rintros ⟨a, h'⟩,
+  simpa using h'
+end
+
+lemma summable_of_nnnorm_bounded {f : ι → E} (g : ι → ℝ≥0) (hg : summable g)
+  (h : ∀i, ∥f i∥₊ ≤ g i) : summable f :=
+summable_of_norm_bounded (λ i, (g i : ℝ)) (nnreal.summable_coe.2 hg) (λ i, by exact_mod_cast h i)
+
+lemma summable_of_summable_norm {f : ι → E} (hf : summable (λa, ∥f a∥)) : summable f :=
+summable_of_norm_bounded _ hf (assume i, le_refl _)
+
+lemma summable_of_summable_nnnorm {f : ι → E} (hf : summable (λ a, ∥f a∥₊)) : summable f :=
+summable_of_nnnorm_bounded _ hf (assume i, le_refl _)

src/analysis/normed_space/basic.lean

@@ -10,7 +10,7 @@ import topology.algebra.group_completion
 import topology.instances.ennreal
 import topology.metric_space.completion
 import topology.sequences
-import analysis.normed.group.basic
+import analysis.normed.group.infinite_sum
 
 /-!
 # Normed spaces
@@ -949,129 +949,6 @@ instance : normed_space 𝕜 (restrict_scalars 𝕜 𝕜' E) :=
 
 end restrict_scalars
 
-section summable
-open_locale classical
-open finset filter
-variables [semi_normed_group α] [semi_normed_group β]
-
-lemma cauchy_seq_finset_iff_vanishing_norm {f : ι → α} :
-  cauchy_seq (λ s : finset ι, ∑ i in s, f i) ↔
-    ∀ε > (0 : ℝ), ∃s:finset ι, ∀t, disjoint t s → ∥ ∑ i in t, f i ∥ < ε :=
-begin
-  rw [cauchy_seq_finset_iff_vanishing, nhds_basis_ball.forall_iff],
-  { simp only [ball_zero_eq, set.mem_set_of_eq] },
-  { rintros s t hst ⟨s', hs'⟩,
-    exact ⟨s', λ t' ht', hst $ hs' _ ht'⟩ }
-end
-
-lemma summable_iff_vanishing_norm [complete_space α] {f : ι → α} :
-  summable f ↔ ∀ε > (0 : ℝ), ∃s:finset ι, ∀t, disjoint t s → ∥ ∑ i in t, f i ∥ < ε :=
-by rw [summable_iff_cauchy_seq_finset, cauchy_seq_finset_iff_vanishing_norm]
-
-lemma cauchy_seq_finset_of_norm_bounded {f : ι → α} (g : ι → ℝ) (hg : summable g)
-  (h : ∀i, ∥f i∥ ≤ g i) : cauchy_seq (λ s : finset ι, ∑ i in s, f i) :=
-cauchy_seq_finset_iff_vanishing_norm.2 $ assume ε hε,
-  let ⟨s, hs⟩ := summable_iff_vanishing_norm.1 hg ε hε in
-  ⟨s, assume t ht,
-    have ∥∑ i in t, g i∥ < ε := hs t ht,
-    have nn : 0 ≤ ∑ i in t, g i := finset.sum_nonneg (assume a _, le_trans (norm_nonneg _) (h a)),
-    lt_of_le_of_lt (norm_sum_le_of_le t (λ i _, h i)) $
-      by rwa [real.norm_eq_abs, abs_of_nonneg nn] at this⟩
-
-lemma cauchy_seq_finset_of_summable_norm {f : ι → α} (hf : summable (λa, ∥f a∥)) :
-  cauchy_seq (λ s : finset ι, ∑ a in s, f a) :=
-cauchy_seq_finset_of_norm_bounded _ hf (assume i, le_refl _)
-
-/-- If a function `f` is summable in norm, and along some sequence of finsets exhausting the space
-its sum is converging to a limit `a`, then this holds along all finsets, i.e., `f` is summable
-with sum `a`. -/
-lemma has_sum_of_subseq_of_summable {f : ι → α} (hf : summable (λa, ∥f a∥))
-  {s : γ → finset ι} {p : filter γ} [ne_bot p]
-  (hs : tendsto s p at_top) {a : α} (ha : tendsto (λ b, ∑ i in s b, f i) p (𝓝 a)) :
-  has_sum f a :=
-tendsto_nhds_of_cauchy_seq_of_subseq (cauchy_seq_finset_of_summable_norm hf) hs ha
-
-lemma has_sum_iff_tendsto_nat_of_summable_norm {f : ℕ → α} {a : α} (hf : summable (λi, ∥f i∥)) :
-  has_sum f a ↔ tendsto (λn:ℕ, ∑ i in range n, f i) at_top (𝓝 a) :=
-⟨λ h, h.tendsto_sum_nat,
-λ h, has_sum_of_subseq_of_summable hf tendsto_finset_range h⟩
-
-/-- The direct comparison test for series:  if the norm of `f` is bounded by a real function `g`
-which is summable, then `f` is summable. -/
-lemma summable_of_norm_bounded
-  [complete_space α] {f : ι → α} (g : ι → ℝ) (hg : summable g) (h : ∀i, ∥f i∥ ≤ g i) :
-  summable f :=
-by { rw summable_iff_cauchy_seq_finset, exact cauchy_seq_finset_of_norm_bounded g hg h }
-
-lemma has_sum.norm_le_of_bounded {f : ι → α} {g : ι → ℝ} {a : α} {b : ℝ}
-  (hf : has_sum f a) (hg : has_sum g b) (h : ∀ i, ∥f i∥ ≤ g i) :
-  ∥a∥ ≤ b :=
-le_of_tendsto_of_tendsto' hf.norm hg $ λ s, norm_sum_le_of_le _ $ λ i hi, h i
-
-/-- Quantitative result associated to the direct comparison test for series:  If `∑' i, g i` is
-summable, and for all `i`, `∥f i∥ ≤ g i`, then `∥∑' i, f i∥ ≤ ∑' i, g i`. Note that we do not
-assume that `∑' i, f i` is summable, and it might not be the case if `α` is not a complete space. -/
-lemma tsum_of_norm_bounded {f : ι → α} {g : ι → ℝ} {a : ℝ} (hg : has_sum g a)
-  (h : ∀ i, ∥f i∥ ≤ g i) :
-  ∥∑' i : ι, f i∥ ≤ a :=
-begin
-  by_cases hf : summable f,
-  { exact hf.has_sum.norm_le_of_bounded hg h },
-  { rw [tsum_eq_zero_of_not_summable hf, norm_zero],
-    exact ge_of_tendsto' hg (λ s, sum_nonneg $ λ i hi, (norm_nonneg _).trans (h i)) }
-end
-
-/-- If `∑' i, ∥f i∥` is summable, then `∥∑' i, f i∥ ≤ (∑' i, ∥f i∥)`. Note that we do not assume
-that `∑' i, f i` is summable, and it might not be the case if `α` is not a complete space. -/
-lemma norm_tsum_le_tsum_norm {f : ι → α} (hf : summable (λi, ∥f i∥)) :
-  ∥∑' i, f i∥ ≤ ∑' i, ∥f i∥ :=
-tsum_of_norm_bounded hf.has_sum $ λ i, le_rfl
-
-/-- Quantitative result associated to the direct comparison test for series: If `∑' i, g i` is
-summable, and for all `i`, `nnnorm (f i) ≤ g i`, then `nnnorm (∑' i, f i) ≤ ∑' i, g i`. Note that we
-do not assume that `∑' i, f i` is summable, and it might not be the case if `α` is not a complete
-space. -/
-lemma tsum_of_nnnorm_bounded {f : ι → α} {g : ι → ℝ≥0} {a : ℝ≥0} (hg : has_sum g a)
-  (h : ∀ i, nnnorm (f i) ≤ g i) :
-  nnnorm (∑' i : ι, f i) ≤ a :=
-begin
-  simp only [← nnreal.coe_le_coe, ← nnreal.has_sum_coe, coe_nnnorm] at *,
-  exact tsum_of_norm_bounded hg h
-end
-
-/-- If `∑' i, nnnorm (f i)` is summable, then `nnnorm (∑' i, f i) ≤ ∑' i, nnnorm (f i)`. Note that
-we do not assume that `∑' i, f i` is summable, and it might not be the case if `α` is not a complete
-space. -/
-lemma nnnorm_tsum_le {f : ι → α} (hf : summable (λi, nnnorm (f i))) :
-  nnnorm (∑' i, f i) ≤ ∑' i, nnnorm (f i) :=
-tsum_of_nnnorm_bounded hf.has_sum (λ i, le_rfl)
-
-variable [complete_space α]
-
-/-- Variant of the direct comparison test for series:  if the norm of `f` is eventually bounded by a
-real function `g` which is summable, then `f` is summable. -/
-lemma summable_of_norm_bounded_eventually {f : ι → α} (g : ι → ℝ) (hg : summable g)
-  (h : ∀ᶠ i in cofinite, ∥f i∥ ≤ g i) : summable f :=
-begin
-  replace h := mem_cofinite.1 h,
-  refine h.summable_compl_iff.mp _,
-  refine summable_of_norm_bounded _ (h.summable_compl_iff.mpr hg) _,
-  rintros ⟨a, h'⟩,
-  simpa using h'
-end
-
-lemma summable_of_nnnorm_bounded {f : ι → α} (g : ι → ℝ≥0) (hg : summable g)
-  (h : ∀i, ∥f i∥₊ ≤ g i) : summable f :=
-summable_of_norm_bounded (λ i, (g i : ℝ)) (nnreal.summable_coe.2 hg) (λ i, by exact_mod_cast h i)
-
-lemma summable_of_summable_norm {f : ι → α} (hf : summable (λa, ∥f a∥)) : summable f :=
-summable_of_norm_bounded _ hf (assume i, le_refl _)
-
-lemma summable_of_summable_nnnorm {f : ι → α} (hf : summable (λ a, ∥f a∥₊)) : summable f :=
-summable_of_nnnorm_bounded _ hf (assume i, le_refl _)
-
-end summable
-
 section cauchy_product
 
 /-! ## Multiplying two infinite sums in a normed ring
@@ -1192,32 +1069,3 @@ end
 end nat
 
 end cauchy_product
-
-namespace uniform_space
-namespace completion
-
-variables (V : Type*)
-
-instance [uniform_space V] [has_norm V] :
-  has_norm (completion V) :=
-{ norm := completion.extension has_norm.norm }
-
-@[simp] lemma norm_coe {V} [semi_normed_group V] (v : V) :
-  ∥(v : completion V)∥ = ∥v∥ :=
-completion.extension_coe uniform_continuous_norm v
-
-instance [semi_normed_group V] : normed_group (completion V) :=
-{ dist_eq :=
-  begin
-    intros x y,
-    apply completion.induction_on₂ x y; clear x y,
-    { refine is_closed_eq (completion.uniform_continuous_extension₂ _).continuous _,
-      exact continuous.comp completion.continuous_extension continuous_sub },
-    { intros x y,
-      rw [← completion.coe_sub, norm_coe, metric.completion.dist_eq, dist_eq_norm] }
-  end,
-  .. (show add_comm_group (completion V), by apply_instance),
-  .. (show metric_space (completion V), by apply_instance) }
-
-end completion
-end uniform_space

src/topology/uniform_space/completion.lean

@@ -452,7 +452,7 @@ cpkg.extend f
 
 variables [separated_space β]
 
-@[simp]lemma extension_coe (hf : uniform_continuous f) (a : α) :
+@[simp] lemma extension_coe (hf : uniform_continuous f) (a : α) :
   (completion.extension f) a = f a :=
 cpkg.extend_coe hf a