AnalyticAt.aeval_mvPolynomial

theorem AnalyticAt.aeval_mvPolynomial : ∀ {𝕜 : Type u_1} {E : Type u_2} {A : Type u_3} {B : Type u_4} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : CommSemiring A] {z : E} [inst_4 : NormedCommRing B] [inst_5 : NormedAlgebra 𝕜 B] [inst_6 : Algebra A B] {σ : Type u_5} {f : E → σ → B}, (∀ (i : σ), AnalyticAt 𝕜 (fun x => f x i) z) → ∀ (p : MvPolynomial σ A), AnalyticAt 𝕜 (fun x => (MvPolynomial.aeval (f x)) p) z

The theorem `AnalyticAt.aeval_mvPolynomial` states that for any type 𝕜, which is a nontrivially normed field, types E and A, which are normed add comm group and comm semiring respectively, a type B which is a normed comm ring and a normed algebra over 𝕜, a type σ, and a function `f : E → σ → B`, if for every i in σ, the function `fun x => f x i` is analytic at a point z in E, then for every multivariate polynomial p with coefficients in A and variables indexed by σ, the function `fun x => (MvPolynomial.aeval (f x)) p` will also be analytic at the point z. In simpler terms, it states that if each component of a vector-valued function is analytic, then the function that maps each point to the evaluation of a multivariate polynomial with coefficients in A and variables replaced by the values of the function at that point, is also analytic.

More concisely: If `f : E → σ → B` is a vector-valued function of analytic components over a nontrivially normed field 𝕜, then the function `x ↦ MvPolynomial.aeval (f x) p` is analytic at a point `z ∈ E` for any multivariate polynomial `p` with coefficients in the normed semiring A.