Coefficient slices in the tail variables

The k-th x_0-coefficient of a series in x_0, …, x_m (under splitFirst) is a series in the tail variables whose majorant norm at the tail radii is at most ρ_0^{-k} times the norm of the whole series: the monomial x'^x of the slice comes from x_0^k x'^x, of weight ρ_0^k times larger. Hence the coefficients of a convergent series are convergent (needed for the c_j of the preparation theorem). Conversely, a tail series lifted by liftTail has the same norm at any radius vector extending the tail radii. Not in the sources as such: these are estimates of the majorant-norm calculus of [GR71, Kapitel I].

The coefficient field K is ℝ or ℂ ([RCLike K]).

theorem Analytic.convNorm_coeff_splitFirst_le {K : Type u_1} [RCLike K] {m : ℕ} (ρ : Radius (m + 1)) (r : MvPowerSeries (Fin (m + 1)) K) (k : ℕ) : ConvNorm (fun (j : Fin m) => ↑ρ j.succ) ((PowerSeries.coeff k) ((splitFirst K m) r)) ≤ ↑((↑ρ 0)⁻¹ ^ k) * ConvNorm (↑ρ) r

The k-th x_0-coefficient of r has tail norm at most ρ_0^{-k} ‖r‖_ρ.

theorem Analytic.coeff_splitFirst_mem_conv {K : Type u_1} [RCLike K] {m : ℕ} {r : MvPowerSeries (Fin (m + 1)) K} (hr : r ∈ Conv K (m + 1)) (k : ℕ) : (PowerSeries.coeff k) ((splitFirst K m) r) ∈ Conv K m

The x_0-coefficients of a convergent series are convergent.

theorem Analytic.convNorm_liftTail {K : Type u_1} [RCLike K] {m : ℕ} (ρ : Fin (m + 1) → NNReal) (a : MvPowerSeries (Fin m) K) : ConvNorm ρ (liftTail a) = ConvNorm (fun (j : Fin m) => ρ j.succ) a

A lifted tail series has the norm of the tail series: ‖liftTail a‖_ρ = ‖a‖_{ρ'}.

theorem Analytic.liftTail_mem_conv {K : Type u_1} [RCLike K] {m : ℕ} {a : MvPowerSeries (Fin m) K} (ha : a ∈ Conv K m) : liftTail a ∈ Conv K (m + 1)