English
Let f: E → σ → B and p be a multivariate polynomial with coefficients in A. If for every i ∈ σ the function x ↦ f(x) i is analytic at z, then the map x ↦ aeval(f(x)) p is analytic at z.
Русский
Пусть f: E → σ → B и p — многочлен по нескольким переменным с коэффициентами в A. Если для каждого i ∈ σ функция x ↦ f(x) i аналитична в точке z, то функция x ↦ aeval(f(x)) p аналитична в z.
LaTeX
$$$\\text{AnalyticAt}_{\\mathbb{k}} \\bigl( x \\mapsto \\operatorname{aeval}(f(x), p) \\bigr) (z) \\quad \\text{при условии } (\\forall i,\\ AnalyticAt_{\\mathbb{k}}(f\\cdot i)\\, z).$$$
Lean4
theorem aeval_mvPolynomial (hf : ∀ i, AnalyticAt 𝕜 (f · i) z) (p : MvPolynomial σ A) :
AnalyticAt 𝕜 (fun x ↦ aeval (f x) p) z :=
by
apply
p.induction_on (fun k ↦ ?_) (fun p q hp hq ↦ ?_) fun p i hp ↦
?_ -- `refine` doesn't work
· simp_rw [aeval_C]; apply analyticAt_const
· simp_rw [map_add]; exact hp.add hq
· simp_rw [map_mul, aeval_X]; exact hp.mul (hf i)
