Commit 2024-06-04 20:41 aecbe3cf

feat: convergent series in the completion of a group (#11998) Prove the following.

• Inducing.hasProd_iff / Inducing.hasSum_iff: Let $g \colon \beta \to \alpha$ be an inducing homomorphism of topological additive commutative monoids. A series $\sum_{i \in I} b_i$ unconditionally converges to $b \in \beta$ if and only if $\sum_{i \in I} g(b_i)$ unconditionally converges to $g(b)$. (That is, if $g$ is inducing, then the converse of HasProd.map / HasSum.map holds.)
• Multipliable.map_tprod / Summable.map_tsum: Let $g \colon \beta \to \alpha$ be a continuous homomorphism of topological additive commutative monoids. If the series $\sum_{i \in I} b_i$ converges unconditionally, then $g\left(\sum_{i \in I} b_i\right) = \sum_{i \in I} g(b_i)$.
• Inducing.multipliable_iff_tprod_comp_mem_range / Inducing.summable_iff_tsum_comp_mem_range: Let $g \colon \beta \to \alpha$ be an inducing homomorphism of topological additive commutative monoids. Assume that $\alpha$ is Hausdorff. Then a series $\sum_{i \in I} b_i$ converges unconditionally if and only if the series $\sum_{i \in I} g(b_i)$ converges unconditionally and its value lies in the range of $g$.
• hasSum_iff_hasSum_compl: Let $\alpha$ be a uniform additive abelian group. An equation $\sum_{i \in I} a_i = a$ holds in $\alpha$ if and only if it holds in $\hat{\alpha}$.
• summable_iff_summable_compl_and_tsum_mem: Let $\alpha$ be a uniform additive abelian group. A series $\sum_{i \in I} a_i$ is unconditionally summable in $\alpha$ if and only if it is unconditionally summable in $\hat{\alpha}$ and its value is in $\alpha$.
• summable_iff_cauchySeq_finset_and_tsum_mem: Let $\alpha$ be a uniform additive abelian group. A series $\sum_{i \in I} a_i$ is unconditionally summable in $\alpha$ if and only if its partial sums form a Cauchy net and its value in $\hat{\alpha}$ lies in $\alpha$.
• Summable.toCompl_tsum: If a series $\sum_{i \in I} a_i$ is unconditionally summable in $\alpha$, then its value in $\alpha$ is equal to its value in $\hat{\alpha}$. Note: This PR does not include multiplicative analogues of hasSum_iff_hasSum_compl, summable_iff_summable_compl_and_tsum_mem, summable_iff_cauchySeq_finset_and_tsum_mem, or Summable.toCompl_tsum. This is because mathlib does not currently put a group structure on the completion of a uniform multiplicative group (see #11837). Once the group structure on the completion of a uniform multiplicative group is defined, the multiplicative analogues of these four theorems can easily be added. Note: The argument (g : G) of Multipliable.map_tprod is explicit to match Multipliable.map. At some point, it might be desirable to make these arguments (and several others) implicit, but that is outside the scope of this PR.