Polynomial coefficients on analytic submanifolds

Specializing a polynomial with multivariate polynomial coefficients along an analytic submanifold gives intrinsically analytic coefficient functions. These supply the coefficient regularity needed for analytic polynomial root sections.

theorem TauCeti.IsAnalyticSubmanifold.analyticOnSubmanifold_coeff_map_eval {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n d : ℕ} {S : Set (Fin n → 𝕜)} (hS : IsAnalyticSubmanifold d S) (b : Polynomial (MvPolynomial (Fin n) 𝕜)) (j : ℕ) : AnalyticOnSubmanifold d (fun (x : Fin n → 𝕜) => (Polynomial.map (MvPolynomial.eval x) b).coeff j) S

The coefficients of a multivariate polynomial specialized along an analytic submanifold are intrinsically analytic.