Summing the coefficients of a multivariate power series along a ray

Fix an exponent d and read the coefficients of u along the rays ν, ν + d, ν + 2d, …. If the coefficients of u converge along the cofinite filter, then the coefficients along each single ray have the same limit once the step d is nonzero. This needs only a topological coefficient semiring, with no continuity assumption on its operations.

For a nonarchimedean coefficient ring, if the coefficients of u tend to zero along the cofinite filter, then so do the ray sums. No completeness or separation hypothesis is needed for this convergence statement about tsum.

Peeling the first term of a ray is a statement about an actual sum, so it asks for more: the coefficient group must also be complete and separated for a compatible uniform structure ([UniformSpace R] [IsUniformAddGroup R] [CompleteSpace R] [T0Space R]), which is what makes each ray summable and its tsum the value one expects.

The rays are what turns a statement about a diagonal — the exponents congruent to one another modulo d — into one about coefficients, which is how the decomposition of a two-variable restricted series modulo 1 - XY is proved.

Main results

• MvPowerSeries.tendsto_tsum_coeff_add_nsmul: the ray sums tend to zero along cofinite.
• MvPowerSeries.tendsto_coeff_add_nsmul: along one ray the coefficients have the same limit as the full coefficient family, provided the step d is nonzero.
• MvPowerSeries.tsum_coeff_add_nsmul_eq: peeling the first term of a ray, over a complete separated nonarchimedean uniform additive group.

theorem MvPowerSeries.tendsto_coeff_add_nsmul {σ : Type u_1} {R : Type u_2} [Semiring R] [TopologicalSpace R] (u : MvPowerSeries σ R) {a : R} (hu : Filter.Tendsto (fun (x : σ →₀ ℕ) => (coeff x) u) Filter.cofinite (nhds a)) {d : σ →₀ ℕ} (hd : d ≠ 0) (ν : σ →₀ ℕ) : Filter.Tendsto (fun (n : ℕ) => (coeff (ν + n • d)) u) Filter.cofinite (nhds a)

Along a ray with nonzero step, the coefficients have the same cofinite limit as the full coefficient family.

theorem MvPowerSeries.tendsto_tsum_coeff_add_nsmul {σ : Type u_1} {R : Type u_2} [Ring R] [TopologicalSpace R] [NonarchimedeanAddGroup R] (u : MvPowerSeries σ R) (hu : Filter.Tendsto (fun (x : σ →₀ ℕ) => (coeff x) u) Filter.cofinite (nhds 0)) (d : σ →₀ ℕ) : Filter.Tendsto (fun (ν : σ →₀ ℕ) => ∑' (n : ℕ), (coeff (ν + n • d)) u) Filter.cofinite (nhds 0)

If the coefficients of u tend to zero along cofinite, so does the family of ray sums ν ↦ ∑' n, coeff (ν + n • d) u in a nonarchimedean coefficient ring.

theorem MvPowerSeries.tsum_coeff_add_nsmul_eq {σ : Type u_1} {R : Type u_2} [Ring R] [UniformSpace R] [IsUniformAddGroup R] [NonarchimedeanAddGroup R] [CompleteSpace R] [T0Space R] (u : MvPowerSeries σ R) (hu : Filter.Tendsto (fun (x : σ →₀ ℕ) => (coeff x) u) Filter.cofinite (nhds 0)) {d : σ →₀ ℕ} (hd : d ≠ 0) (ν : σ →₀ ℕ) : ∑' (n : ℕ), (coeff (ν + n • d)) u = (coeff ν) u + ∑' (n : ℕ), (coeff (ν + d + n • d)) u

The sum along a ray with nonzero step is its first coefficient plus the sum along the ray starting one step further, in a complete separated nonarchimedean coefficient group.