The function of a polynomial in one coordinate with base coefficients

The relations of the local parametrization theorem ([GR84, Chapter 3, §1]; [Fre17, Ch. I, 8.2]) are elements W(X_i) = ∑_k W_k(x_base) X_i^k of 𝒪_n: a polynomial W ∈ 𝒪_d[T] with its coefficients embedded from the base along e and evaluated at the coordinate series X_i. Near 0, the function of such an element at a point x is the polynomial over ℂ obtained by evaluating the coefficients at the base point x ∘ e (specialize, Specialize.lean), evaluated at x_i. This is the bridge between the algebra of the normalization and the division argument (elements of 𝒪_n) and the analysis of the graph structure (functions on ℂⁿ), through the function-level identities evalSeries_conv_{add,mul,pow,sum}_eventually.

theorem Analytic.evalSeries_eval_map_convEmbed_eventually {K : Type u_1} [RCLike K] {n d : ℕ} (e : Fin d ↪ Fin n) (i : Fin n) (W : Polynomial ↥(Conv K d)) : evalSeries ↑(Polynomial.eval (convX K i) (Polynomial.map (convEmbed K e).toRingHom W)) =ᶠ[nhds 0] fun (x : Fin n → K) => Polynomial.eval (x i) (specialize W (x ∘ ⇑e))

Near 0, the function of W(X_i) (coefficients embedded along e) at x is (specialize W (x ∘ e)).eval (x i).