chore(analysis/normed/field/basic): split (#18195)

Split material on infinite sums out of `analysis/normed/field/basic` into a new file `/infinite_sum`.  This mimics the structure of `analysis/normed/group/*`, and reduces the imports of the former.

src/analysis/asymptotics/asymptotics.lean

@@ -3,6 +3,7 @@ Copyright (c) 2019 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Yury Kudryashov
 -/
+import analysis.normed.group.infinite_sum
 import analysis.normed_space.basic
 import topology.algebra.order.liminf_limsup
 import topology.local_homeomorph

src/analysis/normed/field/basic.lean

@@ -4,8 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Patrick Massot, Johannes Hölzl
 -/
 import algebra.algebra.subalgebra.basic
-import analysis.normed.group.infinite_sum
-import topology.algebra.module.basic
+import analysis.normed.group.basic
 import topology.instances.ennreal
 import topology.instances.rat
 
@@ -640,14 +639,6 @@ by simp [real.to_nnreal_of_nonneg, nnnorm, norm_of_nonneg, hx]
 lemma nnnorm_mul_to_nnreal (x : ℝ) {y : ℝ} (hy : 0 ≤ y) : ‖x‖₊ * y.to_nnreal = ‖x * y‖₊ :=
 by simp [real.to_nnreal_of_nonneg, nnnorm, norm_of_nonneg, hy]
 
-/-- If `E` is a nontrivial topological module over `ℝ`, then `E` has no isolated points.
-This is a particular case of `module.punctured_nhds_ne_bot`. -/
-instance punctured_nhds_module_ne_bot
-  {E : Type*} [add_comm_group E] [topological_space E] [has_continuous_add E] [nontrivial E]
-  [module ℝ E] [has_continuous_smul ℝ E] (x : E) :
-  ne_bot (𝓝[≠] x) :=
-module.punctured_nhds_ne_bot ℝ E x
-
 end real
 
 namespace nnreal
@@ -741,127 +732,6 @@ by simpa only [← nnreal.coe_le_coe, nnreal.coe_mul] using norm_zpow_le_mul_nor
 
 end
 
-section cauchy_product
-
-/-! ## Multiplying two infinite sums in a normed ring
-
-In this section, we prove various results about `(∑' x : ι, f x) * (∑' y : ι', g y)` in a normed
-ring. There are similar results proven in `topology/algebra/infinite_sum` (e.g `tsum_mul_tsum`),
-but in a normed ring we get summability results which aren't true in general.
-
-We first establish results about arbitrary index types, `β` and `γ`, and then we specialize to
-`β = γ = ℕ` to prove the Cauchy product formula
-(see `tsum_mul_tsum_eq_tsum_sum_antidiagonal_of_summable_norm`).
-
-### Arbitrary index types
--/
-
-variables {ι' : Type*} [normed_ring α]
-
-open finset
-open_locale classical
-
-lemma summable.mul_of_nonneg {f : ι → ℝ} {g : ι' → ℝ}
-  (hf : summable f) (hg : summable g) (hf' : 0 ≤ f) (hg' : 0 ≤ g) :
-  summable (λ (x : ι × ι'), f x.1 * g x.2) :=
-let ⟨s, hf⟩ := hf in
-let ⟨t, hg⟩ := hg in
-suffices this : ∀ u : finset (ι × ι'), ∑ x in u, f x.1 * g x.2 ≤ s*t,
-  from summable_of_sum_le (λ x, mul_nonneg (hf' _) (hg' _)) this,
-assume u,
-calc  ∑ x in u, f x.1 * g x.2
-    ≤ ∑ x in u.image prod.fst ×ˢ u.image prod.snd, f x.1 * g x.2 :
-      sum_mono_set_of_nonneg (λ x, mul_nonneg (hf' _) (hg' _)) subset_product
-... = ∑ x in u.image prod.fst, ∑ y in u.image prod.snd, f x * g y : sum_product
-... = ∑ x in u.image prod.fst, f x * ∑ y in u.image prod.snd, g y :
-      sum_congr rfl (λ x _, mul_sum.symm)
-... ≤ ∑ x in u.image prod.fst, f x * t :
-      sum_le_sum
-        (λ x _, mul_le_mul_of_nonneg_left (sum_le_has_sum _ (λ _ _, hg' _) hg) (hf' _))
-... = (∑ x in u.image prod.fst, f x) * t : sum_mul.symm
-... ≤ s * t :
-      mul_le_mul_of_nonneg_right (sum_le_has_sum _ (λ _ _, hf' _) hf) (hg.nonneg $ λ _, hg' _)
-
-lemma summable.mul_norm {f : ι → α} {g : ι' → α}
-  (hf : summable (λ x, ‖f x‖)) (hg : summable (λ x, ‖g x‖)) :
-  summable (λ (x : ι × ι'), ‖f x.1 * g x.2‖) :=
-summable_of_nonneg_of_le (λ x, norm_nonneg (f x.1 * g x.2)) (λ x, norm_mul_le (f x.1) (g x.2))
-  (hf.mul_of_nonneg hg (λ x, norm_nonneg $ f x) (λ x, norm_nonneg $ g x) : _)
-
-lemma summable_mul_of_summable_norm [complete_space α] {f : ι → α} {g : ι' → α}
-  (hf : summable (λ x, ‖f x‖)) (hg : summable (λ x, ‖g x‖)) :
-  summable (λ (x : ι × ι'), f x.1 * g x.2) :=
-summable_of_summable_norm (hf.mul_norm hg)
-
-/-- Product of two infinites sums indexed by arbitrary types.
-    See also `tsum_mul_tsum` if `f` and `g` are *not* absolutely summable. -/
-lemma tsum_mul_tsum_of_summable_norm [complete_space α] {f : ι → α} {g : ι' → α}
-  (hf : summable (λ x, ‖f x‖)) (hg : summable (λ x, ‖g x‖)) :
-  (∑' x, f x) * (∑' y, g y) = (∑' z : ι × ι', f z.1 * g z.2) :=
-tsum_mul_tsum (summable_of_summable_norm hf) (summable_of_summable_norm hg)
-  (summable_mul_of_summable_norm hf hg)
-
-/-! ### `ℕ`-indexed families (Cauchy product)
-
-We prove two versions of the Cauchy product formula. The first one is
-`tsum_mul_tsum_eq_tsum_sum_range_of_summable_norm`, where the `n`-th term is a sum over
-`finset.range (n+1)` involving `nat` subtraction.
-In order to avoid `nat` subtraction, we also provide
-`tsum_mul_tsum_eq_tsum_sum_antidiagonal_of_summable_norm`,
-where the `n`-th term is a sum over all pairs `(k, l)` such that `k+l=n`, which corresponds to the
-`finset` `finset.nat.antidiagonal n`. -/
-
-section nat
-
-open finset.nat
-
-lemma summable_norm_sum_mul_antidiagonal_of_summable_norm {f g : ℕ → α}
-  (hf : summable (λ x, ‖f x‖)) (hg : summable (λ x, ‖g x‖)) :
-  summable (λ n, ‖∑ kl in antidiagonal n, f kl.1 * g kl.2‖) :=
-begin
-  have := summable_sum_mul_antidiagonal_of_summable_mul
-    (summable.mul_of_nonneg hf hg (λ _, norm_nonneg _) (λ _, norm_nonneg _)),
-  refine summable_of_nonneg_of_le (λ _, norm_nonneg _) _ this,
-  intros n,
-  calc  ‖∑ kl in antidiagonal n, f kl.1 * g kl.2‖
-      ≤ ∑ kl in antidiagonal n, ‖f kl.1 * g kl.2‖ : norm_sum_le _ _
-  ... ≤ ∑ kl in antidiagonal n, ‖f kl.1‖ * ‖g kl.2‖ : sum_le_sum (λ i _, norm_mul_le _ _)
-end
-
-/-- The Cauchy product formula for the product of two infinite sums indexed by `ℕ`,
-    expressed by summing on `finset.nat.antidiagonal`.
-    See also `tsum_mul_tsum_eq_tsum_sum_antidiagonal` if `f` and `g` are
-    *not* absolutely summable. -/
-lemma tsum_mul_tsum_eq_tsum_sum_antidiagonal_of_summable_norm [complete_space α] {f g : ℕ → α}
-  (hf : summable (λ x, ‖f x‖)) (hg : summable (λ x, ‖g x‖)) :
-  (∑' n, f n) * (∑' n, g n) = ∑' n, ∑ kl in antidiagonal n, f kl.1 * g kl.2 :=
-tsum_mul_tsum_eq_tsum_sum_antidiagonal (summable_of_summable_norm hf) (summable_of_summable_norm hg)
-  (summable_mul_of_summable_norm hf hg)
-
-lemma summable_norm_sum_mul_range_of_summable_norm {f g : ℕ → α}
-  (hf : summable (λ x, ‖f x‖)) (hg : summable (λ x, ‖g x‖)) :
-  summable (λ n, ‖∑ k in range (n+1), f k * g (n - k)‖) :=
-begin
-  simp_rw ← sum_antidiagonal_eq_sum_range_succ (λ k l, f k * g l),
-  exact summable_norm_sum_mul_antidiagonal_of_summable_norm hf hg
-end
-
-/-- The Cauchy product formula for the product of two infinite sums indexed by `ℕ`,
-    expressed by summing on `finset.range`.
-    See also `tsum_mul_tsum_eq_tsum_sum_range` if `f` and `g` are
-    *not* absolutely summable. -/
-lemma tsum_mul_tsum_eq_tsum_sum_range_of_summable_norm [complete_space α] {f g : ℕ → α}
-  (hf : summable (λ x, ‖f x‖)) (hg : summable (λ x, ‖g x‖)) :
-  (∑' n, f n) * (∑' n, g n) = ∑' n, ∑ k in range (n+1), f k * g (n - k) :=
-begin
-  simp_rw ← sum_antidiagonal_eq_sum_range_succ (λ k l, f k * g l),
-  exact tsum_mul_tsum_eq_tsum_sum_antidiagonal_of_summable_norm hf hg
-end
-
-end nat
-
-end cauchy_product
-
 section ring_hom_isometric
 
 variables {R₁ : Type*} {R₂ : Type*} {R₃ : Type*}

src/analysis/normed/field/infinite_sum.lean

@@ -0,0 +1,124 @@
+/-
+Copyright (c) 2021 Anatole Dedecker. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Anatole Dedecker
+-/
+import analysis.normed.field.basic
+import analysis.normed.group.infinite_sum
+
+/-! # Multiplying two infinite sums in a normed ring
+
+In this file, we prove various results about `(∑' x : ι, f x) * (∑' y : ι', g y)` in a normed
+ring. There are similar results proven in `topology/algebra/infinite_sum` (e.g `tsum_mul_tsum`),
+but in a normed ring we get summability results which aren't true in general.
+
+We first establish results about arbitrary index types, `β` and `γ`, and then we specialize to
+`β = γ = ℕ` to prove the Cauchy product formula
+(see `tsum_mul_tsum_eq_tsum_sum_antidiagonal_of_summable_norm`).
+!-/
+
+variables {α : Type*} {ι : Type*} {ι' : Type*} [normed_ring α]
+
+open_locale big_operators classical
+open finset
+
+/-! ### Arbitrary index types -/
+
+lemma summable.mul_of_nonneg {f : ι → ℝ} {g : ι' → ℝ}
+  (hf : summable f) (hg : summable g) (hf' : 0 ≤ f) (hg' : 0 ≤ g) :
+  summable (λ (x : ι × ι'), f x.1 * g x.2) :=
+let ⟨s, hf⟩ := hf in
+let ⟨t, hg⟩ := hg in
+suffices this : ∀ u : finset (ι × ι'), ∑ x in u, f x.1 * g x.2 ≤ s*t,
+  from summable_of_sum_le (λ x, mul_nonneg (hf' _) (hg' _)) this,
+assume u,
+calc  ∑ x in u, f x.1 * g x.2
+    ≤ ∑ x in u.image prod.fst ×ˢ u.image prod.snd, f x.1 * g x.2 :
+      sum_mono_set_of_nonneg (λ x, mul_nonneg (hf' _) (hg' _)) subset_product
+... = ∑ x in u.image prod.fst, ∑ y in u.image prod.snd, f x * g y : sum_product
+... = ∑ x in u.image prod.fst, f x * ∑ y in u.image prod.snd, g y :
+      sum_congr rfl (λ x _, mul_sum.symm)
+... ≤ ∑ x in u.image prod.fst, f x * t :
+      sum_le_sum
+        (λ x _, mul_le_mul_of_nonneg_left (sum_le_has_sum _ (λ _ _, hg' _) hg) (hf' _))
+... = (∑ x in u.image prod.fst, f x) * t : sum_mul.symm
+... ≤ s * t :
+      mul_le_mul_of_nonneg_right (sum_le_has_sum _ (λ _ _, hf' _) hf) (hg.nonneg $ λ _, hg' _)
+
+lemma summable.mul_norm {f : ι → α} {g : ι' → α}
+  (hf : summable (λ x, ‖f x‖)) (hg : summable (λ x, ‖g x‖)) :
+  summable (λ (x : ι × ι'), ‖f x.1 * g x.2‖) :=
+summable_of_nonneg_of_le (λ x, norm_nonneg (f x.1 * g x.2)) (λ x, norm_mul_le (f x.1) (g x.2))
+  (hf.mul_of_nonneg hg (λ x, norm_nonneg $ f x) (λ x, norm_nonneg $ g x) : _)
+
+lemma summable_mul_of_summable_norm [complete_space α] {f : ι → α} {g : ι' → α}
+  (hf : summable (λ x, ‖f x‖)) (hg : summable (λ x, ‖g x‖)) :
+  summable (λ (x : ι × ι'), f x.1 * g x.2) :=
+summable_of_summable_norm (hf.mul_norm hg)
+
+/-- Product of two infinites sums indexed by arbitrary types.
+    See also `tsum_mul_tsum` if `f` and `g` are *not* absolutely summable. -/
+lemma tsum_mul_tsum_of_summable_norm [complete_space α] {f : ι → α} {g : ι' → α}
+  (hf : summable (λ x, ‖f x‖)) (hg : summable (λ x, ‖g x‖)) :
+  (∑' x, f x) * (∑' y, g y) = (∑' z : ι × ι', f z.1 * g z.2) :=
+tsum_mul_tsum (summable_of_summable_norm hf) (summable_of_summable_norm hg)
+  (summable_mul_of_summable_norm hf hg)
+
+/-! ### `ℕ`-indexed families (Cauchy product)
+
+We prove two versions of the Cauchy product formula. The first one is
+`tsum_mul_tsum_eq_tsum_sum_range_of_summable_norm`, where the `n`-th term is a sum over
+`finset.range (n+1)` involving `nat` subtraction.
+In order to avoid `nat` subtraction, we also provide
+`tsum_mul_tsum_eq_tsum_sum_antidiagonal_of_summable_norm`,
+where the `n`-th term is a sum over all pairs `(k, l)` such that `k+l=n`, which corresponds to the
+`finset` `finset.nat.antidiagonal n`. -/
+
+section nat
+
+open finset.nat
+
+lemma summable_norm_sum_mul_antidiagonal_of_summable_norm {f g : ℕ → α}
+  (hf : summable (λ x, ‖f x‖)) (hg : summable (λ x, ‖g x‖)) :
+  summable (λ n, ‖∑ kl in antidiagonal n, f kl.1 * g kl.2‖) :=
+begin
+  have := summable_sum_mul_antidiagonal_of_summable_mul
+    (summable.mul_of_nonneg hf hg (λ _, norm_nonneg _) (λ _, norm_nonneg _)),
+  refine summable_of_nonneg_of_le (λ _, norm_nonneg _) _ this,
+  intros n,
+  calc  ‖∑ kl in antidiagonal n, f kl.1 * g kl.2‖
+      ≤ ∑ kl in antidiagonal n, ‖f kl.1 * g kl.2‖ : norm_sum_le _ _
+  ... ≤ ∑ kl in antidiagonal n, ‖f kl.1‖ * ‖g kl.2‖ : sum_le_sum (λ i _, norm_mul_le _ _)
+end
+
+/-- The Cauchy product formula for the product of two infinite sums indexed by `ℕ`,
+    expressed by summing on `finset.nat.antidiagonal`.
+    See also `tsum_mul_tsum_eq_tsum_sum_antidiagonal` if `f` and `g` are
+    *not* absolutely summable. -/
+lemma tsum_mul_tsum_eq_tsum_sum_antidiagonal_of_summable_norm [complete_space α] {f g : ℕ → α}
+  (hf : summable (λ x, ‖f x‖)) (hg : summable (λ x, ‖g x‖)) :
+  (∑' n, f n) * (∑' n, g n) = ∑' n, ∑ kl in antidiagonal n, f kl.1 * g kl.2 :=
+tsum_mul_tsum_eq_tsum_sum_antidiagonal (summable_of_summable_norm hf) (summable_of_summable_norm hg)
+  (summable_mul_of_summable_norm hf hg)
+
+lemma summable_norm_sum_mul_range_of_summable_norm {f g : ℕ → α}
+  (hf : summable (λ x, ‖f x‖)) (hg : summable (λ x, ‖g x‖)) :
+  summable (λ n, ‖∑ k in range (n+1), f k * g (n - k)‖) :=
+begin
+  simp_rw ← sum_antidiagonal_eq_sum_range_succ (λ k l, f k * g l),
+  exact summable_norm_sum_mul_antidiagonal_of_summable_norm hf hg
+end
+
+/-- The Cauchy product formula for the product of two infinite sums indexed by `ℕ`,
+    expressed by summing on `finset.range`.
+    See also `tsum_mul_tsum_eq_tsum_sum_range` if `f` and `g` are
+    *not* absolutely summable. -/
+lemma tsum_mul_tsum_eq_tsum_sum_range_of_summable_norm [complete_space α] {f g : ℕ → α}
+  (hf : summable (λ x, ‖f x‖)) (hg : summable (λ x, ‖g x‖)) :
+  (∑' n, f n) * (∑' n, g n) = ∑' n, ∑ k in range (n+1), f k * g (n - k) :=
+begin
+  simp_rw ← sum_antidiagonal_eq_sum_range_succ (λ k l, f k * g l),
+  exact tsum_mul_tsum_eq_tsum_sum_antidiagonal_of_summable_norm hf hg
+end
+
+end nat

src/analysis/normed_space/basic.lean

@@ -7,6 +7,7 @@ import algebra.algebra.pi
 import algebra.algebra.restrict_scalars
 import analysis.normed.field.basic
 import data.real.sqrt
+import topology.algebra.module.basic
 
 /-!
 # Normed spaces
@@ -341,6 +342,14 @@ lemma nnnorm_surjective : surjective (nnnorm : E → ℝ≥0) :=
 
 end surj
 
+/-- If `E` is a nontrivial topological module over `ℝ`, then `E` has no isolated points.
+This is a particular case of `module.punctured_nhds_ne_bot`. -/
+instance real.punctured_nhds_module_ne_bot
+  {E : Type*} [add_comm_group E] [topological_space E] [has_continuous_add E] [nontrivial E]
+  [module ℝ E] [has_continuous_smul ℝ E] (x : E) :
+  ne_bot (𝓝[≠] x) :=
+module.punctured_nhds_ne_bot ℝ E x
+
 theorem interior_closed_ball' [normed_space ℝ E] [nontrivial E] (x : E) (r : ℝ) :
   interior (closed_ball x r) = ball x r :=
 begin

src/analysis/normed_space/exponential.lean

@@ -5,6 +5,7 @@ Authors: Anatole Dedecker, Eric Wieser
 -/
 import analysis.analytic.basic
 import analysis.complex.basic
+import analysis.normed.field.infinite_sum
 import data.nat.choose.cast
 import data.finset.noncomm_prod
 import topology.algebra.algebra