theorem BanachSpace.prod_banach_space (B₁ : Type u_1) (B₂ : Type u_2) [NormedAddCommGroup B₁] [NormedAddCommGroup B₂] [CompleteSpace B₁] [CompleteSpace B₂] : CompleteSpace (WithLp 1 (B₁ × B₂))

If $B_1, B_2$ are Banach spaces, then $B_1 \times B_2$ (with operations done entry by entry) with norm $\|(b_1, b_2)\| = \|b_1\| + \|b_2\|$ is a Banach space. Here this is expressed as completeness of the $L^1$ product WithLp 1 (B₁ × B₂).

theorem BanachSpace.cauchySeq_of_summable_norm {E : Type u_1} [SeminormedAddCommGroup E] {v : ℕ → E} (hv : Summable fun (n : ℕ) => ‖v n‖) : CauchySeq fun (m : ℕ) => ∑ i ∈ Finset.range m, v i

If $\sum_n v_n$ is absolutely summable (i.e. $\sum_n \|v_n\|$ is summable), then the sequence of partial sums $\left\{\sum_{i=0}^{m-1} v_i\right\}_{m=1}^{\infty}$ is Cauchy.