Termwise primitives of restricted power series

Over a normed field K of characteristic zero, the termwise primitive ∫ · dXᵢ divides the coefficient aᵥ by νᵢ + 1 and multiplies the weight by the radius cᵢ. Since ‖(νᵢ + 1)⁻¹‖ grows at most polynomially in νᵢ (NormedField.exists_norm_inv_natCast_le_rpow), the primitive loses an arbitrarily small amount of the radius in the variable Xᵢ: for polyradii c' ≤ c with c'ᵢ < cᵢ, it maps series restricted at c to series restricted at c', with a Gauss norm bound

‖∫ f dXᵢ‖_{c'} ≤ C ‖f‖_c.

The radius cannot be kept: over ℚ_p the series ∑ₘ p^m X^(p^m - 1) is restricted at radius 1, but its primitive ∑ₘ X^(p^m) is not. In particular, over an ultrametric field of characteristic zero, termwise primitives preserve the overconvergent series, those restricted at some radius greater than 1.

Main results

• MvPowerSeries.exists_norm_coeff_primitive_mul_prod_le: the weighted coefficient norms of ∫ f dXᵢ at c' are bounded by C times those of f at c.
• MvPowerSeries.exists_gaussNorm_primitive_le: the Gauss norm bound.
• MvPowerSeries.IsRestricted.primitive: the primitive of a series restricted at c is restricted at c'.
• MvPowerSeries.restrictedPrimitive: over an ultrametric field, the primitive as a K-linear map from series restricted at c to series restricted at c', bounded for the Gauss norms (MvPowerSeries.exists_norm_restrictedPrimitive_le) and hence continuous.

References

• E. Grosse-Klönne, Rigid analytic spaces with overconvergent structure sheaf, J. reine angew. Math. 519 (2000), §1.2.

theorem MvPowerSeries.norm_coeff_add_single_primitive {σ : Type u_1} {K : Type u_2} [NormedField K] [CharZero K] {i : σ} (f : MvPowerSeries σ K) (n : σ →₀ ℕ) : ‖(coeff (n + Finsupp.single i 1)) ((primitive i) f)‖ = ‖(↑(n i) + 1)⁻¹‖ * ‖(coeff n) f‖

The coefficient of the termwise primitive at ν + eᵢ has norm ‖(νᵢ + 1)⁻¹‖ ‖aᵥ‖.

theorem MvPowerSeries.exists_norm_coeff_primitive_mul_prod_le {σ : Type u_1} {K : Type u_2} [NormedField K] [CharZero K] (c c' : σ → ℝ) (i : σ) (hc' : ∀ (j : σ), 0 ≤ c' j) (hle : ∀ (j : σ), c' j ≤ c j) (hlt : c' i < c i) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (f : MvPowerSeries σ K) (n : σ →₀ ℕ), (‖(coeff n) ((primitive i) f)‖ * n.prod fun (x1 : σ) (x2 : ℕ) => c' x1 ^ x2) ≤ C * (‖(coeff (n - Finsupp.single i 1)) f‖ * (n - Finsupp.single i 1).prod fun (x1 : σ) (x2 : ℕ) => c x1 ^ x2)

Primitives lose an arbitrarily small amount of radius. Over a normed field of characteristic zero, for polyradii 0 ≤ c' ≤ c with c'ᵢ < cᵢ, there is C ≥ 0 such that the weighted coefficient norms of ∫ f dXᵢ at c' are bounded by C times the weighted coefficient norms of f at c, shifted down by eᵢ.

theorem MvPowerSeries.exists_gaussNorm_primitive_le {σ : Type u_1} {K : Type u_2} [NormedField K] [CharZero K] (c c' : σ → ℝ) (i : σ) (hc' : ∀ (j : σ), 0 ≤ c' j) (hle : ∀ (j : σ), c' j ≤ c j) (hlt : c' i < c i) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (f : MvPowerSeries σ K), HasGaussNorm norm c f → HasGaussNorm norm c' ((primitive i) f) ∧ gaussNorm norm c' ((primitive i) f) ≤ C * gaussNorm norm c f

The Gauss norm bound for primitives. Over a normed field of characteristic zero, for polyradii 0 ≤ c' ≤ c with c'ᵢ < cᵢ, there is C ≥ 0 such that for every f with a Gauss norm at c, ∫ f dXᵢ has a Gauss norm at c' and gaussNorm c' (∫ f dXᵢ) ≤ C * gaussNorm c f.

theorem MvPowerSeries.IsRestricted.primitive {σ : Type u_1} {K : Type u_2} [NormedField K] [CharZero K] {c c' : σ → ℝ} {i : σ} (hc' : ∀ (j : σ), 0 ≤ c' j) (hle : ∀ (j : σ), c' j ≤ c j) (hlt : c' i < c i) {f : MvPowerSeries σ K} (hf : IsRestricted c f) : IsRestricted c' ((MvPowerSeries.primitive i) f)

Primitives of restricted series. Over a normed field of characteristic zero, for polyradii 0 ≤ c' ≤ c with c'ᵢ < cᵢ, the termwise primitive of a series restricted at c is restricted at c'.

noncomputable def MvPowerSeries.restrictedPrimitive {σ : Type u_1} {K : Type u_2} [NormedField K] [IsUltrametricDist K] [CharZero K] {c c' : σ → ℝ} [∀ (j : σ), Fact (0 < c j)] [∀ (j : σ), Fact (0 < c' j)] (i : σ) (hle : ∀ (j : σ), c' j ≤ c j) (hlt : c' i < c i) : ↥(IsRestricted.subring c) →ₗ[K] ↥(IsRestricted.subring c')

The termwise primitive with respect to Xᵢ, as a K-linear map from series restricted at positive polyradii c to series restricted at positive polyradii c' ≤ c with c'ᵢ < cᵢ. The field K is ultrametric, as needed for the restricted series to form a ring.

@[simp]

theorem MvPowerSeries.coe_restrictedPrimitive {σ : Type u_1} {K : Type u_2} [NormedField K] [IsUltrametricDist K] [CharZero K] {c c' : σ → ℝ} [∀ (j : σ), Fact (0 < c j)] [∀ (j : σ), Fact (0 < c' j)] (i : σ) (hle : ∀ (j : σ), c' j ≤ c j) (hlt : c' i < c i) (f : ↥(IsRestricted.subring c)) : ↑((restrictedPrimitive i hle hlt) f) = (primitive i) ↑f

The primitive of a restricted series is its termwise primitive as a formal series.

theorem MvPowerSeries.exists_norm_restrictedPrimitive_le {σ : Type u_1} {K : Type u_2} [NormedField K] [IsUltrametricDist K] [CharZero K] {c c' : σ → ℝ} [∀ (j : σ), Fact (0 < c j)] [∀ (j : σ), Fact (0 < c' j)] (i : σ) (hle : ∀ (j : σ), c' j ≤ c j) (hlt : c' i < c i) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (f : ↥(IsRestricted.subring c)), ‖(restrictedPrimitive i hle hlt) f‖ ≤ C * ‖f‖

The operator bound for primitives. The termwise primitive from series restricted at c to series restricted at c' is bounded for the Gauss norms.

theorem MvPowerSeries.continuous_restrictedPrimitive {σ : Type u_1} {K : Type u_2} [NormedField K] [IsUltrametricDist K] [CharZero K] {c c' : σ → ℝ} [∀ (j : σ), Fact (0 < c j)] [∀ (j : σ), Fact (0 < c' j)] (i : σ) (hle : ∀ (j : σ), c' j ≤ c j) (hlt : c' i < c i) : Continuous ⇑(restrictedPrimitive i hle hlt)

The termwise primitive from series restricted at c to series restricted at c' is continuous for the Gauss norms.