Normally convergent families of formal multilinear series

Mathlib has no generic AnalyticAt.tsum theorem. The criterion below provides the precise replacement needed here: absolute coefficient summability together with one common positive-radius majorant lets us exchange the family sum and the homogeneous-degree sum and produces a HasFPowerSeriesOnBall witness.

noncomputable def ClassicalComplexWPT.seriesTsum {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {I : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (p : I → FormalMultilinearSeries 𝕜 E F) : FormalMultilinearSeries 𝕜 E F

Coefficientwise sum of a family of formal multilinear series.

Equations

• ClassicalComplexWPT.seriesTsum p n = ∑' (i : I), p i n

noncomputable def ClassicalComplexWPT.sumTsum {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {I : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (p : I → FormalMultilinearSeries 𝕜 E F) (x : E) : F

Pointwise sum of the functions represented by a family of formal multilinear series.

Equations

• ClassicalComplexWPT.sumTsum p x = ∑' (i : I), (p i).sum x

theorem ClassicalComplexWPT.norm_seriesTsum_le {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {I : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (p : I → FormalMultilinearSeries 𝕜 E F) (hcoeff : ∀ (n : ℕ), Summable fun (i : I) => ‖p i n‖) (n : ℕ) : ‖seriesTsum p n‖ ≤ ∑' (i : I), ‖p i n‖

theorem ClassicalComplexWPT.seriesTsum_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {I : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] (p : I → FormalMultilinearSeries 𝕜 E F) (n : ℕ) (hcoeff : Summable fun (i : I) => ‖p i n‖) (y : E) : ((seriesTsum p n) fun (x : Fin n) => y) = ∑' (i : I), (p i n) fun (x : Fin n) => y

Evaluation commutes with the coefficientwise sum of a normally summable family.

theorem ClassicalComplexWPT.hasFPowerSeriesOnBall_sumTsum {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {I : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] (p : I → FormalMultilinearSeries 𝕜 E F) (r : NNReal) (hr : 0 < r) (hcoeff : ∀ (n : ℕ), Summable fun (i : I) => ‖p i n‖) (hmajor : Summable fun (n : ℕ) => (∑' (i : I), ‖p i n‖) * ↑r ^ n) : HasFPowerSeriesOnBall (sumTsum p) (seriesTsum p) 0 ↑r

A common-radius normal-convergence criterion for summing an arbitrary family of formal multilinear series.